Library prosa.analysis.facts.priority.inversion

Lemmas about Priority Inversion

This file collects basic facts about the notion of priority inversion in the general context of arbitrary processor models.
Section PI.

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 valid arrival sequence, ...
... and any valid schedule.
Assume a given reflexive JLFP policy...
... and consider an arbitrary job.
  Variable j : Job.

Occurrence of Priority Inversion

First, we observe conditions under which priority inversions does, or does not, arise.
Assume that j is scheduled at time t, then there is no priority inversion at time t.
Conversely, if job j experiences a priority inversion at time t, then some (other) job is scheduled at the time, ...
  Lemma priority_inversion_scheduled_at :
     t,
      priority_inversion arr_seq sched j t
       j', scheduled_at sched j' t.

... and thus there is no priority inversion at idle instants.
  Lemma no_priority_inversion_when_idle :
     t,
      is_idle arr_seq sched t
      ~~ priority_inversion arr_seq sched j t.

  Section Uniprocessors.

Occurrence of Priority Inversion on Uniprocessors

Stronger conditions hold on uniprocessors since only one job can be scheduled at any time.
    Hypothesis H_uni : uniprocessor_model PState.

On a uniprocessor, the job scheduled when j incurs priority inversion necessarily has lower priority than j.
    Lemma priority_inversion_hep_job :
       t j',
        scheduled_at sched j' t
        priority_inversion arr_seq sched j t = ~~ hep_job j' j.
Conversely, if a higher-priority job is scheduled on a uniprocessor, then j does not incur priority inversion.
    Corollary no_priority_inversion_when_hep_job_scheduled :
       t j',
        scheduled_at sched j' t
        hep_job j' j
        ~~ priority_inversion arr_seq sched j t.

From the above lemmas, we obtain a simplified definition of priority_inversion that holds on uniprocessors.
    Lemma uni_priority_inversion_P :
       t,
        reflect (exists2 j', scheduled_at sched j' t & ~~ hep_job j' j)
          (priority_inversion arr_seq sched j t).

  End Uniprocessors.

Cumulative Priority Inversion

We observe that the cumulative priority inversion (CPI) that job j incurs in an interval [t1, t2) can be split arbitrarily: is equal to the sum of CPI in an interval [t1, t_mid) and CPI in an interval [t_mid, t2).