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.