Generic Processor State Interface

Rather than choosing a specific schedule representation up front, we define the notion of a generic processor state, which allows us to state general definitions of core concepts (such as "how much service has a job received") that work across many possible scenarios (e.g., ideal uniprocessor schedules, schedules with overheads, variable-speed processors, multiprocessors, etc.). A concrete processor state type precisely determines how all relevant aspects of the execution environment are modeled (e.g., scheduled jobs, overheads, spinning). Here, we define just the common interface of all possible concrete processor states by means of a type class, i.e., we define a few generic functions and an invariant that must be defined for all concrete processor state types. In the most simple case (i.e., an ideal uniprocessor state—see model/processor/ideal.v), at any given time, either a particular job is scheduled or the processor is idle.

A ProcessorState instance provides a finite set of cores on which jobs can be scheduled. In the case of uniprocessors, this is irrelevant and may be ignored (by convention, the unit type is used as a placeholder in uniprocessor schedules, but this is not important). (Hint to the Coq novice: finType just means some type with finitely many values, i.e., it is possible to enumerate all cores of a multi-processor.)

For a given processor state and core, the scheduled_on predicate checks whether a given job is running on the given core.

For a given processor state and core, the service_on function determines how much service a given job receives on the given core).

We require scheduled_on and service_on to be consistent in the sense that a job can receive service (on a given core) only if it is also scheduled (on that core).

The above definition of the ProcessorState interface provides the predicate scheduled_on and the function service_on, which relate a given job to a given core in a given state. This level of detail is required for generality, but in many situations it suffices and is more convenient to elide the information about individual cores, instead referring to all cores at once. To this end, we next define the short-hand functions scheduled_in and service_in to directly check whether a job is scheduled at all (i.e., on any core), and how much service the job receives anywhere (i.e., across all cores).

Consider any type of jobs...

...and any type of processor state.

For a given processor state, the scheduled_in predicate checks whether a given job is running on any core in that state.

For a given processor state, the service_in function determines how much service a given job receives in that state (across all cores).

Schedule Representation

In Prosa, schedules are represented as functions, which allows us to model potentially infinite schedules. More specifically, a schedule simply maps each instant to a processor state, which reflects state of the computing platform at the specific time (e.g., which job is presently scheduled).

The following line instructs Coq to not let proofs use knowledge of how scheduled_on and service_on are defined. Instead, proofs must rely on basic lemmas about processor state classes.