Library prosa.analysis.facts.busy_interval.hep_at_pt
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.busy_interval.existence.
Require Export prosa.util.tactics.
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.analysis.facts.model.preemption.
Require Export prosa.analysis.facts.busy_interval.existence.
Require Export prosa.util.tactics.
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.analysis.facts.model.preemption.
Processor Executes HEP jobs at Preemption Point
Consider any type of jobs associated with these tasks.
Consider any arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
... and any uniprocessor schedule of this arrival sequence.
Context {PState : ProcessorState Job}.
Hypothesis H_uni : uniprocessor_model PState.
Variable sched : schedule PState.
Hypothesis H_uni : uniprocessor_model PState.
Variable sched : schedule PState.
Consider a JLFP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive.
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
In addition, we assume the existence of a function mapping a job
and its progress to a boolean value saying whether this job is
preemptable at its current point of execution.
Further, allow for any work-bearing notion of job readiness.
Context `{@JobReady Job PState Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
We assume that the schedule is valid and that all jobs come from the arrival sequence.
Next, we assume that the schedule is a work-conserving schedule...
... and the schedule respects the scheduling policy at every preemption point.
Consider any job j with positive job cost.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Consider any busy interval prefix
[t1, t2) of job j.
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix :
busy_interval_prefix arr_seq sched j t1 t2.
Hypothesis H_busy_interval_prefix :
busy_interval_prefix arr_seq sched j t1 t2.
Consider an arbitrary preemption time t ∈
[t1,t2).
Variable t : instant.
Hypothesis H_t_in_busy_interval : t1 ≤ t < t2.
Hypothesis H_t_preemption_time : preemption_time arr_seq sched t.
Hypothesis H_t_in_busy_interval : t1 ≤ t < t2.
Hypothesis H_t_preemption_time : preemption_time arr_seq sched t.
Lemma instant_t_is_not_idle:
¬ is_idle arr_seq sched t.
Proof.
by move ⇒ IDLE; apply: not_quiet_implies_not_idle ⇒ //.
Qed.
¬ is_idle arr_seq sched t.
Proof.
by move ⇒ IDLE; apply: not_quiet_implies_not_idle ⇒ //.
Qed.
Next we consider two cases:
(1) t is less than t2 - 1 and
(2) t is equal to t2 - 1.
In case when t < t2 - 1, we use the fact that time instant
t+1 is not a quiet time. The later implies that there is a
pending higher-or-equal priority job at time t. Thus, the
assumption that the schedule respects priority policy at
preemption points implies that the scheduled job must have a
higher-or-equal priority.
Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_lt:
t < t2.-1 →
∀ jhp,
scheduled_at sched jhp t →
hep_job jhp j.
Proof.
intros LTt2m1 jlp Sched_jlp; apply contraT; move ⇒ /negP NOTHP; exfalso.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) ⇒ /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
apply NOTQUIET with (t := t.+1).
{ apply/andP; split.
- by apply leq_ltn_trans with t1.
- rewrite -subn1 ltn_subRL addnC in LTt2m1.
by rewrite -[t.+1]addn1.
}
intros j_hp ARR HP BEF.
apply contraT ⇒ NCOMP'; exfalso.
have PEND : pending sched j_hp t.
{ apply/andP; split.
- by rewrite /has_arrived.
- by move: NCOMP'; apply contra, completion_monotonic.
}
apply H_job_ready in PEND ⇒ //; destruct PEND as [j' [ARR' [READY' HEP']]].
have HEP : hep_job j' j by apply (H_priority_is_transitive j_hp).
clear HEP' NCOMP' BEF HP ARR j_hp.
have BACK: backlogged sched j' t.
{ apply/andP; split⇒ [//|].
apply/negP; intro SCHED'.
move: (H_uni jlp j' sched t Sched_jlp SCHED') ⇒ EQ.
by subst; apply: NOTHP.
}
apply NOTHP, (H_priority_is_transitive j'); last by eapply HEP.
by eapply H_respects_policy; eauto .
Qed.
t < t2.-1 →
∀ jhp,
scheduled_at sched jhp t →
hep_job jhp j.
Proof.
intros LTt2m1 jlp Sched_jlp; apply contraT; move ⇒ /negP NOTHP; exfalso.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) ⇒ /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
apply NOTQUIET with (t := t.+1).
{ apply/andP; split.
- by apply leq_ltn_trans with t1.
- rewrite -subn1 ltn_subRL addnC in LTt2m1.
by rewrite -[t.+1]addn1.
}
intros j_hp ARR HP BEF.
apply contraT ⇒ NCOMP'; exfalso.
have PEND : pending sched j_hp t.
{ apply/andP; split.
- by rewrite /has_arrived.
- by move: NCOMP'; apply contra, completion_monotonic.
}
apply H_job_ready in PEND ⇒ //; destruct PEND as [j' [ARR' [READY' HEP']]].
have HEP : hep_job j' j by apply (H_priority_is_transitive j_hp).
clear HEP' NCOMP' BEF HP ARR j_hp.
have BACK: backlogged sched j' t.
{ apply/andP; split⇒ [//|].
apply/negP; intro SCHED'.
move: (H_uni jlp j' sched t Sched_jlp SCHED') ⇒ EQ.
by subst; apply: NOTHP.
}
apply NOTHP, (H_priority_is_transitive j'); last by eapply HEP.
by eapply H_respects_policy; eauto .
Qed.
In the case when t = t2 - 1, we cannot use the same proof
since t+1 = t2, but t2 is a quiet time. So we do a similar
case analysis on the fact that t1 = t ∨ t1 < t.
Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_eq:
t = t2.-1 →
∀ jhp,
scheduled_at sched jhp t →
hep_job jhp j.
Proof.
intros EQUALt2m1 jlp Sched_jlp; apply contraT; move ⇒ /negP NOTHP; exfalso.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) ⇒ /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
rewrite leq_eqVlt in GEt; first move: GEt ⇒ /orP [/eqP EQUALt1 | LARGERt1].
{ subst t t1; clear LEt SL.
have ARR : job_arrival j = t2.-1.
{ apply/eqP; rewrite eq_sym eqn_leq.
destruct t2 ⇒ [//|].
rewrite ltnS -pred_Sn in INBI.
by rewrite -pred_Sn.
}
have PEND: pending sched j t2.-1
by rewrite -ARR; apply job_pending_at_arrival.
apply H_job_ready in PEND ⇒ //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
eapply NOTHP, H_priority_is_transitive; last by apply HEPhp.
apply (H_respects_policy _ _ t2.-1); auto.
apply/andP; split⇒ [//|].
apply/negP; intros SCHED.
move: (H_uni _ _ sched _ SCHED Sched_jlp) ⇒ EQ.
by subst; apply: NOTHP.
}
{ feed (NOTQUIET t); first by apply/andP; split.
apply NOTQUIET; intros j_hp' IN HP ARR.
apply contraT ⇒ NOTCOMP'; exfalso.
have PEND : pending sched j_hp' t.
{ apply/andP; split.
- by rewrite /has_arrived ltnW.
- by move: NOTCOMP'; apply contra, completion_monotonic.
}
apply H_job_ready in PEND ⇒ //; destruct PEND as [j' [ARR' [READY' HEP']]].
have HEP : hep_job j' j by apply (H_priority_is_transitive j_hp').
clear ARR HP IN HEP' NOTCOMP' j_hp'.
have BACK: backlogged sched j' t.
{ apply/andP; split⇒ [//|].
apply/negP; intro SCHED'.
move: (H_uni jlp j' sched t Sched_jlp SCHED') ⇒ EQ.
by subst; apply: NOTHP.
}
apply NOTHP, (H_priority_is_transitive j'); last by eapply HEP.
by eapply H_respects_policy; eauto .
}
Qed.
t = t2.-1 →
∀ jhp,
scheduled_at sched jhp t →
hep_job jhp j.
Proof.
intros EQUALt2m1 jlp Sched_jlp; apply contraT; move ⇒ /negP NOTHP; exfalso.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) ⇒ /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
rewrite leq_eqVlt in GEt; first move: GEt ⇒ /orP [/eqP EQUALt1 | LARGERt1].
{ subst t t1; clear LEt SL.
have ARR : job_arrival j = t2.-1.
{ apply/eqP; rewrite eq_sym eqn_leq.
destruct t2 ⇒ [//|].
rewrite ltnS -pred_Sn in INBI.
by rewrite -pred_Sn.
}
have PEND: pending sched j t2.-1
by rewrite -ARR; apply job_pending_at_arrival.
apply H_job_ready in PEND ⇒ //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
eapply NOTHP, H_priority_is_transitive; last by apply HEPhp.
apply (H_respects_policy _ _ t2.-1); auto.
apply/andP; split⇒ [//|].
apply/negP; intros SCHED.
move: (H_uni _ _ sched _ SCHED Sched_jlp) ⇒ EQ.
by subst; apply: NOTHP.
}
{ feed (NOTQUIET t); first by apply/andP; split.
apply NOTQUIET; intros j_hp' IN HP ARR.
apply contraT ⇒ NOTCOMP'; exfalso.
have PEND : pending sched j_hp' t.
{ apply/andP; split.
- by rewrite /has_arrived ltnW.
- by move: NOTCOMP'; apply contra, completion_monotonic.
}
apply H_job_ready in PEND ⇒ //; destruct PEND as [j' [ARR' [READY' HEP']]].
have HEP : hep_job j' j by apply (H_priority_is_transitive j_hp').
clear ARR HP IN HEP' NOTCOMP' j_hp'.
have BACK: backlogged sched j' t.
{ apply/andP; split⇒ [//|].
apply/negP; intro SCHED'.
move: (H_uni jlp j' sched t Sched_jlp SCHED') ⇒ EQ.
by subst; apply: NOTHP.
}
apply NOTHP, (H_priority_is_transitive j'); last by eapply HEP.
by eapply H_respects_policy; eauto .
}
Qed.
By combining the above facts we conclude that a job that is
scheduled at time t has higher-or-equal priority.
Corollary scheduled_at_preemption_time_implies_higher_or_equal_priority:
∀ jhp,
scheduled_at sched jhp t →
hep_job jhp j.
Proof.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) ⇒ /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
have: t ≤ t2.-1 by rewrite -subn1 leq_subRL_impl // addn1.
rewrite leq_eqVlt ⇒ /orP [/eqP EQUALt2m1 | LTt2m1].
- by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_eq.
- by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_lt.
Qed.
∀ jhp,
scheduled_at sched jhp t →
hep_job jhp j.
Proof.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) ⇒ /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
have: t ≤ t2.-1 by rewrite -subn1 leq_subRL_impl // addn1.
rewrite leq_eqVlt ⇒ /orP [/eqP EQUALt2m1 | LTt2m1].
- by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_eq.
- by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_lt.
Qed.
Since a job that is scheduled at time t has higher-or-equal
priority, by properties of a busy interval it cannot arrive
before time instant t1.
Lemma scheduled_at_preemption_time_implies_arrived_between_within_busy_interval:
∀ jhp,
scheduled_at sched jhp t →
arrived_between jhp t1 t2.
Proof.
intros jhp Sched_jhp.
rename H_work_conserving into WORK.
move: (H_busy_interval_prefix) ⇒ [SL [QUIET [NOTQUIET INBI]]].
move: (H_t_in_busy_interval) ⇒ /andP [GEt LEt].
have HP := scheduled_at_preemption_time_implies_higher_or_equal_priority _ Sched_jhp.
move: (Sched_jhp) ⇒ PENDING.
eapply scheduled_implies_pending in PENDING ⇒ //.
apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING ⇒ /andP [ARR _].
apply contraT; rewrite -ltnNge; intro LT; exfalso.
feed (QUIET jhp) ⇒ //.
specialize (QUIET HP LT).
have COMP: completed_by sched jhp t by apply: completion_monotonic QUIET.
apply completed_implies_not_scheduled in COMP ⇒ //.
by move: COMP ⇒ /negP COMP; apply COMP.
Qed.
∀ jhp,
scheduled_at sched jhp t →
arrived_between jhp t1 t2.
Proof.
intros jhp Sched_jhp.
rename H_work_conserving into WORK.
move: (H_busy_interval_prefix) ⇒ [SL [QUIET [NOTQUIET INBI]]].
move: (H_t_in_busy_interval) ⇒ /andP [GEt LEt].
have HP := scheduled_at_preemption_time_implies_higher_or_equal_priority _ Sched_jhp.
move: (Sched_jhp) ⇒ PENDING.
eapply scheduled_implies_pending in PENDING ⇒ //.
apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING ⇒ /andP [ARR _].
apply contraT; rewrite -ltnNge; intro LT; exfalso.
feed (QUIET jhp) ⇒ //.
specialize (QUIET HP LT).
have COMP: completed_by sched jhp t by apply: completion_monotonic QUIET.
apply completed_implies_not_scheduled in COMP ⇒ //.
by move: COMP ⇒ /negP COMP; apply COMP.
Qed.
From the above lemmas we prove that there is a job jhp that is
(1) scheduled at time t, (2) has higher-or-equal priority, and
(3) arrived between t1 and t2.
Corollary not_quiet_implies_exists_scheduled_hp_job_at_preemption_point:
∃ j_hp,
arrived_between j_hp t1 t2
∧ hep_job j_hp j
∧ scheduled_at sched j_hp t.
Proof.
move: (H_busy_interval_prefix) ⇒ [SL [QUIET [NOTQUIET INBI]]].
move: (H_t_in_busy_interval) ⇒ /andP [GEt LEt].
have [IDLE|[j' SCHED]] := scheduled_at_cases _ H_valid_arrivals sched ltac:(by []) ltac:(by []) t.
- by exfalso; apply instant_t_is_not_idle.
- ∃ j'; repeat split ⇒ //.
× exact: scheduled_at_preemption_time_implies_arrived_between_within_busy_interval.
× exact: scheduled_at_preemption_time_implies_higher_or_equal_priority.
Qed.
End ProcessorBusyWithHEPJobAtPreemptionPoints.
∃ j_hp,
arrived_between j_hp t1 t2
∧ hep_job j_hp j
∧ scheduled_at sched j_hp t.
Proof.
move: (H_busy_interval_prefix) ⇒ [SL [QUIET [NOTQUIET INBI]]].
move: (H_t_in_busy_interval) ⇒ /andP [GEt LEt].
have [IDLE|[j' SCHED]] := scheduled_at_cases _ H_valid_arrivals sched ltac:(by []) ltac:(by []) t.
- by exfalso; apply instant_t_is_not_idle.
- ∃ j'; repeat split ⇒ //.
× exact: scheduled_at_preemption_time_implies_arrived_between_within_busy_interval.
× exact: scheduled_at_preemption_time_implies_higher_or_equal_priority.
Qed.
End ProcessorBusyWithHEPJobAtPreemptionPoints.
Processor Executes HEP Jobs after Preemption Point
In this section, we prove that at any time instant after any preemption point (inside the busy interval), the processor is always busy scheduling a job with higher or equal priority.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
... and any uniprocessor schedule of this arrival sequence.
Context {PState : ProcessorState Job}.
Hypothesis H_uni : uniprocessor_model PState.
Variable sched : schedule PState.
Hypothesis H_uni : uniprocessor_model PState.
Variable sched : schedule PState.
Consider a JLFP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive.
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
Consider a valid preemption model with known maximum non-preemptive
segment lengths.
Context `{TaskMaxNonpreemptiveSegment Task} `{JobPreemptable Job}.
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
Further, allow for any work-bearing notion of job readiness.
We assume that the schedule is valid.
Next, we assume that the schedule is work-conserving ...
... and the schedule respects the scheduling policy at every preemption point.
Consider any job j with positive job cost.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Consider any busy interval prefix
[t1, t2) of job j.
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix :
busy_interval_prefix arr_seq sched j t1 t2.
Hypothesis H_busy_interval_prefix :
busy_interval_prefix arr_seq sched j t1 t2.
First, recall from the above section that the processor at any
preemption time is always busy scheduling a job with higher or equal
priority.
We show that, at any time instant after a preemption point, the
processor is always busy with a job with higher or equal
priority.
Lemma not_quiet_implies_exists_scheduled_hp_job_after_preemption_point:
∀ tp t,
preemption_time arr_seq sched tp →
t1 ≤ tp < t2 →
tp ≤ t < t2 →
∃ j_hp,
arrived_between j_hp t1 t.+1 ∧
hep_job j_hp j ∧
scheduled_at sched j_hp t.
Proof.
move ⇒ tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp LTt].
have [Idle|[jhp Sched_jhp]] :=
scheduled_at_cases _ H_valid_arrivals sched ltac:(by []) ltac:(by []) t.
{ eapply instant_t_is_not_idle in Idle ⇒ //.
by apply/andP; split; first apply leq_trans with tp. }
∃ jhp.
have HP: hep_job jhp j.
{ have PP := scheduling_of_any_segment_starts_with_preemption_time _
arr_seq H_valid_arrivals
sched H_sched_valid H_valid_preemption_model jhp t Sched_jhp.
feed PP ⇒ //.
move: PP ⇒ [prt [/andP [_ LE] [PR SCH]]].
case E:(t1 ≤ prt).
- move: E ⇒ /eqP /eqP E; rewrite subn_eq0 in E.
edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point as [jlp [_ [HEP SCHEDjhp]]] ⇒ //.
{ by apply /andP; split; last by apply leq_ltn_trans with t. }
enough (EQ : jhp = jlp); first by subst.
apply: (H_uni _ _ _ prt); eauto;
by apply SCH; apply/andP; split.
- move: E ⇒ /eqP /neqP E; rewrite -lt0n subn_gt0 in E.
apply negbNE; apply/negP; intros LP; rename jhp into jlp.
edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point
as [jhp [_ [HEP SCHEDjhp]]]; try apply PRPOINT; move⇒ //.
× by apply/andP; split.
× move: LP ⇒ /negP LP; apply: LP.
enough (EQ : jhp = jlp); first by subst.
apply: (H_uni jhp _ _ tp); eauto.
by apply SCH; apply/andP; split; first apply leq_trans with t1; auto. }
repeat split⇒ //.
move: (H_busy_interval_prefix) ⇒ [SL [QUIET [NOTQUIET EXj]]]; move: (Sched_jhp) ⇒ PENDING.
eapply scheduled_implies_pending in PENDING ⇒ //.
apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING ⇒ /andP [ARR _].
apply contraT; rewrite -ltnNge; intro LT; exfalso.
feed (QUIET jhp) ⇒ //.
specialize (QUIET HP LT).
move: Sched_jhp; apply/negP/completed_implies_not_scheduled ⇒ //.
apply: completion_monotonic QUIET.
exact: leq_trans LEtp.
Qed.
∀ tp t,
preemption_time arr_seq sched tp →
t1 ≤ tp < t2 →
tp ≤ t < t2 →
∃ j_hp,
arrived_between j_hp t1 t.+1 ∧
hep_job j_hp j ∧
scheduled_at sched j_hp t.
Proof.
move ⇒ tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp LTt].
have [Idle|[jhp Sched_jhp]] :=
scheduled_at_cases _ H_valid_arrivals sched ltac:(by []) ltac:(by []) t.
{ eapply instant_t_is_not_idle in Idle ⇒ //.
by apply/andP; split; first apply leq_trans with tp. }
∃ jhp.
have HP: hep_job jhp j.
{ have PP := scheduling_of_any_segment_starts_with_preemption_time _
arr_seq H_valid_arrivals
sched H_sched_valid H_valid_preemption_model jhp t Sched_jhp.
feed PP ⇒ //.
move: PP ⇒ [prt [/andP [_ LE] [PR SCH]]].
case E:(t1 ≤ prt).
- move: E ⇒ /eqP /eqP E; rewrite subn_eq0 in E.
edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point as [jlp [_ [HEP SCHEDjhp]]] ⇒ //.
{ by apply /andP; split; last by apply leq_ltn_trans with t. }
enough (EQ : jhp = jlp); first by subst.
apply: (H_uni _ _ _ prt); eauto;
by apply SCH; apply/andP; split.
- move: E ⇒ /eqP /neqP E; rewrite -lt0n subn_gt0 in E.
apply negbNE; apply/negP; intros LP; rename jhp into jlp.
edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point
as [jhp [_ [HEP SCHEDjhp]]]; try apply PRPOINT; move⇒ //.
× by apply/andP; split.
× move: LP ⇒ /negP LP; apply: LP.
enough (EQ : jhp = jlp); first by subst.
apply: (H_uni jhp _ _ tp); eauto.
by apply SCH; apply/andP; split; first apply leq_trans with t1; auto. }
repeat split⇒ //.
move: (H_busy_interval_prefix) ⇒ [SL [QUIET [NOTQUIET EXj]]]; move: (Sched_jhp) ⇒ PENDING.
eapply scheduled_implies_pending in PENDING ⇒ //.
apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING ⇒ /andP [ARR _].
apply contraT; rewrite -ltnNge; intro LT; exfalso.
feed (QUIET jhp) ⇒ //.
specialize (QUIET HP LT).
move: Sched_jhp; apply/negP/completed_implies_not_scheduled ⇒ //.
apply: completion_monotonic QUIET.
exact: leq_trans LEtp.
Qed.
Now, suppose there exists some constant K that bounds the
distance to a preemption time from the beginning of the busy
interval.
Variable K : duration.
Hypothesis H_preemption_time_exists :
∃ pr_t, preemption_time arr_seq sched pr_t ∧ t1 ≤ pr_t ≤ t1 + K.
Hypothesis H_preemption_time_exists :
∃ pr_t, preemption_time arr_seq sched pr_t ∧ t1 ≤ pr_t ≤ t1 + K.
Then we prove that the processor is always busy with a job
with higher-or-equal priority after time instant t1 + K.
Lemma not_quiet_implies_exists_scheduled_hp_job:
∀ t,
t1 + K ≤ t < t2 →
∃ j_hp,
arrived_between j_hp t1 t.+1 ∧
hep_job j_hp j ∧
scheduled_at sched j_hp t.
Proof.
move ⇒ t /andP [GE LT].
move: H_preemption_time_exists ⇒ [prt [PR /andP [GEprt LEprt]]].
apply not_quiet_implies_exists_scheduled_hp_job_after_preemption_point with (tp := prt); eauto 2.
- apply/andP; split⇒ [//|].
apply leq_ltn_trans with (t1 + K) ⇒ [//|].
by apply leq_ltn_trans with t.
- apply/andP; split⇒ [|//].
by apply leq_trans with (t1 + K).
Qed.
End ProcessorBusyWithHEPJobAfterPreemptionPoints.
∀ t,
t1 + K ≤ t < t2 →
∃ j_hp,
arrived_between j_hp t1 t.+1 ∧
hep_job j_hp j ∧
scheduled_at sched j_hp t.
Proof.
move ⇒ t /andP [GE LT].
move: H_preemption_time_exists ⇒ [prt [PR /andP [GEprt LEprt]]].
apply not_quiet_implies_exists_scheduled_hp_job_after_preemption_point with (tp := prt); eauto 2.
- apply/andP; split⇒ [//|].
apply leq_ltn_trans with (t1 + K) ⇒ [//|].
by apply leq_ltn_trans with t.
- apply/andP; split⇒ [|//].
by apply leq_trans with (t1 + K).
Qed.
End ProcessorBusyWithHEPJobAfterPreemptionPoints.