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.

  Section Definitions.

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.

  End Definitions.

  Section Facts.

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 Facts.

End FastSearchSpaceComputation.