Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]

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) :=
    forall (j : Job) (t1 t2 : instant),
      arrives_in arr_seq j ->
      P j t1 t2 ->
      forall (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) :=
    forall (δ : 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 [δ]. *)
  
Job: JobType
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
P: Job -> instant -> instant -> Prop
SBF: SupplyBoundFunction
valid_pred_sbf SBF ->
unit_supply_bound_function SBF ->
forall δ : duration, SBF δ <= δ

  
Job: JobType
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
P: Job -> instant -> instant -> Prop
SBF: SupplyBoundFunction
valid_pred_sbf SBF ->
unit_supply_bound_function SBF ->
forall δ : duration, SBF δ <= δ

    
Job: JobType
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
P: Job -> instant -> instant -> Prop
SBF: SupplyBoundFunction
ZERO: SBF 0 = 0
UNIT: unit_supply_bound_function SBF
SBF 0 <= 0
Job: JobType
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
P: Job -> instant -> instant -> Prop
SBF: SupplyBoundFunction
ZERO: SBF 0 = 0
UNIT: unit_supply_bound_function SBF
forall n : nat, SBF n <= n -> SBF n.+1 <= n.+1

    
Job: JobType
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
P: Job -> instant -> instant -> Prop
SBF: SupplyBoundFunction
ZERO: SBF 0 = 0
UNIT: unit_supply_bound_function SBF
SBF 0 <= 0
 by rewrite leqn0; apply/eqP.
    
Job: JobType
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
P: Job -> instant -> instant -> Prop
SBF: SupplyBoundFunction
ZERO: SBF 0 = 0
UNIT: unit_supply_bound_function SBF
forall n : nat, SBF n <= n -> SBF n.+1 <= n.+1
 by move => n; rewrite (leqRW (UNIT _)) ltnS.
  Qed.

End PredSupplyBoundFunctions.