# Library prosa.analysis.facts.edf_definitions

Require Export prosa.analysis.facts.model.ideal.schedule.

Require Export prosa.analysis.facts.behavior.deadlines.

Require Export prosa.analysis.definitions.schedulability.

Require Export prosa.model.priority.edf.

Require Export prosa.model.schedule.edf.

Require Export prosa.model.schedule.priority_driven.

Require Import prosa.model.readiness.basic.

Require Import prosa.model.preemption.fully_preemptive.

Require Export prosa.analysis.facts.behavior.deadlines.

Require Export prosa.analysis.definitions.schedulability.

Require Export prosa.model.priority.edf.

Require Export prosa.model.schedule.edf.

Require Export prosa.model.schedule.priority_driven.

Require Import prosa.model.readiness.basic.

Require Import prosa.model.preemption.fully_preemptive.

# Equivalence of EDF Definitions

We assume the basic (i.e., Liu & Layland)
readiness model under which any pending job is ready.

We assume that jobs are fully preemptive.

For any given type of jobs, each characterized by an arrival time,
an execution cost, and an absolute deadline, ...

...consider a given valid job arrival sequence ...

Variable arr_seq: arrival_sequence Job.

Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

...and a corresponding ideal uniprocessor schedule.

Suppose jobs don't execute before their arrival nor after their
completion, ...

Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.

Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

...all jobs come from the arrival sequence arr_seq, ...

...and jobs from arr_seq don't miss their deadlines.

We first show that a schedule that satisfies the standalone
EDF_schedule predicate is also compliant with the generic notion of EDF
policy defined in Prosa, namely the respects_policy_at_preemption_point
predicate.

Lemma EDF_schedule_implies_respects_policy_at_preemption_point :

EDF_schedule sched →

respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

Proof.

move⇒ EDF j' j t ARR PREEMPTION BL SCHED.

have suff: ∃ t' : nat, t ≤ t' < job_deadline j' ∧ scheduled_at sched j' t'.

{ move⇒ [t' [/andP [LE _] SCHED']].

apply: (EDF t); [by [] | exact: LE | exact: SCHED' |].

by apply: (backlogged_implies_arrived sched j' t). }

apply; apply: incomplete_implies_scheduled_later.

- exact: H_no_deadline_misses.

- exact: (backlogged_implies_incomplete sched j' t).

Qed.

EDF_schedule sched →

respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

Proof.

move⇒ EDF j' j t ARR PREEMPTION BL SCHED.

have suff: ∃ t' : nat, t ≤ t' < job_deadline j' ∧ scheduled_at sched j' t'.

{ move⇒ [t' [/andP [LE _] SCHED']].

apply: (EDF t); [by [] | exact: LE | exact: SCHED' |].

by apply: (backlogged_implies_arrived sched j' t). }

apply; apply: incomplete_implies_scheduled_later.

- exact: H_no_deadline_misses.

- exact: (backlogged_implies_incomplete sched j' t).

Qed.

Conversely, the reverse direction also holds: a schedule that satisfies
the respects_policy_at_preemption_point predicate is also an EDF
schedule in the sense of EDF_schedule.

Lemma respects_policy_at_preemption_point_implies_EDF_schedule :

respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job) →

EDF_schedule sched.

Proof.

move⇒ H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.

case (boolP (j == j_hp)); first by move /eqP ⇒ EQ; subst.

move /neqP ⇒ NEQ.

exploit (H_priority_driven j j_hp t) ⇒ //.

{ by rewrite /preemption_time scheduled_job_at_def //; destruct (sched t). }

{ apply /andP; split ⇒ //.

- apply /andP; split ⇒ //.

apply (incompletion_monotonic _ j _ _ LEQ).

by apply scheduled_implies_not_completed.

- apply /negP; move ⇒ SCHED''.

by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }

Qed.

respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job) →

EDF_schedule sched.

Proof.

move⇒ H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.

case (boolP (j == j_hp)); first by move /eqP ⇒ EQ; subst.

move /neqP ⇒ NEQ.

exploit (H_priority_driven j j_hp t) ⇒ //.

{ by rewrite /preemption_time scheduled_job_at_def //; destruct (sched t). }

{ apply /andP; split ⇒ //.

- apply /andP; split ⇒ //.

apply (incompletion_monotonic _ j _ _ LEQ).

by apply scheduled_implies_not_completed.

- apply /negP; move ⇒ SCHED''.

by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }

Qed.

From the two preceding lemmas, it follows immediately that the two EDF
definitions are indeed equivalent, which we note with the following
corollary.

Corollary EDF_schedule_equiv:

EDF_schedule sched ↔ respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

Proof.

split.

- exact: EDF_schedule_implies_respects_policy_at_preemption_point.

- exact: respects_policy_at_preemption_point_implies_EDF_schedule.

Qed.

End Equivalence.

EDF_schedule sched ↔ respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

Proof.

split.

- exact: EDF_schedule_implies_respects_policy_at_preemption_point.

- exact: respects_policy_at_preemption_point_implies_EDF_schedule.

Qed.

End Equivalence.