Library prosa.analysis.facts.busy_interval.priority_inversion

Lemma about Priority Inversion for arbitrary processors

In this section, we prove a lemma about the notion of priority inversion for arbitrary processors.
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}.

Next, consider any kind of processor state model, ...
  Context {PState : ProcessorState Job}.

... any arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any schedule.
  Variable sched : schedule PState.

Assume a given JLFP policy.
  Context `{JLFP_policy Job}.

Consider an arbitrary job.
  Variable j : Job.

Then we prove that cumulative priority inversion (CPI) that job j incurs in an interval [t1, t2) is equal to the sum of CPI in an interval [t1, t_mid) and CPI in an interval [t_mid, t2).
Assume that j is scheduled at time t, then there is no priority inversion at time t.