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

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