Library prosa.model.processor.spin


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


From mathcomp Require Import all_ssreflect.
Require Export prosa.behavior.all.

In the following, we define a processor state that includes the possibility of spinning, where spinning jobs do not progress (= don't get any service).
NB: For now, the definition serves only to document how this can be done; it is not actually used anywhere in the library.
Section State.

Consider any type of jobs.
  Variable Job: JobType.

We define the state of a processor at a given time to be one of three possible cases: either a specific job is scheduled and makes progress [Progress j], a specific job is scheduled but makes not useful progress [Spin j], or the processor is idle [Idle].
  Inductive processor_state :=
    Idle
  | Spin (j : Job)
  | Progress (j : Job).

Next, we define the semantics of the processor state with spinning.
  Section Service.

Let [j] denote any job.
    Variable j : Job.

It is scheduled in a given state [s] iff the state is not idle and [j] is the job mentioned in the state.
    Definition spin_scheduled_on (s : processor_state) (_ : unit) : bool :=
      match s with
      | Idlefalse
      | Spin j'j' == j
      | Progress j'j' == j
      end.

In contrast, job [j] receives service only if the given state [s] is [Progress j].
    Definition spin_service_in (s : processor_state) : nat :=
      match s with
      | Idle ⇒ 0
      | Spin j' ⇒ 0
      | Progress j'j' == j
      end.

  End Service.

Finally, we connect the above definitions with the generic Prosa interface for abstract processor states.
  Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
    {
      scheduled_on := spin_scheduled_on;
      service_in := spin_service_in
    }.
  Next Obligation.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 583)
  
  Job : JobType
  j : Job
  s : processor_state
  H : ~~ [exists c, spin_scheduled_on j s c]
  ============================
  spin_service_in j s = 0

----------------------------------------------------------------------------- *)


    move: H.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 590)
  
  Job : JobType
  j : Job
  s : processor_state
  ============================
  ~~ [exists c, spin_scheduled_on j s c] -> spin_service_in j s = 0

----------------------------------------------------------------------------- *)


    case: s=>//= j' /existsP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 672)
  
  Job : JobType
  j, j' : Job
  ============================
  ~ (exists _ : unit_finType, j' == j) -> (j' == j) = 0

----------------------------------------------------------------------------- *)


    rewrite /nat_of_bool.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 673)
  
  Job : JobType
  j, j' : Job
  ============================
  ~ (exists _ : unit_finType, j' == j) -> (if j' == j then 1 else 0) = 0

----------------------------------------------------------------------------- *)


    case: ifP=>//=_[].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 754)
  
  Job : JobType
  j, j' : Job
  ============================
  exists _ : unit, true

----------------------------------------------------------------------------- *)


    by .

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Defined.
End State.