Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.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. Style: centered; floating; windowed.
[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]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_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. *)SectionPredSupplyBoundFunctions.(** Consider any type of jobs, ... *)Context {Job : JobType}.(** ... any kind of processor state model, ... *)Context `{PState : ProcessorState Job}.(** ... any arrival sequence, ... *)Variablearr_seq : arrival_sequence Job.(** ... and any schedule. *)Variablesched : schedule PState.(** Consider an arbitrary predicate on jobs and time intervals. *)VariableP : 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. *)Definitionpred_sbf_respected (SBF : duration -> work) :=
forall (j : Job) (t1t2 : 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]. *)Definitionvalid_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]. *)Definitionsbf_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. *)Definitionunit_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 [δ]. *)