Equivalence of EDF Definitions

Recall that we have defined "EDF schedules" in two ways. The generic way to define an EDF schedule is by using the EDF priority policy defined in model.priority.edf and the general notion of priority-compliant schedules defined in model.schedule.priority_driven. Another, more straight-forward way to define an EDF schedule is the standalone definition given in model.schedule.edf, which is less general but simpler and used in the EDF optimality proof. In this file, we show that both definitions are equivalent assuming: (1) ideal uniprocessor schedules, (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.

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

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

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.

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