Library prosa.analysis.facts.priority.edf

Require Export prosa.model.priority.edf.
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.model.task.preemption.parameters.

We first make some trivial observations about EDF priorities to avoid repeating these steps in subsequent proofs.
Section PriorityFacts.
Consider any type of jobs with arrival times.
  Context `{Job : JobType} `{JobArrival Job}.

First, consider the general case where jobs have arbitrary deadlines.
  Section JobDeadline.

Assume EDF priorities based on (arbitrary) job_deadline parameters.
    Context `{JobDeadline Job} {JLFP : JLFP_policy Job}.
    Hypothesis H_policy_is_EDF : policy_is_EDF JLFP.

EDF priorities are reflexive since a job's deadline is no later than itself.
    Fact EDF_policy_is_reflexive :
      reflexive_job_priorities JLFP.
    Proof.
      move⇒ j.
      by rewrite H_policy_is_EDF.
    Qed.

EDF priorities are transitive since deadline order is transitive.
    Fact EDF_policy_is_transitive :
      transitive_job_priorities JLFP.
    Proof.
      move⇒ y x z.
      rewrite !H_policy_is_EDF.
      exact: leq_trans.
    Qed.

EDF priorities are total since any two deadlines are comparable.
    Fact EDF_policy_is_total :
      total_job_priorities JLFP.
    Proof.
      move⇒ j1 j2.
      rewrite !H_policy_is_EDF.
      exact: leq_total.
    Qed.

  End JobDeadline.

Second, consider the case where job (absolute) deadlines are derived from task (relative) deadlines.
  Section TaskDeadline.

If the jobs stem from tasks with relative deadlines ...
    Context {Task : TaskType}.
    Context `{TaskDeadline Task}.
    Context `{JobTask Job Task}.

If EDF priorities are derived from task_deadline, ...
    Context {JLFP : JLFP_policy Job}.
    Hypothesis H_policy_is_EDF : policy_is_EDF JLFP.

... then hep_job is a statement about job arrival times and relative deadlines.
    Fact hep_job_task_deadline :
      ∀ j j',
        hep_job j j' = (job_arrival j + task_deadline (job_task j)
                        ≤ job_arrival j' + task_deadline (job_task j')).
    Proof.
      move⇒ j j'.
      by rewrite H_policy_is_EDF /job_deadline/job_deadline_from_task_deadline.
    Qed.

Furthermore, if we are looking at two jobs of the same task, then hep_job is a statement about their respective arrival times.
    Fact hep_job_arrival_edf :
      ∀ j j',
        same_task j j' →
        hep_job j j' = (job_arrival j ≤ job_arrival j').
    Proof.
      by move⇒ j j' /eqP SAME; rewrite hep_job_task_deadline SAME leq_add2r.
    Qed.

EDF scheduling respects the sequential-tasks hypothesis.
    Fact EDF_policy_respects_sequential_tasks :
      policy_respects_sequential_tasks JLFP.
    Proof.
      by move ⇒ j j' /eqP TSK ?; rewrite hep_job_arrival_edf // /same_task TSK.
    Qed.
  End TaskDeadline.

End PriorityFacts.

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_policy_is_reflexive
  EDF_policy_is_transitive
  EDF_policy_is_total
  EDF_policy_respects_sequential_tasks
  : basic_rt_facts.

Require Export prosa.model.task.sequentiality.
Require Export prosa.analysis.facts.priority.inversion.
Require Export prosa.analysis.facts.priority.sequential.
Require Export prosa.analysis.facts.model.sequential.

In this section, we prove that EDF scheduling implies that tasks are executed sequentially.
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.
  Context `{TaskMaxNonpreemptiveSegment Task}.

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

Allow for any uniprocessor model.
  Context {PState : ProcessorState Job}.
  Hypothesis H_uniproc : uniprocessor_model PState.

Consider any valid arrival sequence.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

Next, consider any schedule of this arrival sequence, ...
  Variable sched : schedule PState.

Assume EDF scheduling.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_policy_is_EDF : policy_is_EDF JLFP.

... allow for any work-bearing notion of job readiness, ...
  Context `{@JobReady Job PState Cost Arrival}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

... and assume that the schedule is valid.
  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 with bounded non-preemptive segments.
  Hypothesis H_valid_preemption_model :
    valid_preemption_model arr_seq sched.

Assume an EDF schedule.
  Hypothesis H_respects_policy :
    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

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_policy_implies_sequential_tasks :
    sequential_tasks arr_seq sched.
  Proof.
    move ⇒ j1 j2 t ARR1 ARR2 SAME LT.
    apply: early_hep_job_is_scheduled ⇒ //.
    rewrite always_higher_priority_jlfp !hep_job_arrival_edf //.
    - by rewrite -ltnNge; apply/andP; split ⇒ //.
    - by rewrite same_task_sym.
  Qed.

End SequentialEDF.