Library prosa.implementation.refinements.EDF.fast_search_space

First, we define the concept of higher-or-equal-priority workload.
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.
Definition blocking_bound_NP (ts : seq Task) (tsk : Task) (A : nat) :=
  \max_(tsk_o <- [seq i | i <- ts] | blocking_relevant tsk_o &&
                                   (task_deadline tsk + A <
                                    task_deadline tsk_o)) (task_cost tsk_o - ε).

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

Assume that an arrival curve based on a concrete prefix is given.
  #[local] Existing Instance ConcreteMaxArrivals.
  Definition Task := [eqType of concrete_task].
  Definition Job := [eqType of concrete_job].

  Context (TMNSP: TaskMaxNonpreemptiveSegment Task).

First, we recall the notion of correct search space as defined by abstract RTA.
  Definition correct_search_space ts (tsk:Task) L :=
    [seq A <- iota 0 L | is_in_search_space ts tsk L A].

Next, we provide a computation-oriented way to compute abstract RTA's search space for fixed-priority schedules, as we will prove that earliest-deadline-first is equivalent. We start with a function that computes the search space in a generic interval [l,r), ...
  Definition search_space_emax_FP_h (tsk : Task) l r :=
    let h := get_horizon_of_task tsk in
    let offsets := map (muln h) (iota l r) in
    let emax_offsets := repeat_steps_with_offset tsk offsets in
    map predn emax_offsets.

... which we then apply to the interval [0, (L %/h).+1).
  Definition search_space_emax_FP L (tsk : Task) :=
    let h := get_horizon_of_task tsk in
    search_space_emax_FP_h (tsk : Task) 0 (L %/h).+1.

Analogously, we define the search space for a task scheduled under earliest-deadline-first in a generic interval [l,r), ...
  Definition task_search_space_emax_EDF_h (tsk tsko : Task) (l r : nat) :=
    let h := get_horizon_of_task tsko in
    let offsets := map (muln h) (iota l r) in
    let emax_offsets := repeat_steps_with_offset tsko offsets in
    let emax_edf_offsets := shift_points_neg (shift_points_pos emax_offsets (task_deadline tsko))
                                             (task_deadline tsk) in
    map predn emax_edf_offsets.

...which we then apply to the interval [0, (L %/h).+1).
  Definition task_search_space_emax_EDF (tsk tsko : Task) (L : nat) :=
    let h := get_horizon_of_task tsko in
    task_search_space_emax_EDF_h tsk tsko
                                 0 ((L + (task_deadline tsk - task_deadline tsko)) %/ h).+1.

Finally, we define the overall search space as the concatenation of per-task search spaces.

Fast Search Space Computation Lemmas

Consider a given maximum busy-interval length L, ...
  Variable L : duration.

... a task set ts with valid arrivals, positive task costs, and arrival curves with positive steps, ...
  Variable ts : seq Task.
  Hypothesis H_valid_task_set : task_set_with_valid_arrivals ts.
  Hypothesis H_all_tsk_positive_cost : tsk, tsk \in ts 0 < task_cost tsk.
  Hypothesis H_all_tsk_positive_step :
     tsk, tsk \in ts fst (head (0,0) (steps_of (get_arrival_curve_prefix tsk))) > 0.

... and a task belonging to ts.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

First, we show that the earliest-deadline-first search space is a generalization of the fixed-priority search space.
Finally, we show that the abstract RTA's standard search space is a subset of the computation-oriented version defined above.