Library prosa.analysis.definitions.sbf.busy
Require Export prosa.util.all.
Require Export prosa.analysis.definitions.sbf.pred.
Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.definitions.sbf.pred.
Require Export prosa.analysis.definitions.busy_interval.classical.
SBF within Busy Interval
Consider any type of jobs, ...
... any kind of processor state model, ...
... any valid arrival sequence, and ...
... any schedule.
Assume a given JLFP policy.
We say that the SBF is respected in a busy interval if, for any
busy interval
[t1, t2)
and a subinterval [t1, t) ⊆ [t1,
t2)>>, at least SBF (t - t1) cumulative supply is provided.
Definition sbf_respected_in_busy_interval (SBF : duration → work) :=
pred_sbf_respected arr_seq sched (busy_interval_prefix arr_seq sched) SBF.
pred_sbf_respected arr_seq sched (busy_interval_prefix arr_seq sched) SBF.
Next, we define an SBF that is valid within a busy interval.
Definition valid_busy_sbf (SBF : duration → work) :=
valid_pred_sbf arr_seq sched (busy_interval_prefix arr_seq sched) SBF.
End BusySupplyBoundFunctions.
valid_pred_sbf arr_seq sched (busy_interval_prefix arr_seq sched) SBF.
End BusySupplyBoundFunctions.