Library prosa.analysis.definitions.request_bound_function

Require Export prosa.model.task.arrival.curve_as_rbf.
Require Export prosa.model.priority.classes.
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.util.sum.

Request Bound Function (RBF)

We recall the notion of a task's request-bound function (RBF), and define the total request bound function of a set of tasks.

Section TaskWorkloadBoundedByArrivalCurves.

Consider any type of task equipped with a maximum request-bound function.
  Context {Task : TaskType}.
  Context `{MaxRequestBound Task}.

RBF of a Single Task

We define the task-level RBF as an alias for the canonical maximum request-bound function provided by the RBF arrival model. This lets models with cumulative bounds provide precise WCET(n) information, while scalar-cost models can still recover the classic linear RBF through the automatic scalar WCET -> linear WCET(n) -> RBF conversion.
  Definition task_request_bound_function := max_request_bound.

Total RBF of Multiple Tasks

Next, we extend the notion of an RBF to multiple tasks in the obvious way.
Consider a set of tasks ts.
  Variable ts : seq Task.

The joint total RBF of all tasks in ts is simply the sum of each task's RBF.
  Definition total_request_bound_function (Δ : duration) :=
    \sum_(tsk <- ts) task_request_bound_function tsk Δ.

For convenience, we additionally introduce specialized notions of total RBF for use under FP scheduling that consider only certain tasks. relation.
  Context `{FP_policy Task}.

We define the following bound for the total workload of tasks of higher-or-equal priority (with respect to tsk) in any interval of length Δ.
  Definition total_hep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
    \sum_(tsk_other <- ts | hep_task tsk_other tsk)
     task_request_bound_function tsk_other Δ.

We also define a bound for the total workload of higher-or-equal-priority tasks other than tsk in any interval of length Δ.
  Definition total_ohep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
    \sum_(tsk_other <- ts | hep_task tsk_other tsk && (tsk_other != tsk))
      task_request_bound_function tsk_other Δ.

We also define a bound for the total workload of higher-or-equal-priority tasks other than tsk in any interval of length Δ.
  Definition total_ep_request_bound_function_FP (tsk : Task) (Δ : duration) :=
    \sum_(tsk_other <- ts | ep_task tsk_other tsk)
      task_request_bound_function tsk_other Δ.

Finally, we define a bound for the total workload of higher-priority tasks in any interval of length Δ.
  Definition total_hp_request_bound_function_FP (tsk : Task) (Δ : duration) :=
    \sum_(tsk_other <- ts | hp_task tsk_other tsk)
     task_request_bound_function tsk_other Δ.

End TaskWorkloadBoundedByArrivalCurves.