Library prosa.analysis.facts.suspension

Require Export prosa.model.readiness.suspension.

Facts about Self-Suspensions

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.

Basic Lemmas

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

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.

Self-Suspension Bound at any Point During a Job's Execution

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 ρ.

Step 1

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).

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

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

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

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.

Step 2

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).

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

Final Bound

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.