add processor state for exceedance analysis

Co-authored-by: Björn Brandenburg <bbb@mpi-sws.org>

analysis/facts/model/ideal_uni_exceed.v

+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).
+  Proof.
+    rewrite /unit_supply_proc_model.
+    move => s.
+    destruct s => //=.
+    all : by rewrite /supply_in //=;rewrite sum_unit1.
+  Qed.
+
+  (** 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.
+  Proof.
+    split.
+    -  move => SCHED.
+      rewrite /scheduled_at /scheduled_in in SCHED.
+      move : SCHED => /existsP [c SCHEDON].
+      unfold scheduled_on in SCHEDON.
+      simpl in SCHEDON.
+      unfold exceedance_scheduled_on in *.
+      destruct (sched t); try done.
+      + left.
+        by move : SCHEDON => /eqP <-.
+      + right.
+        by move : SCHEDON => /eqP <-.
+    - rewrite /scheduled_at.
+      move => [-> | -> ]; rewrite /scheduled_in /scheduled_on //=; by apply /existsP => //=.
+  Qed.
+
+
+  (** 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).
+  Proof.
+    rewrite /uniprocessor_model.
+    move => j1 j2 sched t SCHED1 SCHED2.
+    rewrite /scheduled_at /scheduled_in in SCHED1, SCHED2.
+    move : SCHED1 => /existsP [c SCHED1].
+    move : SCHED2 => /existsP [c' SCHED2].
+    rewrite  /scheduled_on //= /exceedance_scheduled_on in SCHED1, SCHED2.
+    destruct (sched t) eqn: EQ; try done.
+    - move : SCHED1 => /eqP <-.
+      by move : SCHED2 => /eqP <-.
+    - move : SCHED1 => /eqP <-.
+      by move : SCHED2 => /eqP <-.
+  Qed.
+
+  (** 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).
+  Proof.
+    rewrite /fully_consuming_proc_model.
+    move => j sched t SCHED1.
+    rewrite /scheduled_at /scheduled_in in SCHED1.
+    apply scheduled_at_procstate in SCHED1.
+    move : SCHED1 => [SCHED1 | SCHED1].
+    - by rewrite /service_at /service_in /exceedance_service_on /supply_at /supply_in
+      !/exceedance_service_on //= SCHED1 sum_unit1 // sum_unit1 //
+      /exceedance_service_on /exceedance_supply_on eq_refl.
+    - by rewrite /service_at /service_in /exceedance_service_on /supply_at /supply_in
+        !/exceedance_service_on //= SCHED1 sum_unit1 // sum_unit1 //
+        /exceedance_service_on /exceedance_supply_on eq_refl.
+  Qed.
+
+  (** 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).
+  Proof.
+    rewrite /unit_service_proc_model.
+    move => j pstate.
+    rewrite /service_in /service_on //= sum_unit1 /exceedance_service_on.
+    destruct pstate =>//=.
+    by apply leq_b1.
+  Qed.
+
+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.
+  Local Transparent scheduled_in scheduled_on service_on.
+
+
+  (** 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).
+  Proof.
+    rewrite /is_blackout /has_supply /supply_at /supply_in
+    /is_exceedance_exec //= sum_unit1 /exceedance_supply_on.
+    destruct (sched t) eqn : PSTATE; try done.
+  Qed.
+
+End ExceedanceProcStateProperties1.
+
+Global Hint Resolve
+  eps_is_uniproc
+  eps_is_unit_supply
+  eps_is_fully_consuming
+  : basic_rt_facts.

model/processor/ideal_uni_exceed.v

+From HB Require Import structures.
+Require Export prosa.behavior.all.
+
+(** In the following, we define a processor state model for an ideal-uniprocessor
+    system with jobs possibly exhibiting exceedance. *)
+Section State.
+
+  (** For a give type of jobs ...*)
+  Context `{Job : JobType}.
+
+  (** ... the exceedance processor state is defined as follows.
+      Here, the [NominalExecution] processor state refers to the state of the
+      processor when it is executing some job [j]. [ExceedanceExecution] also
+      refers to the state of the processor when a job is executing in addition
+      to its nominal execution time. Finally, [Idle] refers to the state of the
+      processor when no job is executing. *)
+  Inductive exceedance_processor_state :=
+  | NominalExecution (j : Job)
+  | ExceedanceExecution (j : Job)
+  | Idle.
+
+  (** To efficiently use the processor state in our mechanization, we need to
+      define an [eqType] for the processor state. First, we define an inequality
+      on the processor state as follows. *)
+  Definition exceedance_processor_state_eqdef (p1 p2 : exceedance_processor_state) : bool :=
+    match p1, p2 with
+    | NominalExecution j1, NominalExecution j2 => j1 == j2
+    | ExceedanceExecution j1, ExceedanceExecution j2 => j1 == j2
+    | Idle, Idle => true
+    | _, _ => false
+    end.
+
+  (** Next, we prove that the defined notion of equality is in fact an equality. *)
+  Lemma eqn_exceedance_processor_state : Equality.axiom exceedance_processor_state_eqdef.
+  Proof.
+    unfold Equality.axiom.
+    move => s1 s2.
+    destruct (exceedance_processor_state_eqdef s1 s2) eqn: EQ.
+    { apply ReflectT.
+      destruct s1; destruct s2; unfold exceedance_processor_state_eqdef in EQ; try by done.
+      - by move : EQ => /eqP -> .
+      - by move : EQ => /eqP ->.
+    }
+    {
+      apply /ReflectF.
+      destruct s1; destruct s2; unfold exceedance_processor_state_eqdef in EQ;
+        move => CONTRA; try done.
+      - by injection CONTRA => RE; rewrite RE in EQ; contradict EQ; rewrite eq_refl.
+      - by injection CONTRA => RE; rewrite RE in EQ; contradict EQ; rewrite eq_refl.
+    }
+  Qed.
+
+  (** Finally, we register the processor state as an [eqType]. *)
+  HB.instance Definition _ := hasDecEq.Build exceedance_processor_state eqn_exceedance_processor_state.
+
+  (** Next, we need to define the notions of service and supply for the
+      processor state under consideration. *)
+  Section ExceedanceService.
+
+    (** Consider any job [j]. *)
+    Variable j : Job.
+
+    (** [j] is considered to be "scheduled" if the processor state is either
+        [NominalExecution j] or [ExceedanceExecution j] *)
+    Definition exceedance_scheduled_on (proc_state : exceedance_processor_state) (_ : unit)
+      : bool :=
+      match proc_state with
+      | NominalExecution j'
+      | ExceedanceExecution j' => j' == j
+      | _ => false
+      end.
+
+    (** Next, we need to define in which states the processor is offering supply.
+        This is required to specify in which states a processor can offer
+        productive work to a job. Note that when analysing a schedule of the
+        [exceedance_processor_state], we want to model all instances of
+        [ExceedanceExecution] as blackouts w.r.t. to nominal service and, therefore, the supply in this
+        processor state is defined to be [0]. *)
+    Definition exceedance_supply_on (proc_state :  exceedance_processor_state)
+      (_ : unit) : work :=
+      match proc_state with
+      | NominalExecution _ => 1
+      | ExceedanceExecution _ => 0
+      | Idle => 1
+      end.
+
+    (** Finally we need to define in which states a job actually receives
+        nominal service. In our case, a job [j] receives nominal service only when the system
+        is in the [NominalExecution j] state. *)
+    Definition exceedance_service_on (proc_state : exceedance_processor_state) (_ : unit) : work :=
+      match proc_state with
+      | NominalExecution j' => j' == j
+      | ExceedanceExecution _ => 0
+      | Idle => 0
+      end.
+
+  End ExceedanceService.
+
+    (** Finally we can declare our processor state as an instance of the
+        [ProcessorState] typeclass. *)
+    Global Program Instance exceedance_proc_state : ProcessorState Job :=
+      {|
+        State := exceedance_processor_state;
+        scheduled_on := exceedance_scheduled_on;
+        supply_on := exceedance_supply_on;
+        service_on := exceedance_service_on
+      |}.
+    Next Obligation.
+      by move => j [] // s [] /=; case: eqP; lia.
+    Qed.
+    Next Obligation.
+      by move => j [] // s [] /=; case: eqP; lia.
+    Qed.
+
+End State.
+
+Global Arguments exceedance_proc_state : clear implicits.

scripts/wordlist.pws

@@ -131,3 +131,4 @@ RHS
 LHS
 subsequence
 Baruah
+exceedance