Library prosa.implementation.refinements.EDF.nonpreemptive_sched

Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
Require Export prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.definitions.tardiness.
Require Export prosa.implementation.facts.ideal_uni.prio_aware.
Require Export prosa.implementation.definitions.task.
Require Export prosa.model.priority.edf.

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 := concrete_task : eqType.
Definition Job := concrete_job : eqType.

Consider any valid arrival sequence, ...

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

... assume basic readiness, ...

Instance basic_ready_instance : JobReady Job (ideal.processor_state Job) :=
basic.basic_ready_instance.

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

Lemma sched_jobs_must_be_ready_to_execute :
jobs_must_be_ready_to_execute sched.

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.

Lemma sched_nonpreemptive :
nonpreemptive_schedule (uni_schedule arr_seq).

Finally, we show that the earliest-deadline-first policy is respected at each preemption point.

Lemma respects_policy_at_preemption_point_edf_np :
respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

End Schedule.