Library prosa.implementation.refinements.EDF.nonpreemptive_sched

Fully-Nonpreemptive Earliest-Deadline-First Schedules

In this section, we prove that the fully-nonpreemptive preemption policy under earliest-deadline-first schedules is valid, and that the scheduling policy is respected at each preemption point.
Some lemmas in this file are not novel facts; they are used to uniform POET's certificates and minimize their verbosity.
Section Schedule.

In this file, we adopt the Prosa standard implementation of jobs and tasks.
  Definition Task := [eqType of concrete_task].
  Definition Job := [eqType of concrete_job].

Consider any arrival sequence with consistent arrivals, ...
... assume basic readiness, ...
... and consider any fully-nonpreemptive, earliest-deadline-first schedule.
  #[local] Existing Instance fully_nonpreemptive_job_model.
  #[local] Existing Instance EDF.
  Definition sched := uni_schedule arr_seq.

First, we show that only ready jobs execute.
Next, we remark that such a schedule is valid.
  Remark sched_valid :
    valid_schedule sched arr_seq.

Next, we show that an unfinished job scheduled at time t is always scheduled at time t+1 as well. Note that the validity of this fact also depends on which readiness model is used.
  Lemma sched_nonpreemptive_next :
     j t,
      scheduled_at sched j t
      ~~ completed_by sched j t.+1
      scheduled_at sched j t.+1.
Using the lemma above, we show that the schedule is nonpreemptive.
Finally, we show that the earliest-deadline-first policy is respected at each preemption point.