Library prosa.analysis.facts.priority.edf

In this section, we prove a few properties about EDF policy.
Section PropertiesOfEDF.

Consider any type of tasks with relative deadlines ...
  Context {Task : TaskType}.
  Context `{TaskDeadline Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

EDF respects sequential tasks hypothesis.
  Lemma EDF_respects_sequential_tasks:
    policy_respects_sequential_tasks.
  Proof.
    movej1 j2 /eqP TSK ARR.
    rewrite /hep_job /EDF /job_deadline /job_deadline_from_task_deadline TSK.
    by lia.
  Qed.

End PropertiesOfEDF.

We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically.
Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.

Require Export prosa.model.task.sequentiality.
Require Export prosa.analysis.facts.busy_interval.priority_inversion.
Require Export prosa.analysis.facts.priority.sequential.

In this section, we prove that EDF priority policy implies that tasks are sequential.
Section SequentialEDF.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.

... with a bound on the maximum non-preemptive segment length. The bound is needed to ensure that, at any instant, it always exists a subsequent preemption time in which the scheduler can, if needed, switch to another higher-priority job.
Further, consider any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Next, consider any ideal uni-processor schedule of this arrival sequence, ...
... allow for any work-bearing notion of job readiness, ...
... and assume that the schedule is valid.
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 with bounded non-preemptive segments.
Next, we assume that the schedule respects the scheduling policy at every preemption point.
To prove sequentiality, we use lemma early_hep_job_is_scheduled. Clearly, under the EDF priority policy, jobs satisfy the conditions described by the lemma (i.e., given two jobs j1 and j2 from the same task, if j1 arrives earlier than j2, then j1 always has a higher priority than job j2, and hence completes before j2); therefore EDF implies sequential tasks.
  Lemma EDF_implies_sequential_tasks:
    sequential_tasks arr_seq sched.
  Proof.
    movej1 j2 t ARR1 ARR2 /eqP SAME LT.
    eapply early_hep_job_is_scheduled ⇒ //; rt_eautot'.
    rewrite /hep_job_at /JLFP_to_JLDP /hep_job /EDF /job_deadline
      /absolute_deadline.job_deadline_from_task_deadline SAME.
    by lia.
  Qed.

End SequentialEDF.