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. *) Section Progress. (** 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... *) Variable sched : schedule PState. Variable j : Job. Section NotionsOfProgress. (** ...and two ordered points in time... *) Variable t1 t2 : nat. Hypothesis H_t1_before_t2: t1 <= t2. (** ... we say that the job has progressed between the two points iff its total received service has increased. *) Definition job_has_progressed := service sched j t1 < service sched j t2. (** Conversely, if the accumulated service does not change, there is no progress. *) Definition no_progress := service sched j t1 == service sched j t2. (** We note that the negation of the former is equivalent to the latter definition. *)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

~~ job_has_progressed <-> no_progress
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

~~ job_has_progressed <-> no_progress
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

~~ (service sched j t1 < service sched j t2) <-> service sched j t1 == service sched j t2
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

~~ (service sched j t1 < service sched j t2) -> service sched j t1 == service sched j t2
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2
service sched j t1 == service sched j t2 -> ~~ (service sched j t1 < service sched j t2)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

~~ (service sched j t1 < service sched j t2) -> service sched j t1 == service sched j t2
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2
LT: service sched j t2 < service sched j t1

service sched j t1 == service sched j t2
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2
LT: service sched j t2 < service sched j t1

False
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2
LT: service sched j t2 < service sched j t1
MONO: service sched j t1 <= service sched j t2

False
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2
LT: service sched j t2 < service sched j t1
MONO: service sched j t1 <= service sched j t2
NOT_MONO: ~~ (service sched j t1 <= service sched j t2)

False
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2
LT: service sched j t2 < service sched j t1
MONO: service sched j t1 <= service sched j t2
NOT_MONO: ~ service sched j t1 <= service sched j t2

False
contradiction.
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

service sched j t1 == service sched j t2 -> ~~ (service sched j t1 < service sched j t2)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

service sched j t1 == service sched j t2 -> ~~ (service sched j t1 < service sched j t2)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

~~ (service sched j t2 < service sched j t2)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t1, t2: nat
H_t1_before_t2: t1 <= t2

service sched j t2 <= service sched j t2
by apply service_monotonic. } Qed. End NotionsOfProgress. (** 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. *) Definition no_progress_for (t : instant) (delta : duration) := no_progress (t - delta) t. End Progress.