Library prosa.analysis.facts.model.preemption

Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.scheduled.

In this section, we establish two basic facts about preemption times.

Section PreemptionTimes.

Consider any type of jobs.

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

In addition, we assume the existence of a function mapping a job and its progress to a boolean value saying whether this job is preemptable at its current point of execution.

Context `{JobPreemptable Job}.

Consider any valid arrival sequence

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

Allow for any uniprocessor model.

Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.

Next, consider any schedule of the arrival sequence...

Variable sched : schedule PState.

... where jobs come from the arrival sequence and don't execute before their arrival time.

  Hypothesis H_jobs_come_from_arrival_sequence:
    jobs_come_from_arrival_sequence sched arr_seq.
  Hypothesis H_must_arrive: jobs_must_arrive_to_execute sched.

Consider a valid preemption model.

Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.

We start with a trivial fact that, given a time interval

[t1,

t2)>>, the interval either contains a preemption time t or it does not.

  Lemma preemption_time_interval_case :
    ∀ t1 t2,
      (∀ t, t1 ≤ t < t2 → ~~ preemption_time arr_seq sched t )
      ∨ (∃ t ,
            t1 ≤ t < t2
            ∧ preemption_time arr_seq sched t
            ∧ ∀ t', t1 ≤ t' → preemption_time arr_seq sched t' → t ≤ t').

An idle instant is a preemption time.

  Lemma idle_time_is_pt :
    ∀ t,
      is_idle arr_seq sched t →
      preemption_time arr_seq sched t.

We show that time 0 is a preemption time.

Lemma zero_is_pt: preemption_time arr_seq sched 0.

Also, we show that the first instant of execution is a preemption time.

  Lemma first_moment_is_pt:
    ∀ j prt,
      arrives_in arr_seq j →
      ~~ scheduled_at sched j prt →
      scheduled_at sched j prt .+1 →
      preemption_time arr_seq sched prt .+1.

If a job is scheduled at a point in time that is not a preemption time, then it was previously scheduled.

  Lemma neg_pt_scheduled_at :
    ∀ j t,
      scheduled_at sched j t .+1 →
      ~~ preemption_time arr_seq sched t .+1 →
      scheduled_at sched j t.

If a job is scheduled at time t-1 and time t is not a preemption time, then the job is scheduled at time t as well.

  Lemma neg_pt_scheduled_before :
    ∀ j t,
      ~~ preemption_time arr_seq sched t →
      scheduled_at sched j t .-1 →
      scheduled_at sched j t.

Next we extend the above lemma to an interval. That is, as long as there is no preemption time, a job will remain scheduled.

  Lemma neg_pt_scheduled_continuously_before :
    ∀ j t1 t2,
      scheduled_at sched j t1 →
      t1 ≤ t2 →
      (∀ t, t1 < t ≤ t2 → ~~ preemption_time arr_seq sched t ) →
      scheduled_at sched j t2.

Conversely if a job is scheduled at some time t2 and we know that there is no preemption time between t1 and t2 then the job must have been scheduled at t1 too.

  Lemma neg_pt_scheduled_continuously_after :
    ∀ j t1 t2,
      scheduled_at sched j t2 →
      t1 ≤ t2 →
      (∀ t, t1 ≤ t ≤ t2 → ~~ preemption_time arr_seq sched t ) →
      scheduled_at sched j t1.

Finally, using the above two lemmas we can prove that, if there is no preemption time in an interval [t1, t2), then if a job is scheduled at time t ∈ [t1, t2), then the same job is also scheduled at another time t' ∈ [t1, t2).

  Lemma neg_pt_scheduled_continuous :
    ∀ j t1 t2 t t',
      t1 ≤ t < t2 →
      t1 ≤ t' < t2 →
      (∀ t, t1 ≤ t < t2 → ~~ preemption_time arr_seq sched t ) →
      scheduled_at sched j t →
      scheduled_at sched j t'.

If we observe two different jobs scheduled at two points in time, then there necessarily is a preemption time in between.

  Lemma neq_scheduled_at_pt :
    ∀ j t,
      scheduled_at sched j t →
      ∀ j' t',
        scheduled_at sched j' t' →
        j != j' →
        t ≤ t' →
        exists2 pt , preemption_time arr_seq sched pt & t < pt ≤ t'.

We can strengthen the above lemma to say that there exists a preemption time such that, after the preemption point, the next job to be scheduled is scheduled continuously.

  Lemma neq_scheduled_at_pt_continuous_sched :
    ∀ j t,
      scheduled_at sched j t →
      ∀ j' t',
        scheduled_at sched j' t' →
        j != j' →
        t ≤ t' →
        ∃ pt ,
          preemption_time arr_seq sched pt
          ∧ t < pt ≤ t'
          ∧ scheduled_at sched j' pt.
End PreemptionTimes.

In this section, we prove a lemma relating scheduling and preemption times.

Section PreemptionFacts.

Consider any type of jobs.

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

Allow for any uniprocessor model.

  Context {PState : ProcessorState Job}.
  Hypothesis H_uniproc : uniprocessor_model PState.

  Context `{@JobReady Job PState Cost Arrival}.

Consider any valid arrival sequence.

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

Next, consider any valid schedule of this arrival sequence.

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

In addition, we assume the existence of a function mapping jobs to their preemption points ...

Context `{JobPreemptable Job}.

... and assume that it defines a valid preemption model.

Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.

We prove that every nonpreemptive segment always begins with a preemption time.

  Lemma scheduling_of_any_segment_starts_with_preemption_time:
    ∀ j t,
      scheduled_at sched j t →
      ∃ pt ,
        job_arrival j ≤ pt ≤ t ∧
          preemption_time arr_seq sched pt ∧
          (∀ t', pt ≤ t' ≤ t → scheduled_at sched j t').

We strengthen the above lemma to say that the preemption time that a segment starts with must lie between the last preemption time and the instant we know the job is scheduled at.

  Lemma scheduling_of_any_segment_starts_with_preemption_time_continuously_sched :
    ∀ j t1 t2,
      t1 ≤ t2 →
      preemption_time arr_seq sched t1 →
      scheduled_at sched j t2 →
      ∃ ptst ,
        t1 ≤ ptst ≤ t2
        ∧ preemption_time arr_seq sched ptst
        ∧ scheduled_at sched j ptst.

End PreemptionFacts.