Library prosa.analysis.facts.busy_interval.ideal.priority_inversion

Throughout this file, we assume ideal uni-processor schedules.

Lemmas about Priority Inversion for ideal uni-processors

In this section, we prove a few useful properties about the notion of priority inversion for ideal uni-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}.

Consider any valid arrival sequence.
Next, consider any ideal uni-processor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive.
Let tsk be any task to be analyzed.
  Variable tsk : Task.

Consider a job j of task tsk. In this subsection, job j is deemed to be the main job with respect to which the priority inversion is computed.
  Variable j : Job.
  Hypothesis H_j_tsk : job_of_task tsk j.

Consider a time instant t.
  Variable t : instant.

We prove that if the processor is idle at time t, then there is no priority inversion.
  Lemma idle_implies_no_priority_inversion :
    ideal_is_idle sched t
    ~~ priority_inversion arr_seq sched j t.
  Proof.
    moveIDLE.
    apply: no_priority_inversion_when_idle ⇒ //.
    by rewrite is_idle_def.
  Qed.

Next, consider an additional job j' and assume it is scheduled at time t.
  Variable j' : Job.
  Hypothesis H_j'_sched : scheduled_at sched j' t.

Then, we prove that from point of view of job j, priority inversion appears iff s has lower priority than job j.
Assume that j' has higher-or-equal priority than job j, then we prove that there is no priority inversion for job j.
Assume that j' has lower priority than job j, then we prove that j incurs priority inversion.