Optimality of EDF on Ideal Uniprocessors

This module provides the famous EDF optimality theorem: if there is any way to meet all deadlines (assuming an ideal uniprocessor schedule), then there is also an (ideal) EDF schedule in which all deadlines are met.

Optimality Theorem

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

... and any valid arrival sequence of such jobs.

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.

We assume that jobs are fully preemptive.

Under these assumptions, EDF is optimal in the sense that, if there exists any schedule in which all jobs of arr_seq meet their deadline, then there also exists an EDF schedule in which all deadlines are met.

Moreover, we note that, since EDF maintains work conservation, if there exists a schedule in which all jobs of arr_seq meet their deadline, then there also exists a work-conserving EDF in which all deadlines are met.

Remark: EDF_optimality is of course an immediate corollary of EDF_WC_optimality. We nonetheless have two separate proofs for historic reasons as EDF_optimality predates EDF_WC_optimality (in Prosa). Finally, we state the optimality theorem also in terms of a policy-compliant schedule, which a more generic notion used in Prosa for scheduling policies (rather than the simpler, but ad-hoc EDF_schedule predicate used above). Given that we're considering the EDF priority policy and a fully preemptive job model, satisfying the EDF_schedule predicate is equivalent to satisfying the respects_policy_at_preemption_point w.r.t. to the EDF policy predicate. The optimality of priority-compliant schedules that are work-conserving follows hence directly from the above EDF_WC_optimality theorem.

Weak Optimality Theorem

We further state a weaker notion of the above optimality result that avoids a dependency on a given arrival sequence. Specifically, it establishes that, given a reference schedule without deadline misses, there exists an EDF schedule of the same jobs in which no deadlines are missed.

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

... if we have a well-behaved reference schedule ...

... in which no deadlines are missed, ...

...then there also exists an EDF schedule in which no deadlines are missed (and in which exactly the same set of jobs is scheduled, as ensured by the last clause).