Library prosa.model.processor.spin
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.
If the processor is idle, we assume that the supply equals 1,
indicating that the processor is ready to perform work. If the
processor is in the state Spin j, then the job does not make
any progress, so effectively the supply is equal to
0. Finally, the processor being in the state Progress j
indicates that the processor carries out 1 unit of useful work.
Definition spin_supply_on (s : processor_state) (_ : unit) : work :=
match s with
| Idle ⇒ 1
| Spin j ⇒ 0
| Progress j ⇒ 1
end.
match s with
| Idle ⇒ 1
| Spin j ⇒ 0
| Progress j ⇒ 1
end.
Definition spin_service_on (s : processor_state) (_ : unit) : work :=
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.
Program Definition pstate_instance : ProcessorState Job :=
{|
State := processor_state;
scheduled_on := spin_scheduled_on;
supply_on := spin_supply_on;
service_on := spin_service_on
|}.
End State.
{|
State := processor_state;
scheduled_on := spin_scheduled_on;
supply_on := spin_supply_on;
service_on := spin_service_on
|}.
End State.