# Library prosa.analysis.definitions.service_inversion.pred

Require Export prosa.model.priority.classes.

Require Export prosa.analysis.facts.behavior.completion.

Require Export prosa.analysis.definitions.service.

Require Export prosa.analysis.facts.behavior.completion.

Require Export prosa.analysis.definitions.service.

# Service Inversion

In this section, we define the notion of service inversion for arbitrary processors.
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}.

Next, consider

*any*kind of processor state model, ...
... any arrival sequence, ...

... and any schedule of this arrival sequence.

Assume a given JLDP policy.

Consider an arbitrary predicate on time intervals.

Consider a job j.

We say that the job incurs service inversion if it has higher
priority than the job receiving service. Note that this
definition is oblivious to whether job j is ready. Therefore,
it may not apply as intuitively expected in models with jitter
or self-suspensions. Further generalization of the concept is
likely necessary to efficiently analyze models in which jobs may
be pending without being ready.

Definition service_inversion (t : instant) :=

(j \notin served_jobs_at arr_seq sched t)

&& has (fun jlp ⇒ ~~ hep_job_at t jlp j) (served_jobs_at arr_seq sched t).

(j \notin served_jobs_at arr_seq sched t)

&& has (fun jlp ⇒ ~~ hep_job_at t jlp j) (served_jobs_at arr_seq sched t).

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

`[t1, t2)`

.
Definition cumulative_service_inversion (t1 t2 : instant) :=

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

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

For proof purposes, it is often useful to bound the cumulative
service interference in a time interval

`[t1, t2)`

that
satisfies a given predicate (e.g., `[t1, t2)`

is a busy
interval prefix). To this end, we say that the cumulative
service inversion of job j is bounded by a function B :
duration → duration w.r.t. to predicate P iff, for any
interval `[t1, t2)`

that satisfies P j, the cumulative
priority inversion in `[t1, t2)`

is bounded by B (job_arrival
j - t1).
Definition pred_service_inversion_of_job_is_bounded_by (B : duration → duration) :=

∀ (t1 t2 : instant),

P j t1 t2 →

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

End ServiceInversion.

∀ (t1 t2 : instant),

P j t1 t2 →

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

End ServiceInversion.

In this section, we define a notion of the bounded service
inversion for tasks.

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*kind of processor state model, ...
... any arrival sequence, ...

... and any schedule.

Assume a given JLDP policy.

Consider an arbitrary predicate on jobs and time intervals.

Consider an arbitrary task tsk.