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 arrival sequence with consistent arrivals.
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.
  Context `{JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_priorities.

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.
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.