Library prosa.behavior.schedule


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.behavior.arrival_sequence.

Generic Processor State

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 predicates and an invariant that must be defined by 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.
Class ProcessorState (Job : JobType) (State : Type) :=
  {
    
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.)
    Core : finType;
    
For a given processor state and core, the [scheduled_on] predicate checks whether a given job is running on the given core.
    scheduled_on : Job State Core bool;
    
For a given processor state and core, the [service_on] function determines how much service a given job receives on the given core).
    service_on : Job State Core work;
    
For a given processor state and core, a job does not receive service if it is not scheduled in that state on that core.
    service_on_implies_scheduled_on :
       j s r, ~~ scheduled_on j s r service_on j s r = 0
  }.

The definition [ProcessorState] above is based on [scheduled_on] and [service_on], describing the state of a job in a given core. Sometimes, it’s more convenient to directly check whether a job is scheduled at all, and how much service the job receives across all cores. The functions [scheduled_in] and [service_in] compute these notions given an instance of [ProcessorState].
Section ProcessorIn.
  Context {Job : JobType}.
  Context {State : Type}.
  Context `{ProcessorState Job State}.

For a given processor state, the [scheduled_in] predicate checks whether a given job is running on any core in that state.
  Definition scheduled_in (j : Job) (s : State) : bool :=
    [ c : Core, scheduled_on j s c].

For a given processor state, the [service_in] function determines how much service a given job receives in that state (across all cores).
  Definition service_in (j : Job) (s : State) : work :=
    \sum_(r : Core) service_on j s r.

End ProcessorIn.

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

Definition schedule (PState : Type) := instant PState.

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.
Global Opaque scheduled_on service_on.