Multiprocessor State

In the following, we define a model of identical multiprocessors, i.e., of processors with multiple cores of identical capabilities. The multiprocessor model is generic in the type of processor state of the cores. That is, it is possible to combine any uniprocessor state (such as the ideal state) with the following generic multiprocessor construction. (In fact, by combining the below multiprocessor model with variable speed processors, it is even possible to obtain a so-called uniform multiprocessor model.) 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 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).

Similarly, the supply produced by a given multiprocessor state mps on a given core cpu is exactly the supply provided by the core-local state (mps cpu).

Next, 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).

Finally, we connect the above definitions with the generic Prosa interface for processor models.

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.