Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.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.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.model.arrival_curves.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.definitions.job_properties.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.definitions.request_bound_function.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.definitions.schedulability.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * Facts about Request Bound Functions (RBFs) *)
(** In this file, we prove some lemmas about request bound functions. *)
(** ** RBF is a Bound on Workload *)
(** First, we show that a task's RBF is indeed an upper bound on its
workload. *)
Section ProofWorkloadBound .
(** 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 with consistent, non-duplicate arrivals, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... 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.
(** ... and an FP policy that indicates a higher-or-equal priority relation. *)
Context `{FP_policy Task}.
(** Further, consider a task set [ts]... *)
Variable ts : seq Task.
(** ... and let [tsk] be any task in [ts]. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Assume that the job costs are no larger than the task costs ... *)
Hypothesis H_valid_job_cost :
arrivals_have_valid_job_costs arr_seq.
(** ... and that all jobs come from the task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** Let [max_arrivals] be any arrival bound for task-set [ts]. *)
Context `{MaxArrivals Task}.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
(** Next, recall the notions of total workload of jobs... *)
Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2).
(** ... and the workload of jobs of the same task as job j. *)
Let task_workload t1 t2 :=
workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).
(** Finally, let us define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
Let total_rbf := total_request_bound_function ts.
(** In this section, we prove that the workload of all jobs is
no larger than the request bound function. *)
Section WorkloadIsBoundedByRBF .
(** Consider any time [t] and any interval of length [Δ]. *)
Variable t : instant.
Variable Δ : instant.
(** First, we show that workload of task [tsk] is bounded by the number of
arrivals of the task times the cost of the task. *)
Lemma task_workload_le_num_of_arrivals_times_cost :
task_workload t (t + Δ)
<= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
task_workload t (t + Δ) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t (t + Δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
task_workload t (t + Δ) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t (t + Δ)
rewrite /task_workload /workload_of_jobs/ number_of_task_arrivals
/task_arrivals_between -big_filter -sum1_size big_distrr big_filter.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk i)
job_cost i <=
\big[addn_addoid/0 ]_(i <- [seq j <- arrivals_between
arr_seq t
(t + Δ)
| job_of_task tsk j])
muln_muloid (task_cost tsk) 1
destruct (task_arrivals_between arr_seq tsk t (t + Δ)) eqn :TASK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
[::]
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk i)
job_cost i <=
\big[addn_addoid/0 ]_(i <- [seq j <- arrivals_between
arr_seq t
(t + Δ)
| job_of_task tsk j])
muln_muloid (task_cost tsk) 1
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
[::]
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk i)
job_cost i <=
\big[addn_addoid/0 ]_(i <- [seq j <- arrivals_between
arr_seq t
(t + Δ)
| job_of_task tsk j])
muln_muloid (task_cost tsk) 1
unfold task_arrivals_between in TASK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant TASK : [seq j <-
arrivals_between arr_seq t (t + Δ)
| job_of_task tsk j] = [::]
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk i)
job_cost i <=
\big[addn_addoid/0 ]_(i <- [seq j <- arrivals_between
arr_seq t
(t + Δ)
| job_of_task tsk j])
muln_muloid (task_cost tsk) 1
by rewrite -big_filter !TASK !big_nil. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk i)
job_cost i <=
\big[addn_addoid/0 ]_(i <- [seq j <- arrivals_between
arr_seq t
(t + Δ)
| job_of_task tsk j])
muln_muloid (task_cost tsk) 1
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk i)
job_cost i <=
\big[addn_addoid/0 ]_(i <- [seq j <- arrivals_between
arr_seq t
(t + Δ)
| job_of_task tsk j])
muln_muloid (task_cost tsk) 1
rewrite //= big_filter big_seq_cond [in X in _ <= X]big_seq_cond.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
job_of_task
tsk i)
job_cost i <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
job_of_task
tsk i)
task_cost tsk * 1
apply leq_sum.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l
forall i : Job,
(i \in arrivals_between arr_seq t (t + Δ)) &&
job_of_task tsk i -> job_cost i <= task_cost tsk * 1
move => j' /andP [IN TSKj'].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l j' : Job IN : j' \in arrivals_between arr_seq t (t + Δ) TSKj' : job_of_task tsk j'
job_cost j' <= task_cost tsk * 1
rewrite muln1.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l j' : Job IN : j' \in arrivals_between arr_seq t (t + Δ) TSKj' : job_of_task tsk j'
job_cost j' <= task_cost tsk
move : TSKj' => /eqP TSKj'; rewrite -TSKj'.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l j' : Job IN : j' \in arrivals_between arr_seq t (t + Δ) TSKj' : job_task j' = tsk
job_cost j' <= task_cost (job_task j')
apply H_valid_job_cost.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l j' : Job IN : j' \in arrivals_between arr_seq t (t + Δ) TSKj' : job_task j' = tsk
arrives_in arr_seq j'
by apply in_arrivals_implies_arrived in IN. }
Qed .
(** As a corollary, we prove that workload of task is no larger the than
task request bound function. *)
Corollary task_workload_le_task_rbf :
task_workload t (t + Δ) <= task_rbf Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
task_workload t (t + Δ) <= task_rbf Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
task_workload t (t + Δ) <= task_rbf Δ
eapply leq_trans; first by apply task_workload_le_num_of_arrivals_times_cost.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
task_cost tsk *
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
task_rbf Δ
rewrite 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_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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
max_arrivals tsk Δ
rewrite -{2 }[Δ](addKn t).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
max_arrivals tsk (t + Δ - t)
by apply H_is_arrival_bound; last rewrite leq_addr.
Qed .
(** Next, we prove that total workload of tasks is no larger than the total
request bound function. *)
Lemma total_workload_le_total_rbf :
total_workload t (t + Δ) <= total_rbf Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
total_workload t (t + Δ) <= total_rbf Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant
total_workload t (t + Δ) <= total_rbf Δ
set l := arrivals_between arr_seq t (t + Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
total_workload t (t + Δ) <= total_rbf Δ
apply (@leq_trans (\sum_(tsk' <- ts) (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
total_workload t (t + Δ) <=
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
total_workload t (t + Δ) <=
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
rewrite /total_workload.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
have EXCHANGE := exchange_big_dep predT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job EXCHANGE : forall (T : Type )
(y : T)
(c : Monoid.com_law y)
(T0 T1 : Type )
(l : seq T0)
(l0 : seq T1)
(p : pred T0)
(p0 : T0 -> pred T1)
(F : T0 -> T1 -> T),
(forall (i : T0) (j : T1),
p i -> p0 i j -> predT j) ->
\big[c/y]_(i <- l |
p i) \big[c/y]_(j <- l0 | p0 i j) F i j =
\big[c/y]_(j <- l0 |
predT j)
\big[c/y]_(i <- l | p i && p0 i j) F i j
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
rewrite EXCHANGE /=; clear EXCHANGE; last by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(j <- l)
\sum_(i <- ts | job_task j == i) job_cost j
rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(i <- l | (i \in l) && predT i) job_cost i <=
\sum_(i <- l | (i \in l) && true)
\sum_(i0 <- ts | job_task i == i0) job_cost i
apply leq_sum; move => j0 /andP [IN0 HP0].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : true
job_cost j0 <=
\sum_(i <- ts | job_task j0 == i) job_cost j0
rewrite big_mkcond (big_rem (job_task j0)) /=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : true
job_cost j0 <=
(if job_task j0 == job_task j0 then job_cost j0 else 0 ) +
\sum_(y <- rem (T:=Task) (job_task j0) ts)
(if job_task j0 == y then job_cost j0 else 0 )
rewrite eq_refl; apply 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_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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : true
job_task j0 \in ts
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <=
total_rbf Δ
apply leq_sum_seq; intros tsk0 INtsk0 HP0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
task_request_bound_function tsk0 Δ
apply (@leq_trans (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ))
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ))
rewrite -sum1_size big_distrr /= big_filter -/l /workload_of_jobs muln1.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
\sum_(i <- l | job_of_task tsk0 i) task_cost tsk0
apply leq_sum_seq => j0 IN0 /eqP <-.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true j0 : Job IN0 : j0 \in l
job_cost j0 <= task_cost (job_task j0)
apply H_valid_job_cost.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true j0 : Job IN0 : j0 \in l
arrives_in arr_seq j0
by apply in_arrivals_implies_arrived in IN0. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
task_request_bound_function tsk0 Δ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
task_request_bound_function tsk0 Δ
rewrite 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_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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
max_arrivals tsk0 Δ
rewrite -{2 }[Δ](addKn t).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
max_arrivals tsk0 (t + Δ - t)
by apply H_is_arrival_bound; last rewrite leq_addr. }
Qed .
(** Next, we consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_job_of_tsk : job_of_task tsk j.
(** Consider any general predicate defined on tasks. *)
Variable pred : pred Task.
(** We prove that the sum of job cost of jobs whose corresponding task satisfies the predicate
[pred] is bound by the RBF of these tasks. *)
Lemma sum_of_jobs_le_sum_rbf :
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred (job_task j'))
job_cost j' <=
\sum_(tsk' <- ts| pred tsk')
task_request_bound_function tsk' Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function 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_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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
apply (@leq_trans (\sum_(tsk' <- filter pred ts)
(\sum_(j' <- arrivals_between arr_seq t (t + Δ)
| job_task j' == tsk') job_cost j'))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j'
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j'
move : (H_job_of_tsk) => /eqP TSK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j'
rewrite [X in _ <= X]big_filter.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(i <- ts | pred i)
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == i) job_cost j'
set P := fun x => pred (job_task x).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(i <- ts | pred i)
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == i) job_cost j'
rewrite (exchange_big_dep P) //=; last by rewrite /P; move => ???/eqP->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(j <- arrivals_between arr_seq t (t + Δ) | P j)
\sum_(i <- ts | pred i && (job_task j == i))
job_cost j
rewrite /P /workload_of_jobs big_seq_cond [X in _ <= X]big_seq_cond.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
pred
(job_task
i))
job_cost i <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
pred
(job_task
i))
\sum_(i0 <- ts | pred i0 && (job_task i == i0))
job_cost i
apply leq_sum => j0 /andP [IN0 HP0].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_cost j0 <=
\sum_(i <- ts | pred i && (job_task j0 == i))
job_cost j0
rewrite big_mkcond (big_rem (job_task j0)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_cost j0 <=
addn_comoid
(if
pred (job_task j0) && (job_task j0 == job_task j0)
then job_cost j0
else 0 )
(\big[addn_comoid/0 ]_(y <- rem (T:=Task)
(job_task j0) ts)
(if pred y && (job_task j0 == y)
then job_cost j0
else 0 ))
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_cost j0 <=
addn_comoid
(if
pred (job_task j0) && (job_task j0 == job_task j0)
then job_cost j0
else 0 )
(\big[addn_comoid/0 ]_(y <- rem (T:=Task)
(job_task j0) ts)
(if pred y && (job_task j0 == y)
then job_cost j0
else 0 ))
by rewrite HP0 andTb eq_refl; apply 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_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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_task j0 \in ts
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_task j0 \in ts
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
rewrite big_filter.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(i <- ts | pred i)
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == i) job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
apply leq_sum_seq => tsk0 INtsk0 HP0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | job_task
j' ==
tsk0)
job_cost j' <= task_request_bound_function tsk0 Δ
apply (@leq_trans (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | job_task
j' ==
tsk0)
job_cost j' <=
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ))
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | job_task
j' ==
tsk0)
job_cost j' <=
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ))
rewrite -sum1_size big_distrr /= big_filter /workload_of_jobs.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | job_task
j' ==
tsk0)
job_cost j' <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk0
i)
task_cost tsk0 * 1
rewrite muln1 /arrivals_between /arrival_sequence.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_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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- \cat_(t<=t<t + Δ)arrivals_at arr_seq t |
job_task j' == tsk0) job_cost j' <=
\sum_(i <- \cat_(t<=t<t + Δ)arrivals_at arr_seq t |
job_of_task tsk0 i) task_cost tsk0
apply leq_sum_seq; move => j0 IN0 /eqP EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0 j0 : Job IN0 : j0 \in \cat_(t<=t<t + Δ)arrivals_at arr_seq t EQ : job_task j0 = tsk0
job_cost j0 <= task_cost tsk0
by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
task_request_bound_function tsk0 Δ
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
task_request_bound_function tsk0 Δ
rewrite 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_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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
max_arrivals tsk0 Δ
rewrite -{2 }[Δ](addKn t).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : 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 H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_rbf := task_request_bound_function tsk : duration -> nat total_rbf := total_request_bound_function ts : duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
max_arrivals tsk0 (t + Δ - t)
by apply H_is_arrival_bound; last by rewrite leq_addr.
Qed .
End WorkloadIsBoundedByRBF .
End ProofWorkloadBound .
(** ** 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).
(** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
(** We prove that [task_rbf 0] is equal to [0]. *)
Lemma task_rbf_0_zero :
task_rbf 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_rbf := task_request_bound_function tsk : duration -> nat
task_rbf 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_rbf := task_request_bound_function tsk : duration -> nat
task_rbf 0 = 0
rewrite /task_rbf /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_rbf := task_request_bound_function tsk : duration -> nat
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) task_rbf := task_request_bound_function tsk : duration -> nat
max_arrivals tsk 0 = 0
by move : H_valid_arrival_curve => [T1 T2].
Qed .
(** We prove that [task_rbf] is monotone. *)
Lemma task_rbf_monotone :
monotone leq task_rbf.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_rbf := task_request_bound_function tsk : duration -> nat
monotone leq task_rbf
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_rbf := task_request_bound_function tsk : duration -> nat
monotone leq task_rbf
rewrite /monotone; intros ? ? 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) task_rbf := task_request_bound_function tsk : duration -> nat x, y : nat LE : x <= y
task_rbf x <= task_rbf y
rewrite /task_rbf /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) task_rbf := task_request_bound_function tsk : duration -> nat 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) task_rbf := task_request_bound_function tsk : duration -> nat x, y : nat LE : x <= y
max_arrivals tsk x <= max_arrivals tsk y
by move : H_valid_arrival_curve => [_ T]; apply T.
Qed .
(** Consider any job [j] of [tsk]. This guarantees that there exists at least one
job of task [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
(** Then we prove that [task_rbf] at [ε] is greater than or equal to the task's WCET. *)
Lemma task_rbf_1_ge_task_cost :
task_rbf ε >= 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j
task_cost tsk <= task_rbf ε
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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j
task_cost tsk <= task_rbf ε
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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j ALT : forall n : nat, n = 0 \/ 0 < n
task_cost tsk <= task_rbf ε
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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tsk
task_cost tsk <= task_rbf ε
rewrite leqNgt; apply /negP; intros CONTR.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : task_rbf ε < task_cost tsk
False
move : H_is_arrival_curve => ARRB.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : task_rbf ε < task_cost tsk ARRB : respects_max_arrivals arr_seq tsk
(max_arrivals tsk)
False
specialize (ARRB (job_arrival j) (job_arrival j + ε)).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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : task_rbf ε < task_cost tsk ARRB : job_arrival j <= job_arrival j + ε ->
number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + ε) <=
max_arrivals tsk
(job_arrival j + ε - job_arrival j)
False
feed ARRB; first by rewrite 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : task_rbf ε < task_cost tsk ARRB : number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + ε) <=
max_arrivals tsk
(job_arrival j + ε - job_arrival j)
False
move : CONTR; rewrite /task_rbf /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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskARRB : number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + ε) <=
max_arrivals tsk
(job_arrival j + ε - job_arrival j)
task_cost tsk * max_arrivals tsk ε < task_cost tsk ->
False
rewrite -{2 }[task_cost tsk]muln1 ltn_mul2l => /andP [_ CONTR].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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskARRB : number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + ε) <=
max_arrivals tsk
(job_arrival j + ε - job_arrival j) CONTR : max_arrivals tsk ε < 1
False
move : CONTR; rewrite -addn1 -[1 ]add0n leq_add2r leqn0 => /eqP CONTR.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskARRB : number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + ε) <=
max_arrivals tsk
(job_arrival j + ε - job_arrival j) CONTR : max_arrivals tsk ε = 0
False
move : ARRB; rewrite addKn CONTR leqn0 eqn0Ngt => /negP T; apply : 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : max_arrivals tsk ε = 0
0 <
number_of_task_arrivals arr_seq tsk (job_arrival j)
(job_arrival j + ε)
rewrite /number_of_task_arrivals -has_predT /task_arrivals_between.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : max_arrivals tsk ε = 0
has predT
[seq j <- arrivals_between arr_seq (job_arrival j)
(job_arrival j + ε)
| job_of_task tsk j]
apply /hasP; exists j ; last by done .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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : max_arrivals tsk ε = 0
j
\in [seq j <- arrivals_between arr_seq
(job_arrival j) (job_arrival j + ε)
| job_of_task tsk j]
rewrite /arrivals_between addn1 big_nat_recl; last by done .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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : max_arrivals tsk ε = 0
j
\in [seq j <- arrivals_at arr_seq (job_arrival j) ++
\cat_(job_arrival j<=i<job_arrival j)
arrivals_at arr_seq i.+1
| job_of_task tsk j]
rewrite big_geq ?cats0 //= mem_filter.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : max_arrivals tsk ε = 0
job_of_task tsk j &&
(j \in arrivals_at arr_seq (job_arrival j))
apply /andP; split ; first by done .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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : max_arrivals tsk ε = 0
j \in arrivals_at arr_seq (job_arrival j)
move : H_j_arrives => [t ARR]; move : (ARR) => CONS.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : max_arrivals tsk ε = 0 t : instant ARR, CONS : j \in arrivals_at arr_seq t
j \in arrivals_at arr_seq (job_arrival j)
apply H_arrival_times_are_consistent in CONS.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j POS : 0 < task_cost tskCONTR : max_arrivals tsk ε = 0 t : instant ARR : j \in arrivals_at arr_seq t CONS : job_arrival j = t
j \in arrivals_at arr_seq (job_arrival j)
by rewrite CONS.
Qed .
(** As a corollary, we prove that the [task_rbf] 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_rbf 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j
forall A : nat, 0 < A -> task_cost tsk <= task_rbf 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j
forall A : nat, 0 < A -> task_cost tsk <= task_rbf 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j A : nat GEQ : 0 < A.+1
task_cost tsk <= task_rbf 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j A : nat GEQ : 0 < A.+1
task_rbf ε <= task_rbf A.+1
exact : task_rbf_monotone.
Qed .
(** Assume that [tsk] has a positive cost. *)
Hypothesis H_positive_cost : 0 < task_cost tsk.
(** Then, we prove that [task_rbf] at [ε] is greater than [0]. *)
Lemma task_rbf_epsilon_gt_0 : 0 < task_rbf ε.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tsk
0 < task_rbf ε
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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tsk
0 < task_rbf ε
apply leq_trans with (task_cost tsk); first by done .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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tsk
task_cost tsk <= task_rbf ε
by eapply task_rbf_1_ge_task_cost; eauto .
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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tskts : 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tskts : seq Task H_tsk_in_ts : tsk \in ts
forall t : nat,
0 < t ->
task_cost tsk <= total_request_bound_function ts t
move => 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tskts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t
task_cost tsk <= total_request_bound_function ts t
destruct t; first by done .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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tskts : 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 by apply task_rbf_1_ge_task_cost; rt_eauto.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_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tskts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf ε <= 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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tskts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf ε <=
\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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tskts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf ε <=
addn_comoid (task_request_bound_function tsk t.+1 )
(\big[addn_comoid/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) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_positive_cost : 0 < task_cost tskts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf ε <= 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)
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 tsk : Task IN : tsk \in ts
monotone leq (task_request_bound_function tsk)
by apply task_rbf_monotone; rt_auto.
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')
by apply task_rbf_monotone; rt_auto.
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')
by apply task_rbf_monotone; rt_auto.
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 ε = 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 ε = 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 ε = 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 ε = 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 ε = 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 ε == 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 )
- 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 ε = 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 ε = 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 ε = 0
False
have : 0 < max_arrivals tsk ε
by apply : (non_pathological_max_arrivals tsk arr_seq _ j); rt_auto.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 ε = 0
0 < max_arrivals tsk ε -> False
by rewrite NEVER. }
Qed .
(** Second, given a fixed-priority policy with reflexive priorities, ... *)
Context `{FP_policy Task}.
Hypothesis H_reflexive : reflexive_priorities.
(** ... 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 H4 : FP_policy Task H_reflexive : reflexive_priorities
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk ε = 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 H4 : FP_policy Task H_reflexive : reflexive_priorities
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk ε = 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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk ε =
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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk ε =
0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_request_bound_function tsk ε = 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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk ε =
0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_request_bound_function tsk ε == 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 H4 : FP_policy Task H_reflexive : reflexive_priorities 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 => //.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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
hep_task tsk tsk
move : (H_reflexive 0 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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
hep_job_at 0 j j -> hep_task tsk tsk
rewrite /hep_job_at/JLFP_to_JLDP/hep_job/FP_to_JLFP.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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
hep_task (job_task j) (job_task j) -> hep_task tsk tsk
by move : TASK; rewrite /job_of_task => /eqP ->.
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 H4 : FP_policy Task H_reflexive : reflexive_priorities
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk ε = 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 H4 : FP_policy Task H_reflexive : reflexive_priorities
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk ε = 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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk ε =
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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk ε =
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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk ε =
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 H4 : FP_policy Task H_reflexive : reflexive_priorities tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk ε =
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 .