Library prosa.implementation.refinements.FP.refinements

Require Export prosa.implementation.refinements.refinements.
Require Export prosa.implementation.refinements.FP.fast_search_space.
Require Export prosa.implementation.refinements.arrival_bound.

Throughout this file, we work with Prosa's fixed-priority policy implementation.

#[local] Existing Instance NumericFPAscending.

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_of (@task_T T )}.

We define a generic version of higher-or-equal priority task, ...

Definition hep_task_T tsk_o tsk := (task_priority_T tsk ≤ @task_priority_T T tsk_o)%C.

... of total request-bound function of higher-or-equal priority task, ...

  Definition total_hep_rbf_T (ts : seq task_T) (tsk : task_T) (Δ : T) : T :=
    let hep_ts := filter (fun tsk' ⇒ hep_task_T tsk' tsk) ts in
    let work_ts := map (fun tsk' ⇒ task_rbf_T tsk' Δ) hep_ts in
    foldr +%C 0%C work_ts.

... an analogous version of hep_task in without symmetry, ...

Definition ohep_task_T tsk_o tsk :=
(hep_task_T tsk_o tsk ) && (~~ (eq_of2 tsk_o tsk)%C).

... with a respective cumulative version.

  Definition total_ohep_rbf_T (ts : seq task_T) (tsk : task_T) (Δ : T) : T :=
    let hep_ts := filter (fun tsk' ⇒ ohep_task_T tsk' tsk) ts in
    let work_ts := map (fun tsk' ⇒ task_rbf_T tsk' Δ) hep_ts in
    foldr +%C 0%C work_ts.

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) +
     total_ohep_rbf_T ts tsk (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) :=
    let lp_ts := filter (fun tsk_o ⇒ ~~ hep_task_T tsk_o tsk) ts in
    let block_ts := map (fun tsk_o ⇒ task_cost_T tsk_o - 1)%C lp_ts in
    foldr maxn_T 0%C block_ts.

... and 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
     + (task_rbf_T tsk (P .1 + 1) - (task_cost_T tsk - 1))
     + total_ohep_rbf_T ts tsk (P .1 + P .2) ≤ P .1 + P .2)%C
    && (P .2 + (task_cost_T tsk - 1) ≤ R)%C.

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 search_space_emax_FP_h, ...

  Definition search_space_emax_FP_h_N (tsk : task_T) (l r : N) : seq N :=
    let h := get_horizon_of_task_T tsk in
    let offsets := map (N.mul h) (iota_N l r) in
    let emax_offsets := repeat_steps_with_offset_T tsk offsets in
    map predn_T emax_offsets.

... and of search_space_emax_FP.

  Definition search_space_emax_FP_N (tsk : task_T) (L : N) :=
    let h := get_horizon_of_task_T tsk in
    search_space_emax_FP_h_N tsk 0 (((L %/ h)+1))%C.

End DefinitionsN.

Refinements

We now establish the desired refinements.

First, we prove a refinement for the search_space_emax_h function.

Next, we prove a refinement for the search_space_emax_FP function.

Global Instance refine_search_space_emax :
  ∀ tsk,
    refines (Rnat ==> list_R Rnat)%rel
            (search_space_emax_FP (taskT_to_task tsk))
            (search_space_emax_FP_N tsk).

Next, we prove a refinement for the hep_task function.

Global Instance refine_hep_task :
refines ( Rtask ==> Rtask ==> bool_R )%rel hep_task hep_task_T.

Next, we prove a refinement for the total_hep_rbf function.

Global Instance refine_total_hep_rbf :
refines ( list_R Rtask ==> Rtask ==> Rnat ==> Rnat )%rel total_hep_rbf total_hep_rbf_T.

Next, we prove a special-case refinement for the total_hep_rbf 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_hep_rbf' :
  ∀ ts tsk,
    refines (Rnat ==> Rnat)%rel
            (total_hep_rbf (map taskT_to_task ts) (taskT_to_task tsk))
            (total_hep_rbf_T ts tsk) | 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_listNN : eq_of (seq (prod N 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.

Global Instance refine_task_eqdef :
refines (Rtask ==> Rtask ==> bool_R)%rel task_eqdef task_eqdef_T.

Next, we prove a refinement for the ohep_task function.

Global Instance refine_ohep_task :
refines ( Rtask ==> Rtask ==> bool_R )%rel ohep_task ohep_task_T.

Next, we prove a refinement for the total_ohep_rbf function.

Global Instance refine_total_ohep_rbf :
refines ( list_R Rtask ==> Rtask ==> Rnat ==> Rnat )%rel total_ohep_rbf total_ohep_rbf_T.

Next, we prove a refinement for the check_point_FP function.

Global Instance refine_check_point :
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' :
  ∀ 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 )%rel blocking_bound_NP blocking_bound_NP_T.

Next, we prove a special-case refinement for the blocking_bound_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_blocking_bound' :
  ∀ ts tsk,
    refines ( Rnat )%rel
            (blocking_bound_NP (map taskT_to_task ts) (taskT_to_task tsk))
            (blocking_bound_NP_T ts tsk) | 0.

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.