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. (** * Busy Interval for JLFP-models *) (** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *) Section BusyIntervalJLFP. (** Consider any type of jobs. *) Context {Job : JobType}. Context `{JobArrival Job}. Context `{JobCost Job}. (** Consider any kind of processor state model. *) Context {PState : ProcessorState Job}. (** Consider any arrival sequence with consistent arrivals ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq. (** ... and a schedule of this arrival sequence. *) Variable sched : schedule PState. (** Assume a given JLFP policy. *) Context `{JLFP_policy Job}. (** In this section, we define the notion of a busy interval. *) Section BusyInterval. (** Consider any job j. *) Variable j : Job. Hypothesis H_from_arrival_sequence : arrives_in arr_seq j. (** We say that [t] is a quiet time for [j] iff every higher-priority job from the arrival sequence that arrived before [t] has completed by that time. *) Definition quiet_time (t : instant) := forall (j_hp : Job), arrives_in arr_seq j_hp -> hep_job j_hp j -> arrived_before j_hp t -> completed_by sched j_hp t. (** Based on the definition of quiet time, we say that interval <<[t1, t_busy)>> is a (potentially unbounded) busy-interval prefix iff the interval starts with a quiet time where a higher or equal priority job is released and remains non-quiet. We also require job [j] to be released in the interval. *) Definition busy_interval_prefix (t1 t_busy : instant) := t1 < t_busy /\ quiet_time t1 /\ (forall t, t1 < t < t_busy -> ~ quiet_time t) /\ t1 <= job_arrival j < t_busy. (** Next, we say that an interval <<[t1, t2)>> is a busy interval iff <<[t1, t2)>> is a busy-interval prefix and [t2] is a quiet time. *) Definition busy_interval (t1 t2 : instant) := busy_interval_prefix t1 t2 /\ quiet_time t2. End BusyInterval. (** In this section we define the computational version of the notion of quiet time. *) Section DecidableQuietTime. (** We say that t is a quiet time for [j] iff every higher-priority job from the arrival sequence that arrived before [t] has completed by that time. *) Definition quiet_time_dec (j : Job) (t : instant) := all (fun j_hp => hep_job j_hp j ==> (completed_by sched j_hp t)) (arrivals_before arr_seq t). (** We also show that the computational and propositional definitions are equivalent. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job

forall (j : Job) (t : instant), reflect (quiet_time j t) (quiet_time_dec j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job

forall (j : Job) (t : instant), reflect (quiet_time j t) (quiet_time_dec j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant

quiet_time_dec j t -> quiet_time j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant

quiet_time_dec j t -> quiet_time j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time_dec j t
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t

completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: {in arrivals_before arr_seq t, forall x : Job, hep_job x j ==> completed_by sched x t}

completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: s \in arrivals_before arr_seq t -> (fun x : Job => is_true (hep_job x j ==> completed_by sched x t)) s

s \in arrivals_before arr_seq t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: (fun x : Job => is_true (hep_job x j ==> completed_by sched x t)) s
completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: s \in arrivals_before arr_seq t -> (fun x : Job => is_true (hep_job x j ==> completed_by sched x t)) s

s \in arrivals_before arr_seq t
by eapply arrived_between_implies_in_arrivals; eauto 2.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: (fun x : Job => is_true (hep_job x j ==> completed_by sched x t)) s

completed_by sched s t
by move: QT => /implyP Q; apply Q in HPs.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant

~~ quiet_time_dec j t -> ~ quiet_time j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t

quiet_time_dec j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t

hep_job s j ==> completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j

completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j

arrives_in arr_seq s
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j
arrived_before s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j

arrives_in arr_seq s
by apply in_arrivals_implies_arrived in ARRs.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j

arrived_before s t
by eapply in_arrivals_implies_arrived_between in ARRs; eauto 2. Qed. End DecidableQuietTime. End BusyIntervalJLFP.