# 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 {RM : JobReady Job PState}.
Hypothesis H_job_ready : work_bearing_readiness RM 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.
End CondPI.