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 this section, we introduce some functions operating on binary numbers.

Section DefinitionsN.

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.

End DefinitionsN.

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_listN : eq_of (seq N) := fun x y ⇒ x == y.
Global Instance eq_NlistNN : 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.