Library prosa.analysis.abstract.IBF.supply
In this module, we define intra-supply interference as a kind of
conditional interference and use it to define an intra-supply
interference-bound function (intra_IBF). Recall that an
interference-bound function is a function that bounds the
interference experienced by a job of a task under analysis. This
way, the function intra_IBF bounds the cumulative interference
ignoring the interference due to a lack of supply.
Here, the term "intra-supply" is inspired by (but not limited to)
reservation-based schedulers, where a job only receives service
within a corresponding reservation. Similarly, intra-supply
interference refers to interference that occurs "inside" the time
instances where supply is present.
Consider any type of job associated with any type of tasks ...
... with arrival times and costs.
Consider any kind of processor state model.
Consider any arrival sequence ...
... and any schedule of this arrival sequence.
Let tsk be any task that is to be analyzed.
Assume we are provided with abstract functions for interference
and interfering workload.
Next, we introduce the notions of intra-supply interference
and intra-supply IBF. Using these notions, one can separate the
interference due to the lack of supply from all the other
sources of interference.
We define intra-supply interference as interference conditioned
on the fact that there is supply. That is, a job j experiences
intra-supply interference at a time instant t if j
experiences interference at time t and there is supply at
t.
Definition intra_interference (j : Job) (t : instant) :=
cond_interference (fun j t ⇒ has_supply sched t) j t.
cond_interference (fun j t ⇒ has_supply sched t) j t.
We define the cumulative intra-supply interference.
Definition cumul_intra_interference j t1 t2 :=
cumul_cond_interference (fun j t ⇒ has_supply sched t) j t1 t2.
cumul_cond_interference (fun j t ⇒ has_supply sched t) j t1 t2.
Consider an interference bound function intra_IBF.
We say that intra-supply interference is bounded by intra_IBF
iff, for any job j of task tsk, cumulative intra-supply
interference within the interval
[t1, t1 + R) is bounded by
intra_IBF(A, R).
Definition intra_interference_is_bounded_by :=
cond_interference_is_bounded_by
arr_seq sched tsk intra_IBF
(relative_arrival_time_of_job_is_A sched) (fun j t ⇒ has_supply sched t).
End IntraInterferenceBound.
cond_interference_is_bounded_by
arr_seq sched tsk intra_IBF
(relative_arrival_time_of_job_is_A sched) (fun j t ⇒ has_supply sched t).
End IntraInterferenceBound.