Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.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]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_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]
(** * Deadlines *) (** In this file, we observe basic properties of the behavioral job model w.r.t. deadlines. *) Section DeadlineFacts. (** Consider any given type of jobs with costs and deadlines... *) Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}. (** ... any given type of processor states. *) Context {PState: ProcessorState Job}. (** First, we derive two properties from the fact that a job is incomplete at some point in time. *) Section Incompletion. (** Consider any given schedule. *) Variable sched: schedule PState. (** Trivially, a job that both meets its deadline and is incomplete at a time [t] must have a deadline later than [t]. *)
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState

forall (j : Job) (t : instant), job_meets_deadline sched j -> ~~ completed_by sched j t -> t < job_deadline j
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState

forall (j : Job) (t : instant), job_meets_deadline sched j -> ~~ completed_by sched j t -> t < job_deadline j
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t
PAST_DL: job_deadline j <= t

false
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t
PAST_DL: job_deadline j <= t

~~ completed_by sched j (job_deadline j)
exact: incompletion_monotonic INCOMP. Qed. (** Furthermore, a job that both meets its deadline and is incomplete at a time [t] must be scheduled at some point between [t] and its deadline. *)
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState

forall (j : Job) (t : instant), job_meets_deadline sched j -> ~~ completed_by sched j t -> exists t' : nat, t <= t' < job_deadline j /\ scheduled_at sched j t'
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState

forall (j : Job) (t : instant), job_meets_deadline sched j -> ~~ completed_by sched j t -> exists t' : nat, t <= t' < job_deadline j /\ scheduled_at sched j t'
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t

exists t' : nat, t <= t' < job_deadline j /\ scheduled_at sched j t'
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t

0 < service_during sched j t (job_deadline j)
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t

service sched j t < service sched j t + service_during sched j t (job_deadline j)
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t

service sched j t < service sched j (job_deadline j)
by apply: leq_trans MET; rewrite less_service_than_cost_is_incomplete. Qed. End Incompletion. (** Next, we look at schedules / processor models in which scheduled jobs always receive service. *) Section IdealProgressSchedules. (** Consider a given reference schedule... *) Variable sched: schedule PState. (** ...in which complete jobs don't execute... *) Hypothesis H_completed_jobs: completed_jobs_dont_execute sched. (** ...and scheduled jobs always receive service. *) Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState. (** We observe that if a job meets its deadline and is scheduled at time [t], then then its deadline is at a time later than t. *)
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall (j : Job) (t : instant), job_meets_deadline sched j -> scheduled_at sched j t -> t < job_deadline j
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall (j : Job) (t : instant), job_meets_deadline sched j -> scheduled_at sched j t -> t < job_deadline j
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState
j: Job
t: instant
MET: job_meets_deadline sched j
SCHED_AT: scheduled_at sched j t

t < job_deadline j
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState
j: Job
t: instant
MET: job_meets_deadline sched j
SCHED_AT: scheduled_at sched j t

~~ completed_by sched j t
exact: scheduled_implies_not_completed. Qed. End IdealProgressSchedules. (** In the following section, we observe that it is sufficient to establish that service is invariant across two schedules at a job's deadline to establish that it either meets its deadline in both schedules or none. *) Section EqualProgress. (** Consider any two schedules [sched] and [sched']. *) Variable sched sched': schedule PState. (** We observe that, if the service is invariant at the time of a job's absolute deadline, and if the job meets its deadline in one of the schedules, then it meets its deadline also in the other schedule. *)
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched, sched': schedule PState

forall j : Job, service sched j (job_deadline j) = service sched' j (job_deadline j) -> job_meets_deadline sched j <-> job_meets_deadline sched' j
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched, sched': schedule PState

forall j : Job, service sched j (job_deadline j) = service sched' j (job_deadline j) -> job_meets_deadline sched j <-> job_meets_deadline sched' j
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched, sched': schedule PState
j: Job
SERVICE: service sched j (job_deadline j) = service sched' j (job_deadline j)

job_meets_deadline sched j <-> job_meets_deadline sched' j
by split; rewrite /job_meets_deadline /completed_by -SERVICE. Qed. End EqualProgress. End DeadlineFacts.