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.analysis.facts.model.workload.[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.facts.model.arrival_curves.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.util.tactics.
Require Export prosa.analysis.definitions.workload.bounded.
(** * Facts about Request-Bound Functions (RBFs) *)
(** In this file, we prove some lemmas about RBFs. *)
(** ** RBF is a Bound on Workload *)
Section ProofRequestBoundFunction .
(** Consider any type of tasks characterized by WCETs and arrival curves ... *)
Context {Task : TaskType}.
Context `{TaskCost Task} `{MaxArrivals Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any valid arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any schedule corresponding to this arrival sequence. *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** In this section, we establish that a task's RBF is indeed an upper bound
on the task's workload. *)
Section RBF .
(** Consider a given task [tsk]. *)
Variable tsk : Task.
(** First, as a stepping stone, we observe that any sequence of jobs of the
task jointly satisfy the task's WCET. *)
Lemma task_workload_between_bounded :
forall t1 t2 ,
task_workload_between arr_seq tsk t1 t2
<= task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task
forall t1 t2 : instant,
task_workload_between arr_seq tsk t1 t2 <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 t2
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task
forall t1 t2 : instant,
task_workload_between arr_seq tsk t1 t2 <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 t2
move => t Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task t, Δ : instant
task_workload_between arr_seq tsk t Δ <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t Δ
rewrite /number_of_task_arrivals/task_arrivals_between.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task t, Δ : instant
task_workload_between arr_seq tsk t Δ <=
task_cost tsk *
size
[seq j <- arrivals_between arr_seq t Δ
| job_of_task tsk j]
rewrite /task_workload_between/task_workload/workload_of_jobs -big_filter.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task t, Δ : instant
\sum_(i <- [seq x <- arrivals_between arr_seq t Δ
| job_of_task tsk x]) job_cost i <=
task_cost tsk *
size
[seq j <- arrivals_between arr_seq t Δ
| job_of_task tsk j]
apply : sum_job_costs_bounded.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task t, Δ : instant
{in [seq x <- arrivals_between arr_seq t Δ
| job_of_task tsk x],
forall j : Job,
job_of_task tsk j && valid_job_cost j}
move => j /[! mem_filter ] /andP [TSK IN]; apply /andP; split => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task t, Δ : instant j : Job TSK : job_of_task tsk j IN : j \in arrivals_between arr_seq t Δ
valid_job_cost j
by apply /H_valid_job_cost/in_arrivals_implies_arrived.
Qed .
(** Next, suppose that task [tsk] respects its arrival curve [max_arrivals]. *)
Hypothesis H_tsk_arrivals_bounded : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
(** From this assumption, we establish the RBF spec: In any interval of any
length, the RBF upper-bounds the task's actual workload. *)
Lemma rbf_spec :
forall t Δ ,
task_workload_between arr_seq tsk t (t + Δ)
<= task_request_bound_function tsk Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk)
forall (t : instant) (Δ : nat),
task_workload_between arr_seq tsk t (t + Δ) <=
task_request_bound_function tsk Δ
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk)
forall (t : instant) (Δ : nat),
task_workload_between arr_seq tsk t (t + Δ) <=
task_request_bound_function tsk Δ
move => t Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) t : instant Δ : nat
task_workload_between arr_seq tsk t (t + Δ) <=
task_request_bound_function tsk Δ
apply : leq_trans; first by apply : task_workload_between_bounded.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) t : instant Δ : nat
task_cost tsk *
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
task_request_bound_function tsk Δ
rewrite /task_request_bound_function.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) t : instant Δ : nat
task_cost tsk *
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
task_cost tsk * max_arrivals tsk Δ
rewrite leq_mul2l; apply /orP; right .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) t : instant Δ : nat
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
max_arrivals tsk Δ
rewrite -{2 }[Δ](addKn t).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) t : instant Δ : nat
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
max_arrivals tsk (t + Δ - t)
by apply /H_tsk_arrivals_bounded/leq_addr.
Qed .
End RBF .
(** In this section, we prove a trivial corollary stating that the RBF still
upper-bounds the workload when considering only a subset of a task's jobs
(namely those satisfying a filter predicate). *)
Section SubsetOfJobs .
(** Consider any predicate [P] on jobs. *)
Variable P : pred Job.
(** Consider any task [tsk] that respects its arrival curve [max_arrivals] *)
Variable tsk : Task.
Hypothesis H_tsk_arrivals_bounded : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
(** Assume that all jobs that satisfy [P] come from task [tsk]. *)
Hypothesis H_jobs_of_tsk : forall j , P j -> job_of_task tsk j.
(** Trivially, the workload of jobs from task [tsk] that satisfy the
predicate [P] is bounded by the task's RBF. *)
Corollary rbf_spec' :
forall t Δ ,
workload_of_jobs P
(arrivals_between arr_seq t (t + Δ))
<= task_request_bound_function tsk Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq P : pred Job tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) H_jobs_of_tsk : forall j : Job,
P j -> job_of_task tsk j
forall (t : instant) (Δ : nat),
workload_of_jobs P
(arrivals_between arr_seq t (t + Δ)) <=
task_request_bound_function tsk Δ
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq P : pred Job tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) H_jobs_of_tsk : forall j : Job,
P j -> job_of_task tsk j
forall (t : instant) (Δ : nat),
workload_of_jobs P
(arrivals_between arr_seq t (t + Δ)) <=
task_request_bound_function tsk Δ
move => t Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq P : pred Job tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) H_jobs_of_tsk : forall j : Job,
P j -> job_of_task tsk jt : instant Δ : nat
workload_of_jobs P
(arrivals_between arr_seq t (t + Δ)) <=
task_request_bound_function tsk Δ
apply : leq_trans; last by apply : rbf_spec.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq P : pred Job tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) H_jobs_of_tsk : forall j : Job,
P j -> job_of_task tsk jt : instant Δ : nat
workload_of_jobs P
(arrivals_between arr_seq t (t + Δ)) <=
task_workload_between arr_seq tsk t (t + Δ)
rewrite /task_workload_between/task_workload/workload_of_jobs.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq P : pred Job tsk : Task H_tsk_arrivals_bounded : respects_max_arrivals arr_seq
tsk (max_arrivals tsk) H_jobs_of_tsk : forall j : Job,
P j -> job_of_task tsk jt : instant Δ : nat
\sum_(j <- arrivals_between arr_seq t (t + Δ) | P j)
job_cost j <=
\sum_(j <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk j)
job_cost j
by apply leq_sum_seq_pred.
Qed .
End SubsetOfJobs .
(** Now, consider a task set [ts] ... *)
Variable ts : seq Task.
(** ... and assume that all jobs come from the task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** Assume that all tasks in the task set respect [max_arrivals]. *)
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
(** Next, we prove that total workload is upper-bounded by the total RBF. *)
Lemma total_workload_le_total_rbf :
forall t Δ ,
total_workload_between arr_seq t (t + Δ) <= total_request_bound_function ts Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts
forall (t : instant) (Δ : nat),
total_workload_between arr_seq t (t + Δ) <=
total_request_bound_function ts Δ
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts
forall (t : instant) (Δ : nat),
total_workload_between arr_seq t (t + Δ) <=
total_request_bound_function ts Δ
move => t Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : nat
total_workload_between arr_seq t (t + Δ) <=
total_request_bound_function ts Δ
apply leq_trans with (n := \sum_(tsk <- ts) task_workload_between arr_seq tsk t (t + Δ)).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : nat
total_workload_between arr_seq t (t + Δ) <=
\sum_(tsk <- ts)
task_workload_between arr_seq tsk t (t + Δ)
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : nat
total_workload_between arr_seq t (t + Δ) <=
\sum_(tsk <- ts)
task_workload_between arr_seq tsk t (t + Δ)
apply : workload_of_jobs_le_sum_over_partitions => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : nat
{in arrivals_between arr_seq t (t + Δ),
forall j : Job, job_task j \in ts}
move => j IN; by apply in_arrivals_implies_arrived in IN. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : nat
\sum_(tsk <- ts)
task_workload_between arr_seq tsk t (t + Δ) <=
total_request_bound_function ts Δ
rewrite /total_request_bound_function.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : nat
\sum_(tsk <- ts)
task_workload_between arr_seq tsk t (t + Δ) <=
\sum_(tsk <- ts) task_request_bound_function tsk Δ
apply leq_sum_seq => tsk' tsk_IN ?.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : nat tsk' : Task tsk_IN : tsk' \in ts _Hyp_ : true
task_workload_between arr_seq tsk' t (t + Δ) <=
task_request_bound_function tsk' Δ
by apply rbf_spec.
Qed .
(** In this section, we prove a more general result about the workload of
arbitrary sets of jobs. *)
Section SumRBF .
(** Consider two predicates, one on jobs and one on tasks. *)
Variable pred1 : pred Job.
Variable pred2 : pred Task.
(** Assume that for all jobs satisfying [pred1], the task it belongs to
satisfies [pred2]. *)
Hypothesis H_also_satisfied : forall j , pred1 j -> pred2 (job_task j).
(** We prove that the workload of all jobs satisfying predicate [pred1] is
bounded by the sum of task RBFs over tasks that satisfy the predicate
[pred2]. *)
Lemma workload_of_jobs_bounded :
forall t Δ ,
workload_of_jobs (pred1) (arrivals_between arr_seq t (t + Δ))
<= \sum_(tsk' <- ts | pred2 tsk') task_request_bound_function tsk' Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)
forall (t : instant) (Δ : nat),
workload_of_jobs pred1
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(tsk' <- ts | pred2 tsk')
task_request_bound_function tsk' Δ
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)
forall (t : instant) (Δ : nat),
workload_of_jobs pred1
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(tsk' <- ts | pred2 tsk')
task_request_bound_function tsk' Δ
move => t Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
workload_of_jobs pred1
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(tsk' <- ts | pred2 tsk')
task_request_bound_function tsk' Δ
rewrite /workload_of_jobs.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
\sum_(j <- arrivals_between arr_seq t (t + Δ) | pred1
j)
job_cost j <=
\sum_(tsk' <- ts | pred2 tsk')
task_request_bound_function tsk' Δ
apply (@leq_trans (\sum_(tsk <- ts | pred2 tsk)
(\sum_(j <- arrivals_between arr_seq t (t + Δ) | (job_task j == tsk) && (pred1 j))
job_cost j))).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
\sum_(j <- arrivals_between arr_seq t (t + Δ) | pred1
j)
job_cost j <=
\sum_(tsk <- ts | pred2 tsk)
\sum_(j <- arrivals_between arr_seq t (t + Δ) |
(job_task j == tsk) && pred1 j) job_cost j
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
\sum_(j <- arrivals_between arr_seq t (t + Δ) | pred1
j)
job_cost j <=
\sum_(tsk <- ts | pred2 tsk)
\sum_(j <- arrivals_between arr_seq t (t + Δ) |
(job_task j == tsk) && pred1 j) job_cost j
rewrite (exchange_big_dep pred1) //=;
last by move => ? ? ? /andP[].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
\sum_(j <- arrivals_between arr_seq t (t + Δ) | pred1
j)
job_cost j <=
\sum_(j <- arrivals_between arr_seq t (t + Δ) | pred1
j)
\sum_(i <- ts | [&& pred2 i, job_task j == i
& pred1 j]) job_cost j
rewrite big_seq_cond [X in _ <= X]big_seq_cond.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
pred1
i)
job_cost i <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
pred1
i)
\sum_(i0 <- ts | [&& pred2 i0, job_task i == i0
& pred1 i]) job_cost i
rewrite leq_sum //= => j' /andP [IN' Pj'].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat j' : Job IN' : j' \in arrivals_between arr_seq t (t + Δ) Pj' : pred1 j'
job_cost j' <=
\sum_(i <- ts | [&& pred2 i, job_task j' == i
& pred1 j']) job_cost j'
rewrite Pj'.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat j' : Job IN' : j' \in arrivals_between arr_seq t (t + Δ) Pj' : pred1 j'
job_cost j' <=
\sum_(i <- ts | [&& pred2 i, job_task j' == i & true])
job_cost j'
under eq_bigl do [rewrite andbA; rewrite andbT].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat j' : Job IN' : j' \in arrivals_between arr_seq t (t + Δ) Pj' : pred1 j'
job_cost j' <=
\sum_(i <- ts | pred2 i && (job_task j' == i))
job_cost j'
rewrite (big_rem (job_task j')) //=;
last by apply /H_all_jobs_from_taskset/in_arrivals_implies_arrived.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat j' : Job IN' : j' \in arrivals_between arr_seq t (t + Δ) Pj' : pred1 j'
job_cost j' <=
(if
pred2 (job_task j') && (job_task j' == job_task j')
then job_cost j'
else 0 ) +
\sum_(y <- rem (T:=Task) (job_task j') ts | pred2 y &&
(job_task
j' == y))
job_cost j'
rewrite (H_also_satisfied _ Pj') eq_refl //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat j' : Job IN' : j' \in arrivals_between arr_seq t (t + Δ) Pj' : pred1 j'
job_cost j' <=
job_cost j' +
\sum_(y <- rem (T:=Task) (job_task j') ts | pred2 y &&
(job_task
j' == y))
job_cost j'
by apply leq_addr. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
\sum_(tsk <- ts | pred2 tsk)
\sum_(j <- arrivals_between arr_seq t (t + Δ) |
(job_task j == tsk) && pred1 j) job_cost j <=
\sum_(tsk' <- ts | pred2 tsk')
task_request_bound_function tsk' Δ
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
\sum_(tsk <- ts | pred2 tsk)
\sum_(j <- arrivals_between arr_seq t (t + Δ) |
(job_task j == tsk) && pred1 j) job_cost j <=
\sum_(tsk' <- ts | pred2 tsk')
task_request_bound_function tsk' Δ
rewrite leq_sum_seq //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat
forall i : Task,
i \in ts ->
pred2 i ->
\sum_(j <- arrivals_between arr_seq t (t + Δ) | (job_task
j ==
i) &&
pred1
j)
job_cost j <= task_request_bound_function i Δ
move => tsk' tsk_in_ts' P_tsk'.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat tsk' : Task tsk_in_ts' : tsk' \in ts P_tsk' : pred2 tsk'
\sum_(j <- arrivals_between arr_seq t (t + Δ) | (job_task
j ==
tsk') &&
pred1
j)
job_cost j <= task_request_bound_function tsk' Δ
apply (@leq_trans (\sum_(j <- arrivals_between arr_seq t (t + Δ)
| job_task j == tsk') job_cost j)).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat tsk' : Task tsk_in_ts' : tsk' \in ts P_tsk' : pred2 tsk'
\sum_(j <- arrivals_between arr_seq t (t + Δ) | (job_task
j ==
tsk') &&
pred1
j)
job_cost j <=
\sum_(j <- arrivals_between arr_seq t (t + Δ) | job_task
j ==
tsk')
job_cost j
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat tsk' : Task tsk_in_ts' : tsk' \in ts P_tsk' : pred2 tsk'
\sum_(j <- arrivals_between arr_seq t (t + Δ) | (job_task
j ==
tsk') &&
pred1
j)
job_cost j <=
\sum_(j <- arrivals_between arr_seq t (t + Δ) | job_task
j ==
tsk')
job_cost j
rewrite leq_sum_seq_pred //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat tsk' : Task tsk_in_ts' : tsk' \in ts P_tsk' : pred2 tsk'
forall i : Job,
i \in arrivals_between arr_seq t (t + Δ) ->
(job_task i == tsk') && pred1 i -> job_task i == tsk'
by move => ? ? /andP[].
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts pred1 : pred Job pred2 : pred Task H_also_satisfied : forall j : Job,
pred1 j -> pred2 (job_task j)t : instant Δ : nat tsk' : Task tsk_in_ts' : tsk' \in ts P_tsk' : pred2 tsk'
\sum_(j <- arrivals_between arr_seq t (t + Δ) | job_task
j ==
tsk')
job_cost j <= task_request_bound_function tsk' Δ
exact : rbf_spec. }
Qed .
End SumRBF .
(** Next, we establish bounds specific to fixed-priority scheduling. *)
Section FP .
(** Consider an arbitrary fixed-priority policy ... *)
Context {FP : FP_policy Task}.
(** ... and any given task. *)
Variable tsk : Task.
(** The [athep_workload_is_bounded] predicate used below allows the workload
bound to depend on two arguments: the relative offset [A] (w.r.t. the
beginning of the corresponding busy interval) of a job to be analyzed
and the length of an interval [Δ]. In the case of FP scheduling, the
relative offset ([A]) does not play a role and is therefore ignored.
Let's abbreviate [total_ohep_request_bound_function_FP] such that the
[A] argument is ignored. *)
Let total_ohep_rbf (_A Δ : duration) :=
total_ohep_request_bound_function_FP ts tsk Δ.
(** We next prove that the higher-or-equal-priority workload of tasks
different from [tsk] is bounded by [total_ohep_rbf]. *)
Lemma athep_workload_le_total_ohep_rbf :
athep_workload_is_bounded arr_seq sched tsk total_ohep_rbf.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat
athep_workload_is_bounded arr_seq sched tsk
total_ohep_rbf
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat
athep_workload_is_bounded arr_seq sched tsk
total_ohep_rbf
move => j t1 Δ POS TSK _.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
total_ohep_rbf (job_arrival j - t1) Δ
rewrite /workload_of_jobs /total_ohep_request_bound_function_FP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
another_task_hep_job j0 j) job_cost j0 <=
total_ohep_rbf (job_arrival j - t1) Δ
rewrite /another_task_hep_job /hep_job /FP_to_JLFP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
hep_task (job_task j0) (job_task j) &&
(job_task j0 != job_task j)) job_cost j0 <=
total_ohep_rbf (job_arrival j - t1) Δ
apply : workload_of_jobs_bounded.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j
forall j0 : Job,
hep_task (job_task j0) (job_task j) &&
(job_task j0 != job_task j) ->
hep_task (job_task j0) tsk && (job_task j0 != tsk)
by move : TSK => /eqP ->.
Qed .
(** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_job_of_tsk : job_of_task tsk j.
(** Using lemma [workload_of_jobs_bounded], we prove that the
workload of higher-or-equal priority jobs (w.r.t. task [tsk])
is no larger than the total request-bound function of
higher-or-equal priority tasks. *)
Lemma hep_workload_le_total_hep_rbf :
forall t Δ ,
workload_of_hep_jobs arr_seq j t (t + Δ)
<= total_hep_request_bound_function_FP ts tsk Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job H_job_of_tsk : job_of_task tsk j
forall (t : instant) (Δ : nat),
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_hep_request_bound_function_FP ts tsk Δ
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job H_job_of_tsk : job_of_task tsk j
forall (t : instant) (Δ : nat),
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_hep_request_bound_function_FP ts tsk Δ
move => t Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job H_job_of_tsk : job_of_task tsk j t : instant Δ : nat
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_hep_request_bound_function_FP ts tsk Δ
apply workload_of_jobs_bounded.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job H_job_of_tsk : job_of_task tsk j t : instant Δ : nat
forall j0 : Job,
hep_job j0 j -> hep_task (job_task j0) tsk
rewrite /hep_job /FP_to_JLFP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts FP : FP_policy Task tsk : Task total_ohep_rbf := fun => [eta
total_ohep_request_bound_function_FP
ts tsk]: duration -> duration -> nat j : Job H_job_of_tsk : job_of_task tsk j t : instant Δ : nat
forall j0 : Job,
hep_task (job_task j0) (job_task j) ->
hep_task (job_task j0) tsk
by move : H_job_of_tsk => /eqP <-.
Qed .
End FP .
(** In this section, we show that the total RBF is a bound on higher-or-equal
priority workload under any JLFP policy. *)
Section JLFP .
(** Consider a JLFP policy that indicates a higher-or-equal priority
relation ... *)
Context `{JLFP_policy Job}.
(** ... and any job [j]. *)
Variable j : Job.
(** A simple consequence of lemma [hep_workload_le_total_hep_rbf] is that
the workload of higher-or-equal priority jobs is bounded by the total
request-bound function. *)
Corollary hep_workload_le_total_rbf :
forall t Δ ,
workload_of_hep_jobs arr_seq j t (t + Δ)
<= total_request_bound_function ts Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H4 : JLFP_policy Job j : Job
forall (t : instant) (Δ : nat),
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_request_bound_function ts Δ
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H4 : JLFP_policy Job j : Job
forall (t : instant) (Δ : nat),
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_request_bound_function ts Δ
move => t Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H4 : JLFP_policy Job j : Job t : instant Δ : nat
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_request_bound_function ts Δ
rewrite /workload_of_hep_jobs (leqRW (workload_of_jobs_weaken _ predT _ _ )); last by done .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts H4 : JLFP_policy Job j : Job t : instant Δ : nat
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
total_request_bound_function ts Δ
by apply total_workload_le_total_rbf.
Qed .
End JLFP .
End ProofRequestBoundFunction .
(** ** RBF Properties *)
(** In this section, we prove simple properties and identities of RBFs. *)
Section RequestBoundFunctions .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent :
consistent_arrival_times arr_seq.
(** Let [tsk] be any task. *)
Variable tsk : Task.
(** Let [max_arrivals] be a family of valid arrival curves, i.e.,
for any task [tsk] in [ts] [max_arrival tsk] is (1) an arrival
bound of [tsk], and (2) it is a monotonic function that equals 0
for the empty interval [Δ = 0]. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
(** We prove that [task_request_bound_function 0] is equal to [0]. *)
Lemma task_rbf_0_zero :
task_request_bound_function tsk 0 = 0 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk)
task_request_bound_function tsk 0 = 0
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk)
task_request_bound_function tsk 0 = 0
rewrite /task_request_bound_function.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk)
task_cost tsk * max_arrivals tsk 0 = 0
apply /eqP; rewrite muln_eq0; apply /orP; right ; apply /eqP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk)
max_arrivals tsk 0 = 0
by move : H_valid_arrival_curve => [T1 T2].
Qed .
(** We prove that [task_request_bound_function] is monotone. *)
Lemma task_rbf_monotone :
monotone leq (task_request_bound_function tsk).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk)
monotone leq (task_request_bound_function tsk)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk)
monotone leq (task_request_bound_function tsk)
rewrite /monotone => ? ? LE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) _x_, _y_ : nat LE : _x_ <= _y_
task_request_bound_function tsk _x_ <=
task_request_bound_function tsk _y_
rewrite /task_request_bound_function leq_mul2l.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) _x_, _y_ : nat LE : _x_ <= _y_
(task_cost tsk == 0 )
|| (max_arrivals tsk _x_ <= max_arrivals tsk _y_)
apply /orP; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) _x_, _y_ : nat LE : _x_ <= _y_
max_arrivals tsk _x_ <= max_arrivals tsk _y_
by move : H_valid_arrival_curve => [_ T]; apply T.
Qed .
(** In the following, we assume that [tsk] has a positive cost ... *)
Hypothesis H_positive_cost : 0 < task_cost tsk.
(** ... and [max_arrivals tsk ε] is positive. *)
Hypothesis H_arrival_curve_positive : max_arrivals tsk ε > 0 .
(** Then we prove that [task_request_bound_function] at [ε] is greater than or equal to the task's WCET. *)
Lemma task_rbf_1_ge_task_cost :
task_request_bound_function tsk ε >= task_cost tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
task_cost tsk <= task_request_bound_function tsk 1
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
task_cost tsk <= task_request_bound_function tsk 1
have ALT: forall n , n = 0 \/ n > 0 by clear ; intros n; destruct n; [left | right ].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ALT : forall n : nat, n = 0 \/ 0 < n
task_cost tsk <= task_request_bound_function tsk 1
specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 POS : 0 < task_cost tsk
task_cost tsk <= task_request_bound_function tsk 1
rewrite -[task_cost tsk]muln1 /task_request_bound_function.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 POS : 0 < task_cost tsk
task_cost tsk * 1 <=
task_cost tsk * max_arrivals tsk 1
by rewrite leq_pmul2l //=.
Qed .
(** As a corollary, we prove that the [task_request_bound_function] at any point [A] greater than
[0] is no less than the task's WCET. *)
Lemma task_rbf_ge_task_cost :
forall A ,
A > 0 ->
task_request_bound_function tsk A >= task_cost tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
forall A : nat,
0 < A ->
task_cost tsk <= task_request_bound_function tsk A
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
forall A : nat,
0 < A ->
task_cost tsk <= task_request_bound_function tsk A
case => // A GEQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 A : nat GEQ : 0 < A.+1
task_cost tsk <= task_request_bound_function tsk A.+1
apply : (leq_trans task_rbf_1_ge_task_cost).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 A : nat GEQ : 0 < A.+1
task_request_bound_function tsk 1 <=
task_request_bound_function tsk A.+1
exact : task_rbf_monotone.
Qed .
(** Then, we prove that [task_request_bound_function] at [ε] is greater than [0]. *)
Lemma task_rbf_epsilon_gt_0 : 0 < task_request_bound_function tsk ε.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
0 < task_request_bound_function tsk 1
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
0 < task_request_bound_function tsk 1
apply leq_trans with (task_cost tsk) => [//|].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
task_cost tsk <= task_request_bound_function tsk 1
exact : task_rbf_1_ge_task_cost.
Qed .
(** Consider a set of tasks [ts] containing the task [tsk]. *)
Variable ts : seq Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Next, we prove that cost of [tsk] is less than or equal to the
[total_request_bound_function]. *)
Lemma task_cost_le_sum_rbf :
forall t ,
t > 0 ->
task_cost tsk <= total_request_bound_function ts t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts
forall t : nat,
0 < t ->
task_cost tsk <= total_request_bound_function ts t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts
forall t : nat,
0 < t ->
task_cost tsk <= total_request_bound_function ts t
case => [//|t] GE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_cost tsk <= total_request_bound_function ts t.+1
eapply leq_trans; first exact : task_rbf_1_ge_task_cost.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_request_bound_function tsk 1 <=
total_request_bound_function ts t.+1
rewrite /total_request_bound_function.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_request_bound_function tsk 1 <=
\sum_(tsk <- ts) task_request_bound_function tsk t.+1
erewrite big_rem; last by exact H_tsk_in_ts.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_request_bound_function tsk 1 <=
ssrnat_addn__canonical__Monoid_ComLaw
(task_request_bound_function tsk t.+1 )
(\big[ssrnat_addn__canonical__Monoid_ComLaw/0 ]_(y <-
rem (T:=Task) tsk ts)
task_request_bound_function y t.+1 )
apply leq_trans with (task_request_bound_function tsk t.+1 ); last by apply leq_addr.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_request_bound_function tsk 1 <=
task_request_bound_function tsk t.+1
by apply task_rbf_monotone.
Qed .
End RequestBoundFunctions .
(** ** Monotonicity of the Total RBF *)
(** In the following section, we note some trivial facts about the monotonicity
of various total RBF variants. *)
Section TotalRBFMonotonic .
(** Consider a set of tasks characterized by WCETs and arrival curves. *)
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
(** We observe that the total RBF is monotonically increasing. *)
Lemma total_rbf_monotone :
monotone leq (total_request_bound_function ts).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals
monotone leq (total_request_bound_function ts)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals
monotone leq (total_request_bound_function ts)
by apply : sum_leq_mono => tsk IN; apply : task_rbf_monotone. Qed .
(** Furthermore, for any fixed-priority policy, ... *)
Context `{FP_policy Task}.
(** ... the total RBF of higher- or equal-priority tasks is also monotonic, ... *)
Lemma total_hep_rbf_monotone :
forall tsk ,
monotone leq (total_hep_request_bound_function_FP ts tsk).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
monotone leq
(total_hep_request_bound_function_FP ts tsk)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
monotone leq
(total_hep_request_bound_function_FP ts tsk)
move => tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
monotone leq
(total_hep_request_bound_function_FP ts tsk)
apply : sum_leq_mono => tsk' IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk' \in ts
monotone leq (task_request_bound_function tsk')
exact : task_rbf_monotone.
Qed .
(** ... as is the variant that excludes the reference task. *)
Lemma total_ohep_rbf_monotone :
forall tsk ,
monotone leq (total_ohep_request_bound_function_FP ts tsk).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
monotone leq
(total_ohep_request_bound_function_FP ts tsk)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
monotone leq
(total_ohep_request_bound_function_FP ts tsk)
move => tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
monotone leq
(total_ohep_request_bound_function_FP ts tsk)
apply : sum_leq_mono => tsk' IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk' \in ts
monotone leq (task_request_bound_function tsk')
exact : task_rbf_monotone.
Qed .
End TotalRBFMonotonic .
(** ** RBFs Equal to Zero for Duration ε *)
(** In the following section, we derive simple properties that follow in
the pathological case of an RBF that yields zero for duration ε. *)
Section DegenerateTotalRBFs .
(** Consider a set of tasks characterized by WCETs and arrival curves ... *)
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
(** ... and any consistent arrival sequence of valid jobs of these tasks. *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobCost Job}.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Suppose the arrival curves are correct. *)
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Consider any valid schedule corresponding to this arrival sequence. *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_jobs_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq.
(** First, we observe that, if a task's RBF is zero for a duration [ε], then it
trivially has a response-time bound of zero. *)
Lemma pathological_rbf_response_time_bound :
forall tsk ,
tsk \in ts ->
task_request_bound_function tsk ε = 0 ->
task_response_time_bound arr_seq sched tsk 0 .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq
forall tsk : Task,
tsk \in ts ->
task_request_bound_function tsk 1 = 0 ->
task_response_time_bound arr_seq sched tsk 0
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq
forall tsk : Task,
tsk \in ts ->
task_request_bound_function tsk 1 = 0 ->
task_response_time_bound arr_seq sched tsk 0
move => tsk IN ZERO j ARR TASK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts ZERO : task_request_bound_function tsk 1 = 0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
job_response_time_bound sched j 0
rewrite /job_response_time_bound/completed_by.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts ZERO : task_request_bound_function tsk 1 = 0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
job_cost j <= service sched j (job_arrival j + 0 )
move : ZERO.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_request_bound_function tsk 1 = 0 ->
job_cost j <= service sched j (job_arrival j + 0 )
rewrite /task_request_bound_function => /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_cost tsk * max_arrivals tsk 1 == 0 ->
job_cost j <= service sched j (job_arrival j + 0 )
rewrite muln_eq0 => /orP [/eqP COST|/eqP NEVER].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
job_cost j <= service sched j (job_arrival j + 0 )
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
job_cost j <= service sched j (job_arrival j + 0 )
apply : leq_trans.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
job_cost j <= ?Goal0
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
job_cost j <= ?Goal0
by apply : H_valid_job_cost.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
task_cost (job_task j) <=
service sched j (job_arrival j + 0 )
move : TASK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j COST : task_cost tsk = 0
job_of_task tsk j ->
task_cost (job_task j) <=
service sched j (job_arrival j + 0 )
rewrite /job_of_task => /eqP ->.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j COST : task_cost tsk = 0
task_cost tsk <= service sched j (job_arrival j + 0 )
by rewrite COST. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j NEVER : max_arrivals tsk 1 = 0
job_cost j <= service sched j (job_arrival j + 0 )
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j NEVER : max_arrivals tsk 1 = 0
job_cost j <= service sched j (job_arrival j + 0 )
exfalso .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j NEVER : max_arrivals tsk 1 = 0
False
have : 0 < max_arrivals tsk ε
by apply : (non_pathological_max_arrivals tsk arr_seq _ j).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j NEVER : max_arrivals tsk 1 = 0
0 < max_arrivals tsk 1 -> False
by rewrite NEVER. }
Qed .
(** Second, given a fixed-priority policy with reflexive priorities, ... *)
Context {FP : FP_policy Task}.
Hypothesis H_reflexive : reflexive_task_priorities FP.
(** ... if the total RBF of all equal- and higher-priority tasks is zero, then
the reference task's response-time bound is also trivially zero. *)
Lemma pathological_total_hep_rbf_response_time_bound :
forall tsk ,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk ε = 0 ->
task_response_time_bound arr_seq sched tsk 0 .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk 1 = 0 ->
task_response_time_bound arr_seq sched tsk 0
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk 1 = 0 ->
task_response_time_bound arr_seq sched tsk 0
move => tsk IN ZERO j ARR TASK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
job_response_time_bound sched j 0
apply : pathological_rbf_response_time_bound; eauto .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_request_bound_function tsk 1 = 0
apply /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_request_bound_function tsk 1 == 0
move : ZERO => /eqP; rewrite sum_nat_eq0_nat => /allP; apply .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
tsk \in [seq x <- ts | hep_task x tsk]
rewrite mem_filter; apply /andP; split => //.
Qed .
(** Thus we we can prove any response-time bound from such a pathological
case, which is useful to eliminate this case in higher-level analyses. *)
Corollary pathological_total_hep_rbf_any_bound :
forall tsk ,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk ε = 0 ->
forall R ,
task_response_time_bound arr_seq sched tsk R.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk 1 = 0 ->
forall R : duration,
task_response_time_bound arr_seq sched tsk R
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk 1 = 0 ->
forall R : duration,
task_response_time_bound arr_seq sched tsk R
move => tsk IN ZERO R.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 R : duration
task_response_time_bound arr_seq sched tsk R
move : (pathological_total_hep_rbf_response_time_bound tsk IN ZERO).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 R : duration
task_response_time_bound arr_seq sched tsk 0 ->
task_response_time_bound arr_seq sched tsk R
rewrite /task_response_time_bound/job_response_time_bound => COMP j INj TASK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 R : duration COMP : forall j : Job,
arrives_in arr_seq j ->
job_of_task tsk j ->
completed_by sched j (job_arrival j + 0 )j : Job INj : arrives_in arr_seq j TASK : job_of_task tsk j
completed_by sched j (job_arrival j + R)
apply : completion_monotonic; last by apply : COMP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 R : duration COMP : forall j : Job,
arrives_in arr_seq j ->
job_of_task tsk j ->
completed_by sched j (job_arrival j + 0 )j : Job INj : arrives_in arr_seq j TASK : job_of_task tsk j
job_arrival j + 0 <= job_arrival j + R
by lia .
Qed .
End DegenerateTotalRBFs .
(** In this section, we establish results about the task-wise partitioning of
total RBFs of multiple tasks. *)
Section FP_RBF_partitioning .
(** Consider any type of tasks ... *)
Context {Task : TaskType} `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks, where each task has
a cost and an associated arrival curve. *)
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{MaxArrivals Task}.
(** Consider an FP policy that indicates a higher-or-equal priority
relation. *)
Context `{FP : FP_policy Task}.
(** Consider a task set ts... *)
Variable ts : seq Task.
(** ...and let [tsk] be any task that serves as the reference point for
"higher or equal priority" (usually, but not necessarily, from [ts]). *)
Variable tsk : Task.
(** We establish that the bound on the total workload due to
higher-or-equal-priority tasks can be partitioned task-wise.
In other words, it is equal to the sum of the bound on the
total workload due to higher-priority tasks and the bound on
the total workload due to equal- priority tasks. *)
Lemma hep_rbf_taskwise_partitioning :
forall L ,
total_hep_request_bound_function_FP ts tsk L
= total_hp_request_bound_function_FP ts tsk L
+ total_ep_request_bound_function_FP ts tsk L.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task
forall L : duration,
total_hep_request_bound_function_FP ts tsk L =
total_hp_request_bound_function_FP ts tsk L +
total_ep_request_bound_function_FP ts tsk L
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task
forall L : duration,
total_hep_request_bound_function_FP ts tsk L =
total_hp_request_bound_function_FP ts tsk L +
total_ep_request_bound_function_FP ts tsk L
move => L; apply sum_split_exhaustive_mutually_exclusive_preds => t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task L : duration t : Task
hep_task t tsk = hp_task t tsk || ep_task t tsk
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task L : duration t : Task
hep_task t tsk = hp_task t tsk || ep_task t tsk
by rewrite -andb_orr orNb Bool.andb_true_r.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task L : duration t : Task
~~ (hp_task t tsk && ep_task t tsk)
rewrite !negb_and; case : (hep_task _ _) =>//=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task L : duration t : Task
~~ ~~ hep_task tsk t || ~~ hep_task tsk t
by case : (hep_task _ _)=>//.
Qed .
(** Now, assume that the priorities are reflexive. *)
Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
(** If the task set does not contain duplicates, then the total
higher-or-equal-priority RBF for any task can be split as the sum of
the total _other_ higher-or-equal-priority workload and the RBF of the
task itself. *)
Lemma split_hep_rbf :
forall Δ ,
tsk \in ts ->
uniq ts ->
total_hep_request_bound_function_FP ts tsk Δ
= total_ohep_request_bound_function_FP ts tsk Δ
+ task_request_bound_function tsk Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP
forall Δ : duration,
tsk \in ts ->
uniq ts ->
total_hep_request_bound_function_FP ts tsk Δ =
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP
forall Δ : duration,
tsk \in ts ->
uniq ts ->
total_hep_request_bound_function_FP ts tsk Δ =
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ
move => Δ IN UNIQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
total_hep_request_bound_function_FP ts tsk Δ =
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ
rewrite /total_hep_request_bound_function_FP /total_ohep_request_bound_function_FP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
\sum_(tsk_other <- ts | hep_task tsk_other tsk)
task_request_bound_function tsk_other Δ =
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ +
task_request_bound_function tsk Δ
rewrite (bigID_idem _ _ (fun tsko => tsko != tsk)) //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
\sum_(i <- ts | hep_task i tsk && (i != tsk))
task_request_bound_function i Δ +
\sum_(i <- ts | hep_task i tsk && ~~ (i != tsk))
task_request_bound_function i Δ =
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ +
task_request_bound_function tsk Δ
apply /eqP; rewrite eqn_add2l.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
\sum_(i <- ts | hep_task i tsk && ~~ (i != tsk))
task_request_bound_function i Δ ==
task_request_bound_function tsk Δ
rewrite (eq_bigl (fun i => i == tsk)); last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
(fun i : Task => hep_task i tsk && ~~ (i != tsk)) =1
eq_op^~ tsk
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
(fun i : Task => hep_task i tsk && ~~ (i != tsk)) =1
eq_op^~ tsk
move => tsko.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
hep_task tsko tsk && ~~ (tsko != tsk) = (tsko == tsk)
case (tsko == tsk) eqn : EQ; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task EQ : (tsko == tsk) = true
hep_task tsko tsk && ~~ ~~ true = true
move : EQ => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
hep_task tsk tsk && ~~ ~~ true = true
by rewrite H_priority_is_reflexive //=.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
\sum_(i <- ts | i == tsk)
task_request_bound_function i Δ ==
task_request_bound_function tsk Δ
rewrite (big_rem tsk) //= eq_refl.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
task_request_bound_function tsk Δ +
\sum_(y <- rem (T:=Task) tsk ts | y == tsk)
task_request_bound_function y Δ ==
task_request_bound_function tsk Δ
rewrite big_seq_cond big_pred0; first by rewrite addn0 //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
(fun i : Task =>
(i \in rem (T:=Task) tsk ts) && (i == tsk)) =1 xpred0
move => tsko.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
(tsko \in rem (T:=Task) tsk ts) && (tsko == tsk) =
false
case (tsko == tsk) eqn : EQ; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task EQ : (tsko == tsk) = true
(tsko \in rem (T:=Task) tsk ts) && true = false
move : EQ => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
(tsk \in rem (T:=Task) tsk ts) && true = false
rewrite andbT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
(tsk \in rem (T:=Task) tsk ts) = false
by apply mem_rem_uniqF => //=.
Qed .
(** If the task set may contain duplicates, then the we can only say that
the sum of other higher-or-equal-priority [RBF] and task [tsk]'s [RBF]
is at most the total higher-or-equal-priority workload. *)
Lemma split_hep_rbf_weaken :
forall Δ ,
tsk \in ts ->
total_ohep_request_bound_function_FP ts tsk Δ + task_request_bound_function tsk Δ
<= total_hep_request_bound_function_FP ts tsk Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP
forall Δ : duration,
tsk \in ts ->
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ <=
total_hep_request_bound_function_FP ts tsk Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP
forall Δ : duration,
tsk \in ts ->
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ <=
total_hep_request_bound_function_FP ts tsk Δ
move => Δ IN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ <=
total_hep_request_bound_function_FP ts tsk Δ
rewrite /total_hep_request_bound_function_FP /total_ohep_request_bound_function_FP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ +
task_request_bound_function tsk Δ <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk)
task_request_bound_function tsk_other Δ
rewrite [leqRHS](bigID_idem _ _ (fun tsko => tsko != tsk)) //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ +
task_request_bound_function tsk Δ <=
\sum_(i <- ts | hep_task i tsk && (i != tsk))
task_request_bound_function i Δ +
\sum_(i <- ts | hep_task i tsk && ~~ (i != tsk))
task_request_bound_function i Δ
apply leq_add; first by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
task_request_bound_function tsk Δ <=
\sum_(i <- ts | hep_task i tsk && ~~ (i != tsk))
task_request_bound_function i Δ
rewrite (eq_bigl (fun tsko => tsko == tsk)); last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
(fun i : Task => hep_task i tsk && ~~ (i != tsk)) =1
eq_op^~ tsk
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
(fun i : Task => hep_task i tsk && ~~ (i != tsk)) =1
eq_op^~ tsk
move => tsko.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts tsko : Task
hep_task tsko tsk && ~~ (tsko != tsk) = (tsko == tsk)
case (tsko ==tsk) eqn : TSKEQ; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts tsko : Task TSKEQ : (tsko == tsk) = true
hep_task tsko tsk && ~~ ~~ true = true
move : TSKEQ => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts tsko : Task
hep_task tsk tsk && ~~ ~~ true = true
by rewrite (H_priority_is_reflexive tsk) //=.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
task_request_bound_function tsk Δ <=
\sum_(i <- ts | i == tsk)
task_request_bound_function i Δ
rewrite (big_rem tsk) //= eq_refl.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
task_request_bound_function tsk Δ <=
task_request_bound_function tsk Δ +
\sum_(y <- rem (T:=Task) tsk ts | y == tsk)
task_request_bound_function y Δ
by apply leq_addr.
Qed .
End FP_RBF_partitioning .
(** In this section, we state a few facts for RBFs in the context of a
fixed-priority policy. *)
Section RBFFOrFP .
(** Consider a set of tasks characterized by WCETs and arrival curves. *)
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
(** For any fixed-priority policy, ... *)
Context `{FP_policy Task}.
(** ... [total_ohep_request_bound_function_FP] at [0] is always [0]. *)
Lemma total_ohep_rbf0 :
forall (tsk : Task),
total_ohep_request_bound_function_FP ts tsk 0 = 0 .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
total_ohep_request_bound_function_FP ts tsk 0 = 0
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
total_ohep_request_bound_function_FP ts tsk 0 = 0
rewrite /total_ohep_request_bound_function_FP => tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other 0 = 0
apply /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other 0 == 0
rewrite sum_nat_eq0_nat.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
all
(fun x : Task =>
task_request_bound_function x 0 == 0 )
[seq x <- ts | hep_task x tsk & x != tsk]
apply /allP => tsk' IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk'
\in [seq x <- ts | hep_task x tsk & x != tsk]
task_request_bound_function tsk' 0 == 0
apply /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk'
\in [seq x <- ts | hep_task x tsk & x != tsk]
task_request_bound_function tsk' 0 = 0
apply task_rbf_0_zero => //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk'
\in [seq x <- ts | hep_task x tsk & x != tsk]
valid_arrival_curve (max_arrivals tsk')
apply H_valid_arrival_curve.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk'
\in [seq x <- ts | hep_task x tsk & x != tsk]
tsk' \in ts
rewrite mem_filter in IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : hep_task tsk' tsk && (tsk' != tsk) &&
(tsk' \in ts)
tsk' \in ts
by move : IN => /andP[_ ->].
Qed .
(** Next we show how [total_ohep_request_bound_function_FP] can bound the
workload of jobs in a given interval. *)
(** Consider any types of jobs. *)
Context `{Job : JobType} `{JobTask Job Task} `{JobCost Job}.
(** Consider any arrival sequence that only has jobs from the task set and
where all arrivals have a valid job cost. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Assume there exists an arrival curve and that the arrival sequence
respects this curve. *)
Context `{MaxArrivals Task}.
Hypothesis H_respects_max_arrivals : taskset_respects_max_arrivals arr_seq ts.
(** Consider any task [tsk] and any job [j] of the task [tsk]. *)
Variable j : Job.
Variable tsk : Task.
Hypothesis H_job_of_task : job_of_task tsk j.
(** For any interval <<[t1, t1 + Δ)>>, the workload of jobs that have higher
task priority than the task priority of [j] is bounded by
[total_ohep_request_bound_function_FP] for the duration [Δ]. *)
Lemma ohep_workload_le_rbf :
forall Δ t1 ,
workload_of_jobs (another_task_hep_job^~ j) (arrivals_between arr_seq t1 (t1 + Δ))
<= total_ohep_request_bound_function_FP ts tsk Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j
forall (Δ : nat) (t1 : instant),
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
total_ohep_request_bound_function_FP ts tsk Δ
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j
forall (Δ : nat) (t1 : instant),
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
total_ohep_request_bound_function_FP ts tsk Δ
move => Δ t1.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
total_ohep_request_bound_function_FP ts tsk Δ
rewrite /workload_of_jobs /total_ohep_request_bound_function_FP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
another_task_hep_job j0 j) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
rewrite /another_task_hep_job /hep_job /FP_to_JLFP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
hep_task (job_task j0) (job_task j) &&
(job_task j0 != job_task j)) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
set (pred_task tsk_other := hep_task tsk_other tsk && (tsk_other != tsk)).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
hep_task (job_task j0) (job_task j) &&
(job_task j0 != job_task j)) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
rewrite (eq_big (fun j => pred_task (job_task j)) job_cost) //;
last by move => j'; rewrite /pred_task; move : H_job_of_task => /eqP ->.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(i <- arrivals_between arr_seq t1 (t1 + Δ) |
pred_task (job_task i)) job_cost i <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
erewrite (eq_big pred_task); [|by done |by move => tsk'; eauto ].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(i <- arrivals_between arr_seq t1 (t1 + Δ) |
pred_task (job_task i)) job_cost i <=
\sum_(i <- ts | pred_task i)
(task_request_bound_function^~ Δ) i
by apply : workload_of_jobs_bounded.
Qed .
End RBFFOrFP .
(** We know that the workload of a task in any interval must be
bounded by the task's RBF in that interval. However, in the proofs
of several lemmas, we are required to reason about the workload of
a task in an interval excluding the cost of a particular job
(usually the job under analysis). Such a workload can be tightly
bounded by the task's RBF for the interval excluding the cost of
one task.
Notice, however, that this is not a trivial result since a naive
approach to proving it would fail. Suppose we want to prove that
some quantity [A - B] is upper bounded by some quantity [C -
D]. This usually requires us to prove that [A] is upper bounded by
[C] _and_ [D] is upper bounded by [B]. In our case, this would be
equivalent to proving that the task cost is upper-bounded by the
job cost, which of course is not true.
So, a different approach is needed, which we show in this
section. *)
Section TaskWorkload .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent :
consistent_arrival_times arr_seq.
(** ... and assume that WCETs are respected. *)
Hypothesis H_arrivals_have_valid_job_costs :
arrivals_have_valid_job_costs arr_seq.
(** Let [tsk] be any task ... *)
Variable tsk : Task.
(** ... characterized by a valid arrival curve. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
(** Consider any job [j] of [tsk] ... *)
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
(** ... that arrives in the given arrival sequence. *)
Hypothesis H_j_arrives_in : arrives_in arr_seq j.
(** Consider any time instant [t1] and duration [Δ] such that [j]
arrives before [t1 + Δ]. *)
Variables (t1 : instant) (Δ : duration).
Hypothesis H_job_arrival_lt : job_arrival j < t1 + Δ.
(** As a preparatory step, we restrict our attention to the sub-interval
containing the job's arrival. We know that the job's arrival necessarily
happens in the interval (<<[job_arrival j], t1 + Δ>>). This allows us to
show that the task workload excluding the task cost can be bounded by the
cost of the arrivals in the interval as follows. *)
Lemma task_rbf_without_job_under_analysis_from_arrival :
task_workload_between arr_seq tsk (job_arrival j) (t1 + Δ) - job_cost j
<= task_cost tsk * number_of_task_arrivals arr_seq tsk (job_arrival j) (t1 + Δ)
- task_cost tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
task_workload_between arr_seq tsk (job_arrival j)
(t1 + Δ) - job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
task_workload_between arr_seq tsk (job_arrival j)
(t1 + Δ) - job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk
rewrite /task_workload_between /task_workload /workload_of_jobs /number_of_task_arrivals.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
\sum_(j <- arrivals_between arr_seq (job_arrival j)
(t1 + Δ) | job_of_task tsk j) job_cost j -
job_cost j <=
task_cost tsk *
size
(task_arrivals_between arr_seq tsk (job_arrival j)
(t1 + Δ)) - task_cost tsk
rewrite (big_rem j) //= addnC //= H_job_of_task addnK (filter_size_rem j)//.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
\sum_(y <- rem (T:=Job) j
(arrivals_between arr_seq (job_arrival j)
(t1 + Δ)) | job_of_task tsk y)
job_cost y <=
task_cost tsk *
(size
[seq y <- rem (T:=Job) j
(arrivals_between arr_seq
(job_arrival j) (t1 + Δ))
| job_of_task tsk y] + 1 ) - task_cost tsk
rewrite mulnDr mulnC muln1 addnK mulnC.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
\sum_(y <- rem (T:=Job) j
(arrivals_between arr_seq (job_arrival j)
(t1 + Δ)) | job_of_task tsk y)
job_cost y <=
task_cost tsk *
size
[seq y <- rem (T:=Job) j
(arrivals_between arr_seq
(job_arrival j) (t1 + Δ))
| job_of_task tsk y]
apply sum_majorant_constant => j' ARR' /eqP TSK2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ j' : Job ARR' : j'
\in rem (T:=Job) j
(arrivals_between arr_seq
(job_arrival j)
(t1 + Δ)) TSK2 : job_task j' = tsk
job_cost j' <= task_cost tsk
rewrite -TSK2; apply H_arrivals_have_valid_job_costs.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ j' : Job ARR' : j'
\in rem (T:=Job) j
(arrivals_between arr_seq
(job_arrival j)
(t1 + Δ)) TSK2 : job_task j' = tsk
arrives_in arr_seq j'
apply rem_in in ARR'.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ j' : Job ARR' : j'
\in arrivals_between arr_seq
(job_arrival j)
(t1 + Δ) TSK2 : job_task j' = tsk
arrives_in arr_seq j'
by eapply in_arrivals_implies_arrived => //=.
Qed .
(** To use the above lemma in our final theorem, we require that the arrival
of the job under analysis necessarily happens in the interval we are
considering. *)
Hypothesis H_j_arrives_after_t : t1 <= job_arrival j.
(** Under the above assumption, we can finally establish the desired bound. *)
Lemma task_rbf_without_job_under_analysis :
task_workload_between arr_seq tsk t1 (t1 + Δ) - job_cost j
<= task_request_bound_function tsk Δ - task_cost tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_request_bound_function tsk Δ - task_cost tsk
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_request_bound_function tsk Δ - task_cost tsk
apply leq_trans with
(task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) - task_cost tsk); last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) -
task_cost tsk <=
task_request_bound_function tsk Δ - task_cost tsk
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) -
task_cost tsk <=
task_request_bound_function tsk Δ - task_cost tsk
rewrite leq_sub2r // leq_mul2l; apply /orP => //=; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk Δ
have POSE: Δ = (t1 + Δ - t1) by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j POSE : Δ = t1 + Δ - t1
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk Δ
rewrite [in leqRHS]POSE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j POSE : Δ = t1 + Δ - t1
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk (t1 + Δ - t1)
eapply (H_is_arrival_curve t1 (t1 + Δ)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j POSE : Δ = t1 + Δ - t1
t1 <= t1 + Δ
by lia .
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) -
task_cost tsk
rewrite (@num_arrivals_of_task_cat _ _ _ _ _ (job_arrival j)); last by apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_cost tsk *
(number_of_task_arrivals arr_seq tsk t1
(job_arrival j) +
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ)) - task_cost tsk
rewrite mulnDr.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j) +
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk
rewrite /task_workload_between /task_workload (workload_of_jobs_cat _ (job_arrival j) );
last by apply /andP; split ; lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1 (job_arrival j)) +
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ)) -
job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j) +
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk
rewrite -!addnBA; first last .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
job_cost j <=
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ))
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
job_cost j <=
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ))
by rewrite /task_workload
/workload_of_jobs (big_rem j) //= H_job_of_task leq_addr.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_cost tsk <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ)
rewrite -{1 }[task_cost tsk]muln1 leq_mul2l; apply /orP; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
0 <
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ)
rewrite /number_of_task_arrivals /task_arrivals_between.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
0 <
size
[seq j <- arrivals_between arr_seq (job_arrival j)
(t1 + Δ)
| job_of_task tsk j]
rewrite size_filter -has_count; apply /hasP; exists j ; last by rewrite H_job_of_task.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
j
\in arrivals_between arr_seq (job_arrival j)
(t1 + Δ)
apply (mem_bigcat _ Job _ (job_arrival j) _); last by apply job_in_arrivals_at => //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
job_arrival j \in index_iota (job_arrival j) (t1 + Δ)
rewrite mem_index_iota.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
job_arrival j <= job_arrival j < t1 + Δ
by apply /andP;split .
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1 (job_arrival j)) +
(workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ)) -
job_cost j) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j) +
(task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk)
rewrite leq_add //; last by apply : task_rbf_without_job_under_analysis_from_arrival.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1 (job_arrival j)) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j)
rewrite -/(task_workload _ _) -/(task_workload_between _ _ _ _).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (job_arrival j) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j)
by apply : task_workload_between_bounded.
Qed .
End TaskWorkload .