Library prosa.implementation.refinements.fast_search_space_computation

Require Export prosa.implementation.refinements.arrival_curve_prefix.

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.