Library prosa.analysis.definitions.busy_interval
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.model.priority.classes.
Require Export prosa.analysis.facts.behavior.completion.
Throughout this file, we assume ideal uniprocessor schedules.
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 32)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : JLFP_policy Job
============================
forall (j : Job) (t : instant),
reflect (quiet_time j t) (quiet_time_dec j t)
----------------------------------------------------------------------------- *)
Proof.
intros; apply/introP.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 2) (ID 161)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : JLFP_policy Job
j : Job
t : instant
============================
quiet_time_dec j t -> quiet_time j t
subgoal 2 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
- intros QT s ARRs HPs BEFs.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 168)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
move: QT ⇒ /allP QT.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 203)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
specialize (QT s); feed QT.
(* ----------------------------------[ coqtop ]---------------------------------
3 focused subgoals
(shelved: 1) (ID 206)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 211) is:
completed_by sched s t
subgoal 3 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
eapply arrived_between_implies_in_arrivals; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 211)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
by move: QT ⇒ /implyP Q; apply Q in HPs.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 162)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : JLFP_policy Job
j : Job
t : instant
============================
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
- move ⇒ /negP DEC; intros QT; apply: DEC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 283)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
============================
quiet_time_dec j t
----------------------------------------------------------------------------- *)
apply/allP; intros s ARRs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 314)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
----------------------------------------------------------------------------- *)
apply/implyP; intros HPs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 339)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
----------------------------------------------------------------------------- *)
apply QT; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 340)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 342) is:
arrived_before s t
----------------------------------------------------------------------------- *)
+ by apply in_arrivals_implies_arrived in ARRs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 342)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End DecidableQuietTime.
End BusyIntervalJLFP.
∀ j t, reflect (quiet_time j t) (quiet_time_dec j t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 32)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : JLFP_policy Job
============================
forall (j : Job) (t : instant),
reflect (quiet_time j t) (quiet_time_dec j t)
----------------------------------------------------------------------------- *)
Proof.
intros; apply/introP.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 2) (ID 161)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : JLFP_policy Job
j : Job
t : instant
============================
quiet_time_dec j t -> quiet_time j t
subgoal 2 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
- intros QT s ARRs HPs BEFs.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 168)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
move: QT ⇒ /allP QT.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 203)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
specialize (QT s); feed QT.
(* ----------------------------------[ coqtop ]---------------------------------
3 focused subgoals
(shelved: 1) (ID 206)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 211) is:
completed_by sched s t
subgoal 3 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
eapply arrived_between_implies_in_arrivals; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 211)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 162) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
by move: QT ⇒ /implyP Q; apply Q in HPs.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 162)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : JLFP_policy Job
j : Job
t : instant
============================
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
- move ⇒ /negP DEC; intros QT; apply: DEC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 283)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
============================
quiet_time_dec j t
----------------------------------------------------------------------------- *)
apply/allP; intros s ARRs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 314)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
----------------------------------------------------------------------------- *)
apply/implyP; intros HPs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 339)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
----------------------------------------------------------------------------- *)
apply QT; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 340)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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
subgoal 2 (ID 342) is:
arrived_before s t
----------------------------------------------------------------------------- *)
+ by apply in_arrivals_implies_arrived in ARRs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 342)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule PState
H2 : 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End DecidableQuietTime.
End BusyIntervalJLFP.