Library prosa.model.schedule.edf
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
From mathcomp Require Import ssrnat ssrbool fintype.
Require Export prosa.behavior.all.
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.