# Library prosa.model.task.arrival.curve_as_rbf

Require Export prosa.util.all.
Require Export prosa.analysis.facts.model.cumulative_cost.
Require Export prosa.model.task.arrival.request_bound_functions.
Require Export prosa.model.task.arrival.curves.

# Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF)

In the following, we show a way to convert a given arrival curve, paired with a worst-case/best-case execution time, to a request-bound function. Definitions and proofs will handle both lower-bounding and upper-bounding arrival curves.
Section ArrivalCurveToRBF.
Consider any type of tasks with a given cumulative cost and minimum scalar cost.
Context {Task : TaskType} `{TaskCumulativeCost Task} `{TaskMinCost Task}.
... and any type of jobs associated with these tasks.
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job}.
Let MaxArr and MinArr represent two arrivals curves. MaxArr upper-bounds the possible number or arrivals for a given task, whereas MinArr lower-bounds it.
Context `{MaxArr : MaxArrivals Task} `{MinArr : MinArrivals Task}.
We define the upper-bounding conversion as the cumulative cost of the maximum number of arrivals during Δ. Symmetrically, in the lower-bounding case, the cumulative cost of the jobs is derived from the task's BCET via scalar multiplication.
Definition task_max_rbf (arrivals : Task → duration → nat) task Δ :=
task_cumulative_cost task (arrivals task Δ).
Definition task_min_rbf (arrivals : Task → duration → nat) task Δ := task_min_cost task × arrivals task Δ.
Finally, we show that the newly defined functions are indeed request-bound functions.
Global Program Instance max_arrivals_rbf : MaxRequestBound Task :=
{
max_request_bound := task_max_rbf max_arrivals
}.
Global Program Instance min_arrivals_rbf : MinRequestBound Task :=
{
min_request_bound := task_min_rbf min_arrivals
}.
In the following section, we prove that the transformation yields a request-bound function that conserves correctness properties in both the upper-bounding and lower-bounding cases.
First, we establish the validity of the transformation for a single, given task.
Section SingleTask.
Consider an arbitrary task tsk ...
Variable tsk : Task.
... and any job arrival sequence.
Variable arr_seq : arrival_sequence Job.
First, note that any valid upper-bounding arrival curve, after being converted, is a valid request-bound function.
Fact valid_arrival_curve_to_max_rbf :
valid_task_cumulative_cost tsk →
valid_arrival_curve (max_arrivals tsk) →
valid_request_bound_function (max_request_bound tsk).
The same idea can be applied in the lower-bounding case.
Fact valid_arrival_curve_to_min_rbf :
valid_arrival_curve (min_arrivals tsk) →
valid_request_bound_function (min_request_bound tsk).
Next, we prove that the task respects the request-bound function in the upper-bounding case. Note that, for this to work, we assume that the cost of tasks upper-bounds the cost of the jobs belonging to them (i.e., the task cost is the worst case).
Fact respects_arrival_curve_to_max_rbf :
valid_task_cumulative_cost tsk →
respects_task_cumulative_cost arr_seq tsk →
respects_max_arrivals arr_seq tsk (max_arrivals tsk) →
respects_max_request_bound arr_seq tsk (max_request_bound tsk).
Finally, we prove that the task respects the request-bound function also in the lower-bounding case. This time, we assume that the cost of tasks lower-bounds the cost of the jobs belonging to them. (i.e., the task cost is the best-case).
Fact respects_arrival_curve_to_min_rbf :
jobs_have_valid_min_job_costs →
respects_min_arrivals arr_seq tsk (min_arrivals tsk) →
respects_min_request_bound arr_seq tsk (min_request_bound tsk).
End SingleTask.
Next, we lift the results to the previous section to an arbitrary task set.
Section TaskSet.
Let ts be an arbitrary task set ...
Variable ts : TaskSet Task.
... and consider any job arrival sequence.
Variable arr_seq : arrival_sequence Job.
First, we generalize the validity of the transformation to a task set both in the upper-bounding case ...
Corollary valid_taskset_arrival_curve_to_max_rbf :
taskset_has_valid_cumulative_cost_bounds ts →
valid_taskset_arrival_curve ts max_arrivals →
valid_taskset_request_bound_function ts max_request_bound.
... and in the lower-bounding case.
Corollary valid_taskset_arrival_curve_to_min_rbf :
valid_taskset_arrival_curve ts min_arrivals →
valid_taskset_request_bound_function ts min_request_bound.
Second, we show that a task set that respects a given arrival curve also respects the produced request-bound function, lifting the result obtained in the single-task case. The result is valid in the upper-bounding case...
Corollary taskset_respects_arrival_curve_to_max_rbf :
taskset_has_valid_cumulative_cost_bounds ts →
taskset_respects_cumulative_cost_bounds arr_seq ts →
taskset_respects_max_arrivals arr_seq ts →
taskset_respects_max_request_bound arr_seq ts.
...as well as in the lower-bounding case.
Corollary taskset_respects_arrival_curve_to_min_rbf :
jobs_have_valid_min_job_costs →
taskset_respects_min_arrivals arr_seq ts →
taskset_respects_min_request_bound arr_seq ts.
End TaskSet.
End ArrivalCurveToRBF.
We add the lemmas into the "Hint Database" basic_rt_facts so that they become available for proof automation.
Global Hint Resolve
valid_arrival_curve_to_max_rbf
respects_arrival_curve_to_max_rbf
valid_taskset_arrival_curve_to_max_rbf
taskset_respects_arrival_curve_to_max_rbf
: basic_rt_facts.