Built with
Alectryon , running Coq+SerAPI v8.14.0+0.14.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.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]
(** * 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_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
(** ... any schedule corresponding to this arrival sequence, ... *)
Context {PState : Type } `{ProcessorState Job PState}.
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}.
Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.
(** Further, consider a task set [ts]... *)
Variable ts : list 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.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
(** 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_task j == tsk])
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_task j == tsk])
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_task j == tsk])
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant TASK : [seq j <- arrivals_between arr_seq t (t + Δ)
| job_task j == tsk] = [::]
\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_task j == tsk])
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_task j == tsk])
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_task j == tsk])
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_task
i ==
tsk))
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_task i == tsk) -> 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_task i == tsk0) 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : 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_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
(** We say that two jobs [j1] and [j2] are in relation
[other_higher_eq_priority], iff [j1] has higher or equal priority than [j2] and
is produced by a different task. *)
Let other_higher_eq_priority j1 j2 :=
jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
(** Recall the notion of workload of higher or equal priority jobs... *)
Let total_hep_workload t1 t2 :=
workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j)
(arrivals_between arr_seq t1 t2).
(** ... and workload of other higher or equal priority jobs. *)
Let total_ohep_workload t1 t2 :=
workload_of_jobs (fun j_other => other_higher_eq_priority j_other j)
(arrivals_between arr_seq t1 t2).
(** We prove that total workload of other tasks with higher-or-equal
priority is no larger than the total request bound function. *)
Lemma total_workload_le_total_ohep_rbf :
total_ohep_workload t (t + Δ) <= total_ohep_rbf Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload t (t + Δ) <= total_ohep_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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload t (t + Δ) <= total_ohep_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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
total_ohep_workload t (t + Δ) <= total_ohep_rbf Δ
apply (@leq_trans (\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
(\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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
total_ohep_workload t (t + Δ) <=
\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
\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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
total_ohep_workload t (t + Δ) <=
\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(j0 <- arrivals_between arr_seq t (t + Δ) | jlfp_higher_eq_priority
j0 j &&
~~
same_task
j0 j)
job_cost j0 <=
\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(j <- arrivals_between arr_seq t (t + Δ) | hep_task
(job_task
j)
tsk &&
(job_task
j
!= tsk))
job_cost j <=
\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
set P := fun x => hep_task (job_task x) tsk && (job_task x != tsk).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job P := fun x : Job =>
hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
\sum_(j <- arrivals_between arr_seq t (t + Δ) | hep_task
(job_task
j)
tsk &&
(job_task
j
!= tsk))
job_cost j <=
\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job P := fun x : Job =>
hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
\sum_(j <- arrivals_between arr_seq t (t + Δ) | hep_task
(job_task
j)
tsk &&
(job_task
j
!= tsk))
job_cost j <=
\sum_(j <- l | P j)
\sum_(i <- ts | hep_task i tsk && (i != tsk) &&
(job_task j == i)) job_cost j
rewrite /P /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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job P := fun x : Job =>
hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
\sum_(i <- l | [&& i \in l, hep_task (job_task i) tsk
& job_task i != tsk]) job_cost i <=
\sum_(i <- l | [&& i \in l, hep_task (job_task i) tsk
& job_task i != tsk])
\sum_(i0 <- ts | hep_task i0 tsk && (i0 != tsk) &&
(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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job P := fun x : Job =>
hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk &&
(job_task j0 != tsk)
job_cost j0 <=
\sum_(i <- ts | hep_task i tsk && (i != tsk) &&
(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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job P := fun x : Job =>
hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk &&
(job_task j0 != tsk)
job_cost j0 <=
addn_comoid
(if
hep_task (job_task j0) tsk && (job_task j0 != tsk) &&
(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
hep_task y tsk && (y != tsk) &&
(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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job P := fun x : Job =>
hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk &&
(job_task j0 != tsk)
job_cost j0 <=
addn_comoid
(if
hep_task (job_task j0) tsk && (job_task j0 != tsk) &&
(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
hep_task y tsk && (y != tsk) &&
(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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job P := fun x : Job =>
hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk &&
(job_task j0 != tsk)
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job P := fun x : Job =>
hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk &&
(job_task j0 != tsk)
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <=
total_ohep_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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
\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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
\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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
\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 /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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_task
i ==
tsk0)
task_cost tsk0 * 1
rewrite muln1 /l /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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
\sum_(j0 <- \cat_(t<=t<t + Δ)arrivals_at arr_seq t |
job_task j0 == tsk0) job_cost j0 <=
\sum_(i <- \cat_(t<=t<t + Δ)arrivals_at arr_seq t |
job_task i == tsk0) 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk) 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk && (tsk0 != tsk)
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 prove that total workload of all tasks with higher-or-equal
priority is no larger than the total request bound function. *)
Lemma total_workload_le_total_hep_rbf :
total_hep_workload t (t + Δ) <= total_hep_rbf Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_hep_workload t (t + Δ) <= total_hep_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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_hep_workload t (t + Δ) <= total_hep_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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
total_hep_workload t (t + Δ) <= total_hep_rbf Δ
apply (@leq_trans (\sum_(tsk' <- ts | hep_task tsk' tsk)
(\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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
total_hep_workload t (t + Δ) <=
\sum_(tsk' <- ts | hep_task tsk' tsk)
\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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
total_hep_workload t (t + Δ) <=
\sum_(tsk' <- ts | hep_task tsk' tsk)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
workload_of_jobs
(fun j_other : Job =>
hep_task (job_task j_other) tsk)
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(tsk' <- ts | hep_task tsk' tsk)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
have EXCHANGE := exchange_big_dep (fun x => hep_task (job_task x) tsk).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job EXCHANGE : forall (T : Type )
(y : T) (c : Monoid.com_law y)
(T0 : Type )
(j : JobType)
(l : seq T0)
(l0 : seq j)
(p : pred T0)
(p0 : T0 -> pred j)
(f : FP_policy Task)
(j0 : JobTask j Task)
(F : T0 -> j -> T),
(forall (i : T0) (j1 : j),
p i ->
p0 i j1 -> hep_task (job_task j1) tsk) ->
\big[c/y]_(i <- l |
p i) \big[c/y]_(j1 <- l0 | p0 i j1) F i j1 =
\big[c/y]_(j1 <- l0 |
hep_task (job_task j1) tsk)
\big[c/y]_(i <- l |
p i && p0 i j1)
F i j1
workload_of_jobs
(fun j_other : Job =>
hep_task (job_task j_other) tsk)
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(tsk' <- ts | hep_task tsk' tsk)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
workload_of_jobs
(fun j_other : Job =>
hep_task (job_task j_other) tsk)
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(j <- l | hep_task (job_task j) tsk)
\sum_(i <- ts | hep_task i tsk && (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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(i <- l | (i \in l) && hep_task (job_task i) tsk)
job_cost i <=
\sum_(i <- l | (i \in l) && hep_task (job_task i) tsk)
\sum_(i0 <- ts | hep_task i0 tsk &&
(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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk
job_cost j0 <=
\sum_(i <- ts | hep_task i tsk && (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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk
job_cost j0 <=
addn_comoid
(if
hep_task (job_task j0) tsk &&
(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 hep_task y tsk && (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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk
job_cost j0 <=
addn_comoid
(if
hep_task (job_task j0) tsk &&
(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 hep_task y tsk && (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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : hep_task (job_task j0) tsk
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(tsk' <- ts | hep_task tsk' tsk)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <=
total_hep_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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
\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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
\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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
\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.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_task
i ==
tsk0)
task_cost tsk0 * 1
rewrite -/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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
\sum_(i <- l | job_task i == tsk0) task_cost tsk0
apply leq_sum_seq; move => 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk 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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
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_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq PState : Type H3 : ProcessorState Job PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H4 : FP_policy Task jlfp_higher_eq_priority := FP_to_JLFP Job Task : JLFP_policy Job 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 H5 : 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 total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat t, Δ : instant j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk other_higher_eq_priority := fun j1 j2 : Job =>
jlfp_higher_eq_priority j1
j2 && ~~ same_task j1 j2: Job -> Job -> bool total_hep_workload := fun t1 t2 : instant =>
workload_of_jobs
(jlfp_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_ohep_workload := fun t1 t2 : instant =>
workload_of_jobs
(other_higher_eq_priority^~ j)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : hep_task tsk0 tsk
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 .
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_task j = tsk.
(** Then we prove that [task_rbf 1] is greater than or equal to task cost. *)
Lemma task_rbf_1_ge_task_cost :
task_rbf 1 >= 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_task j = tsk
task_cost tsk <= task_rbf 1
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk
task_cost tsk <= task_rbf 1
have ALT: forall n , n = 0 \/ n > 0 by clear ; intros n; destruct n; [left | right ].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk ALT : forall n : nat, n = 0 \/ 0 < n
task_cost tsk <= task_rbf 1
specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk POS : 0 < task_cost tsk
task_cost tsk <= task_rbf 1
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_task j = tsk POS : 0 < task_cost tskCONTR : task_rbf 1 < 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_task j = tsk POS : 0 < task_cost tskCONTR : task_rbf 1 < task_cost tsk ARRB : respects_max_arrivals arr_seq tsk
(max_arrivals tsk)
False
specialize (ARRB (job_arrival j) (job_arrival j + 1 )).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_task j = tsk POS : 0 < task_cost tskCONTR : task_rbf 1 < task_cost tsk ARRB : job_arrival j <= job_arrival j + 1 ->
number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + 1 ) <=
max_arrivals tsk
(job_arrival j + 1 - 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_task j = tsk POS : 0 < task_cost tskCONTR : task_rbf 1 < task_cost tsk ARRB : number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + 1 ) <=
max_arrivals tsk
(job_arrival j + 1 - 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_task j = tsk POS : 0 < task_cost tskARRB : number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + 1 ) <=
max_arrivals tsk
(job_arrival j + 1 - job_arrival j)
task_cost tsk * max_arrivals tsk 1 < 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_task j = tsk POS : 0 < task_cost tskARRB : number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + 1 ) <=
max_arrivals tsk
(job_arrival j + 1 - job_arrival j) CONTR : max_arrivals tsk 1 < 1
False
move : CONTR; rewrite -addn1 -{3 }[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_task j = tsk POS : 0 < task_cost tskARRB : number_of_task_arrivals arr_seq tsk
(job_arrival j)
(job_arrival j + 1 ) <=
max_arrivals tsk
(job_arrival j + 1 - job_arrival j) CONTR : max_arrivals tsk 1 = 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_task j = tsk POS : 0 < task_cost tskCONTR : max_arrivals tsk 1 = 0
0 <
number_of_task_arrivals arr_seq tsk (job_arrival j)
(job_arrival j + 1 )
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_task j = tsk POS : 0 < task_cost tskCONTR : max_arrivals tsk 1 = 0
has predT
[seq j <- arrivals_between arr_seq (job_arrival j)
(job_arrival j + 1 )
| job_task j == tsk]
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_task j = tsk POS : 0 < task_cost tskCONTR : max_arrivals tsk 1 = 0
j
\in [seq j <- arrivals_between arr_seq
(job_arrival j) (job_arrival j + 1 )
| job_task j == tsk]
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_task j = tsk POS : 0 < task_cost tskCONTR : max_arrivals tsk 1 = 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_task j == tsk]
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_task j = tsk POS : 0 < task_cost tskCONTR : max_arrivals tsk 1 = 0
(job_task j == tsk) &&
(j \in arrivals_at arr_seq (job_arrival j))
apply /andP; split ; first by 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 j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk POS : 0 < task_cost tskCONTR : max_arrivals tsk 1 = 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_task j = tsk POS : 0 < task_cost tskCONTR : max_arrivals tsk 1 = 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_task j = tsk POS : 0 < task_cost tskCONTR : max_arrivals tsk 1 = 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 .
(** 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_task j = tsk ts : seq Task H_tsk_in_ts : tsk \in ts
forall t : nat,
0 < t ->
task_cost tsk <= total_request_bound_function ts t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk ts : 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_task j = tsk ts : 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_task j = tsk ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_cost tsk <= total_request_bound_function ts t.+1
eapply leq_trans; first by apply task_rbf_1_ge_task_cost; eauto with basic_facts.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_task j = tsk ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf 1 <= total_request_bound_function ts t.+1
rewrite /total_request_bound_function.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf 1 <=
\sum_(tsk <- ts) task_request_bound_function tsk t.+1
erewrite big_rem; last by exact H_tsk_in_ts.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_task j = tsk ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf 1 <=
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_task j = tsk ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf 1 <= task_request_bound_function tsk t.+1
by apply task_rbf_monotone.
Qed .
End RequestBoundFunctions .