# Library prosa.analysis.definitions.priority_inversion

Require Export prosa.analysis.definitions.busy_interval.

Require Import prosa.model.processor.ideal.

Require Import prosa.model.processor.ideal.

# Cumulative Priority Inversion for JLFP-models

In this module we define the notion of cumulative priority inversion for uni-processor for JLFP schedulers.
Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Consider any arrival sequence with consistent arrivals.

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Next, consider any ideal uniprocessor schedule of this arrival sequence.

Assume a given JLFP policy.

In this section, we define a notion of bounded priority inversion experienced by a job.

Consider an arbitrary task tsk.

Consider any job j of tsk.

Variable j : Job.

Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.

Hypothesis H_job_task : job_of_task tsk j.

Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.

Hypothesis H_job_task : job_of_task tsk j.

We say that the job incurs priority inversion if it has higher
priority than the scheduled job. Note that this definition
implicitly assumes that the scheduler is
work-conserving. Therefore, it cannot be applied to models
with jitter or self-suspensions.

Definition is_priority_inversion (t : instant) :=

if sched t is Some jlp then

~~ hep_job jlp j

else false.

if sched t is Some jlp then

~~ hep_job jlp j

else false.

Then we compute the cumulative priority inversion incurred by
a job within some time interval

`[t1, t2)`

.
Definition cumulative_priority_inversion (t1 t2 : instant) :=

\sum_(t1 ≤ t < t2) is_priority_inversion t.

\sum_(t1 ≤ t < t2) is_priority_inversion t.

We say that the priority inversion experienced by a job j is bounded
by a constant B if the cumulative priority inversion within any busy
interval prefix is bounded by B.

Definition priority_inversion_of_job_is_bounded_by_constant (B : duration) :=

∀ (t1 t2 : instant),

busy_interval_prefix arr_seq sched j t1 t2 →

cumulative_priority_inversion t1 t2 ≤ B.

∀ (t1 t2 : instant),

busy_interval_prefix arr_seq sched j t1 t2 →

cumulative_priority_inversion t1 t2 ≤ B.

More generally, if the priority inversion experienced by a job j
depends on its relative arrival time w.r.t. the beginning of its busy
interval at a time t1, we say that the priority inversion of job j
is bounded by a function B : duration → duration if the cumulative
priority inversion within any busy interval prefix is bounded by B
(job_arrival j - t1)

Definition priority_inversion_of_job_is_bounded_by (B : duration → duration) :=

∀ (t1 t2 : instant),

busy_interval_prefix arr_seq sched j t1 t2 →

cumulative_priority_inversion t1 t2 ≤ B (job_arrival j - t1).

End JobPriorityInversionBound.

∀ (t1 t2 : instant),

busy_interval_prefix arr_seq sched j t1 t2 →

cumulative_priority_inversion t1 t2 ≤ B (job_arrival j - t1).

End JobPriorityInversionBound.

In this section, we define a notion of the bounded priority inversion for task.

Consider an arbitrary task tsk.

We say that priority inversion of task tsk is bounded by a constant
B if all jobs released by the task have cumulative priority inversion
bounded by B

Definition priority_inversion_is_bounded_by_constant (B : duration) :=

∀ (j : Job),

arrives_in arr_seq j →

job_of_task tsk j →

job_cost j > 0 →

priority_inversion_of_job_is_bounded_by_constant j B.

∀ (j : Job),

arrives_in arr_seq j →

job_of_task tsk j →

job_cost j > 0 →

priority_inversion_of_job_is_bounded_by_constant j B.

We say that task tsk has bounded priority inversion if all its jobs
have bounded cumulative priority inversion that depends on its relative
arrival time w.r.t. the beginning of the busy interval.

Definition priority_inversion_is_bounded_by (B : duration → duration) :=

∀ (j : Job),

arrives_in arr_seq j →

job_of_task tsk j →

job_cost j > 0 →

priority_inversion_of_job_is_bounded_by j B.

End TaskPriorityInversionBound.

End CumulativePriorityInversion.

∀ (j : Job),

arrives_in arr_seq j →

job_of_task tsk j →

job_cost j > 0 →

priority_inversion_of_job_is_bounded_by j B.

End TaskPriorityInversionBound.

End CumulativePriorityInversion.