Project Page Index Table of Contents

# Library prosa.analysis.definitions.sbf.pred

Require Export prosa.util.all.
Require Export prosa.behavior.schedule.
Require Export prosa.model.processor.supply.
Require Export prosa.analysis.definitions.sbf.sbf.

## SBF Parameter Semantics

In the following, we define the semantics of the supply-bound functions (SBF) parametrized by a predicate.
In our development, we use several different types of SBF (such as the classical SBF, SBF within a busy interval, and SBF within an abstract busy interval). The parametrization of the definition with a predicate serves to avoid superfluous duplication.
Section PredSupplyBoundFunctions.
Consider any type of jobs, ...
Context {Job : JobType}.
... 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 an arbitrary predicate on jobs and time intervals.
Variable P : Job → instant → instant → Prop.
We say that the SBF is respected w.r.t. predicate P if, for any job j, an interval `[t1, t2)` satisfying P j, and a subinterval `[t1, t) ⊆ [t1, t2)`, at least SBF (t - t1) cumulative supply is provided.
Definition pred_sbf_respected (SBF : duration → work) :=
∀ (j : Job) (t1 t2 : instant),
arrives_in arr_seq j →
P j t1 t2 →
∀ (t : instant),
t1 ≤ t ≤ t2 →
SBF (t - t1) ≤ supply_during sched t1 t.
We say that the SBF is valid w.r.t. predicate P if two conditions are satisfied: (1) SBF 0 = 0 and (2) the SBF is respected w.r.t. predicate P.
Definition valid_pred_sbf (SBF : duration → work) :=
SBF 0 = 0
∧ pred_sbf_respected SBF.
An SBF is monotone iff for any δ1 and δ2 such that δ1 ≤ δ2, SBF δ1 ≤ SBF δ2.
Definition sbf_is_monotone (SBF : duration → work) :=
monotone leq SBF.
In the context of unit-supply processor models, it is known that the amount of supply provided by the processor is bounded by 1 at any time instant. Hence, we can consider a restricted notion of SBF, where the bound can only increase by at most 1 at each time instant.
Definition unit_supply_bound_function (SBF : duration → work) :=
∀ (δ : duration),
SBF δ.+1 ≤ (SBF δ).+1.
Next, suppose we are given an SBF characterizing the schedule.
Context {SBF : SupplyBoundFunction}.
The assumption unit_supply_bound_function together with the introduced validity assumption implies that SBF δ ≤ δ for any δ.
Remark sbf_bounded_by_duration :
valid_pred_sbf SBF →
unit_supply_bound_function SBF →
∀ δ, SBF δ ≤ δ.
Proof.
move ⇒ [ZERO _] UNIT; elim.
- by rewrite leqn0; apply/eqP.
- by move ⇒ n; rewrite (leqRW (UNIT _)) ltnS.
Qed.
End PredSupplyBoundFunctions.