Library rt.restructuring.model.schedule.edf
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From mathcomp Require Import ssrnat ssrbool fintype.
From rt.restructuring.behavior Require Export all.
In this file, we define what it means to be an "EDF schedule".
For any given type of jobs...
... any given type of processor states:
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'.
∀ (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.