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
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).
For a given processor state and core, a job does not receive service if it is
not scheduled in that state on that core.
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}.
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.
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.
\sum_(r : Core) service_on j s r.
End ProcessorIn.
Schedule Representation
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.