Library prosa.implementation.refinements.FP.fast_search_space

Throughout this file, we work with Prosa's fixed-priority policy implementation.
#[local] Existing Instance NumericFPAscending.

First, we define the concept of higher-or-equal-priority and different task, ...
Definition ohep_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), ...
... and an analogous definition that does not include the task under analysis.
Next, we provide a function that checks a single point P=(A,F) of the search space when adopting a fully-preemptive policy.
Further, we provide a way to compute the blocking bound when using nonpreemptive policies.
Finally, we provide a function that checks a single point P=(A,F) of the search space when adopting a fully-nonpreemptive policy.

Search Space Definitions

First, we recall the notion of correct search space as defined by abstract RTA.
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), ...
... which we then apply to the interval [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.
Consider a given maximum busy-interval length L, ...
  Variable L : duration.

... a task set with valid arrivals, ...
  Variable ts : seq Task.
  Hypothesis H_valid_arrivals : task_set_with_valid_arrivals ts.

... and a task belonging to ts with positive cost.
  Variable tsk : Task.
  Hypothesis H_positive_cost : 0 < task_cost tsk.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Then, abstract RTA's standard search space is a subset of the computation-oriented version defined above.
  Lemma search_space_subset_FP :
     A, A \in correct_search_space tsk L A \in search_space_emax_FP tsk L.
  Proof.
    moveA IN.
    move: IN; rewrite mem_filter ⇒ /andP[/andP[LEQ_L NEQ] _].
    by apply (task_search_space_subset _ ts) ⇒ //.
  Qed.

End FastSearchSpaceComputationSubset.