Fully-Preemptive EDF Schedules

This module provides an alternative definition of what it means to be an "EDF schedule". Note that the "proper" way to define an EDF schedule in Prosa is to use the EDF priority policy defined in model.priority.edf and the notion of priority-compliant schedules defined in model.schedule.priority_driven, as well as the general notion of work-conservation provided in model.schedule.work_conserving, which will have the benefit of taking into account issues such as various readiness models (e.g., jitter) and diverse preemption models (e.g., limited-preemptive jobs). The simpler definition offered in this module is (intentionally) oblivious to (i.e., not compatible with) issues such as non-preemptive regions or self-suspensions, and does not imply anything about work-conservation. In other words, it implicitly assumes that pending jobs are always ready and at all times preemptable. The advantage of this alternative definition is, however, that it is largely self-contained and fairly simple, following primarily from first principles. This makes it easier to use in certain contexts such as the proof of optimality of EDF.

Consider any type of jobs with arrival times, costs, and deadlines ...

... and any processor model.

We say that a schedule is locally EDF-compliant at a given point in time t if the job j scheduled at time t has a deadline that is earlier than or equal to the deadline of any other job j' that could be scheduled at time t (i.e., arrives at or before time t) but is actually scheduled later in the given schedule. In other words, a schedule is locally EDF-compliant at time t if there is no witness of a priority inversion (= an already arrived job with an earlier deadline) at a later point in the schedule.

Based on the notion of a locally EDF-compliant schedule given by EDF_at, we say that a schedule is (globally) EDF-compliant schedule if it is locally EDF-compliant at every point in time.