Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** Throughout this file, we work with Prosa's fixed-priority policy implementation. *)#[local] Existing InstanceNumericFPAscending.(** First, we define the concept of higher-or-equal-priority and different task, ... *)Definitionohep_task (tsk1 : Task) (tsk2 : Task) :=
hep_task tsk1 tsk2 && (tsk1 != tsk2).(** ... cumulative request-bound function for higher-or-equal-priority tasks (including the task under analysis), ... *)Definitiontotal_hep_rbf (ts : seq Task) (tsk : Task) (Δ : duration) :=
total_hep_request_bound_function_FP ts tsk Δ.(** ... and an analogous definition that does not include the task under analysis. *)Definitiontotal_ohep_rbf (ts : seq Task) (tsk : Task) (Δ : duration) :=
total_ohep_request_bound_function_FP ts tsk Δ.(** Next, we provide a function that checks a single point [P=(A,F)] of the search space when adopting a fully-preemptive policy. *)Definitioncheck_point_FP (ts : seq Task) (tsk : Task) (R : nat) (P : nat * nat) :=
(task_rbf tsk (P.1 + ε) + total_ohep_rbf ts tsk (P.1 + P.2) <= P.1 + P.2) && (P.2 <= R).(** Further, we provide a way to compute the blocking bound when using nonpreemptive policies. *)Definitionblocking_bound_NP (ts : seq Task) (tsk : Task) :=
\max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (concept.task_cost tsk_other - ε).(** Finally, we provide a function that checks a single point [P=(A,F)] of the search space when adopting a fully-nonpreemptive policy. *)Definitioncheck_point_NP (ts : seq Task) (tsk : Task) (R : nat) (P : nat * nat) :=
(blocking_bound_NP ts tsk
+ (task_rbf tsk (P.1 + ε) - (concept.task_cost tsk - ε))
+ total_ohep_rbf ts tsk (P.1 + P.2) <= P.1 + P.2)
&& (P.2 + (concept.task_cost tsk - ε) <= R).(** * Search Space Definitions *)(** First, we recall the notion of correct search space as defined by abstract RTA. *)Definitioncorrect_search_space (tsk : Task) (L : duration) :=
[seq A <- iota 0 L | is_in_search_space tsk L A].(** Next, we provide a computation-oriented way to compute abstract RTA's search space. We start with a function that computes the search space in a generic interval <<[a,b)>>, ... *)Definitionsearch_space_emax_FP_h (tsk : Task) ab :=
leth := get_horizon_of_task tsk inletoffsets := map (muln h) (iota a b) inletemax_offsets := repeat_steps_with_offset tsk offsets in
map predn emax_offsets.(** ... which we then apply to the interval <<[0, (L %/h).+1)>>. *)Definitionsearch_space_emax_FP (tsk : Task) (L : duration) :=
leth := get_horizon_of_task tsk in
search_space_emax_FP_h tsk 0 (L %/h).+1.(** In this section, we prove that the computation-oriented search space defined above contains each of the points contained in abstract RTA's standard definition. *)SectionFastSearchSpaceComputationSubset.(** Consider a given maximum busy-interval length [L], ... *)VariableL : duration.(** ... a task set with valid arrivals, ... *)Variablets : seq Task.HypothesisH_valid_arrivals : task_set_with_valid_arrivals ts.(** ... and a task belonging to [ts] with positive cost. *)Variabletsk : Task.HypothesisH_positive_cost : 0 < task_cost tsk.HypothesisH_tsk_in_ts : tsk \in ts.(** Then, abstract RTA's standard search space is a subset of the computation-oriented version defined above. *)