Library prosa.analysis.definitions.busy_interval
Require Export prosa.model.priority.classes.
Require Export prosa.analysis.facts.behavior.completion.
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.
Consider any type of jobs.
Consider any kind of processor state model.
Consider any arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
... and a schedule of this arrival sequence.
Assume a given JLFP policy.
In this section, we define the notion of a busy interval.
Consider any job 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) :=
∀ (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.
∀ (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 ∧
(∀ t, t1 < t < t_busy → ¬ quiet_time t) ∧
t1 ≤ job_arrival j < t_busy.
t1 < t_busy ∧
quiet_time t1 ∧
(∀ 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.
busy_interval_prefix t1 t2 ∧
quiet_time t2.
End BusyInterval.
In this section we define the computational
version of the notion of quiet time.
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).
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.
Lemma quiet_time_P :
∀ j t, reflect (quiet_time j t) (quiet_time_dec j t).
Proof.
intros; apply/introP.
- intros QT s ARRs HPs BEFs.
move: QT ⇒ /allP QT.
specialize (QT s); feed QT.
eapply arrived_between_implies_in_arrivals; eauto 2.
by move: QT ⇒ /implyP Q; apply Q in HPs.
- move ⇒ /negP DEC; intros QT; apply: DEC.
apply/allP; intros s ARRs.
apply/implyP; intros HPs.
apply QT; try done.
+ by apply in_arrivals_implies_arrived in ARRs.
+ by eapply in_arrivals_implies_arrived_between in ARRs; eauto 2.
Qed.
End DecidableQuietTime.
End BusyIntervalJLFP.
∀ j t, reflect (quiet_time j t) (quiet_time_dec j t).
Proof.
intros; apply/introP.
- intros QT s ARRs HPs BEFs.
move: QT ⇒ /allP QT.
specialize (QT s); feed QT.
eapply arrived_between_implies_in_arrivals; eauto 2.
by move: QT ⇒ /implyP Q; apply Q in HPs.
- move ⇒ /negP DEC; intros QT; apply: DEC.
apply/allP; intros s ARRs.
apply/implyP; intros HPs.
apply QT; try done.
+ by apply in_arrivals_implies_arrived in ARRs.
+ by eapply in_arrivals_implies_arrived_between in ARRs; eauto 2.
Qed.
End DecidableQuietTime.
End BusyIntervalJLFP.