Library prosa.model.task.arrival.request_bound_functions
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.util.rel.
Require Export prosa.model.task.arrivals.
Request Bound Functions (RBF)
Task Parameters for the Request Bound Functions
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 [Δ].
Parameter Semantics
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Consider any job arrival sequence.
Definition of Request Bound Functions
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.
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).
∀ (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.
∀ (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
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Consider any job arrival sequence...
...and all kinds of request bounds.
Let [ts] be an arbitrary task set.
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).
∀ (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.