# Library prosa.implementation.refinements.fast_search_space_computation

Require Export prosa.implementation.refinements.arrival_curve_prefix.
Require Import prosa.analysis.facts.model.rbf.
In this section, we provide definitions and lemmas to show Abstract RTA' s search space can be rewritten in an equivalent, computation-oriented way.
Section FastSearchSpaceComputation.
Let L be a constant which bounds any busy interval of task tsk.
Variable L : duration.
Consider a task set ts with valid arrivals...
Variable ts : seq Task.
Hypothesis H_valid_task_set : task_set_with_valid_arrivals ts.
... and a task tsk of ts with positive cost.
Variable tsk : Task.
Hypothesis H_positive_cost : 0 < task_cost tsk.
Hypothesis H_tsk_in_ts : tsk \in ts.
We generically define the search space for fixed-priority tasks in the interval `[l,r)` by repeating the time steps of the task in the interval `[l*h,r*h)`.
Definition search_space_arrival_curve_prefix_FP_h (tsk : Task) l r :=
let h := get_horizon_of_task tsk in
let offsets := map (muln h) (iota l r) in
let arrival_curve_prefix_offsets := repeat_steps_with_offset tsk offsets in
map predn arrival_curve_prefix_offsets.
By using the above definition, we give a concrete definition of the search space for fixed-priority tasks.
Definition search_space_arrival_curve_prefix_FP (tsk : Task) L :=
let h := get_horizon_of_task tsk in
search_space_arrival_curve_prefix_FP_h (tsk : Task) 0 (L %/h).+1.
We begin by showing that either each time step of an arrival curve prefix is either strictly less than the horizon, or it is the horizon.
Lemma steps_lt_horizon_last_eq_horizon :
(∀ s, s \in get_time_steps_of_task tsk → s < get_horizon_of_task tsk)
∨ (last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk).
Next, we show that for each offset A in the search space for fixed-priority tasks, either (1) A+ε is zero or a multiple of the horizon, offset by one of the time steps of the arrival curve prefix, or (2) A+ε is exactly a multiple of the horizon.
Lemma structure_of_correct_search_space :
∀ A,
A < L →
task_rbf tsk A != task_rbf tsk (A + ε) →
(∃ i t,
i < (L %/ get_horizon_of_task tsk).+1
∧ (t \in get_time_steps_of_task tsk)
∧ A + ε = i × get_horizon_of_task tsk + t )
∨ (∃ i,
i < (L %/ get_horizon_of_task tsk).+1
∧ A + ε = i × get_horizon_of_task tsk).
Conversely, every multiple of the horizon that is strictly less than L is contained in the search space for fixed-priority tasks...
Lemma multiple_of_horizon_in_approx_ss :
∀ A,
A < L →
get_horizon_of_task tsk %| A →
A \in search_space_arrival_curve_prefix_FP tsk L.
... and every A for which A+ε is a multiple of the horizon offset by a time step of the arrival curve prefix is also in the search space for fixed-priority tasks.
Lemma steps_in_approx_ss :
∀ i t A,
i < (L %/ get_horizon_of_task tsk).+1 →
(t \in get_time_steps_of_task tsk) →
A + ε = i × get_horizon_of_task tsk + t →
A \in search_space_arrival_curve_prefix_FP tsk L.
Next, we show that if the horizon of the arrival curve prefix divides A+ε, then A is not contained in the search space for fixed-priority tasks.
Lemma constant_max_arrivals :
∀ A,
(∀ s, s \in get_time_steps_of_task tsk → s < get_horizon_of_task tsk) →
get_horizon_of_task tsk %| (A + ε) →
max_arrivals tsk A = max_arrivals tsk (A + ε).
Finally, we show that steps in the request-bound function correspond to points in the search space for fixed-priority tasks.
Lemma task_search_space_subset :
∀ A,
A < L →
task_rbf tsk A != task_rbf tsk (A + ε) →
A \in search_space_arrival_curve_prefix_FP tsk L.
End FastSearchSpaceComputation.