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 := concrete_task : eqType.
  Definition Job := concrete_job : eqType.

  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.