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.
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 moven; rewrite (leqRW (UNIT _)) ltnS.
  Qed.

End PredSupplyBoundFunctions.