Library rt.restructuring.model.schedule.edf
In this file, we define what it means to be an "EDF schedule".
Section DefinitionOfEDF.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ... any given type of processor states: *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
(* We say that a schedule is locally an EDF schedule at a point in
time [t] if the job scheduled at time [t] has a deadline that is
earlier than or equal to the deadline of any other job that could
be scheduled at time t but is scheduled later.
Note that this simple definition is (intentionally) oblivious to
(i.e., not compatible with) issues such as non-preemptive regions
or self-suspensions. *)
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'.
(* A schedule is an EDF schedule if it is locally EDF at every point in time. *)
Definition is_EDF_schedule (sched: schedule PState) := ∀ t, EDF_at sched t.
End DefinitionOfEDF.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ... any given type of processor states: *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
(* We say that a schedule is locally an EDF schedule at a point in
time [t] if the job scheduled at time [t] has a deadline that is
earlier than or equal to the deadline of any other job that could
be scheduled at time t but is scheduled later.
Note that this simple definition is (intentionally) oblivious to
(i.e., not compatible with) issues such as non-preemptive regions
or self-suspensions. *)
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'.
(* A schedule is an EDF schedule if it is locally EDF at every point in time. *)
Definition is_EDF_schedule (sched: schedule PState) := ∀ t, EDF_at sched t.
End DefinitionOfEDF.