Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.util.all .[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.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 cost ... *)
Context {Task : TaskType} `{TaskCost 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 conversion to a request-bound function as the product of the task cost and the
number of arrivals during [Δ]. In the upper-bounding case, the cost of a task will represent
the WCET of its jobs. Symmetrically, in the lower-bounding case, the cost of a task will
represent the BCET of its jobs. *)
Definition task_max_rbf (arrivals : Task -> duration -> nat) task Δ := task_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 MaxArrivalsRBF : MaxRequestBound Task := task_max_rbf max_arrivals.
Global Program Instance MinArrivalsRBF : MinRequestBound Task := 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. *)
Section Facts .
(** 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. *)
Theorem valid_arrival_curve_to_max_rbf :
forall (arrivals : Task -> duration -> nat),
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function ((task_max_rbf arrivals) tsk).Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job
forall arrivals : Task -> duration -> nat,
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function
(task_max_rbf arrivals tsk)
Proof .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job
forall arrivals : Task -> duration -> nat,
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function
(task_max_rbf arrivals tsk)
move => ARR [ZERO MONO].Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk)
valid_request_bound_function (task_max_rbf ARR tsk)
split .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk)
task_max_rbf ARR tsk 0 = 0
- Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk)
task_max_rbf ARR tsk 0 = 0
by rewrite /task_max_rbf ZERO muln0.
- Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk)
monotone leq (task_max_rbf ARR tsk)
move => x y LEQ.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk) x, y : nat LEQ : x <= y
task_max_rbf ARR tsk x <= task_max_rbf ARR tsk y
rewrite /task_max_rbf.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk) x, y : nat LEQ : x <= y
task_cost tsk * ARR tsk x <= task_cost tsk * ARR tsk y
destruct (task_cost tsk); first by rewrite mul0n.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk) x, y : nat LEQ : x <= y d : nat
d.+1 * ARR tsk x <= d.+1 * ARR tsk y
by rewrite leq_pmul2l //; apply MONO.
Qed .
(** The same idea can be applied in the lower-bounding case. *)
Theorem valid_arrival_curve_to_min_rbf :
forall (arrivals : Task -> duration -> nat),
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function ((task_min_rbf arrivals) tsk).Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job
forall arrivals : Task -> duration -> nat,
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function
(task_min_rbf arrivals tsk)
Proof .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job
forall arrivals : Task -> duration -> nat,
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function
(task_min_rbf arrivals tsk)
move => ARR [ZERO MONO].Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk)
valid_request_bound_function (task_min_rbf ARR tsk)
split .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk)
task_min_rbf ARR tsk 0 = 0
- Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk)
task_min_rbf ARR tsk 0 = 0
by rewrite /task_min_rbf ZERO muln0.
- Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk)
monotone leq (task_min_rbf ARR tsk)
move => x y LEQ.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk) x, y : nat LEQ : x <= y
task_min_rbf ARR tsk x <= task_min_rbf ARR tsk y
rewrite /task_min_rbf.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk) x, y : nat LEQ : x <= y
task_min_cost tsk * ARR tsk x <=
task_min_cost tsk * ARR tsk y
destruct (task_min_cost tsk); first by rewrite mul0n.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job ARR : Task -> duration -> nat ZERO : ARR tsk 0 = 0 MONO : monotone leq (ARR tsk) x, y : nat LEQ : x <= y d : nat
d.+1 * ARR tsk x <= d.+1 * ARR tsk y
by rewrite leq_pmul2l //; apply MONO.
Qed .
(** 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). *)
Theorem respects_arrival_curve_to_max_rbf :
jobs_have_valid_job_costs ->
respects_max_arrivals arr_seq tsk (MaxArr tsk) ->
respects_max_request_bound arr_seq tsk ((task_max_rbf MaxArr) tsk).Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job
jobs_have_valid_job_costs ->
respects_max_arrivals arr_seq tsk (MaxArr tsk) ->
respects_max_request_bound arr_seq tsk
(task_max_rbf MaxArr tsk)
Proof .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job
jobs_have_valid_job_costs ->
respects_max_arrivals arr_seq tsk (MaxArr tsk) ->
respects_max_request_bound arr_seq tsk
(task_max_rbf MaxArr tsk)
move => TASK_COST RESPECT t1 t2 LEQ.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs RESPECT : respects_max_arrivals arr_seq tsk
(MaxArr tsk) t1, t2 : instant LEQ : t1 <= t2
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
specialize (RESPECT t1 t2 LEQ).Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs t1, t2 : instant RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <=
MaxArr tsk (t2 - t1) LEQ : t1 <= t2
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
apply leq_trans with (n := task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs t1, t2 : instant RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <=
MaxArr tsk (t2 - t1) LEQ : t1 <= t2
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 t2
- Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs t1, t2 : instant RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <=
MaxArr tsk (t2 - t1) LEQ : t1 <= t2
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 t2
rewrite /max_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs t1, t2 : instant RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <=
MaxArr tsk (t2 - t1) LEQ : t1 <= t2 j : Job
j \in task_arrivals_between arr_seq tsk t1 t2 ->
true -> job_cost j <= task_cost tsk
rewrite mem_filter => /andP [/eqP TSK _] _.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs t1, t2 : instant RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <=
MaxArr tsk (t2 - t1) LEQ : t1 <= t2 j : Job TSK : job_task j = tsk
job_cost j <= task_cost tsk
rewrite -TSK.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs t1, t2 : instant RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <=
MaxArr tsk (t2 - t1) LEQ : t1 <= t2 j : Job TSK : job_task j = tsk
job_cost j <= task_cost (job_task j)
by apply TASK_COST.
- Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs t1, t2 : instant RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <=
MaxArr tsk (t2 - t1) LEQ : t1 <= t2
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
by destruct (task_cost tsk) eqn :C; rewrite /task_max_rbf C // leq_pmul2l.
Qed .
(** 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). *)
Theorem respects_arrival_curve_to_min_rbf :
jobs_have_valid_min_job_costs ->
respects_min_arrivals arr_seq tsk (MinArr tsk) ->
respects_min_request_bound arr_seq tsk ((task_min_rbf MinArr) tsk).Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job
jobs_have_valid_min_job_costs ->
respects_min_arrivals arr_seq tsk (MinArr tsk) ->
respects_min_request_bound arr_seq tsk
(task_min_rbf MinArr tsk)
Proof .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job
jobs_have_valid_min_job_costs ->
respects_min_arrivals arr_seq tsk (MinArr tsk) ->
respects_min_request_bound arr_seq tsk
(task_min_rbf MinArr tsk)
move => TASK_COST RESPECT t1 t2 LEQ.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs RESPECT : respects_min_arrivals arr_seq tsk
(MinArr tsk) t1, t2 : instant LEQ : t1 <= t2
task_min_rbf MinArr tsk (t2 - t1) <=
cost_of_task_arrivals arr_seq tsk t1 t2
specialize (RESPECT t1 t2 LEQ).Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs t1, t2 : instant RESPECT : MinArr tsk (t2 - t1) <=
number_of_task_arrivals arr_seq tsk t1 t2 LEQ : t1 <= t2
task_min_rbf MinArr tsk (t2 - t1) <=
cost_of_task_arrivals arr_seq tsk t1 t2
apply leq_trans with (n := task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs t1, t2 : instant RESPECT : MinArr tsk (t2 - t1) <=
number_of_task_arrivals arr_seq tsk t1 t2 LEQ : t1 <= t2
task_min_rbf MinArr tsk (t2 - t1) <=
task_min_cost tsk *
number_of_task_arrivals arr_seq tsk t1 t2
- Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs t1, t2 : instant RESPECT : MinArr tsk (t2 - t1) <=
number_of_task_arrivals arr_seq tsk t1 t2 LEQ : t1 <= t2
task_min_rbf MinArr tsk (t2 - t1) <=
task_min_cost tsk *
number_of_task_arrivals arr_seq tsk t1 t2
by destruct (task_min_cost tsk) eqn :C; rewrite /task_min_rbf C // leq_pmul2l.
- Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs t1, t2 : instant RESPECT : MinArr tsk (t2 - t1) <=
number_of_task_arrivals arr_seq tsk t1 t2 LEQ : t1 <= t2
task_min_cost tsk *
number_of_task_arrivals arr_seq tsk t1 t2 <=
cost_of_task_arrivals arr_seq tsk t1 t2
rewrite /min_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs t1, t2 : instant RESPECT : MinArr tsk (t2 - t1) <=
number_of_task_arrivals arr_seq tsk t1 t2 LEQ : t1 <= t2 j : Job
j \in task_arrivals_between arr_seq tsk t1 t2 ->
true -> task_min_cost tsk <= job_cost j
rewrite mem_filter => /andP [/eqP TSK _] _.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs t1, t2 : instant RESPECT : MinArr tsk (t2 - t1) <=
number_of_task_arrivals arr_seq tsk t1 t2 LEQ : t1 <= t2 j : Job TSK : job_task j = tsk
task_min_cost tsk <= job_cost j
rewrite -TSK.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task tsk : Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs t1, t2 : instant RESPECT : MinArr tsk (t2 - t1) <=
number_of_task_arrivals arr_seq tsk t1 t2 LEQ : t1 <= t2 j : Job TSK : job_task j = tsk
task_min_cost (job_task j) <= job_cost j
by apply TASK_COST.
Qed .
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 :
valid_taskset_arrival_curve ts MaxArr ->
valid_taskset_request_bound_function ts MaxArrivalsRBF.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job
valid_taskset_arrival_curve ts MaxArr ->
valid_taskset_request_bound_function ts MaxArrivalsRBF
Proof .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job
valid_taskset_arrival_curve ts MaxArr ->
valid_taskset_request_bound_function ts MaxArrivalsRBF
move => VALID tsk IN.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job VALID : valid_taskset_arrival_curve ts MaxArr tsk : Task IN : tsk \in ts
valid_request_bound_function (MaxArrivalsRBF tsk)
specialize (VALID tsk IN).Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job tsk : Task VALID : valid_arrival_curve (MaxArr tsk) IN : tsk \in ts
valid_request_bound_function (MaxArrivalsRBF tsk)
by apply valid_arrival_curve_to_max_rbf.
Qed .
(** ... and in the lower-bounding case. *)
Corollary valid_taskset_arrival_curve_to_min_rbf :
valid_taskset_arrival_curve ts MinArr ->
valid_taskset_request_bound_function ts MinArrivalsRBF.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job
valid_taskset_arrival_curve ts MinArr ->
valid_taskset_request_bound_function ts MinArrivalsRBF
Proof .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job
valid_taskset_arrival_curve ts MinArr ->
valid_taskset_request_bound_function ts MinArrivalsRBF
move => VALID tsk IN.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job VALID : valid_taskset_arrival_curve ts MinArr tsk : Task IN : tsk \in ts
valid_request_bound_function (MinArrivalsRBF tsk)
specialize (VALID tsk IN).Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job tsk : Task VALID : valid_arrival_curve (MinArr tsk) IN : tsk \in ts
valid_request_bound_function (MinArrivalsRBF tsk)
by apply valid_arrival_curve_to_min_rbf.
Qed .
(** 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 :
jobs_have_valid_job_costs ->
taskset_respects_max_arrivals arr_seq ts ->
taskset_respects_max_request_bound arr_seq ts.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job
jobs_have_valid_job_costs ->
taskset_respects_max_arrivals arr_seq ts ->
taskset_respects_max_request_bound arr_seq ts
Proof .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job
jobs_have_valid_job_costs ->
taskset_respects_max_arrivals arr_seq ts ->
taskset_respects_max_request_bound arr_seq ts
move => TASK_COST SET_RESPECTS tsk IN.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_job_costs SET_RESPECTS : taskset_respects_max_arrivals arr_seq
ts tsk : Task IN : tsk \in ts
respects_max_request_bound arr_seq tsk
(max_request_bound tsk)
by apply respects_arrival_curve_to_max_rbf, SET_RESPECTS.
Qed .
(** ...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.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job
jobs_have_valid_min_job_costs ->
taskset_respects_min_arrivals arr_seq ts ->
taskset_respects_min_request_bound arr_seq ts
Proof .Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job
jobs_have_valid_min_job_costs ->
taskset_respects_min_arrivals arr_seq ts ->
taskset_respects_min_request_bound arr_seq ts
move => TASK_COST SET_RESPECTS tsk IN.Task : TaskType H : TaskCost Task H0 : TaskMinCost Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job MaxArr : MaxArrivals Task MinArr : MinArrivals Task ts : TaskSet Task arr_seq : arrival_sequence Job TASK_COST : jobs_have_valid_min_job_costs SET_RESPECTS : taskset_respects_min_arrivals arr_seq
ts tsk : Task IN : tsk \in ts
respects_min_request_bound arr_seq tsk
(min_request_bound tsk)
by apply respects_arrival_curve_to_min_rbf, SET_RESPECTS.
Qed .
End TaskSet .
End Facts .
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.