Library prosa.model.processor.varspeed
(* ----------------------------------[ 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 model of processors with variable execution
speeds.
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 variable-speed processor at a given time to be
one of two possible cases: either a specific job is scheduled and
progresses with a specific speed, or the processor is idle.
Next, we define the semantics of the variable-speed processor state.
Consider any job [j].
Job [j] is scheduled in a given state [s] if [s] is not idle and [j]
matches the job recorded in [s].
Definition varspeed_scheduled_on (s : processor_state) (_ : unit) : bool :=
match s with
| Idle ⇒ false
| Progress j' _ ⇒ j' == j
end.
match s with
| Idle ⇒ false
| Progress j' _ ⇒ j' == j
end.
If it is scheduled in state [s], job [j] receives service proportional
to the speed recorded in the state.
Definition varspeed_service_on (s : processor_state) (_ : unit) : work :=
match s with
| Idle ⇒ 0
| Progress j' speed ⇒ if j' == j then speed else 0
end.
End Service.
match s with
| Idle ⇒ 0
| Progress j' speed ⇒ if j' == j then speed else 0
end.
End Service.
Finally, we connect the above definitions to the generic Prosa interface
for processor states.
Global Program Instance pstate_instance : ProcessorState Job processor_state :=
{
scheduled_on := varspeed_scheduled_on;
service_on := varspeed_service_on
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 585)
Job : JobType
j : Job
s : processor_state
r : unit
H : ~~ varspeed_scheduled_on j s r
============================
varspeed_service_on j s r = 0
----------------------------------------------------------------------------- *)
move: r H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 594)
Job : JobType
j : Job
s : processor_state
============================
forall r : unit,
~~ varspeed_scheduled_on j s r -> varspeed_service_on j s r = 0
----------------------------------------------------------------------------- *)
case: s=>//= j' v _.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 641)
Job : JobType
j, j' : Job
v : nat
============================
j' != j -> (if j' == j then v else 0) = 0
----------------------------------------------------------------------------- *)
by case: ifP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.
{
scheduled_on := varspeed_scheduled_on;
service_on := varspeed_service_on
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 585)
Job : JobType
j : Job
s : processor_state
r : unit
H : ~~ varspeed_scheduled_on j s r
============================
varspeed_service_on j s r = 0
----------------------------------------------------------------------------- *)
move: r H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 594)
Job : JobType
j : Job
s : processor_state
============================
forall r : unit,
~~ varspeed_scheduled_on j s r -> varspeed_service_on j s r = 0
----------------------------------------------------------------------------- *)
case: s=>//= j' v _.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 641)
Job : JobType
j, j' : Job
v : nat
============================
j' != j -> (if j' == j then v else 0) = 0
----------------------------------------------------------------------------- *)
by case: ifP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.