# Library prosa.analysis.definitions.service_inversion.busy_prefix

Require Export prosa.model.priority.classes.

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

Require Export prosa.analysis.definitions.service.

Require Export prosa.analysis.definitions.service_inversion.pred.

Require Export prosa.analysis.definitions.busy_interval.classical.

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

Require Export prosa.analysis.definitions.service.

Require Export prosa.analysis.definitions.service_inversion.pred.

Require Export prosa.analysis.definitions.busy_interval.classical.

# Service Inversion Bounded

In this section, we define the notion of bounded cumulative service inversion in a busy interval prefix.
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 JLFP policy.

If the priority inversion experienced by 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 service inversion of job j is
bounded by a function B : duration → duration if the
cumulative service inversion within any busy interval prefix is
bounded by B (job_arrival j - t1).

Definition service_inversion_of_job_is_bounded_by (j : Job) (B : duration → duration) :=

pred_service_inversion_of_job_is_bounded_by

arr_seq sched (busy_interval_prefix arr_seq sched) j B.

pred_service_inversion_of_job_is_bounded_by

arr_seq sched (busy_interval_prefix arr_seq sched) j B.

We say that task tsk has bounded service inversion if all its
jobs have cumulative service inversion bounded by function B :
duration → duration, where B may depend on jobs' relative
arrival times w.r.t. the beginning of the busy interval.

Definition service_inversion_is_bounded_by (tsk : Task) (B : duration → duration) :=

pred_service_inversion_is_bounded_by

arr_seq sched (busy_interval_prefix arr_seq sched) tsk B.

End ServiceInversion.

pred_service_inversion_is_bounded_by

arr_seq sched (busy_interval_prefix arr_seq sched) tsk B.

End ServiceInversion.