Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** * Job Progress (or Lack Thereof) *)(** In the following section, we define a notion of "job progress", and conversely a notion of a lack of progress. *)SectionProgress.(** Consider any type of jobs with a known cost... *)Context {Job : JobType}.Context `{JobCost Job}.(** ... and any kind of schedule. *)Context {PState : ProcessorState Job}.(** For a given job and a given schedule... *)Variablesched : schedule PState.Variablej : Job.SectionNotionsOfProgress.(** ...and two ordered points in time... *)Variablet1t2 : nat.HypothesisH_t1_before_t2: t1 <= t2.(** ... we say that the job has progressed between the two points iff its total received service has increased. *)Definitionjob_has_progressed := service sched j t1 < service sched j t2.(** Conversely, if the accumulated service does not change, there is no progress. *)Definitionno_progress := service sched j t1 == service sched j t2.(** We note that the negation of the former is equivalent to the latter definition. *)
byapply service_monotonic.}Qed.EndNotionsOfProgress.(** For convenience, we define a lack of progress also in terms of given reference point [t] and the length of the preceding interval of inactivity [delta], meaning that no progress has been made for at least [delta] time units. *)Definitionno_progress_for (t : instant) (delta : duration) := no_progress (t - delta) t.EndProgress.