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.
Consider any type of jobs.
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].
Next, we define the semantics of the processor state with spinning.
Let [j] denote any 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
| Idle ⇒ false
| Spin j' ⇒ j' == j
| Progress j' ⇒ j' == j
end.
match s with
| Idle ⇒ false
| 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.
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.
{
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.