Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.model.workload.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.model.arrival_curves.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.util.tactics.
Require Export prosa.analysis.definitions.workload.bounded.
(** * Facts about Request Bound Functions (RBFs) *)
(** In this file, we prove some lemmas about request bound functions. *)
(** ** RBF is a Bound on Workload *)
(** First, we show that a task's RBF is indeed an upper bound on its
workload. *)
Section ProofWorkloadBound .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any arrival sequence with consistent, non-duplicate arrivals, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... any schedule corresponding to this arrival sequence, ... *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... and an FP policy that indicates a higher-or-equal priority relation. *)
Context `{FP_policy Task}.
(** Further, consider a task set [ts]... *)
Variable ts : seq Task.
(** ... and let [tsk] be any task in [ts]. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Assume that the job costs are no larger than the task costs ... *)
Hypothesis H_valid_job_cost :
arrivals_have_valid_job_costs arr_seq.
(** ... and that all jobs come from the task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** Let [max_arrivals] be any arrival bound for task-set [ts]. *)
Context `{MaxArrivals Task}.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
(** Next, recall the notions of total workload of jobs... *)
Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2).
(** ... and the workload of jobs of the same task as job j. *)
Let task_workload t1 t2 :=
workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).
(** Finally, let us define some local names for clarity. *)
Let rbf := task_request_bound_function.
Let total_rbf := total_request_bound_function ts.
Let total_hep_rbf := total_hep_request_bound_function_FP ts.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts.
(** In this section, we prove that the workload of all jobs is
no larger than the request bound function. *)
Section WorkloadIsBoundedByRBF .
(** Consider any time [t] and any interval of length [Δ]. *)
Variable t : instant.
Variable Δ : instant.
(** First, we show that workload of task [tsk] is bounded by the number of
arrivals of the task times the cost of the task. *)
Lemma task_workload_le_num_of_arrivals_times_cost :
task_workload t (t + Δ)
<= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
task_workload t (t + Δ) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t (t + Δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
task_workload t (t + Δ) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t (t + Δ)
rewrite /task_workload /workload_of_jobs/ number_of_task_arrivals
/task_arrivals_between -big_filter -sum1_size big_distrr big_filter.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk i)
job_cost i <=
\big[ssrnat_addn__canonical__Monoid_AddLaw/0 ]_(i <- [
seq j <- arrivals_between arr_seq t (t + Δ)
| job_of_task tsk j])
ssrnat_muln__canonical__Monoid_MulLaw
(task_cost tsk) 1
destruct (task_arrivals_between arr_seq tsk t (t + Δ)) eqn :TASK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> 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[ssrnat_addn__canonical__Monoid_AddLaw/0 ]_(i <- [
seq j <- arrivals_between arr_seq t (t + Δ)
| job_of_task tsk j])
ssrnat_muln__canonical__Monoid_MulLaw
(task_cost tsk) 1
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> 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[ssrnat_addn__canonical__Monoid_AddLaw/0 ]_(i <- [
seq j <- arrivals_between arr_seq t (t + Δ)
| job_of_task tsk j])
ssrnat_muln__canonical__Monoid_MulLaw
(task_cost tsk) 1
unfold task_arrivals_between in TASK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant TASK : [seq j <-
arrivals_between arr_seq t (t + Δ)
| job_of_task tsk j] = [::]
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk i)
job_cost i <=
\big[ssrnat_addn__canonical__Monoid_AddLaw/0 ]_(i <- [
seq j <- arrivals_between arr_seq t (t + Δ)
| job_of_task tsk j])
ssrnat_muln__canonical__Monoid_MulLaw
(task_cost tsk) 1
by rewrite -big_filter !TASK !big_nil. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> 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[ssrnat_addn__canonical__Monoid_AddLaw/0 ]_(i <- [
seq j <- arrivals_between arr_seq t (t + Δ)
| job_of_task tsk j])
ssrnat_muln__canonical__Monoid_MulLaw
(task_cost tsk) 1
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> 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[ssrnat_addn__canonical__Monoid_AddLaw/0 ]_(i <- [
seq j <- arrivals_between arr_seq t (t + Δ)
| job_of_task tsk j])
ssrnat_muln__canonical__Monoid_MulLaw
(task_cost tsk) 1
rewrite //= big_filter big_seq_cond [in X in _ <= X]big_seq_cond.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
job_of_task
tsk i)
job_cost i <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
job_of_task
tsk i)
task_cost tsk * 1
apply leq_sum.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l
forall i : Job,
(i \in arrivals_between arr_seq t (t + Δ)) &&
job_of_task tsk i -> job_cost i <= task_cost tsk * 1
move => j' /andP [IN TSKj'].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l j' : Job IN : j' \in arrivals_between arr_seq t (t + Δ) TSKj' : job_of_task tsk j'
job_cost j' <= task_cost tsk * 1
rewrite muln1.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l j' : Job IN : j' \in arrivals_between arr_seq t (t + Δ) TSKj' : job_of_task tsk j'
job_cost j' <= task_cost tsk
move : TSKj' => /eqP TSKj'; rewrite -TSKj'.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant s : Job l : seq Job TASK : task_arrivals_between arr_seq tsk t (t + Δ) =
s :: l j' : Job IN : j' \in arrivals_between arr_seq t (t + Δ) TSKj' : job_task j' = tsk
job_cost j' <= task_cost (job_task j')
apply H_valid_job_cost.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> 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 + Δ) <= rbf tsk Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
task_workload t (t + Δ) <= rbf tsk Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
task_workload t (t + Δ) <= rbf tsk Δ
eapply leq_trans; first by apply task_workload_le_num_of_arrivals_times_cost.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
task_cost tsk *
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
rbf tsk Δ
rewrite leq_mul2l; apply /orP; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
max_arrivals tsk Δ
rewrite -{2 }[Δ](addKn t).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
number_of_task_arrivals arr_seq tsk t (t + Δ) <=
max_arrivals tsk (t + Δ - t)
by apply H_is_arrival_bound; last rewrite leq_addr.
Qed .
(** Next, we prove that total workload of tasks is no larger than the total
request bound function. *)
Lemma total_workload_le_total_rbf :
total_workload t (t + Δ) <= total_rbf Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
total_workload t (t + Δ) <= total_rbf Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant
total_workload t (t + Δ) <= total_rbf Δ
set l := arrivals_between arr_seq t (t + Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
total_workload t (t + Δ) <= total_rbf Δ
apply (@leq_trans (\sum_(tsk' <- ts) (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
total_workload t (t + Δ) <=
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
total_workload t (t + Δ) <=
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
rewrite /total_workload.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0
have EXCHANGE := exchange_big_dep predT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job EXCHANGE : forall (T : Type )
(y : T)
(t : 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[t/y]_(i <- l |
p i) \big[t/y]_(j <- l0 | p0 i j) F i j =
\big[t/y]_(j <- l0 |
predT j)
\big[t/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.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
\sum_(j <- l)
\sum_(i <- ts | job_task j == i) job_cost j
rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(i <- l | (i \in l) && predT i) job_cost i <=
\sum_(i <- l | (i \in l) && true)
\sum_(i0 <- ts | job_task i == i0) job_cost i
apply leq_sum; move => j0 /andP [IN0 HP0].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : true
job_cost j0 <=
\sum_(i <- ts | job_task j0 == i) job_cost j0
rewrite big_mkcond (big_rem (job_task j0)) /=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> 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 )
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> 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 )
by rewrite eq_refl; apply leq_addr.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job j0 : Job IN0 : j0 \in l HP0 : true
job_task j0 \in ts
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job
\sum_(tsk' <- ts)
\sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <=
total_rbf Δ
apply leq_sum_seq; intros tsk0 INtsk0 HP0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
task_request_bound_function tsk0 Δ
apply (@leq_trans (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ))
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ))
rewrite -sum1_size big_distrr /= big_filter -/l /workload_of_jobs muln1.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <=
\sum_(i <- l | job_of_task tsk0 i) task_cost tsk0
apply leq_sum_seq => j0 IN0 /eqP <-.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true j0 : Job IN0 : j0 \in l
job_cost j0 <= task_cost (job_task j0)
apply H_valid_job_cost.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true j0 : Job IN0 : j0 \in l
arrives_in arr_seq j0
by apply in_arrivals_implies_arrived in IN0. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
task_request_bound_function tsk0 Δ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
task_request_bound_function tsk0 Δ
rewrite leq_mul2l; apply /orP; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
max_arrivals tsk0 Δ
rewrite -{2 }[Δ](addKn t).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant l := arrivals_between arr_seq t (t + Δ) : seq Job tsk0 : Task INtsk0 : tsk0 \in ts HP0 : true
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
max_arrivals tsk0 (t + Δ - t)
by apply H_is_arrival_bound; last rewrite leq_addr. }
Qed .
(** Next, we consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_job_of_tsk : job_of_task tsk j.
(** We prove that the sum of job cost of jobs whose corresponding
task satisfies a predicate [pred] is bounded by the RBF of
these tasks. *)
Lemma sum_of_jobs_le_sum_rbf :
forall (pred : pred Task),
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred (job_task j'))
job_cost j' <=
\sum_(tsk' <- ts| pred tsk')
task_request_bound_function tsk' Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j
forall pred : pred Task,
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j
forall pred : pred Task,
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
move => pred.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
apply (@leq_trans (\sum_(tsk' <- filter pred ts)
(\sum_(j' <- arrivals_between arr_seq t (t + Δ)
| job_task j' == tsk') job_cost j'))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j'
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j'
move : (H_job_of_tsk) => /eqP TSK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j'
rewrite [X in _ <= X]big_filter.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(i <- ts | pred i)
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == i) job_cost j'
set P := fun x => pred (job_task x).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(i <- ts | pred i)
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == i) job_cost j'
rewrite (exchange_big_dep P) //=; last by rewrite /P; move => ???/eqP->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred
(job_task
j'))
job_cost j' <=
\sum_(j <- arrivals_between arr_seq t (t + Δ) | P j)
\sum_(i <- ts | pred i && (job_task j == i))
job_cost j
rewrite /P /workload_of_jobs big_seq_cond [X in _ <= X]big_seq_cond.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
pred
(job_task
i))
job_cost i <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i
\in
arrivals_between
arr_seq
t
(t +
Δ)) &&
pred
(job_task
i))
\sum_(i0 <- ts | pred i0 && (job_task i == i0))
job_cost i
apply leq_sum => j0 /andP [IN0 HP0].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_cost j0 <=
\sum_(i <- ts | pred i && (job_task j0 == i))
job_cost j0
rewrite big_mkcond (big_rem (job_task j0)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_cost j0 <=
ssrnat_addn__canonical__Monoid_ComLaw
(if
pred (job_task j0) && (job_task j0 == job_task j0)
then job_cost j0
else 0 )
(\big[ssrnat_addn__canonical__Monoid_ComLaw/0 ]_(y <-
rem (T:=Task) (job_task j0) ts)
(if pred y && (job_task j0 == y)
then job_cost j0
else 0 ))
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_cost j0 <=
ssrnat_addn__canonical__Monoid_ComLaw
(if
pred (job_task j0) && (job_task j0 == job_task j0)
then job_cost j0
else 0 )
(\big[ssrnat_addn__canonical__Monoid_ComLaw/0 ]_(y <-
rem (T:=Task) (job_task j0) ts)
(if pred y && (job_task j0 == y)
then job_cost j0
else 0 ))
by rewrite HP0 andTb eq_refl; apply leq_addr.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task TSK : job_task j = tsk P := fun x : Job => pred (job_task x): Job -> bool j0 : Job IN0 : j0 \in arrivals_between arr_seq t (t + Δ) HP0 : pred (job_task j0)
job_task j0 \in ts
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(tsk' <- [seq x <- ts | pred x])
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == tsk') job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
rewrite big_filter.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task
\sum_(i <- ts | pred i)
\sum_(j' <- arrivals_between arr_seq t (t + Δ) |
job_task j' == i) job_cost j' <=
\sum_(tsk' <- ts | pred tsk')
task_request_bound_function tsk' Δ
apply leq_sum_seq => tsk0 INtsk0 HP0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | job_task
j' ==
tsk0)
job_cost j' <= task_request_bound_function tsk0 Δ
apply (@leq_trans (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | job_task
j' ==
tsk0)
job_cost j' <=
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ))
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | job_task
j' ==
tsk0)
job_cost j' <=
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ))
rewrite -sum1_size big_distrr /= big_filter /workload_of_jobs.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | job_task
j' ==
tsk0)
job_cost j' <=
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task
tsk0
i)
task_cost tsk0 * 1
rewrite muln1 /arrivals_between /arrival_sequence.arrivals_between.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
\sum_(j' <- \cat_(t<=t<t + Δ)arrivals_at arr_seq t |
job_task j' == tsk0) job_cost j' <=
\sum_(i <- \cat_(t<=t<t + Δ)arrivals_at arr_seq t |
job_of_task tsk0 i) task_cost tsk0
apply leq_sum_seq; move => j0 IN0 /eqP EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0 j0 : Job IN0 : j0 \in \cat_(t<=t<t + Δ)arrivals_at arr_seq t EQ : job_task j0 = tsk0
job_cost j0 <= task_cost tsk0
by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
task_cost tsk0 *
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
task_request_bound_function tsk0 Δ
rewrite leq_mul2l; apply /orP; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
max_arrivals tsk0 Δ
rewrite -{2 }[Δ](addKn t).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred : ssrbool.pred Task tsk0 : Task INtsk0 : tsk0 \in ts HP0 : pred tsk0
size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <=
max_arrivals tsk0 (t + Δ - t)
by apply H_is_arrival_bound; last by rewrite leq_addr.
Qed .
(** Using lemma [sum_of_jobs_le_sum_rbf], we prove that the
workload of higher-or-equal priority jobs (w.r.t. task [tsk])
is no larger than the total request-bound function of
higher-or-equal priority tasks. *)
Lemma hep_workload_le_total_hep_rbf :
workload_of_hep_jobs arr_seq j t (t + Δ) <= total_hep_rbf tsk Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_hep_rbf tsk Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_hep_rbf tsk Δ
rewrite /workload_of_hep_jobs /workload_of_jobs /total_hep_rbf /total_hep_request_bound_function_FP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j
\sum_(j0 <- arrivals_between arr_seq t (t + Δ) | hep_job
j0 j)
job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk)
task_request_bound_function tsk_other Δ
rewrite /another_task_hep_job /hep_job /FP_to_JLFP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j
\sum_(j0 <- arrivals_between arr_seq t (t + Δ) | hep_task
(job_task
j0)
(job_task
j))
job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk)
task_request_bound_function tsk_other Δ
set (pred_task tsk_other := hep_task tsk_other tsk).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred_task := hep_task^~ tsk : Task -> bool
\sum_(j0 <- arrivals_between arr_seq t (t + Δ) | hep_task
(job_task
j0)
(job_task
j))
job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk)
task_request_bound_function tsk_other Δ
rewrite (eq_big (fun j => pred_task (job_task j)) job_cost) //;
last by move => j'; rewrite /pred_task; move : H_job_of_tsk => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred_task := hep_task^~ tsk : Task -> bool
\sum_(i <- arrivals_between arr_seq t (t + Δ) | pred_task
(job_task
i))
job_cost i <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk)
task_request_bound_function tsk_other Δ
erewrite (eq_big pred_task); [|by done |by move => tsk'; eauto ].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat t, Δ : instant j : Job H_job_of_tsk : job_of_task tsk j pred_task := hep_task^~ tsk : Task -> bool
\sum_(i <- arrivals_between arr_seq t (t + Δ) | pred_task
(job_task
i))
job_cost i <=
\sum_(i <- ts | pred_task i)
(task_request_bound_function^~ Δ) i
by apply : sum_of_jobs_le_sum_rbf.
Qed .
End WorkloadIsBoundedByRBF .
(** We next prove that the higher-or-equal-priority workload of
tasks different from [tsk] is bounded by [total_ohep_rbf].
The [athep_workload_is_bounded] predicate allows the workload
bound to depend on two arguments: the relative offset [A]
(w.r.t. the beginning of the corresponding busy interval) of a
job to be analyzed and the length of an interval [Δ]. In the
case of FP and [total_ohep_rbf] function, the relative offset
([A]) does not play a role and is therefore ignored. *)
Lemma athep_workload_le_total_ohep_rbf :
athep_workload_is_bounded
arr_seq sched tsk (fun (A Δ : duration) => total_ohep_rbf tsk Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat
athep_workload_is_bounded arr_seq sched tsk
(fun => [eta total_ohep_rbf tsk])
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat
athep_workload_is_bounded arr_seq sched tsk
(fun => [eta total_ohep_rbf tsk])
move => j t1 Δ POS TSK _.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
total_ohep_rbf tsk Δ
rewrite /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
another_task_hep_job j0 j) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
rewrite /another_task_hep_job /hep_job /FP_to_JLFP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
hep_task (job_task j0) (job_task j) &&
(job_task j0 != job_task j)) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
set (pred_task tsk_other := hep_task tsk_other tsk && (tsk_other != tsk)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
hep_task (job_task j0) (job_task j) &&
(job_task j0 != job_task j)) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
rewrite (eq_big (fun j => pred_task (job_task j)) job_cost) //;
last by move => j'; rewrite /pred_task; move : TSK => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(i <- arrivals_between arr_seq t1 (t1 + Δ) |
pred_task (job_task i)) job_cost i <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
erewrite (eq_big pred_task) => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H3 : FP_policy Task ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat task_workload := fun t1 t2 : instant =>
workload_of_jobs
(job_of_task tsk)
(arrivals_between arr_seq t1 t2): instant -> instant -> nat rbf := task_request_bound_function : Task -> duration -> nat total_rbf := total_request_bound_function ts : duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts : Task -> duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts : Task -> duration -> nat j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(i <- arrivals_between arr_seq t1 (t1 + Δ) |
pred_task (job_task i)) job_cost i <=
\sum_(i <- ts | pred_task i)
(task_request_bound_function^~ Δ) i
by eapply sum_of_jobs_le_sum_rbf => //.
Qed .
End ProofWorkloadBound .
(** In this section, we show that total RBF is a bound on
higher-or-equal priority workload under any JLFP policy. *)
Section TotalRBFBound .
(** 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 a JLFP policy that indicates a higher-or-equal priority
relation ... *)
Context `{JLFP_policy Job}.
(** ... and any valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Further, consider a task set [ts]. *)
Variable ts : seq Task.
(** 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.
(** Consider any time [t] and any interval of length [Δ]. *)
Variable t : instant.
Variable Δ : duration.
(** Next, we consider any job [j]. *)
Variable j : Job.
(** A simple consequence of lemma [hep_workload_le_total_hep_rbf] is
that the workload of higher-or-equal priority jobs is bounded by
the total request-bound function. *)
Corollary hep_workload_le_total_rbf :
workload_of_hep_jobs arr_seq j t (t + Δ)
<= total_request_bound_function ts Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : duration j : Job
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_request_bound_function ts Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : duration j : Job
workload_of_hep_jobs arr_seq j t (t + Δ) <=
total_request_bound_function ts Δ
rewrite /workload_of_hep_jobs (leqRW (workload_of_jobs_weaken _ predT _ _ )); last by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H4 : MaxArrivals Task H_is_arrival_bound : taskset_respects_max_arrivals
arr_seq ts t : instant Δ : duration j : Job
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
total_request_bound_function ts Δ
by apply total_workload_le_total_rbf.
Qed .
End TotalRBFBound .
(** ** 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 .
(** In the following, we assume that [tsk] has a positive cost ... *)
Hypothesis H_positive_cost : 0 < task_cost tsk.
(** ... and [max_arrivals tsk ε] is positive. *)
Hypothesis H_arrival_curve_positive : max_arrivals tsk ε > 0 .
(** Then we prove that [task_rbf] at [ε] is greater than or equal to the task's WCET. *)
Lemma task_rbf_1_ge_task_cost :
task_rbf ε >= task_cost tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
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 H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
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 H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ALT : forall n : nat, n = 0 \/ 0 < n
task_cost tsk <= task_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 H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 POS : 0 < task_cost tsk
task_cost tsk <= task_rbf 1
rewrite -[task_cost tsk]muln1 /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 H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 POS : 0 < task_cost tsk
task_cost tsk * 1 <=
task_cost tsk * max_arrivals tsk 1
by rewrite leq_pmul2l //=.
Qed .
(** As a corollary, we prove that the [task_rbf] at any point [A] greater than
[0] is no less than the task's WCET. *)
Lemma task_rbf_ge_task_cost :
forall A ,
A > 0 ->
task_rbf A >= task_cost tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
forall A : nat, 0 < A -> task_cost tsk <= task_rbf A
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
forall A : nat, 0 < A -> task_cost tsk <= task_rbf A
case => // A GEQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 A : nat GEQ : 0 < A.+1
task_cost tsk <= task_rbf A.+1
apply : (leq_trans task_rbf_1_ge_task_cost).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 A : nat GEQ : 0 < A.+1
task_rbf 1 <= task_rbf A.+1
exact : task_rbf_monotone.
Qed .
(** Then, we prove that [task_rbf] at [ε] is greater than [0]. *)
Lemma task_rbf_epsilon_gt_0 : 0 < task_rbf ε.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
0 < 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 H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
0 < task_rbf 1
apply leq_trans with (task_cost tsk) => [//|].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1
task_cost tsk <= task_rbf 1
exact : task_rbf_1_ge_task_cost.
Qed .
(** Consider a set of tasks [ts] containing the task [tsk]. *)
Variable ts : seq Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Next, we prove that cost of [tsk] is less than or equal to the
[total_request_bound_function]. *)
Lemma task_cost_le_sum_rbf :
forall t ,
t > 0 ->
task_cost tsk <= total_request_bound_function ts t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts
forall t : nat,
0 < t ->
task_cost tsk <= total_request_bound_function ts t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts
forall t : nat,
0 < t ->
task_cost tsk <= total_request_bound_function ts t
case => [//|t] GE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_cost tsk <= total_request_bound_function ts t.+1
eapply leq_trans; first exact : task_rbf_1_ge_task_cost.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_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 H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_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 H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf 1 <=
ssrnat_addn__canonical__Monoid_ComLaw
(task_request_bound_function tsk t.+1 )
(\big[ssrnat_addn__canonical__Monoid_ComLaw/0 ]_(y <-
rem (T:=Task) tsk ts)
task_request_bound_function y t.+1 )
apply leq_trans with (task_request_bound_function tsk t.+1 ); last by apply leq_addr.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq tsk : Task H2 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) task_rbf := task_request_bound_function tsk : duration -> nat H_positive_cost : 0 < task_cost tskH_arrival_curve_positive : 0 < max_arrivals tsk 1 ts : seq Task H_tsk_in_ts : tsk \in ts t : nat GE : 0 < t.+1
task_rbf 1 <= task_request_bound_function tsk t.+1
by apply task_rbf_monotone.
Qed .
End RequestBoundFunctions .
(** ** Monotonicity of the Total RBF *)
(** In the following section, we note some trivial facts about the monotonicity
of various total RBF variants. *)
Section TotalRBFMonotonic .
(** Consider a set of tasks characterized by WCETs and arrival curves. *)
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
(** We observe that the total RBF is monotonically increasing. *)
Lemma total_rbf_monotone :
monotone leq (total_request_bound_function ts).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals
monotone leq (total_request_bound_function ts)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals
monotone leq (total_request_bound_function ts)
by apply : sum_leq_mono => tsk IN; apply : task_rbf_monotone. Qed .
(** Furthermore, for any fixed-priority policy, ... *)
Context `{FP_policy Task}.
(** ... the total RBF of higher- or equal-priority tasks is also monotonic, ... *)
Lemma total_hep_rbf_monotone :
forall tsk ,
monotone leq (total_hep_request_bound_function_FP ts tsk).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
monotone leq
(total_hep_request_bound_function_FP ts tsk)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
monotone leq
(total_hep_request_bound_function_FP ts tsk)
move => tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
monotone leq
(total_hep_request_bound_function_FP ts tsk)
apply : sum_leq_mono => tsk' IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk' \in ts
monotone leq (task_request_bound_function tsk')
exact : task_rbf_monotone.
Qed .
(** ... as is the variant that excludes the reference task. *)
Lemma total_ohep_rbf_monotone :
forall tsk ,
monotone leq (total_ohep_request_bound_function_FP ts tsk).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
monotone leq
(total_ohep_request_bound_function_FP ts tsk)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
monotone leq
(total_ohep_request_bound_function_FP ts tsk)
move => tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
monotone leq
(total_ohep_request_bound_function_FP ts tsk)
apply : sum_leq_mono => tsk' IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk' \in ts
monotone leq (task_request_bound_function tsk')
exact : task_rbf_monotone.
Qed .
End TotalRBFMonotonic .
(** ** RBFs Equal to Zero for Duration ε *)
(** In the following section, we derive simple properties that follow in
the pathological case of an RBF that yields zero for duration ε. *)
Section DegenerateTotalRBFs .
(** Consider a set of tasks characterized by WCETs and arrival curves ... *)
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
(** ... and any consistent arrival sequence of valid jobs of these tasks. *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobCost Job}.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Suppose the arrival curves are correct. *)
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Consider any valid schedule corresponding to this arrival sequence. *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_jobs_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq.
(** First, we observe that, if a task's RBF is zero for a duration [ε], then it
trivially has a response-time bound of zero. *)
Lemma pathological_rbf_response_time_bound :
forall tsk ,
tsk \in ts ->
task_request_bound_function tsk ε = 0 ->
task_response_time_bound arr_seq sched tsk 0 .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq
forall tsk : Task,
tsk \in ts ->
task_request_bound_function tsk 1 = 0 ->
task_response_time_bound arr_seq sched tsk 0
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq
forall tsk : Task,
tsk \in ts ->
task_request_bound_function tsk 1 = 0 ->
task_response_time_bound arr_seq sched tsk 0
move => tsk IN ZERO j ARR TASK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts ZERO : task_request_bound_function tsk 1 = 0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
job_response_time_bound sched j 0
rewrite /job_response_time_bound/completed_by.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts ZERO : task_request_bound_function tsk 1 = 0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
job_cost j <= service sched j (job_arrival j + 0 )
move : ZERO.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_request_bound_function tsk 1 = 0 ->
job_cost j <= service sched j (job_arrival j + 0 )
rewrite /task_request_bound_function => /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_cost tsk * max_arrivals tsk 1 == 0 ->
job_cost j <= service sched j (job_arrival j + 0 )
rewrite muln_eq0 => /orP [/eqP COST|/eqP NEVER].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
job_cost j <= service sched j (job_arrival j + 0 )
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
job_cost j <= service sched j (job_arrival j + 0 )
apply : leq_trans.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
job_cost j <= ?Goal0
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
job_cost j <= ?Goal0
by apply : H_valid_job_cost.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j COST : task_cost tsk = 0
task_cost (job_task j) <=
service sched j (job_arrival j + 0 )
move : TASK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j COST : task_cost tsk = 0
job_of_task tsk j ->
task_cost (job_task j) <=
service sched j (job_arrival j + 0 )
rewrite /job_of_task => /eqP ->.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j COST : task_cost tsk = 0
task_cost tsk <= service sched j (job_arrival j + 0 )
by rewrite COST. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j NEVER : max_arrivals tsk 1 = 0
job_cost j <= service sched j (job_arrival j + 0 )
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j NEVER : max_arrivals tsk 1 = 0
job_cost j <= service sched j (job_arrival j + 0 )
exfalso .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j NEVER : max_arrivals tsk 1 = 0
False
have : 0 < max_arrivals tsk ε
by apply : (non_pathological_max_arrivals tsk arr_seq _ j).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j NEVER : max_arrivals tsk 1 = 0
0 < max_arrivals tsk 1 -> False
by rewrite NEVER. }
Qed .
(** Second, given a fixed-priority policy with reflexive priorities, ... *)
Context {FP : FP_policy Task}.
Hypothesis H_reflexive : reflexive_task_priorities FP.
(** ... if the total RBF of all equal- and higher-priority tasks is zero, then
the reference task's response-time bound is also trivially zero. *)
Lemma pathological_total_hep_rbf_response_time_bound :
forall tsk ,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk ε = 0 ->
task_response_time_bound arr_seq sched tsk 0 .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk 1 = 0 ->
task_response_time_bound arr_seq sched tsk 0
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk 1 = 0 ->
task_response_time_bound arr_seq sched tsk 0
move => tsk IN ZERO j ARR TASK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
job_response_time_bound sched j 0
apply : pathological_rbf_response_time_bound; eauto .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_request_bound_function tsk 1 = 0
apply /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
task_request_bound_function tsk 1 == 0
move : ZERO => /eqP; rewrite sum_nat_eq0_nat => /allP; apply .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts j : Job ARR : arrives_in arr_seq j TASK : job_of_task tsk j
tsk \in [seq x <- ts | hep_task x tsk]
rewrite mem_filter; apply /andP; split => //.
Qed .
(** Thus we we can prove any response-time bound from such a pathological
case, which is useful to eliminate this case in higher-level analyses. *)
Corollary pathological_total_hep_rbf_any_bound :
forall tsk ,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk ε = 0 ->
forall R ,
task_response_time_bound arr_seq sched tsk R.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk 1 = 0 ->
forall R : duration,
task_response_time_bound arr_seq sched tsk R
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP
forall tsk : Task,
tsk \in ts ->
total_hep_request_bound_function_FP ts tsk 1 = 0 ->
forall R : duration,
task_response_time_bound arr_seq sched tsk R
move => tsk IN ZERO R.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 R : duration
task_response_time_bound arr_seq sched tsk R
move : (pathological_total_hep_rbf_response_time_bound tsk IN ZERO).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 R : duration
task_response_time_bound arr_seq sched tsk 0 ->
task_response_time_bound arr_seq sched tsk R
rewrite /task_response_time_bound/job_response_time_bound => COMP j INj TASK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 R : duration COMP : forall j : Job,
arrives_in arr_seq j ->
job_of_task tsk j ->
completed_by sched j (job_arrival j + 0 )j : Job INj : arrives_in arr_seq j TASK : job_of_task tsk j
completed_by sched j (job_arrival j + R)
apply : completion_monotonic; last by apply : COMP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts PState : ProcessorState Job sched : schedule PState H_jobs_from_arr_seq : jobs_come_from_arrival_sequence
sched arr_seq FP : FP_policy Task H_reflexive : reflexive_task_priorities FP tsk : Task IN : tsk \in ts ZERO : total_hep_request_bound_function_FP ts tsk 1 =
0 R : duration COMP : forall j : Job,
arrives_in arr_seq j ->
job_of_task tsk j ->
completed_by sched j (job_arrival j + 0 )j : Job INj : arrives_in arr_seq j TASK : job_of_task tsk j
job_arrival j + 0 <= job_arrival j + R
by lia .
Qed .
End DegenerateTotalRBFs .
(** In this section, we establish results about the task-wise partitioning of
total RBFs of multiple tasks. *)
Section FP_RBF_partitioning .
(** Consider any type of tasks ... *)
Context {Task : TaskType} `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks, where each task has
a cost and an associated arrival curve. *)
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{MaxArrivals Task}.
(** Consider an FP policy that indicates a higher-or-equal priority
relation. *)
Context `{FP : FP_policy Task}.
(** Consider a task set ts... *)
Variable ts : seq Task.
(** ...and let [tsk] be any task that serves as the reference point for
"higher or equal priority" (usually, but not necessarily, from [ts]). *)
Variable tsk : Task.
(** We establish that the bound on the total workload due to
higher-or-equal-priority tasks can be partitioned task-wise.
In other words, it is equal to the sum of the bound on the
total workload due to higher-priority tasks and the bound on
the total workload due to equal- priority tasks. *)
Lemma hep_rbf_taskwise_partitioning :
forall L ,
total_hep_request_bound_function_FP ts tsk L
= total_hp_request_bound_function_FP ts tsk L
+ total_ep_request_bound_function_FP ts tsk L.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task
forall L : duration,
total_hep_request_bound_function_FP ts tsk L =
total_hp_request_bound_function_FP ts tsk L +
total_ep_request_bound_function_FP ts tsk L
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task
forall L : duration,
total_hep_request_bound_function_FP ts tsk L =
total_hp_request_bound_function_FP ts tsk L +
total_ep_request_bound_function_FP ts tsk L
move => L; apply sum_split_exhaustive_mutually_exclusive_preds => t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task L : duration t : Task
hep_task t tsk = hp_task t tsk || ep_task t tsk
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task L : duration t : Task
hep_task t tsk = hp_task t tsk || ep_task t tsk
by rewrite -andb_orr orNb Bool.andb_true_r.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task L : duration t : Task
~~ (hp_task t tsk && ep_task t tsk)
rewrite !negb_and; case : (hep_task _ _) =>//=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task L : duration t : Task
~~ ~~ hep_task tsk t || ~~ hep_task tsk t
by case : (hep_task _ _)=>//.
Qed .
(** Now, assume that the priorities are reflexive. *)
Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
(** If the task set does not contain duplicates, then the total
higher-or-equal-priority RBF for any task can be split as the sum of
the total _other_ higher-or-equal-priority workload and the RBF of the
task itself. *)
Lemma split_hep_rbf :
forall Δ ,
tsk \in ts ->
uniq ts ->
total_hep_request_bound_function_FP ts tsk Δ
= total_ohep_request_bound_function_FP ts tsk Δ
+ task_request_bound_function tsk Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP
forall Δ : duration,
tsk \in ts ->
uniq ts ->
total_hep_request_bound_function_FP ts tsk Δ =
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP
forall Δ : duration,
tsk \in ts ->
uniq ts ->
total_hep_request_bound_function_FP ts tsk Δ =
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ
move => Δ IN UNIQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
total_hep_request_bound_function_FP ts tsk Δ =
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ
rewrite /total_hep_request_bound_function_FP /total_ohep_request_bound_function_FP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
\sum_(tsk_other <- ts | hep_task tsk_other tsk)
task_request_bound_function tsk_other Δ =
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ +
task_request_bound_function tsk Δ
rewrite (bigID_idem _ _ (fun tsko => tsko != tsk)) //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
\sum_(i <- ts | hep_task i tsk && (i != tsk))
task_request_bound_function i Δ +
\sum_(i <- ts | hep_task i tsk && ~~ (i != tsk))
task_request_bound_function i Δ =
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ +
task_request_bound_function tsk Δ
apply /eqP; rewrite eqn_add2l.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
\sum_(i <- ts | hep_task i tsk && ~~ (i != tsk))
task_request_bound_function i Δ ==
task_request_bound_function tsk Δ
rewrite (eq_bigl (fun i => i == tsk)); last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
(fun i : Task => hep_task i tsk && ~~ (i != tsk)) =1
eq_op^~ tsk
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
(fun i : Task => hep_task i tsk && ~~ (i != tsk)) =1
eq_op^~ tsk
move => tsko.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
hep_task tsko tsk && ~~ (tsko != tsk) = (tsko == tsk)
case (tsko == tsk) eqn : EQ; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task EQ : (tsko == tsk) = true
hep_task tsko tsk && ~~ ~~ true = true
move : EQ => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
hep_task tsk tsk && ~~ ~~ true = true
by rewrite H_priority_is_reflexive //=.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
\sum_(i <- ts | i == tsk)
task_request_bound_function i Δ ==
task_request_bound_function tsk Δ
rewrite (big_rem tsk) //= eq_refl.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
task_request_bound_function tsk Δ +
\sum_(y <- rem (T:=Task) tsk ts | y == tsk)
task_request_bound_function y Δ ==
task_request_bound_function tsk Δ
rewrite big_seq_cond big_pred0; first by rewrite addn0 //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts
(fun i : Task =>
(i \in rem (T:=Task) tsk ts) && (i == tsk)) =1 xpred0
move => tsko.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
(tsko \in rem (T:=Task) tsk ts) && (tsko == tsk) =
false
case (tsko == tsk) eqn : EQ; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task EQ : (tsko == tsk) = true
(tsko \in rem (T:=Task) tsk ts) && true = false
move : EQ => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
(tsk \in rem (T:=Task) tsk ts) && true = false
rewrite andbT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts UNIQ : uniq ts tsko : Task
(tsk \in rem (T:=Task) tsk ts) = false
by apply mem_rem_uniqF => //=.
Qed .
(** If the task set may contain duplicates, then the we can only say that
the sum of other higher-or-equal-priority [RBF] and task [tsk]'s [RBF]
is at most the total higher-or-equal-priority workload. *)
Lemma split_hep_rbf_weaken :
forall Δ ,
tsk \in ts ->
total_ohep_request_bound_function_FP ts tsk Δ + task_request_bound_function tsk Δ
<= total_hep_request_bound_function_FP ts tsk Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP
forall Δ : duration,
tsk \in ts ->
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ <=
total_hep_request_bound_function_FP ts tsk Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP
forall Δ : duration,
tsk \in ts ->
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ <=
total_hep_request_bound_function_FP ts tsk Δ
move => Δ IN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
total_ohep_request_bound_function_FP ts tsk Δ +
task_request_bound_function tsk Δ <=
total_hep_request_bound_function_FP ts tsk Δ
rewrite /total_hep_request_bound_function_FP /total_ohep_request_bound_function_FP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ +
task_request_bound_function tsk Δ <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk)
task_request_bound_function tsk_other Δ
rewrite [leqRHS](bigID_idem _ _ (fun tsko => tsko != tsk)) //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ +
task_request_bound_function tsk Δ <=
\sum_(i <- ts | hep_task i tsk && (i != tsk))
task_request_bound_function i Δ +
\sum_(i <- ts | hep_task i tsk && ~~ (i != tsk))
task_request_bound_function i Δ
apply leq_add; first by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
task_request_bound_function tsk Δ <=
\sum_(i <- ts | hep_task i tsk && ~~ (i != tsk))
task_request_bound_function i Δ
rewrite (eq_bigl (fun tsko => tsko == tsk)); last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
(fun i : Task => hep_task i tsk && ~~ (i != tsk)) =1
eq_op^~ tsk
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
(fun i : Task => hep_task i tsk && ~~ (i != tsk)) =1
eq_op^~ tsk
move => tsko.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts tsko : Task
hep_task tsko tsk && ~~ (tsko != tsk) = (tsko == tsk)
case (tsko ==tsk) eqn : TSKEQ; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts tsko : Task TSKEQ : (tsko == tsk) = true
hep_task tsko tsk && ~~ ~~ true = true
move : TSKEQ => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts tsko : Task
hep_task tsk tsk && ~~ ~~ true = true
by rewrite (H_priority_is_reflexive tsk) //=.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
task_request_bound_function tsk Δ <=
\sum_(i <- ts | i == tsk)
task_request_bound_function i Δ
rewrite (big_rem tsk) //= eq_refl.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job H2 : MaxArrivals Task FP : FP_policy Task ts : seq Task tsk : Task H_priority_is_reflexive : reflexive_task_priorities FP Δ : duration IN : tsk \in ts
task_request_bound_function tsk Δ <=
task_request_bound_function tsk Δ +
\sum_(y <- rem (T:=Task) tsk ts | y == tsk)
task_request_bound_function y Δ
by apply leq_addr.
Qed .
End FP_RBF_partitioning .
(** In this section, we state a few facts for RBFs in the context of a
fixed-priority policy. *)
Section RBFFOrFP .
(** Consider a set of tasks characterized by WCETs and arrival curves. *)
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
(** For any fixed-priority policy, ... *)
Context `{FP_policy Task}.
(** ... [total_ohep_request_bound_function_FP] at [0] is always [0]. *)
Lemma total_ohep_rbf0 :
forall (tsk : Task),
total_ohep_request_bound_function_FP ts tsk 0 = 0 .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
total_ohep_request_bound_function_FP ts tsk 0 = 0
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task
forall tsk : Task,
total_ohep_request_bound_function_FP ts tsk 0 = 0
rewrite /total_ohep_request_bound_function_FP => tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other 0 = 0
apply /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other 0 == 0
rewrite sum_nat_eq0_nat.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk : Task
all
(fun x : Task =>
task_request_bound_function x 0 == 0 )
[seq x <- ts | hep_task x tsk & x != tsk]
apply /allP => tsk' IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk'
\in [seq x <- ts | hep_task x tsk & x != tsk]
task_request_bound_function tsk' 0 == 0
apply /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk'
\in [seq x <- ts | hep_task x tsk & x != tsk]
task_request_bound_function tsk' 0 = 0
apply task_rbf_0_zero => //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk'
\in [seq x <- ts | hep_task x tsk & x != tsk]
valid_arrival_curve (max_arrivals tsk')
apply H_valid_arrival_curve.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : tsk'
\in [seq x <- ts | hep_task x tsk & x != tsk]
tsk' \in ts
rewrite mem_filter in IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task tsk, tsk' : Task IN : hep_task tsk' tsk && (tsk' != tsk) &&
(tsk' \in ts)
tsk' \in ts
by move : IN => /andP[_ ->].
Qed .
(** Next we show how [total_ohep_request_bound_function_FP] can bound the
workload of jobs in a given interval. *)
(** Consider any types of jobs. *)
Context `{Job : JobType} `{JobTask Job Task} `{JobCost Job}.
(** Consider any arrival sequence that only has jobs from the task set and
where all arrivals have a valid job cost. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Assume there exists an arrival curve and that the arrival sequence
respects this curve. *)
Context `{MaxArrivals Task}.
Hypothesis H_respects_max_arrivals : taskset_respects_max_arrivals arr_seq ts.
(** Consider any task [tsk] and any job [j] of the task [tsk]. *)
Variable j : Job.
Variable tsk : Task.
Hypothesis H_job_of_task : job_of_task tsk j.
(** For any interval <<[t1, t1 + Δ)>>, the workload of jobs that have higher
task priority than the task priority of [j] is bounded by
[total_ohep_request_bound_function_FP] for the duration [Δ]. *)
Lemma ohep_workload_le_rbf :
forall Δ t1 ,
workload_of_jobs (another_task_hep_job^~ j) (arrivals_between arr_seq t1 (t1 + Δ))
<= total_ohep_request_bound_function_FP ts tsk Δ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j
forall (Δ : nat) (t1 : instant),
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
total_ohep_request_bound_function_FP ts tsk Δ
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j
forall (Δ : nat) (t1 : instant),
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
total_ohep_request_bound_function_FP ts tsk Δ
move => Δ t1.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
total_ohep_request_bound_function_FP ts tsk Δ
rewrite /workload_of_jobs /total_ohep_request_bound_function_FP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
another_task_hep_job j0 j) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
rewrite /another_task_hep_job /hep_job /FP_to_JLFP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
hep_task (job_task j0) (job_task j) &&
(job_task j0 != job_task j)) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
set (pred_task tsk_other := hep_task tsk_other tsk && (tsk_other != tsk)).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) |
hep_task (job_task j0) (job_task j) &&
(job_task j0 != job_task j)) job_cost j0 <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
rewrite (eq_big (fun j => pred_task (job_task j)) job_cost) //;
last by move => j'; rewrite /pred_task; move : H_job_of_task => /eqP ->.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(i <- arrivals_between arr_seq t1 (t1 + Δ) |
pred_task (job_task i)) job_cost i <=
\sum_(tsk_other <- ts | hep_task tsk_other tsk &&
(tsk_other != tsk))
task_request_bound_function tsk_other Δ
erewrite (eq_big pred_task); [|by done |by move => tsk'; eauto ].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task ts : seq Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H1 : FP_policy Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job arr_seq : arrival_sequence Job H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H4 : MaxArrivals Task H_respects_max_arrivals : taskset_respects_max_arrivals
arr_seq ts j : Job tsk : Task H_job_of_task : job_of_task tsk j Δ : nat t1 : instant pred_task := fun tsk_other : Task =>
hep_task tsk_other tsk &&
(tsk_other != tsk): Task -> bool
\sum_(i <- arrivals_between arr_seq t1 (t1 + Δ) |
pred_task (job_task i)) job_cost i <=
\sum_(i <- ts | pred_task i)
(task_request_bound_function^~ Δ) i
by apply : sum_of_jobs_le_sum_rbf.
Qed .
End RBFFOrFP .
(** We know that the workload of a task in any interval must be
bounded by the task's RBF in that interval. However, in the proofs
of several lemmas, we are required to reason about the workload of
a task in an interval excluding the cost of a particular job
(usually the job under analysis). Such a workload can be tightly
bounded by the task's RBF for the interval excluding the cost of
one task.
Notice, however, that this is not a trivial result since a naive
approach to proving it would fail. Suppose we want to prove that
some quantity [A - B] is upper bounded by some quantity [C -
D]. This usually requires us to prove that [A] is upper bounded by
[C] _and_ [D] is upper bounded by [B]. In our case, this would be
equivalent to proving that the task cost is upper-bounded by the
job cost, which of course is not true.
So, a different approach is needed, which we show in this
section. *)
Section TaskWorkload .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent :
consistent_arrival_times arr_seq.
(** ... and assume that WCETs are respected. *)
Hypothesis H_arrivals_have_valid_job_costs :
arrivals_have_valid_job_costs arr_seq.
(** Let [tsk] be any task ... *)
Variable tsk : Task.
(** ... characterized by a valid arrival curve. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
(** Consider any job [j] of [tsk] ... *)
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
(** ... that arrives in the given arrival sequence. *)
Hypothesis H_j_arrives_in : arrives_in arr_seq j.
(** Consider any time instant [t1] and duration [Δ] such that [j]
arrives before [t1 + Δ]. *)
Variables (t1 : instant) (Δ : duration).
Hypothesis H_job_arrival_lt : job_arrival j < t1 + Δ.
(** As a preparatory step, we restrict our attention to the sub-interval
containing the job's arrival. We know that the job's arrival necessarily
happens in the interval (<<[job_arrival j], t1 + Δ>>). This allows us to
show that the task workload excluding the task cost can be bounded by the
cost of the arrivals in the interval as follows. *)
Lemma task_rbf_without_job_under_analysis_from_arrival :
task_workload_between arr_seq tsk (job_arrival j) (t1 + Δ) - job_cost j
<= task_cost tsk * number_of_task_arrivals arr_seq tsk (job_arrival j) (t1 + Δ)
- task_cost tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
task_workload_between arr_seq tsk (job_arrival j)
(t1 + Δ) - job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
task_workload_between arr_seq tsk (job_arrival j)
(t1 + Δ) - job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk
rewrite /task_workload_between /workload.task_workload_between /task_workload
/workload_of_jobs /number_of_task_arrivals /task_arrivals_between.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
\sum_(j <- arrivals_between arr_seq (job_arrival j)
(t1 + Δ) | job_of_task tsk j) job_cost j -
job_cost j <=
task_cost tsk *
size
[seq j <- arrivals_between arr_seq (job_arrival j)
(t1 + Δ)
| job_of_task tsk j] - task_cost tsk
rewrite (big_rem j) //= addnC //= H_job_of_task addnK (filter_size_rem j)//.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
\sum_(y <- rem (T:=Job) j
(arrivals_between arr_seq (job_arrival j)
(t1 + Δ)) | job_of_task tsk y)
job_cost y <=
task_cost tsk *
(size
[seq y <- rem (T:=Job) j
(arrivals_between arr_seq
(job_arrival j) (t1 + Δ))
| job_of_task tsk y] + 1 ) - task_cost tsk
rewrite mulnDr mulnC muln1 addnK mulnC.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ
\sum_(y <- rem (T:=Job) j
(arrivals_between arr_seq (job_arrival j)
(t1 + Δ)) | job_of_task tsk y)
job_cost y <=
task_cost tsk *
size
[seq y <- rem (T:=Job) j
(arrivals_between arr_seq
(job_arrival j) (t1 + Δ))
| job_of_task tsk y]
apply sum_majorant_constant => j' ARR' /eqP TSK2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ j' : Job ARR' : j'
\in rem (T:=Job) j
(arrivals_between arr_seq
(job_arrival j)
(t1 + Δ)) TSK2 : job_task j' = tsk
job_cost j' <= task_cost tsk
rewrite -TSK2; apply H_arrivals_have_valid_job_costs.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ j' : Job ARR' : j'
\in rem (T:=Job) j
(arrivals_between arr_seq
(job_arrival j)
(t1 + Δ)) TSK2 : job_task j' = tsk
arrives_in arr_seq j'
apply rem_in in ARR'.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ j' : Job ARR' : j'
\in arrivals_between arr_seq
(job_arrival j)
(t1 + Δ) TSK2 : job_task j' = tsk
arrives_in arr_seq j'
by eapply in_arrivals_implies_arrived => //=.
Qed .
(** To use the above lemma in our final theorem, we require that the arrival
of the job under analysis necessarily happens in the interval we are
considering. *)
Hypothesis H_j_arrives_after_t : t1 <= job_arrival j.
(** Under the above assumption, we can finally establish the desired bound. *)
Lemma task_rbf_without_job_under_analysis :
task_workload_between arr_seq tsk t1 (t1 + Δ) - job_cost j
<= task_request_bound_function tsk Δ - task_cost tsk.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_request_bound_function tsk Δ - task_cost tsk
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_request_bound_function tsk Δ - task_cost tsk
apply leq_trans with
(task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) - task_cost tsk); last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) -
task_cost tsk <=
task_request_bound_function tsk Δ - task_cost tsk
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) -
task_cost tsk <=
task_request_bound_function tsk Δ - task_cost tsk
rewrite leq_sub2r // leq_mul2l; apply /orP => //=; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk Δ
have POSE: Δ = (t1 + Δ - t1) by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j POSE : Δ = t1 + Δ - t1
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk Δ
rewrite [in leqRHS]POSE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j POSE : Δ = t1 + Δ - t1
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk (t1 + Δ - t1)
eapply (H_is_arrival_curve t1 (t1 + Δ)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j POSE : Δ = t1 + Δ - t1
t1 <= t1 + Δ
by lia .
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) -
task_cost tsk
rewrite (@num_arrivals_of_task_cat _ _ _ _ _ (job_arrival j)); last by apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_cost tsk *
(number_of_task_arrivals arr_seq tsk t1
(job_arrival j) +
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ)) - task_cost tsk
rewrite mulnDr.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_workload_between arr_seq tsk t1 (t1 + Δ) -
job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j) +
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk
rewrite /task_workload_between /task_workload (workload_of_jobs_cat _ (job_arrival j) );
last by apply /andP; split ; lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1 (job_arrival j)) +
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ)) -
job_cost j <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j) +
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk
rewrite -!addnBA; first last .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
job_cost j <=
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ))
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
job_cost j <=
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ))
by rewrite /task_workload_between /task_workload
/workload_of_jobs (big_rem j) //= H_job_of_task leq_addr.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
task_cost tsk <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ)
rewrite -{1 }[task_cost tsk]muln1 leq_mul2l; apply /orP; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
0 <
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ)
rewrite /number_of_task_arrivals /task_arrivals_between.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
0 <
size
[seq j <- arrivals_between arr_seq (job_arrival j)
(t1 + Δ)
| job_of_task tsk j]
rewrite size_filter -has_count; apply /hasP; exists j ; last by rewrite H_job_of_task.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
j
\in arrivals_between arr_seq (job_arrival j)
(t1 + Δ)
apply (mem_bigcat _ Job _ (job_arrival j) _); last by apply job_in_arrivals_at => //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
job_arrival j \in index_iota (job_arrival j) (t1 + Δ)
rewrite mem_index_iota.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
job_arrival j <= job_arrival j < t1 + Δ
by apply /andP;split .
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1 (job_arrival j)) +
(workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ)) -
job_cost j) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j) +
(task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk)
have ->: job_arrival j = t1 + (job_arrival j - t1) by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1
(t1 + (job_arrival j - t1))) +
(workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq
(t1 + (job_arrival j - t1)) (t1 + Δ)) -
job_cost j) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1
(t1 + (job_arrival j - t1)) +
(task_cost tsk *
number_of_task_arrivals arr_seq tsk
(t1 + (job_arrival j - t1)) (t1 + Δ) -
task_cost tsk)
have ->: t1 + (job_arrival j - t1) = job_arrival j by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1 (job_arrival j)) +
(workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq (job_arrival j) (t1 + Δ)) -
job_cost j) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j) +
(task_cost tsk *
number_of_task_arrivals arr_seq tsk (job_arrival j)
(t1 + Δ) - task_cost tsk)
rewrite leq_add//; last by apply task_rbf_without_job_under_analysis_from_arrival => //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1 (job_arrival j)) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (job_arrival j)
have ->: job_arrival j = t1 + (job_arrival j - t1) by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H3 : MaxArrivals Task H_valid_arrival_curve : valid_arrival_curve
(max_arrivals tsk) H_is_arrival_curve : respects_max_arrivals arr_seq tsk
(max_arrivals tsk) j : Job H_job_of_task : job_of_task tsk j H_j_arrives_in : arrives_in arr_seq j t1 : instant Δ : duration H_job_arrival_lt : job_arrival j < t1 + Δ H_j_arrives_after_t : t1 <= job_arrival j
workload_of_jobs (job_of_task tsk)
(arrivals_between arr_seq t1
(t1 + (job_arrival j - t1))) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1
(t1 + (job_arrival j - t1))
by eapply (task_workload_le_num_of_arrivals_times_cost ) => //=.
Qed .
End TaskWorkload .