Library prosa.analysis.definitions.request_bound_function

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.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks, where each task has a cost.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.

Also assume an FP policy that indicates a higher-or-equal priority relation.
  Context `{FP_policy Task}.

Let MaxArrivals denote any function that takes a task and an interval length and returns the associated number of job arrivals of the task.
  Context `{MaxArrivals Task}.

RBF of a Single Task

In this section, we define a bound for the workload of a single task under uni-processor FP scheduling.
  Section SingleTask.

Consider any task tsk that is to be scheduled in an interval of length delta.
    Variable tsk : Task.
    Variable delta : duration.

We define the following workload bound for the task.
    Definition task_request_bound_function :=
      task_cost tsk × max_arrivals tsk delta.

  End SingleTask.

Total RBF of Multiple Tasks

In this section, we define a bound for the workload of multiple tasks.
  Section AllTasks.

Consider a task set ts...
    Variable ts : list Task.

...and let tsk be any task in task set.
    Variable tsk : Task.

Let delta be the length of the interval of interest.
    Variable delta : duration.

Recall the definition of higher-or-equal-priority task for FP scheduling.
Using the sum of individual workload bounds, we define the following bound for the total workload of tasks in any interval of length delta.
Similarly, 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 delta.
We also define a bound for the total workload of higher-or-equal-priority tasks other than tsk in any interval of length delta.
We also define a bound for the total workload of higher-or-equal-priority tasks other than tsk in any interval of length delta.
Finally, we define a bound for the total workload of higher-priority tasks in any interval of length delta.