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

#[local] Existing Instance basic_ready_instance.

We assume that jobs are fully preemptive.

#[local] Existing Instance fully_preemptive_job_model.

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.