Library prosa.implementation.refinements.FP.preemptive_sched

Fully-Preemptive Fixed-Priority Schedules

In this section, we prove that the fully-preemptive preemption policy under fixed-priority schedules is valid, and that the scheduling policy is respected at each preemption point.
This file does not contain novel facts; it is 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 sequential readiness, ...
... and consider any fully-preemptive, fixed-priority schedule.
  #[local] Existing Instance fully_preemptive_job_model.
  #[local] Existing Instance NumericFPAscending.
  Definition sched := uni_schedule arr_seq.

First, we remark that such a schedule is valid.
  Remark sched_valid :
    valid_schedule sched arr_seq.
  Proof.
    apply uni_schedule_valid ⇒ //.
    by apply sequential_readiness_nonclairvoyance.
  Qed.

Finally, we show that the fixed-priority policy is respected at each preemption point.