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.model.task.absolute_deadline.[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.analysis.definitions.demand_bound_function.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.workload.
(** * Facts about the Demand Bound Function (DBF) *)
(** In this file we establish some properties of DBFs. *)
Section ProofDemandBoundDefinition .
(** Consider any type of task with relative deadlines and any type of jobs associated with such tasks. *)
Context {Task : TaskType} `{TaskDeadline Task}
{Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
(** Consider a valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** First, we establish a relation between a task's arrivals in a given interval and
those arrivals that also have a deadline contained within the given interval. *)
Lemma task_arrivals_with_deadline_within_eq :
forall (tsk : Task) (t : instant) (delta : duration),
task_arrivals_with_deadline_within arr_seq tsk t (t + delta)
= task_arrivals_between arr_seq tsk t (t + (delta - (task_deadline tsk -1 ))).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall (tsk : Task) (t : instant) (delta : duration),
task_arrivals_with_deadline_within arr_seq tsk t
(t + delta) =
task_arrivals_between arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 )))
Proof .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall (tsk : Task) (t : instant) (delta : duration),
task_arrivals_with_deadline_within arr_seq tsk t
(t + delta) =
task_arrivals_between arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 )))
move => tsk t delta.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
task_arrivals_with_deadline_within arr_seq tsk t
(t + delta) =
task_arrivals_between arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 )))
rewrite /task_arrivals_with_deadline_within/job_deadline
/job_deadline_from_task_deadline/task_arrivals_between.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
[seq j <- arrivals_between arr_seq t (t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] =
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
| job_of_task tsk j]
rewrite (@arrivals_between_cat _ _ _ (t + (delta - (task_deadline tsk - 1 )))); try lia .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))) ++
arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] =
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
| job_of_task tsk j]
rewrite filter_cat.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] ++
[seq j <- arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] =
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
| job_of_task tsk j]
rewrite (@eq_in_filter _ _ (fun j => job_of_task tsk j)).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] ++
[seq j <- arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] =
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
| job_of_task tsk j]
{ Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] ++
[seq j <- arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] =
[seq j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
| job_of_task tsk j]
set nilS := [seq j <- arrivals_between arr_seq t (t + (delta - (task_deadline tsk - 1 ))) | job_of_task tsk j].Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job
nilS ++
[seq j <- arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] = nilS
rewrite -[in RHS](@cats0 _ nilS).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job
nilS ++
[seq j <- arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] = nilS ++ [::]
apply /eqP; rewrite eqseq_cat => //=.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job
(nilS == nilS) &&
([seq j <- arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] == [::])
apply /andP; split => //=.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job
[seq j <- arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
| job_of_task tsk j
& job_arrival j + task_deadline (job_task j) <=
t + delta] == [::]
rewrite (@eq_in_filter _ _ pred0);
first by rewrite filter_pred0.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job
{in arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta),
(fun j : Job =>
job_of_task tsk j &&
(job_arrival j + task_deadline (job_task j) <=
t + delta)) =1 pred0}
move => j IN.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job j : Job IN : j
\in arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
job_of_task tsk j &&
(job_arrival j + task_deadline (job_task j) <=
t + delta) = pred0 j
have [/eqP ->|] := boolP (job_of_task tsk j) => //=.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job j : Job IN : j
\in arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta)
(job_arrival j + task_deadline tsk <= t + delta) =
false
have GEQ: job_arrival j >= t + (delta - (task_deadline tsk - 1 ))
by apply : job_arrival_between_ge.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job j : Job IN : j
\in arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta) GEQ : t + (delta - (task_deadline tsk - 1 )) <=
job_arrival j
(job_arrival j + task_deadline tsk <= t + delta) =
false
have LT := (arrivals_between_nonempty _ _ _ _ IN).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration nilS := [seq j <- arrivals_between arr_seq t
(t +
(delta - (task_deadline tsk - 1 )))
| job_of_task tsk j] : seq Job j : Job IN : j
\in arrivals_between arr_seq
(t + (delta - (task_deadline tsk - 1 )))
(t + delta) GEQ : t + (delta - (task_deadline tsk - 1 )) <=
job_arrival j LT : t + (delta - (task_deadline tsk - 1 )) < t + delta
(job_arrival j + task_deadline tsk <= t + delta) =
false
by lia . } Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
{in arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))),
(fun j : Job =>
job_of_task tsk j &&
(job_arrival j + task_deadline (job_task j) <=
t + delta)) =1 [eta job_of_task tsk]}
{ Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
{in arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))),
(fun j : Job =>
job_of_task tsk j &&
(job_arrival j + task_deadline (job_task j) <=
t + delta)) =1 [eta job_of_task tsk]}
move => j IN.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration j : Job IN : j
\in arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
job_of_task tsk j &&
(job_arrival j + task_deadline (job_task j) <=
t + delta) = job_of_task tsk j
have [/eqP ->|] := boolP (job_of_task tsk j) => //=.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration j : Job IN : j
\in arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
(job_arrival j + task_deadline tsk <= t + delta) =
true
have -> : (job_arrival j + task_deadline tsk <= t + delta) => //.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration j : Job IN : j
\in arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))
job_arrival j + task_deadline tsk <= t + delta
have LT := (arrivals_between_nonempty _ _ _ _ IN).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration j : Job IN : j
\in arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))) LT : t < t + (delta - (task_deadline tsk - 1 ))
job_arrival j + task_deadline tsk <= t + delta
have LTj: job_arrival j < t + (delta - (task_deadline tsk - 1 ))
by apply : job_arrival_between_lt.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration j : Job IN : j
\in arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))) LT : t < t + (delta - (task_deadline tsk - 1 )) LTj : job_arrival j <
t + (delta - (task_deadline tsk - 1 ))
job_arrival j + task_deadline tsk <= t + delta
by lia . }
Qed .
(** As a corollary, we also show a much more useful result that arises when we count these jobs. *)
Corollary num_task_arrivals_with_deadline_within_eq :
forall (tsk : Task) (t : instant) (delta : duration),
number_of_task_arrivals_with_deadline_within arr_seq tsk t (t + delta)
= number_of_task_arrivals arr_seq tsk t (t + (delta - (task_deadline tsk - 1 ))).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall (tsk : Task) (t : instant) (delta : duration),
number_of_task_arrivals_with_deadline_within arr_seq
tsk t (t + delta) =
number_of_task_arrivals arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 )))
Proof .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq
forall (tsk : Task) (t : instant) (delta : duration),
number_of_task_arrivals_with_deadline_within arr_seq
tsk t (t + delta) =
number_of_task_arrivals arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 )))
move => tsk t delta.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
number_of_task_arrivals_with_deadline_within arr_seq
tsk t (t + delta) =
number_of_task_arrivals arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 )))
rewrite /number_of_task_arrivals_with_deadline_within
/number_of_task_arrivals.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task t : instant delta : duration
size
(task_arrivals_with_deadline_within arr_seq tsk t
(t + delta)) =
size
(task_arrivals_between arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 ))))
by rewrite task_arrivals_with_deadline_within_eq.
Qed .
(** In the following, assume we are given a valid WCET bound for each task. *)
Context `{TaskCost Task} `{JobCost Job}.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** A task's _demand_ in a given interval is the sum of the execution costs (i.e., the workload) of the task's jobs
that both arrive in the interval and have a deadline within it. *)
Definition task_demand_within (tsk : Task) (t1 t2 : instant) :=
let
causing_demand (j : Job) := (job_deadline j <= t2) && (job_of_task tsk j)
in
workload_of_jobs causing_demand (arrivals_between arr_seq t1 t2).
(** Consider a task set [ts]. *)
Variable ts : seq Task.
(** Let [max_arrivals] be any arrival curve. *)
Context `{MaxArrivals Task}.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
(** The task's processor demand [task_demand_within] is upper-bounded by the task's DBF [task_demand_bound_function]. *)
Lemma task_demand_within_le_task_dbf :
forall (tsk : Task) t delta ,
tsk \in ts ->
task_demand_within tsk t (t + delta) <= task_demand_bound_function tsk delta.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts
forall (tsk : Task) (t : instant) (delta : nat),
tsk \in ts ->
task_demand_within tsk t (t + delta) <=
task_demand_bound_function tsk delta
Proof .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts
forall (tsk : Task) (t : instant) (delta : nat),
tsk \in ts ->
task_demand_within tsk t (t + delta) <=
task_demand_bound_function tsk delta
move => tsk t delta IN0.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
task_demand_within tsk t (t + delta) <=
task_demand_bound_function tsk delta
have ->: task_demand_within tsk t (t + delta)
= task_workload_between arr_seq tsk t (t + (delta - (task_deadline tsk - 1 ))).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
task_demand_within tsk t (t + delta) =
task_workload_between arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 )))
{ Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
task_demand_within tsk t (t + delta) =
task_workload_between arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 )))
rewrite /task_demand_within/task_workload_between/task_workload/workload_of_jobs.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
\sum_(j <- arrivals_between arr_seq t (t + delta) |
(job_deadline j <= t + delta) && job_of_task tsk j)
job_cost j =
\sum_(j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))) |
job_of_task tsk j) job_cost j
under eq_bigl do rewrite andbC.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
\sum_(i <- arrivals_between arr_seq t (t + delta) |
job_of_task tsk i && (job_deadline i <= t + delta))
job_cost i =
\sum_(j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))) |
job_of_task tsk j) job_cost j
rewrite -big_filter.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
\sum_(i <- [seq i <- arrivals_between arr_seq t
(t + delta)
| job_of_task tsk i
& job_deadline i <= t + delta])
job_cost i =
\sum_(j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))) |
job_of_task tsk j) job_cost j
move : (task_arrivals_with_deadline_within_eq tsk t delta).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
task_arrivals_with_deadline_within arr_seq tsk t
(t + delta) =
task_arrivals_between arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 ))) ->
\sum_(i <- [seq i <- arrivals_between arr_seq t
(t + delta)
| job_of_task tsk i
& job_deadline i <= t + delta])
job_cost i =
\sum_(j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))) |
job_of_task tsk j) job_cost j
rewrite /task_arrivals_with_deadline_within/task_arrivals_between => ->.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
\sum_(i <- [seq j <- arrivals_between arr_seq t
(t +
(delta -
(task_deadline tsk - 1 )))
| job_of_task tsk j]) job_cost i =
\sum_(j <- arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 ))) |
job_of_task tsk j) job_cost j
by rewrite big_filter. } Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
task_workload_between arr_seq tsk t
(t + (delta - (task_deadline tsk - 1 ))) <=
task_demand_bound_function tsk delta
rewrite /task_demand_bound_function/task_workload_between/task_workload.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t
(t + (delta - (task_deadline tsk - 1 )))) <=
task_request_bound_function tsk
(delta - (task_deadline tsk - 1 ))
by apply workload_le_rbf.
Qed .
(** We also prove that [task_demand_within] is less than shifted RBF. *)
Corollary task_demand_within_le_task_rbf_shifted :
forall (tsk : Task) t delta ,
tsk \in ts ->
task_demand_within tsk t (t + delta) <= task_request_bound_function tsk (delta - (task_deadline tsk - 1 )).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts
forall (tsk : Task) (t : instant) (delta : nat),
tsk \in ts ->
task_demand_within tsk t (t + delta) <=
task_request_bound_function tsk
(delta - (task_deadline tsk - 1 ))
Proof .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts
forall (tsk : Task) (t : instant) (delta : nat),
tsk \in ts ->
task_demand_within tsk t (t + delta) <=
task_request_bound_function tsk
(delta - (task_deadline tsk - 1 ))
move => tsk t delta IN0.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts tsk : Task t : instant delta : nat IN0 : tsk \in ts
task_demand_within tsk t (t + delta) <=
task_request_bound_function tsk
(delta - (task_deadline tsk - 1 ))
by apply task_demand_within_le_task_dbf.
Qed .
(** Next, we define the total workload of all jobs that arrives in a given interval that also have a
deadline within the interval. *)
Definition total_demand_within (t1 t2 : instant) :=
let
causing_demand (j : Job) := job_deadline j <= t2
in
workload_of_jobs causing_demand (arrivals_between arr_seq t1 t2).
(** Assume that all jobs come from the task set [ts]. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** We relate [total_demand_within] to the sum of each task's demand [task_demand_within]. *)
Lemma total_demand_within_le_sum_over_partitions :
forall (t : instant) (delta : duration),
total_demand_within t (t + delta) <= \sum_(tsk <- ts) task_demand_within tsk t (t + delta).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall (t : instant) (delta : duration),
total_demand_within t (t + delta) <=
\sum_(tsk <- ts) task_demand_within tsk t (t + delta)
Proof .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall (t : instant) (delta : duration),
total_demand_within t (t + delta) <=
\sum_(tsk <- ts) task_demand_within tsk t (t + delta)
move => t delta.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration
total_demand_within t (t + delta) <=
\sum_(tsk <- ts) task_demand_within tsk t (t + delta)
rewrite /total_demand_within/task_demand_within.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration
workload_of_jobs
(fun j : Job => job_deadline j <= t + delta)
(arrivals_between arr_seq t (t + delta)) <=
\sum_(tsk <- ts)
workload_of_jobs
(fun j : Job =>
(job_deadline j <= t + delta) &&
job_of_task tsk j)
(arrivals_between arr_seq t (t + delta))
rewrite /workload_of_jobs.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration
\sum_(j <- arrivals_between arr_seq t (t + delta) |
job_deadline j <= t + delta) job_cost j <=
\sum_(tsk <- ts)
\sum_(j <- arrivals_between arr_seq t (t + delta) |
(job_deadline j <= t + delta) && job_of_task tsk j)
job_cost j
apply sum_over_partitions_le.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration
forall x : Job,
x \in arrivals_between arr_seq t (t + delta) ->
job_deadline x <= t + delta -> job_task x \in ts
move => j' IN ?.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration j' : Job IN : j' \in arrivals_between arr_seq t (t + delta) _Hyp_ : job_deadline j' <= t + delta
job_task j' \in ts
apply H_all_jobs_from_taskset.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration j' : Job IN : j' \in arrivals_between arr_seq t (t + delta) _Hyp_ : job_deadline j' <= t + delta
arrives_in arr_seq j'
by apply in_arrivals_implies_arrived in IN.
Qed .
(** Here we prove a stronger version of the above lemma by assuming that the task set [ts] is indeed a set. *)
Lemma total_demand_within_partitioned_by_tasks :
forall (t : instant) (delta : duration),
uniq ts ->
total_demand_within t (t + delta) = \sum_(tsk <- ts) task_demand_within tsk t (t + delta).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall (t : instant) (delta : duration),
uniq ts ->
total_demand_within t (t + delta) =
\sum_(tsk <- ts) task_demand_within tsk t (t + delta)
Proof .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall (t : instant) (delta : duration),
uniq ts ->
total_demand_within t (t + delta) =
\sum_(tsk <- ts) task_demand_within tsk t (t + delta)
move => t delta UniqTS.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration UniqTS : uniq ts
total_demand_within t (t + delta) =
\sum_(tsk <- ts) task_demand_within tsk t (t + delta)
rewrite /total_demand_within/task_demand_within.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration UniqTS : uniq ts
workload_of_jobs
(fun j : Job => job_deadline j <= t + delta)
(arrivals_between arr_seq t (t + delta)) =
\sum_(tsk <- ts)
workload_of_jobs
(fun j : Job =>
(job_deadline j <= t + delta) &&
job_of_task tsk j)
(arrivals_between arr_seq t (t + delta))
rewrite /job_of_task.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration UniqTS : uniq ts
workload_of_jobs
(fun j : Job => job_deadline j <= t + delta)
(arrivals_between arr_seq t (t + delta)) =
\sum_(tsk <- ts)
workload_of_jobs
(fun j : Job =>
(job_deadline j <= t + delta) &&
(job_task j == tsk))
(arrivals_between arr_seq t (t + delta))
apply workload_of_jobs_partitioned_by_tasks => //=.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration UniqTS : uniq ts
{in arrivals_between arr_seq t (t + delta),
forall j : Job, job_task j \in ts}
move => j' IN.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration UniqTS : uniq ts j' : Job IN : j' \in arrivals_between arr_seq t (t + delta)
job_task j' \in ts
apply H_all_jobs_from_taskset.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration UniqTS : uniq ts j' : Job IN : j' \in arrivals_between arr_seq t (t + delta)
arrives_in arr_seq j'
by apply in_arrivals_implies_arrived in IN.
Qed .
(** Finally we establish that [total_demand_within] is bounded by [total_demand_bound_function]. *)
Lemma total_demand_within_le_total_dbf :
forall (t : instant) (delta : duration),
total_demand_within t (t + delta) <= total_demand_bound_function ts delta.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall (t : instant) (delta : duration),
total_demand_within t (t + delta) <=
total_demand_bound_function ts delta
Proof .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall (t : instant) (delta : duration),
total_demand_within t (t + delta) <=
total_demand_bound_function ts delta
move => t delta.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration
total_demand_within t (t + delta) <=
total_demand_bound_function ts delta
apply (@leq_trans (\sum_(tsk <- ts) task_demand_within tsk t (t + delta)));
first by apply total_demand_within_le_sum_over_partitions.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration
\sum_(tsk <- ts) task_demand_within tsk t (t + delta) <=
total_demand_bound_function ts delta
rewrite /total_demand_bound_function.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration
\sum_(tsk <- ts) task_demand_within tsk t (t + delta) <=
\sum_(tsk <- ts) task_demand_bound_function tsk delta
apply leq_sum_seq => tsk' tsk_IN P_tsk.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t : instant delta : duration tsk' : Task tsk_IN : tsk' \in ts P_tsk : true
task_demand_within tsk' t (t + delta) <=
task_demand_bound_function tsk' delta
by apply task_demand_within_le_task_dbf.
Qed .
(** As a corollary, we also note that [total_demand_within] is less than
the sum of each task's shifted RBF. *)
Corollary total_demand_within_le_sum_task_rbf_shifted :
forall (t : instant ) (delta : instant),
total_demand_within t (t + delta)
<= \sum_(tsk <- ts) task_request_bound_function tsk (delta - (task_deadline tsk - 1 )).Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall t delta : instant,
total_demand_within t (t + delta) <=
\sum_(tsk <- ts)
task_request_bound_function tsk
(delta - (task_deadline tsk - 1 ))
Proof .Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall t delta : instant,
total_demand_within t (t + delta) <=
\sum_(tsk <- ts)
task_request_bound_function tsk
(delta - (task_deadline tsk - 1 ))
move => t delta.Task : TaskType H : TaskDeadline Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H2 : TaskCost Task H3 : JobCost Job H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t, delta : instant
total_demand_within t (t + delta) <=
\sum_(tsk <- ts)
task_request_bound_function tsk
(delta - (task_deadline tsk - 1 ))
by apply total_demand_within_le_total_dbf.
Qed .
End ProofDemandBoundDefinition .