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.