# Library prosa.analysis.facts.busy_interval.pi_cond

Require Export prosa.analysis.facts.busy_interval.pi.
This file relates the general notion of cumulative_priority_inversion with the more specialized notion cumulative_priority_inversion_cond.
Section CondPI.
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 `{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 ideal 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 Cost Arrival}.
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 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 of tsk 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.
We establish a technical rewriting lemma that allows us to replace cumulative_priority_inversion with cumulative_priority_inversion_cond by exploiting the observation that a single job remains scheduled throughout the interval in which job j suffers priority inversion.
Lemma cum_task_pi_eq :
∀ (jlp : Job) (P : pred Job),
scheduled_at sched jlp t1 →
P jlp →
cumulative_priority_inversion arr_seq sched j t1 t2
= cumulative_priority_inversion_cond arr_seq sched j P t1 t2.
Proof.
move⇒ jlp P SCHED Pjlp.
apply: eq_big_nat ⇒ // t /andP [t1t tt2].
f_equal; apply/andb_id2l ⇒ NSCHED.
have suff:
∀ j',
j' \in scheduled_jobs_at arr_seq sched t →
~~ hep_job j' j →
P j'.
{ move⇒ SUFF.
apply: eq_in_has ⇒ j' ⇒ SCHED'.
have [_|NHEP] := boolP (hep_job j' j); first by rewrite andFb.
by rewrite andTb SUFF. }
{ apply ⇒ j' SCHED' NHEP.
move: SCHED'; rewrite scheduled_jobs_at_iff // ⇒ SCHED''.
have PI: priority_inversion arr_seq sched j t by apply /uni_priority_inversion_P.
have j't1: scheduled_at sched j' t1
by apply: (pi_job_remains_scheduled arr_seq) =>//; apply /andP.
have → // : j' = jlp.
{ apply /eqP/contraT ⇒ NEQ; move: SCHED; apply /contraLR ⇒ _.
by apply scheduled_job_at_neq with (j:= j'). } }
Qed.
End CondPI.