Library prosa.implementation.refinements.fast_search_space_computation
In this section, we provide definitions and lemmas to show
Abstract RTA' s search space can be rewritten in an equivalent,
computation-oriented way.
Let L be a constant which bounds any busy interval of task tsk.
Consider a task set ts with valid arrivals...
Variable tsk : Task.
Hypothesis H_positive_cost : 0 < task_cost tsk.
Hypothesis H_tsk_in_ts : tsk \in ts.
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.
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.
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).
(∀ 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).
∀ 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.
∀ 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.
∀ 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 + ε).
∀ 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.