Library rt.restructuring.analysis.definitions.busy_interval
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Export all.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Export all.
From rt.restructuring.model Require Export job task.
From rt.restructuring.model.schedule Require Export work_conserving.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
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 →
higher_eq_priority j_hp j →
arrived_before j_hp t →
completed_by sched j_hp t.
∀ (j_hp : Job),
arrives_in arr_seq j_hp →
higher_eq_priority 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 ⇒ higher_eq_priority j_hp j ==> (completed_by sched j_hp t))
(arrivals_before arr_seq t).
all
(fun j_hp ⇒ higher_eq_priority 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 179)
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)
higher_eq_priority : 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 308)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
============================
quiet_time_dec j t -> quiet_time j t
subgoal 2 (ID 309) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
- intros QT s ARRs HPs BEFs.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 315)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time_dec j t
s : Job
ARRs : arrives_in arr_seq s
HPs : higher_eq_priority s j
BEFs : arrived_before s t
============================
completed_by sched s t
subgoal 2 (ID 309) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
move: QT ⇒ /allP QT.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 351)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
s : Job
ARRs : arrives_in arr_seq s
HPs : higher_eq_priority s j
BEFs : arrived_before s t
QT : {in arrivals_before arr_seq t,
forall x : Job, higher_eq_priority x j ==> completed_by sched x t}
============================
completed_by sched s t
subgoal 2 (ID 309) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
specialize (QT s); feed QT.
(* ----------------------------------[ coqtop ]---------------------------------
3 focused subgoals
(shelved: 1) (ID 354)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
s : Job
ARRs : arrives_in arr_seq s
HPs : higher_eq_priority s j
BEFs : arrived_before s t
QT : s \in arrivals_before arr_seq t ->
(fun x : Job =>
is_true (higher_eq_priority x j ==> completed_by sched x t)) s
============================
s \in arrivals_before arr_seq t
subgoal 2 (ID 359) is:
completed_by sched s t
subgoal 3 (ID 309) 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 359)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
s : Job
ARRs : arrives_in arr_seq s
HPs : higher_eq_priority s j
BEFs : arrived_before s t
QT : (fun x : Job =>
is_true (higher_eq_priority x j ==> completed_by sched x t)) s
============================
completed_by sched s t
subgoal 2 (ID 309) 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 309)
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)
higher_eq_priority : 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 434)
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)
higher_eq_priority : 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 465)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
s : Job
ARRs : s \in arrivals_before arr_seq t
============================
higher_eq_priority s j ==> completed_by sched s t
----------------------------------------------------------------------------- *)
apply/implyP; intros HPs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 490)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
s : Job
ARRs : s \in arrivals_before arr_seq t
HPs : higher_eq_priority s j
============================
completed_by sched s t
----------------------------------------------------------------------------- *)
apply QT; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 491)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
s : Job
ARRs : s \in arrivals_before arr_seq t
HPs : higher_eq_priority s j
============================
arrives_in arr_seq s
subgoal 2 (ID 493) is:
arrived_before s t
----------------------------------------------------------------------------- *)
+ by apply in_arrivals_implies_arrived in ARRs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 493)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
s : Job
ARRs : s \in arrivals_before arr_seq t
HPs : higher_eq_priority 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 179)
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)
higher_eq_priority : 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 308)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
============================
quiet_time_dec j t -> quiet_time j t
subgoal 2 (ID 309) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
- intros QT s ARRs HPs BEFs.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 315)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time_dec j t
s : Job
ARRs : arrives_in arr_seq s
HPs : higher_eq_priority s j
BEFs : arrived_before s t
============================
completed_by sched s t
subgoal 2 (ID 309) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
move: QT ⇒ /allP QT.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 351)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
s : Job
ARRs : arrives_in arr_seq s
HPs : higher_eq_priority s j
BEFs : arrived_before s t
QT : {in arrivals_before arr_seq t,
forall x : Job, higher_eq_priority x j ==> completed_by sched x t}
============================
completed_by sched s t
subgoal 2 (ID 309) is:
~~ quiet_time_dec j t -> ~ quiet_time j t
----------------------------------------------------------------------------- *)
specialize (QT s); feed QT.
(* ----------------------------------[ coqtop ]---------------------------------
3 focused subgoals
(shelved: 1) (ID 354)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
s : Job
ARRs : arrives_in arr_seq s
HPs : higher_eq_priority s j
BEFs : arrived_before s t
QT : s \in arrivals_before arr_seq t ->
(fun x : Job =>
is_true (higher_eq_priority x j ==> completed_by sched x t)) s
============================
s \in arrivals_before arr_seq t
subgoal 2 (ID 359) is:
completed_by sched s t
subgoal 3 (ID 309) 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 359)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
s : Job
ARRs : arrives_in arr_seq s
HPs : higher_eq_priority s j
BEFs : arrived_before s t
QT : (fun x : Job =>
is_true (higher_eq_priority x j ==> completed_by sched x t)) s
============================
completed_by sched s t
subgoal 2 (ID 309) 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 309)
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)
higher_eq_priority : 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 434)
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)
higher_eq_priority : 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 465)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
s : Job
ARRs : s \in arrivals_before arr_seq t
============================
higher_eq_priority s j ==> completed_by sched s t
----------------------------------------------------------------------------- *)
apply/implyP; intros HPs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 490)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
s : Job
ARRs : s \in arrivals_before arr_seq t
HPs : higher_eq_priority s j
============================
completed_by sched s t
----------------------------------------------------------------------------- *)
apply QT; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 491)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
s : Job
ARRs : s \in arrivals_before arr_seq t
HPs : higher_eq_priority s j
============================
arrives_in arr_seq s
subgoal 2 (ID 493) is:
arrived_before s t
----------------------------------------------------------------------------- *)
+ by apply in_arrivals_implies_arrived in ARRs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 493)
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)
higher_eq_priority : JLFP_policy Job
j : Job
t : instant
QT : quiet_time j t
s : Job
ARRs : s \in arrivals_before arr_seq t
HPs : higher_eq_priority 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.