Library prosa.model.processor.platform_properties

Require Export prosa.behavior.all.
Require Export prosa.model.processor.supply.

To reason about classes of schedule types / processor models, we define the following properties that group processor models into classes of similar models.
Section ProcessorModels.
Consider any job type and any processor state.
Note: we make the processor state an explicit variable (rather than implicit context) because it is the primary subject of the following definitions.
  Context {Job : JobType}.
  Variable PState : ProcessorState Job.

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 : Job) (s : PState), 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 : Job) (s : PState),
      scheduled_in j s service_in j s > 0.

In a uniprocessor model, the scheduled job is always unique.
  Definition uniprocessor_model :=
     (j1 j2 : Job) (s : schedule PState) (t : instant),
      scheduled_at s j1 t
      scheduled_at s j2 t
      j1 = j2.

We say that a processor model is a unit-supply model if no state ever produces more than one unit of supply at any time.
  Definition unit_supply_proc_model :=
     (s : PState), supply_in s 1.

Note that unit_supply_proc_model implies unit_service_proc_model because of the requirement service_on_le_supply_on. But not vice versa --- a unit-service processor model is not necessarily a unit-supply processor model.
  Remark unit_supply_is_unit_service :
    unit_supply_proc_model
    unit_service_proc_model.
  Proof.
    moveUSUP j s; move: (USUP s).
    apply leq_trans, leq_sumr _.
    by apply service_on_le_supply_on.
  Qed.

We say that a processor model is a fully consuming processor model if a job scheduled at time t receives the entire supply produced at that time as service.
  Definition fully_consuming_proc_model :=
     (j : Job) (s : schedule PState) (t : instant),
      scheduled_at s j t service_at s j t = supply_at s t.

End ProcessorModels.

We add the reduction from unit_supply_proc_model to unit_service_proc_model into the "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically where needed.
Global Hint Resolve
       unit_supply_is_unit_service
  : basic_rt_facts.