Project Page Index Table of Contents

# Library prosa.analysis.abstract.restricted_supply.busy_sbf

Require Export prosa.util.all.
Require Export prosa.analysis.definitions.sbf.pred.
Require Export prosa.analysis.abstract.definitions.

# SBF within Abstract Busy Interval

In the following, we define a weak notion of a supply-bound function, which is a valid SBF only within an abstract busy interval of a task's job.
Section BusySupplyBoundFunctions.
Consider any type of tasks, ...
Context {Task : TaskType}.
... and any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
... any kind of processor state model, ...
Context `{PState : ProcessorState Job}.
... any arrival sequence, ...
Variable arr_seq : arrival_sequence Job.
... and any schedule.
Variable sched : schedule PState.
Consider a task tsk.
Variable tsk : Task.
Assume we are provided with abstract functions for Interference and Interfering Workload.
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
We define a predicate that determines whether an interval `[t1, t2)` is a busy-interval prefix of a job j of task tsk.
Let bi_prefix_of_tsk j t1 t2 :=
job_of_task tsk j ∧ busy_interval_prefix sched j t1 t2.
We say that the SBF is respected in a busy interval w.r.t. task tsk if, for any busy interval `[t1, t2)` of a job j ∈ tsk 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 bi_prefix_of_tsk SBF.
Next, we define an SBF that is valid within an (abstract) busy interval.
Definition valid_busy_sbf (SBF : duration → work) :=
valid_pred_sbf arr_seq sched bi_prefix_of_tsk SBF.
End BusySupplyBoundFunctions.