Library prosa.analysis.facts.model.ideal_uni_exceed

Require Import prosa.model.processor.ideal_uni_exceed.
Require Export prosa.model.processor.platform_properties.

In the following section, we prove some general properties about the ideal uniprocessor with exceedance processor state.

Section ExceedanceProcStateProperties.

In this section, we consider any type of jobs.

Context `{Job : JobType}.

First we prove that the processor state provides unit supply.

Lemma eps_is_unit_supply : unit_supply_proc_model (exceedance_proc_state Job).

The usually opaque predicates are made transparent for this section to enable us to prove some processor properties.

Local Transparent scheduled_in scheduled_on service_on.

A job j is said to be scheduled_at some time t if and only if the processor state at that time is NominalExecution j or ExceedanceExecution j.

   Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t:
    scheduled_at sched j t ↔
      sched t = NominalExecution j ∨ sched t = ExceedanceExecution j.

Next we prove that the processor model under consideration is a uniprocessor model i.e., only one job can be scheduled at any time instant.

Lemma eps_is_uniproc : uniprocessor_model (exceedance_proc_state Job).

Next, we prove that the processor model under consideration is fully consuming i.e., all the supply offered is consumed by the scheduled job.

Lemma eps_is_fully_consuming :
fully_consuming_proc_model (exceedance_proc_state Job).

Finally we prove that the processor model under consideration is unit service i.e., it provides at most one unit of service at any time instant.

Lemma eps_is_unit_service : unit_service_proc_model (exceedance_proc_state Job).

End ExceedanceProcStateProperties.

Next, we prove some general properties specific to the ideal uniprocessor with exceedance processor state.

Section ExceedanceProcStateProperties1.

In this section we consider any type of jobs.

Context `{Job : JobType}.

First let us define the notion of exceedance execution. A processor state is said to be an exceedance execution state if is equal to ExceedanceExecution j for some j.

  Definition is_exceedance_exec (pstate : (exceedance_proc_state Job)) :=
    match pstate with
    | ExceedanceExecution _ ⇒ true
    | _ ⇒ false
    end.

Next, let us consider any schedule of the exceedance_proc_state.

Variable sched : schedule (exceedance_proc_state Job).

We prove that the schedule being in blackout at any time t is equivalent to the processor state at t being an exceedance execution state.

  Lemma blackout_implies_exceedance_execution t :
    is_blackout sched t = is_exceedance_exec (sched t).

End ExceedanceProcStateProperties1.

Global Hint Resolve
  eps_is_uniproc
  eps_is_unit_supply
  eps_is_fully_consuming
  : basic_rt_facts.