Library prosa.analysis.definitions.request_bound_function

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

Request Bound Function (RBF)

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

Section TaskWorkloadBoundedByArrivalCurves.

Consider any type of task characterized by a WCET bound and an arrival curve.
  Context {Task : TaskType}.
  Context `{TaskCost Task} `{MaxArrivals Task}.

RBF of a Single Task

We define the classic notion of an RBF, which for a given task tsk and interval length Δ, bounds the maximum cumulative processor demand of all jobs released by tsk in any interval of length Δ.
  Definition task_request_bound_function (tsk : Task) (Δ : duration) :=
    task_cost tsk × max_arrivals tsk Δ.

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.