# Library prosa.implementation.refinements.EDF.fast_search_space

Require Export prosa.results.rta.ideal.edf.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 concrete_max_arrivals_instance.
Definition Task := concrete_task : eqType.
Definition Job := concrete_job : eqType.
... and that we know the maximum non-preemptive segment for each task.
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.