Library prosa.analysis.definitions.busy_interval
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
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 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.
Next, consider any ideal uniprocessor 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 638)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
H1 : 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 767)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
H1 : JLFP_policy Job
j : Job
t : instant
============================
quiet_time_dec j t -> quiet_time j t
subgoal 2 (ID 768) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
- intros QT s ARRs HPs BEFs.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 774)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 768) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
move: QT ⇒ /allP QT.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 810)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 768) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
specialize (QT s); feed QT.
(* ----------------------------------[ coqtop ]---------------------------------
3 focused subgoals
(shelved: 1) (ID 813)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 818) is:
completed_by sched s t
subgoal 3 (ID 768) 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 818)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 768) 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 768)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
H1 : 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 893)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
H1 : 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 924)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
----------------------------------------------------------------------------- *)
apply/implyP; intros HPs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 949)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
----------------------------------------------------------------------------- *)
apply QT; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 950)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 952) is:
arrived_before s t
----------------------------------------------------------------------------- *)
+ by apply in_arrivals_implies_arrived in ARRs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 952)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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.
(* ----------------------------------[ 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 638)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
H1 : 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 767)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
H1 : JLFP_policy Job
j : Job
t : instant
============================
quiet_time_dec j t -> quiet_time j t
subgoal 2 (ID 768) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
- intros QT s ARRs HPs BEFs.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 774)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 768) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
move: QT ⇒ /allP QT.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 810)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 768) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
specialize (QT s); feed QT.
(* ----------------------------------[ coqtop ]---------------------------------
3 focused subgoals
(shelved: 1) (ID 813)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 818) is:
completed_by sched s t
subgoal 3 (ID 768) 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 818)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 768) 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 768)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
H1 : 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 893)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
H1 : 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 924)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
----------------------------------------------------------------------------- *)
apply/implyP; intros HPs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 949)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
----------------------------------------------------------------------------- *)
apply QT; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 950)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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
subgoal 2 (ID 952) is:
arrived_before s t
----------------------------------------------------------------------------- *)
+ by apply in_arrivals_implies_arrived in ARRs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 952)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (processor_state Job)
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End DecidableQuietTime.
End BusyIntervalJLFP.