# Library prosa.implementation.refinements.EDF.refinements

Require Export prosa.implementation.refinements.refinements.
Require Export prosa.implementation.refinements.task.
Require Export prosa.implementation.refinements.EDF.fast_search_space.
Require Export prosa.implementation.refinements.arrival_bound.
We begin by defining a generic version of the functions we seek to define.
Section Definitions.
Consider a generic type T supporting basic arithmetic operations, neutral elements, and comparisons.
Context {T : Type}.
Context `{!zero_of T, !one_of T, !sub_of T, !add_of T, !mul_of T,
!div_of T, !mod_of T, !eq_of T, !leq_of T, !lt_of T}.
Context `{!eq_of (seq T)}.
Context {eq_of2 : eq_of (@task_T T)}.
We define a generic version of total request-bound function of higher-or-equal priority task, ...
Definition total_rbf_T (ts : seq task_T) (Δ : T) : T :=
let work_ts := map (fun tsk' ⇒ task_rbf_T tsk' Δ) ts in
foldr +%C 0%C work_ts.
... of bound on total higher-or-equal priority workload, ...
Definition bound_on_total_hep_workload_T (ts : seq task_T) (tsk : task_T) (A Δ : T) : T :=
let o_ts := filter (fun tsk_o ⇒ ~~ (eq_of2 tsk_o tsk)) ts in
let o_work := map (fun tsk_o ⇒ task_rbf_T tsk_o (minn_T ((A + 1) + task_deadline_T tsk - task_deadline_T tsk_o) Δ))%C o_ts in
foldr +%C 0%C o_work.
Next, we define a generic version of check_point_FP, ...
Definition check_point_FP_T (ts : seq task_T) (tsk : task_T) (R : T) (P : T × T) : bool :=
(task_rbf_T tsk (P.1 + 1) + bound_on_total_hep_workload_T ts tsk P.1 (P.1 + P.2) ≤ P.1 + P.2)%C
&& (P.2 ≤ R)%C.
... a generic version of blocking_bound_NP, ...
Definition blocking_bound_NP_T (ts : seq task_T) (tsk : task_T) A :=
let blocking_relevant tsk_o := (0 < ConcreteMaxArrivals_T tsk_o 1)%C && (0 < task_cost_T tsk_o)%C in
let ts_lp := filter (fun tsk_o ⇒ (blocking_relevant tsk_o)
&& (@task_deadline_T T tsk + A < @task_deadline_T T tsk_o))%C ts in
let ts_block := map (fun tsk_o ⇒ task_cost_T tsk_o - 1)%C ts_lp in
foldr maxn_T 0%C ts_block.
... of check_point_NP, ...
Definition check_point_NP_T (ts : seq task_T) (tsk : task_T) (R : T) (P : T × T) : bool :=
(blocking_bound_NP_T ts tsk P.1
+ (task_rbf_T tsk (P.1 + 1) - (task_cost_T tsk - 1))
+ bound_on_total_hep_workload_T ts tsk P.1 (P.1 + P.2) ≤ P.1 + P.2)%C
&& (P.2 + (task_cost_T tsk - 1) ≤ R)%C.
... of valid_arrivals.
Definition valid_arrivals_T (tsk : task_T) : bool :=
match @task_arrival_T T tsk with
| Periodic_T p ⇒ (1 ≤ p)%C
| Sporadic_T m ⇒ (1 ≤ m)%C
| ArrivalPrefix_T emax_vec ⇒ valid_extrapolated_arrival_curve_T emax_vec
end.
End Definitions.
In the following, we introduce some functions operating on binary numbers.
We provide a definition of iota, ...
Definition iota_N (a Δ : N) := iota_T a Δ.
... of task_search_space_emax_EDF_h, ...
Definition task_search_space_emax_EDF_h_N (tsk tsko : task_T) (l r : N) : seq N :=
let h := get_horizon_of_task_T tsko in
let offsets := map (N.mul h) (iota_N l r) in
let emax_offsets := repeat_steps_with_offset_T tsko offsets in
let emax_edf_offsets :=
shift_points_neg_T
(shift_points_pos_T emax_offsets (task_deadline_T tsko))
(task_deadline_T tsk) in
map predn_T emax_edf_offsets.
... of task_search_space_emax_EDF, ...
Definition task_search_space_emax_EDF_N (tsk tsko : task_T) (L : N) :=
let h := get_horizon_of_task_T tsko in
task_search_space_emax_EDF_h_N
tsk tsko 0
(((L + (task_deadline_T tsk - task_deadline_T tsko)) %/ h) + 1)%C.
... and of search_space_emax_EDF_N.
Definition search_space_emax_EDF_N (ts : seq task_T) (tsk : task_T) (L : N) :=
let points := map (fun tsko ⇒ task_search_space_emax_EDF_N tsk tsko L) ts in
flatten points.

## Refinements

We now establish the desired refinements.
First, we prove a refinement for the task_search_space_emax_EDF_h function.
Local Instance refine_task_search_space_emax_edf_h :
refines (Rtask ==> Rtask ==> Rnat ==> Rnat ==> list_R Rnat)%rel
task_search_space_emax_EDF_h
task_search_space_emax_EDF_h_N.
Next, we prove a refinement for the task_search_space_emax_EDF function.
Global Instance refine_task_search_space_emax_edf :
∀ tsk tsko,
refines (Rnat ==> list_R Rnat)%rel
(task_search_space_emax_EDF (taskT_to_task tsk) (taskT_to_task tsko))
(task_search_space_emax_EDF_N tsk tsko).
Next, we prove a refinement for the search_space_emax_EDF function.
Global Instance refine_search_space_emax_edf :
∀ ts tsk,
refines (Rnat ==> list_R Rnat)%rel
(search_space_emax_EDF (map taskT_to_task ts) (taskT_to_task tsk))
(search_space_emax_EDF_N ts tsk).
Next, we prove a refinement for the total_request_bound_function function.
Local Instance refine_total_rbf :
refines (list_R Rtask ==> Rnat ==> Rnat)%rel total_request_bound_function total_rbf_T.
Next, we prove a special-case refinement for the total_request_bound_function function when applied to a refined task set and a refined task. This special case is required to guide the typeclass engine.
Global Instance refine_total_rbf' :
∀ ts,
refines (Rnat ==> Rnat)%rel
(total_request_bound_function (map taskT_to_task ts))
(total_rbf_T ts) | 0.
Next, we provide equality comparisons between different pairs of objects manipulated in Poet's certificates.
Global Instance eq_list_n : eq_of (seq N) := fun x y ⇒ x == y.
Global Instance eq_n_list_nn : eq_of (prod N (seq (prod N N))) := fun x y ⇒ x == y.
Global Instance eq_taskab : eq_of (@task_arrivals_bound_T N) := taskab_eqdef_T.
Global Instance eq_task : eq_of (@task_T N) := task_eqdef_T.
Next, we prove a refinement for the task_eqdef function.
Local Instance refine_task_eqdef :
refines (Rtask ==> Rtask ==> bool_R)%rel task_eqdef task_eqdef_T.
Next, we prove a refinement for the bound_on_total_hep_workload function.
Global Instance refine_bound_on_total_hep_workload :
refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat ==> Rnat)%rel
bound_on_total_hep_workload bound_on_total_hep_workload_T.
Next, we prove a refinement for the check_point_FP function.
Global Instance refine_check_point_fp :
refines (list_R Rtask ==> Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
check_point_FP check_point_FP_T.
Next, we prove a special-case refinement for the check_point_FP function when applied to a refined task set and a refined task. This special case is required to guide the typeclass engine.
Global Instance refine_check_point_fp' :
∀ ts tsk,
refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
(check_point_FP (map taskT_to_task ts) (taskT_to_task tsk))
(check_point_FP_T ts tsk) | 0.
Next, we prove a refinement for the blocking_bound_NP function.
Global Instance refine_blocking_bound :
refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)%rel blocking_bound_NP blocking_bound_NP_T.
Next, we prove a refinement for the check_point_NP function.
Global Instance refine_check_point_np :
refines (list_R Rtask ==> Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
check_point_NP check_point_NP_T.
Finally, we prove a special-case refinement for the check_point_NP function when applied to a refined task set and a refined task. This special case is required to guide the typeclass engine.
Global Instance refine_check_point_np' :
∀ ts tsk,
refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
(check_point_NP (map taskT_to_task ts) (taskT_to_task tsk))
(check_point_NP_T ts tsk) | 0.