Library rt.restructuring.behavior.schedule.platform_properties
From rt.restructuring.behavior Require Export schedule.
(* To reason about classes of schedule types / processor models, we define the
following properties that a processor model might possess. *)
Section ProcessorModels.
(* Consider any job type and any processor state. *)
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(* We say that a processor model provides unit service if no
job ever receives more than one unit of service at any time. *)
Definition unit_service_proc_model :=
∀ j s, service_in j s ≤ 1.
(* We say that a processor model offers ideal progress if a scheduled job
always receives non-zero service. *)
Definition ideal_progress_proc_model :=
∀ j s, scheduled_in j s → service_in j s > 0.
(* In a uniprocessor model, the scheduled job is always unique. *)
Definition uniprocessor_model :=
∀ j1 j2 s t,
scheduled_at s j1 t →
scheduled_at s j2 t →
j1 = j2.
End ProcessorModels.
(* To reason about classes of schedule types / processor models, we define the
following properties that a processor model might possess. *)
Section ProcessorModels.
(* Consider any job type and any processor state. *)
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(* We say that a processor model provides unit service if no
job ever receives more than one unit of service at any time. *)
Definition unit_service_proc_model :=
∀ j s, service_in j s ≤ 1.
(* We say that a processor model offers ideal progress if a scheduled job
always receives non-zero service. *)
Definition ideal_progress_proc_model :=
∀ j s, scheduled_in j s → service_in j s > 0.
(* In a uniprocessor model, the scheduled job is always unique. *)
Definition uniprocessor_model :=
∀ j1 j2 s t,
scheduled_at s j1 t →
scheduled_at s j2 t →
j1 = j2.
End ProcessorModels.