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 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.
Equivalence of EDF Definitions
... (2) the classic Liu & Layland model of readiness without jitter and
without self-suspensions, where pending jobs are always ready, and ...
... (3) 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 ...
...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_policy_at_preemption_point arr_seq sched.
EDF_schedule sched →
respects_policy_at_preemption_point arr_seq sched.
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_policy_at_preemption_point arr_seq sched →
EDF_schedule sched.
respects_policy_at_preemption_point arr_seq sched →
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_policy_at_preemption_point arr_seq sched.
End Equivalence.
EDF_schedule sched ↔ respects_policy_at_preemption_point arr_seq sched.
End Equivalence.