Require Export prosa.model.task.arrival.curves.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
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.