# 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.

# Processor Executes HEP jobs at Preemption Point

In this file, we show that, given a busy interval of a job j, the processor is always busy scheduling a higher-or-equal-priority job at any preemptive point inside the busy interval.
Section ProcessorBusyWithHEPJobAtPreemptionPoints.
Consider any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
Consider any arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
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.
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.
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.
Context `{JobPreemptable Job}.
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.
We assume that the schedule is valid and that all jobs come from the arrival sequence.
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
Next, we assume that the schedule is a work-conserving schedule...
Hypothesis H_work_conserving : work_conserving arr_seq sched.
... and the schedule respects the scheduling policy at every preemption point.
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
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.
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.
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.
First note since t lies inside the busy interval, the processor cannot be idle at time t.
Lemma instant_t_is_not_idle :
¬ 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 ⇒ /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 ⇒ /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.
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.
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.

# 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.
Section ProcessorBusyWithHEPJobAfterPreemptionPoints.
Consider any type of tasks ...
Context {Task : TaskType}.
Context `{TaskCost Task}.
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
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.
... and any uniprocessor schedule of this arrival sequence.
Context {PState : ProcessorState Job}.
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.
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.
Further, allow for any work-bearing notion of job readiness.
Context `{!JobReady Job PState}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
We assume that the schedule is valid.
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
Next, we assume that the schedule is work-conserving ...
Hypothesis H_work_conserving : work_conserving arr_seq sched.
... and the schedule respects the scheduling policy at every preemption point.
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
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.
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.
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.
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.
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.