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.analysis.abstract.search_space.Require Export prosa.analysis.definitions.blocking_bound.fp.(** * Abstract Search Space is a Subset of Restricted Supply FP Search Space *)(** A response-time analysis usually involves solving the response-time equation for various relative arrival times (w.r.t. the beginning of the corresponding busy interval) of a job under analysis. To reduce the time complexity of the analysis, the state of the art uses the notion of a search space. Intuitively, this corresponds to all "interesting" arrival offsets that the job under analysis might have with regard to the beginning of its busy window. In this file, we prove that the search space derived from the aRTA theorem is a subset of the search space for the FP scheduling policy with restricted supply. In other words, by solving the response-time equation for points in the FP search space, one also checks all points in the aRTA search space, which makes FP compatible with aRTA w.r.t. the search space. *)SectionSearchSpaceSubset.(** Consider any type of tasks. *)Context {Task : TaskType}.Context `{TaskCost Task}.Context `{TaskMaxNonpreemptiveSegment Task}.(** Consider an FP policy that indicates a higher-or-equal priority relation. *)Context {FP : FP_policy Task}.(** Consider an arbitrary task set [ts]. *)Variablets : list Task.(** Let [max_arrivals] be a family of valid arrival curves, i.e., for any task [tsk] in [ts] [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function that equals [0] for the empty interval [delta = 0]. *)Context `{MaxArrivals Task}.HypothesisH_valid_arrival_curve :
valid_taskset_arrival_curve ts max_arrivals.(** Let [tsk] be any task in [ts] that is to be analyzed. *)Variabletsk : Task.HypothesisH_tsk_in_ts : tsk \in ts.(** Let's define some local names for clarity. *)Lettask_rbf := task_request_bound_function tsk.Lettotal_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.(** Let [L] be an arbitrary positive constant. Typically, [L] denotes an upper bound on the length of a busy interval of a job of [tsk]. In this file, however, [L] can be any positive constant. *)VariableL : duration.HypothesisH_L_positive : 0 < L.(** For the fixed-priority scheduling policy, the search space is defined as the set of offsets below [L] where the RBF of the task under analysis makes a step. *)Definitionis_in_search_spaceA :=
(A < L) && (task_rbf A != task_rbf (A + ε)).(** To rule out pathological cases with the search space, we assume that the task cost is positive and the arrival curve is non-pathological. *)HypothesisH_task_cost_pos : 0 < task_cost tsk.HypothesisH_arrival_curve_pos : 0 < max_arrivals tsk ε.(** For brevity, let us introduce a shorthand for an intra-IBF (used by aRTA). The abstract search space is derived via intra-IBF. *)Letintra_IBF (AF : duration) :=
task_rbf (A + ε) - task_cost tsk
+ (blocking_bound ts tsk + total_ohep_rbf F).(** Then, abstract RTA's standard search space is a subset of the computation-oriented version defined above. *)