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]
Require Export prosa.analysis.facts.behavior.completion. Require Export prosa.analysis.definitions.readiness. Require Export prosa.analysis.definitions.work_bearing_readiness. Section LiuAndLaylandReadiness. (** We assume the basic (i.e., Liu & Layland) readiness model under which any pending job is ready. *) #[local] Existing Instance basic_ready_instance. (** Consider any kind of jobs ... *) Context {Job : JobType}. (** ... and any kind of processor state. *) Context {PState : ProcessorState Job}. (** Suppose jobs have an arrival time and a cost. *) Context `{JobArrival Job} `{JobCost Job}. (** The Liu & Layland readiness model is trivially non-clairvoyant. *)
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job

nonclairvoyant_readiness basic_ready_instance
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job

nonclairvoyant_readiness basic_ready_instance
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
sched, sched': schedule PState
j: Job
h: instant
PREFIX: identical_prefix sched sched' h
t: nat
IN: t <= h

job_ready sched j t = job_ready sched' j t
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
sched, sched': schedule PState
j: Job
h: instant
PREFIX: identical_prefix sched sched' h
t: nat
IN: t <= h

pending sched j t = pending sched' j t
now apply (identical_prefix_pending _ _ h). Qed. (** Consider any job arrival sequence ... *) Variable arr_seq : arrival_sequence Job. (** ... and any schedule of these jobs. *) Variable sched : schedule PState. (** In the basic Liu & Layland model, a schedule satisfies that only ready jobs execute as long as jobs must arrive to execute and completed jobs don't execute, which we note with the following theorem. *)
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState

jobs_must_arrive_to_execute sched -> completed_jobs_dont_execute sched -> jobs_must_be_ready_to_execute sched
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState

jobs_must_arrive_to_execute sched -> completed_jobs_dont_execute sched -> jobs_must_be_ready_to_execute sched
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched

jobs_must_be_ready_to_execute sched
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t

job_ready sched j t
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t

has_arrived j t && ~~ completed_by sched j t
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t

has_arrived j t
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t
~~ completed_by sched j t
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t

has_arrived j t
by apply ARR.
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t

~~ completed_by sched j t
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
ARR: jobs_must_arrive_to_execute sched
COMP: completed_jobs_dont_execute sched
j: Job
t: instant
SCHED: scheduled_at sched j t

service sched j t < job_cost j
by apply COMP. Qed. (** Consider a JLFP policy that indicates a reflexive higher-or-equal priority relation. *) Context {JLFP : JLFP_policy Job}. Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP. (** We show that the basic readiness model is a work-bearing readiness model. That is, at any time instant [t], if a job [j] is pending, then there exists a job (namely [j] itself) with higher-or-equal priority that is ready at time [t]. *)
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP

work_bearing_readiness arr_seq sched
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP

work_bearing_readiness arr_seq sched
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities JLFP
j: Job
t: instant
ARR: arrives_in arr_seq j
PEND: pending sched j t

exists j_hp : Job, arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
exists j; repeat split => //. Qed. End LiuAndLaylandReadiness. (** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically. *) Global Hint Resolve basic_readiness_is_work_bearing_readiness : basic_rt_facts.