Library prosa.analysis.facts.suspension

Require Export prosa.model.readiness.suspension.

In this file, we establish some basic facts related to self-suspensions.

Section Suspensions.

Consider any kind of jobs.

  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Suppose that the jobs can exhibit self-suspensions.

Context `{JobSuspension Job}.

Consider any valid arrival sequence of jobs ...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and assume the notion of readiness for self-suspending jobs.

#[local] Existing Instance suspension_ready_instance.

Consider any kind of processor model.

Context `{PState : ProcessorState Job}.

Consider any valid schedule.

Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

First, we establish some basic lemmas regarding self-suspending jobs.

Section BasicLemmas.

We show that a self-suspended job cannot be ready, ...

    Lemma suspended_implies_job_not_ready :
      ∀ j t,
        suspended sched j t →
        ~~ job_ready sched j t.

... which trivially implies that the job cannot be scheduled.

    Lemma suspended_implies_not_scheduled :
      ∀ j t,
        suspended sched j t →
        ~~ scheduled_at sched j t.

Next, we observe that a self-suspended job has already arrived.

    Lemma suspended_implies_arrived :
      ∀ j t,
        suspended sched j t →
        has_arrived j t.

By definition, only pending jobs can be self-suspended.

    Lemma suspended_implies_pending :
      ∀ j t,
        suspended sched j t →
        pending sched j t.

Next, we note that self-suspended jobs are not backlogged.

    Lemma suspended_implies_not_backlogged :
      ∀ j t,
        suspended sched j t →
        ~~ backlogged sched j t.

Further, we prove that if a job is pending and not self-suspended then it is ready.

    Lemma pending_and_not_suspended_implies_ready :
      ∀ j t,
        pending sched j t →
        ~~ suspended sched j t →
        job_ready sched j t.

  End BasicLemmas.

Next, we focus on bounding the self-suspension period of a job after receiving some amount of service.

Section SuspensionBoundedinInterval.

Consider any job j ...

Variable j : Job.

... and any time interval [t1, t2).

Variable t1 t2 : instant.

Now consider any amount of work ρ.

Variable ρ : work.

Our aim is to prove a bound on the self-suspension period of j after receiving an amount of service ρ. Note that it is possible that the job may not self-suspend after receiving ρ amount of service in which case job_suspension j ρ = 0.

Additionally, it is also important to note that the job may self-suspend multiple times within an interval, and these self-suspension intervals are separated by an interval where the job gets serviced. We can refer each such self-suspension interval as a segment, and each such segment is characterized by the amount of service received by the job.

Essentially here we are establishing a bound on the length of the self-suspension segment of j characterized by ρ.

Note that we can have two cases here, either the job j starts a suspension segment within the interval [t1, t2), or the job is already suspended at t1.

Section Step1.

Consider a point tf inside [t1, t2).

Variable tf : instant.
Hypothesis INtf : t1 ≤ tf < t2.

Let tf be the first point in the interval [t1, t2) that is also inside the self-suspension segment.

      Hypothesis H_suspended_tf : suspended sched j tf.
      Hypothesis H_service_at_tf : service sched j tf = ρ.
      Hypothesis H_before_tf :
        ∀ to,
          t1 ≤ to < tf →
          ~~ (suspended sched j to && (service sched j to == ρ )).

First, we prove a trivial result that the total suspension before tf is zero.

Local Lemma suspension_zero_before:
\sum_(t1 ≤ t < tf | service sched j t == ρ ) suspended sched j t = 0.

Next we consider the trivial case when the suspension period exceeds the interval [tf, t2).

      Section TrivialCase.
        Hypothesis H_LEQ : t2 - tf ≤ job_suspension j ρ.

        Lemma suspension_bounded_trivial:
          \sum_(tf ≤ t < t2 | service sched j t == ρ ) suspended sched j t ≤ job_suspension j ρ.

      End TrivialCase.

Next, we consider the case when the suspension period is within the interval [tf, t2).

      Section IntervalLengthLonger.
        Hypothesis H_GT : t2 - tf > job_suspension j ρ.

        Lemma suspension_bounded_longer_interval:
          \sum_(tf ≤ t < t2 | service sched j t == ρ ) suspended sched j t ≤ job_suspension j ρ.

      End IntervalLengthLonger.

Now we prove the required bound in case a point like tf exists. This helps to simplify our final proof.

      Lemma suspension_bounded_in_interval_aux :
        \sum_(t1 ≤ t < t2 | service sched j t == ρ ) suspended sched j t ≤ job_suspension j ρ.

    End Step1.

    Section Step2.

Now we prove that the point tf, as used in the above lemmas, always exists if suspended is true at some point inside [t1, t2).

      Hypothesis H_exists : (exists2 t , t \in index_iota t1 t2 & (suspended sched j t && (service sched j t == ρ ))).

      Lemma exists_some_point :
        ∃ t',
          t1 ≤ t' < t2 ∧
          suspended sched j t' ∧
          service sched j t' = ρ ∧
          ∀ to,
            t1 ≤ to < t' →
            ~~ (suspended sched j to && (service sched j to == ρ )).

    End Step2.

Finally we prove the required result.

    Lemma suspension_bounded_in_interval :
      \sum_(t1 ≤ t < t2 | service sched j t == ρ ) suspended sched j t ≤ job_suspension j ρ.

  End SuspensionBoundedinInterval.

End Suspensions.