# Library prosa.analysis.abstract.restricted_supply.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.abstract.definitions.

# Service Inversion Bounded

In this section, we define the notion of bounded cumulative service inversion in an abstract busy interval prefix.
Section ServiceInversion.
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}.
Next, consider any kind of processor state model, ...
Context {PState : ProcessorState Job}.
... any arrival sequence, ...
Variable arr_seq : arrival_sequence Job.
... and any schedule of this arrival sequence.
Variable sched : schedule PState.
Assume we are provided with abstract functions for interference and interfering workload.
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
Assume a given JLFP policy.
Context `{JLFP_policy Job}.
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 (abstract) 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 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 an abstract busy interval prefix.
Definition service_inversion_is_bounded_by (tsk : Task) (B : duration → duration) :=
pred_service_inversion_is_bounded_by
arr_seq sched (busy_interval_prefix sched) tsk B.
End ServiceInversion.