Library prosa.model.schedule.edf
Fully-Preemptive EDF Schedules
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.
Definition EDF_at (sched : schedule PState) (t : instant) :=
∀ (j : Job),
scheduled_at sched j t →
∀ (t' : instant) (j' : Job),
t ≤ t' →
scheduled_at sched j' t' →
job_arrival j' ≤ t →
job_deadline j ≤ job_deadline j'.
∀ (j : Job),
scheduled_at sched j t →
∀ (t' : instant) (j' : Job),
t ≤ t' →
scheduled_at sched j' t' →
job_arrival j' ≤ t →
job_deadline j ≤ job_deadline j'.
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.
Definition EDF_schedule (sched : schedule PState) := ∀ t, EDF_at sched t.
End AlternativeDefinitionOfEDF.
End AlternativeDefinitionOfEDF.