Library prosa.model.processor.multiprocessor
From mathcomp Require Export fintype.
Require Export prosa.behavior.all.
Require Import prosa.analysis.facts.behavior.service.
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.
#[local] Program Instance multiproc_state : ProcessorState Job :=
{|
State := multiprocessor_state;
scheduled_on := multiproc_scheduled_on;
service_on := multiproc_service_on
|}.
{|
State := multiprocessor_state;
scheduled_on := multiproc_scheduled_on;
service_on := multiproc_service_on
|}.
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.