Multiprocessor State

In the following, we define a model of identical multiprocessors, i.e., of machines that comprise several identical cores. Each core is modeled by its own processor state and is required to be a uniprocessor, so that "core" and "processor" are synonymous throughout this file. The construction is generic in the type of the per-core state: any uniprocessor state (such as the ideal state) can be plugged into the generic multiprocessor construction below. (In fact, by combining it with variable-speed processors, one even obtains a so-called uniform multiprocessor model.) The uniprocessor requirement rules out nesting, i.e., using a multiprocessor state as a core to form a multiprocessor of multiprocessors. It is needed because this construction reports at most one scheduled job per core (see multiproc_job_on below): lossless when each core is a uniprocessor, but lossy for a core that is itself a multiprocessor, which could schedule several jobs at once. We impose the requirement below as the hypothesis H_cores_are_uniprocessors; lifting it is left to future work. 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-core state.

We formalize the restriction discussed above: each core is required to be a uniprocessor.

Given a desired number of cores num_cores, we define a finite type of integers from 0 to num_cores - 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_cores is ssreflect syntax for the finite set of integers from zero to num_cores - 1.

Next, for any given number of cores num_cores...

...we represent the type of the "multiprocessor state" as a function that maps core IDs (as defined by core_ids num_cores, see above) to the given state on each core.

Based on this notion of multiprocessor state, the job running on a specific core c, according to the given multiprocessor state mps, is the job scheduled in (mps c), the state of core c, if any. By H_cores_are_uniprocessors there is at most one such job, so taking the head of the list of jobs scheduled in (mps c) loses no information.

Whenever a job j is scheduled in (mps c), the state of core c, multiproc_job_on reports it, i.e., returns Some j. By H_cores_are_uniprocessors at most one job is scheduled per core, so the head of jobs_scheduled_in (mps c) can only be j. Although H_cores_are_uniprocessors is phrased in terms of schedules, it quantifies over all schedules, so the constant schedule fun _⇒ mps c recovers the fact for the single state mps c.

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

Next, the service received by a given job j in a given multiprocessor state mps on a given core c is exactly the service received by j in (mps c).

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 cores of the multiprocessor.