Library prosa.implementation.refinements.EDF.fast_search_space

Require Export prosa.results.edf.rta.bounded_nps.
Require Export prosa.implementation.refinements.fast_search_space_computation.

First, we define the concept of higher-or-equal-priority workload.
Definition bound_on_total_hep_workload (ts : seq Task) (tsk : Task) A Δ :=
  \sum_(tsk_o <- ts | tsk_o != tsk)
   task_rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).

Next, we provide a function that checks a single point P=(A,F) of the search space when adopting a fully-preemptive policy.
Definition check_point_FP (ts : seq Task) (tsk : Task) (R : nat) (P : nat × nat) :=
  (task_rbf tsk (P.1 + ε) + bound_on_total_hep_workload ts tsk P.1 (P.1 + P.2) ≤ P.1 + P.2)
  && (P.2 ≤ R).

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.
Definition check_point_NP (ts : seq Task) (tsk : Task) (R : nat) (P : nat × nat) :=
  (blocking_bound_NP ts tsk P.1
   + (task_rbf tsk (P.1 + ε) - (task_cost tsk - ε))
   + bound_on_total_hep_workload ts tsk P.1 (P.1 + P.2) ≤ P.1 + P.2)
  && (P.2 + (task_cost tsk - ε) ≤ R).

Search Space Definitions

Section SearchSpaceDefinition.

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.
  Definition search_space_emax_EDF ts (tsk : Task) (L : nat) :=
    \cat_(tsko <- ts) task_search_space_emax_EDF tsk tsko L.

End SearchSpaceDefinition.

Fast Search Space Computation Lemmas

Section FastSearchSpaceComputationSubset.

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.
  Lemma EDF_ss_generalize_FP_ss :
    task_search_space_emax_EDF_h
      tsk tsk 0 ((L + (task_deadline tsk - task_deadline tsk)) %/ get_horizon_of_task tsk).+1
    = search_space_emax_FP L tsk.

Finally, we show that the abstract RTA's standard search space is a subset of the computation-oriented version defined above.
  Lemma search_space_subset_EDF :
    ∀ A, A \in correct_search_space ts tsk L → A \in search_space_emax_EDF ts tsk L.

End FastSearchSpaceComputationSubset.