Library prosa.model.processor.multiprocessor
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
From mathcomp Require Export fintype.
Require Export prosa.behavior.all.
Require Import prosa.analysis.facts.behavior.service.
Multiprocessor State
Consider any types of jobs...
... and consider any type of per-processor state.
Given a desired number of processors [num_cpus], we define a finite type
of integers from [0] to [num_cpus - 1]. The purpose of this definition is
to obtain a finite type (i.e., set of values) that can be enumerated in a
terminating computation.
Syntax hint: the ['I_] before [num_cpus] is ssreflect syntax for the
finite set of integers from zero to [num_cpus - 1].
Next, for any given number of processors [num_cpus]...
...we represent the type of the "multiprocessor state" as a function that
maps processor IDs (as defined by [processor num_cpus], see above) to the
given state on each core.
Based on this notion of multiprocessor state, we say that a given job [j]
is currently scheduled on a specific processor [cpu], according to the
given multiprocessor state [mps], iff [j] is scheduled in the
processor-local state [(mps cpu)].
Definition multiproc_scheduled_on
(j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= scheduled_in j (mps cpu).
(j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= scheduled_in j (mps cpu).
Similarly, the service received by a given job [j] in a given
multiprocessor state [mps] on a given processor of ID [cpu] is exactly
the service given by [j] in the processor-local state [(mps cpu)].
Definition multiproc_service_on
(j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= service_in j (mps cpu).
(j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= service_in j (mps cpu).
Finally, we connect the above definitions with the generic Prosa
interface for processor models.
Global Program Instance multiproc_state : ProcessorState Job multiprocessor_state :=
{
scheduled_on := multiproc_scheduled_on;
service_on := multiproc_service_on
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 411)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
j : Job
s : multiprocessor_state
r : 'I_num_cpus
H0 : ~~ multiproc_scheduled_on j s r
============================
multiproc_service_on j s r = 0
----------------------------------------------------------------------------- *)
move: j s r H0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 424)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
============================
forall (j : Job) (s : multiprocessor_state) (r : 'I_num_cpus),
~~ multiproc_scheduled_on j s r -> multiproc_service_on j s r = 0
----------------------------------------------------------------------------- *)
move⇒ j mps cpu.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 427)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
j : Job
mps : multiprocessor_state
cpu : 'I_num_cpus
============================
~~ multiproc_scheduled_on j mps cpu -> multiproc_service_on j mps cpu = 0
----------------------------------------------------------------------------- *)
by apply: service_in_implies_scheduled_in.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
{
scheduled_on := multiproc_scheduled_on;
service_on := multiproc_service_on
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 411)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
j : Job
s : multiprocessor_state
r : 'I_num_cpus
H0 : ~~ multiproc_scheduled_on j s r
============================
multiproc_service_on j s r = 0
----------------------------------------------------------------------------- *)
move: j s r H0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 424)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
============================
forall (j : Job) (s : multiprocessor_state) (r : 'I_num_cpus),
~~ multiproc_scheduled_on j s r -> multiproc_service_on j s r = 0
----------------------------------------------------------------------------- *)
move⇒ j mps cpu.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 427)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
j : Job
mps : multiprocessor_state
cpu : 'I_num_cpus
============================
~~ multiproc_scheduled_on j mps cpu -> multiproc_service_on j mps cpu = 0
----------------------------------------------------------------------------- *)
by apply: service_in_implies_scheduled_in.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
From the instance [multiproc_state], we get the function [service_in].
The service received by a given job [j] in a given multiprocessor state
[mps] is given by the sum of the service received across all individual
processors of the multiprocessor.
Lemma multiproc_service_in_eq : ∀ (j : Job) (mps : multiprocessor_state),
service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 432)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
============================
forall (j : Job) (mps : multiprocessor_state),
service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu)
----------------------------------------------------------------------------- *)
Proof.
reflexivity.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Schedule.
service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 432)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
============================
forall (j : Job) (mps : multiprocessor_state),
service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu)
----------------------------------------------------------------------------- *)
Proof.
reflexivity.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Schedule.