# Library prosa.analysis.definitions.service_inversion.readiness_aware

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

# Readiness-Aware Service Inversion

Section ServiceInversion.
Consider any kind of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Next, consider any kind of uniprocessor model.
Context {PState : ProcessorState Job}.
Hypothesis H_uni : uniprocessor_model PState.
Consider any notion of readiness.
Context `{!JobReady Job PState}.
Consider any arrival sequence, ...
Variable arr_seq : arrival_sequence Job.
... and any schedule of this arrival sequence.
Variable sched : schedule PState.
Assume a JLFP policy.
Context `{JLFP_policy Job}.
In this section, we define a readiness-aware notion of service inversion.
Section Definitions.
Consider a job j.
Variable j : Job.
Recall the existing notion of service inversion that does not take job readiness into account.
Let readiness_oblivious_service_inversion := pred.service_inversion arr_seq sched.
We say that readiness-aware service inversion is taking place at some instant t if a lower-priority job (w.r.t j) is being served in spite of a higher-or-equal-priority job (w.r.t j) being schedulable, ...
Definition service_inversion (t : instant) :=
some_hep_job_ready arr_seq sched j t
&& readiness_oblivious_service_inversion j t.
... with the obvious extension to intervals.
Definition cumulative_service_inversion (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) service_inversion t.
End Definitions.
In this section, we define the notion of a bound on readiness-aware service inversion in a busy-window prefix.
Section ServiceInversionBound.
Assume that we have some definition of interference and interfering workload.
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
We say that B is a bound on the readiness-aware service inversion incurred by any job j inside its busy interval `[t1, t2]` if B bounds the readiness-aware cumulative service inversion within the interval `[t1, t2]`.
Definition service_inversion_is_bounded (B : duration → duration) :=
∀ j t1 t2,
busy_interval_prefix sched j t1 t2 →
cumulative_service_inversion j t1 t2 ≤ B (job_arrival j - t1).
End ServiceInversionBound.
End ServiceInversion.