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

...and a corresponding schedule.

Suppose jobs don't execute after their completion, ...

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

EDF_schedule sched →

respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

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.

respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job) →

EDF_schedule sched.

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

End Equivalence.

EDF_schedule sched ↔ respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

End Equivalence.