Library prosa.implementation.refinements.arrival_curve

Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.implementation.refinements.task.

Arrival Curve Refinements.

In this module, we provide a series of definitions related to arrival curves when working with generic tasks.
First, we define a helper function that yields the horizon of the arrival curve prefix of a task ...
Definition get_horizon_of_task (tsk : Task) : duration :=
  horizon_of (get_arrival_curve_prefix tsk).

... another one that yields the time steps of the arrival curve, ...
Definition get_time_steps_of_task (tsk : Task) : seq duration :=
  time_steps_of (get_arrival_curve_prefix tsk).

... a function that yields the same time steps, offset by δ, ...
Definition time_steps_with_offset tsk δ := [seq t + δ | t <- get_time_steps_of_task tsk].

... and a generalization of the previous function that repeats the time steps for each given offset.
Definition repeat_steps_with_offset (tsk : Task) (offsets : seq nat): seq nat :=
  flatten (map (time_steps_with_offset tsk) offsets).

For convenience, we provide a short form to indicate the request-bound function of a task.
Definition task_rbf (tsk : Task) (Δ : duration) :=
  task_request_bound_function tsk Δ.

Further, we define a valid arrival bound as (1) a positive minimum inter-arrival time/period, or (2) a valid arrival curve prefix.
Definition valid_arrivals (tsk : Task) : bool :=
  match task_arrival tsk with
  | Periodic p ⇒ p ≥ 1
  | Sporadic m ⇒ m ≥ 1
  | ArrivalPrefix emax_vec ⇒ valid_arrival_curve_prefix_dec emax_vec
  end.

Next, we define some helper functions, that indicate whether the given task is periodic, ...
Definition is_periodic_arrivals (tsk : Task) : Prop :=
  ∃ p, task_arrival tsk = Periodic p.

... sporadic, ...
Definition is_sporadic_arrivals (tsk : Task) : Prop :=
  ∃ m, task_arrival tsk = Sporadic m.

... or bounded by an arrival curve.
Definition is_etamax_arrivals (tsk : Task) : Prop :=
  ∃ ac_prefix_vec, task_arrival tsk = ArrivalPrefix ac_prefix_vec.

Further, for convenience, we define the notion of task having a valid arrival curve.
Definition has_valid_arrival_curve_prefix (tsk: Task) :=
  ∃ ac_prefix_vec, get_arrival_curve_prefix tsk = ac_prefix_vec ∧
                    valid_arrival_curve_prefix ac_prefix_vec.

Finally, we define define the notion of task set with valid arrivals.
Definition task_set_with_valid_arrivals (ts : seq Task) :=
  ∀ tsk,
    tsk \in ts → valid_arrivals tsk.

In this section, we prove some facts regarding the above definitions.
Section Facts.

Consider a task tsk.
  Variable tsk : Task.

First, we show that valid_arrivals matches valid_arrivals_dec.
  Lemma valid_arrivals_P :
    reflect (valid_arrivals tsk) (valid_arrivals tsk).

Next, we show that a task is either periodic, sporadic, or bounded by an arrival-curve prefix.
  Lemma arrival_cases :
    is_periodic_arrivals tsk
    ∨ is_sporadic_arrivals tsk
    ∨ is_etamax_arrivals tsk.

End Facts.

In this fairly technical section, we prove a series of refinements aimed to be able to convert between a standard natural-number task arrival bound and an arrival bound that uses, instead of numbers, a generic type T.
Section Theory.

First, we prove a refinement for positive_horizon.

Next, we prove a refinement for large_horizon.

Next, we prove a refinement for no_inf_arrivals.

Next, we prove a refinement for specified_bursts.

Next, we prove a refinement for the arrival curve prefix validity.

Next, we prove a refinement for the arrival curve validity.
  Global Instance refine_valid_arrivals :
    ∀ tsk,
      refines (bool_R)%rel
              (valid_arrivals (taskT_to_task tsk))
              (valid_arrivals_T tsk) | 0.
Next, we prove a refinement for repeat_steps_with_offset.
  Global Instance refine_repeat_steps_with_offset :
    refines (Rtask ==> list_R Rnat ==> list_R Rnat)%rel
            repeat_steps_with_offset repeat_steps_with_offset_T.

Next, we prove a refinement for get_horizon_of_task.
  Global Instance refine_get_horizon_of_task :
    refines (Rtask ==> Rnat)%rel get_horizon_of_task get_horizon_of_task_T.
Next, we prove a refinement for the extrapolated arrival curve.

Next, we prove a refinement for the arrival bound definition.
Next, we prove a refinement for the arrival bound definition applied to the task conversion function.
  Global Instance refine_ConcreteMaxArrivals' :
    ∀ tsk,
      refines (Rnat ==> Rnat)%rel (ConcreteMaxArrivals (taskT_to_task tsk))
              (ConcreteMaxArrivals_T tsk) | 0.
Next, we prove a refinement for get_arrival_curve_prefix.
  Global Instance refine_get_arrival_curve_prefix :
    refines (Rtask ==> prod_R Rnat (list_R (prod_R Rnat Rnat)))%rel
            get_arrival_curve_prefix get_extrapolated_arrival_curve_T.

Next, we prove a refinement for get_arrival_curve_prefix applied to lists.
  Global Instance refine_get_arrival_curve_prefix' :
    ∀ tsk,
      refines
        (prod_R Rnat (list_R (prod_R Rnat Rnat)))%rel
        (get_arrival_curve_prefix (taskT_to_task tsk))
        (get_extrapolated_arrival_curve_T tsk) | 0.

Next, we prove a refinement for sorted when applied to leq_steps.
  Global Instance refine_sorted_leq_steps :
    ∀ tsk,
      refines (bool_R)%rel
              (sorted leq_steps (steps_of (get_arrival_curve_prefix (taskT_to_task tsk))))
              (sorted leq_steps_T (get_extrapolated_arrival_curve_T tsk).2) | 0.

Lastly, we prove a refinement for the task request-bound function.
  Global Instance refine_task_rbf :
    refines ( Rtask ==> Rnat ==> Rnat )%rel task_rbf task_rbf_T.

End Theory.