Library prosa.model.task.arrival.request_bound_functions


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)

Require Export prosa.util.rel.
Require Export prosa.model.task.arrivals.

Request Bound Functions (RBF)

In the following, we define the notion of Request Bound Functions (RBF), which can be used to reason about the job cost arrivals. In contrast to arrival curves which constrain the number of arrivals per time interval, request bound functions bound the sum of costs of arriving jobs.

Task Parameters for the Request Bound Functions

The request bound functions give an upper bound and, optionally, a lower bound on the cost of new job arrivals during any given interval.
We let [max_request_bound tsk Δ] denote a bound on the maximum cost of arrivals of jobs of task [tsk] in any interval of length [Δ].
Class MaxRequestBound (Task : TaskType) := max_request_bound : Task → duration → work.

Conversely, we let [min_request_bound tsk Δ] denote a bound on the minimum cost of arrivals of jobs of task [tsk] in any interval of length [Δ].
Class MinRequestBound (Task : TaskType) := min_request_bound : Task → duration → work.

Parameter Semantics

In the following, we precisely define the semantics of the request bound functions.
Section RequestBoundFunctions.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.

Consider any job arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Definition of Request Bound Functions

First, what constitutes a valid request bound function for a task?
  Section RequestBoundFunctions.

We say that a given bound [request_bound] is a valid request bound function iff [request_bound] is a monotonic function that equals 0 for the empty interval [delta = 0].
    Definition valid_request_bound_function (request_bound : duration → work) :=
      request_bound 0 = 0 ∧
      monotone request_bound leq.

We say that [request_bound] is an upper request bound for task [tsk] iff, for any interval [t1, t2), [request_bound (t2 - t1)] bounds the sum of costs of jobs of [tsk] that arrive in that interval.
    Definition respects_max_request_bound (tsk : Task) (max_request_bound : duration → work) :=
      ∀ (t1 t2 : instant),
        t1 ≤ t2 →
        cost_of_task_arrivals arr_seq tsk t1 t2 ≤ max_request_bound (t2 - t1).

We analogously define the lower request bound.
    Definition respects_min_request_bound (tsk : Task) (min_request_bound : duration → work) :=
      ∀ (t1 t2 : instant),
        t1 ≤ t2 →
        min_request_bound (t2 - t1) ≤ cost_of_task_arrivals arr_seq tsk t1 t2.

  End RequestBoundFunctions.

End RequestBoundFunctions.

Model Validity

Based on the just-established semantics, we define the properties of a valid request bound model.
Section RequestBoundFunctionsModel.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.

Consider any job arrival sequence...
  Variable arr_seq : arrival_sequence Job.

...and all kinds of request bounds.
  Context `{MaxRequestBound Task}
          `{MinRequestBound Task}.

Let [ts] be an arbitrary task set.
  Variable ts : TaskSet Task.

We say that [request_bound] is a valid arrival curve for a task set if it is valid for any task in the task set
  Definition valid_taskset_request_bound_function (request_bound : Task → duration → work) :=
    ∀ (tsk : Task), tsk \in ts → valid_request_bound_function (request_bound tsk).

Finally, we lift the per-task semantics of the respective request bound functions to the entire task set.

  Definition taskset_respects_max_request_bound :=
    ∀ (tsk : Task), tsk \in ts → respects_max_request_bound arr_seq tsk (max_request_bound tsk).

  Definition taskset_respects_min_request_bound :=
    ∀ (tsk : Task), tsk \in ts → respects_min_request_bound arr_seq tsk (min_request_bound tsk).

End RequestBoundFunctionsModel.