Library prosa.model.processor.multiprocessor
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
From mathcomp Require Export fintype.
Require Export prosa.behavior.all.
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], if [j] is scheduled in the
processor-local state [(mps cpu)].
Let multiproc_scheduled_on (j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= scheduled_in j (mps cpu).
:= scheduled_in j (mps cpu).
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.
Let multiproc_service_in (j : Job) (mps : multiprocessor_state)
:= \sum_(cpu < num_cpus) service_in j (mps cpu).
:= \sum_(cpu < 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_in := multiproc_service_in
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
H0 : ~~ [exists c, multiproc_scheduled_on j s c]
============================
multiproc_service_in j s = 0
----------------------------------------------------------------------------- *)
move: j s H0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
============================
forall (j : Job) (s : multiprocessor_state),
~~ [exists c, multiproc_scheduled_on j s c] -> multiproc_service_in j s = 0
----------------------------------------------------------------------------- *)
move⇒ j s /existsP Hsched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
============================
multiproc_service_in j s = 0
----------------------------------------------------------------------------- *)
apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 157)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
============================
multiproc_service_in j s == 0
----------------------------------------------------------------------------- *)
rewrite sum_nat_eq0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
============================
[forall (i | true), service_in j (s i) == 0]
----------------------------------------------------------------------------- *)
apply/forallP=>/= c.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 188)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
c : 'I_num_cpus
============================
service_in j (s c) == 0
----------------------------------------------------------------------------- *)
rewrite service_implies_scheduled//.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 200)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
c : 'I_num_cpus
============================
~~ scheduled_in j (s c)
----------------------------------------------------------------------------- *)
case: (boolP (scheduled_in _ _))=>//= Habs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 297)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
c : 'I_num_cpus
Habs : scheduled_in j (s c)
============================
false
----------------------------------------------------------------------------- *)
exfalso; apply: Hsched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 304)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
c : 'I_num_cpus
Habs : scheduled_in j (s c)
============================
exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x
----------------------------------------------------------------------------- *)
by ∃ c.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End Schedule.
{
scheduled_on := multiproc_scheduled_on;
service_in := multiproc_service_in
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
H0 : ~~ [exists c, multiproc_scheduled_on j s c]
============================
multiproc_service_in j s = 0
----------------------------------------------------------------------------- *)
move: j s H0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
============================
forall (j : Job) (s : multiprocessor_state),
~~ [exists c, multiproc_scheduled_on j s c] -> multiproc_service_in j s = 0
----------------------------------------------------------------------------- *)
move⇒ j s /existsP Hsched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
============================
multiproc_service_in j s = 0
----------------------------------------------------------------------------- *)
apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 157)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
============================
multiproc_service_in j s == 0
----------------------------------------------------------------------------- *)
rewrite sum_nat_eq0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
============================
[forall (i | true), service_in j (s i) == 0]
----------------------------------------------------------------------------- *)
apply/forallP=>/= c.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 188)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
c : 'I_num_cpus
============================
service_in j (s c) == 0
----------------------------------------------------------------------------- *)
rewrite service_implies_scheduled//.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 200)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
c : 'I_num_cpus
============================
~~ scheduled_in j (s c)
----------------------------------------------------------------------------- *)
case: (boolP (scheduled_in _ _))=>//= Habs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 297)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
Hsched : ~
(exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x)
c : 'I_num_cpus
Habs : scheduled_in j (s c)
============================
false
----------------------------------------------------------------------------- *)
exfalso; apply: Hsched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 304)
Job : JobType
processor_state : Type
H : ProcessorState Job processor_state
num_cpus : nat
multiproc_scheduled_on := fun (j : Job) (mps : multiprocessor_state)
(cpu : processor num_cpus) =>
scheduled_in j (mps cpu)
: Job -> multiprocessor_state -> processor num_cpus -> bool
multiproc_service_in := fun (j : Job) (mps : multiprocessor_state) =>
\sum_(cpu < num_cpus) service_in j (mps cpu)
: Job -> multiprocessor_state -> nat
j : Job
s : multiprocessor_state
c : 'I_num_cpus
Habs : scheduled_in j (s c)
============================
exists x : ordinal_finType num_cpus, multiproc_scheduled_on j s x
----------------------------------------------------------------------------- *)
by ∃ c.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End Schedule.