Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.priority.elf.[Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] New coercion path [GRing.subring_closedM;
GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.sdivr_closed_div;
GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.subalg_closedBM;
GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.divring_closed_div;
GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.divalg_closedBdiv;
GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default] Notation "_ - _" was already used in scope
distn_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]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.definitions.workload.bounded.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.workload.elf_athep_bound.
Require Export prosa.analysis.facts.model.rbf.
(** * Bound on Higher-or-Equal Priority Workload under ELF Scheduling is Valid *)
(** In this file, we prove that the upper bound on interference
incurred by a job from jobs with higher-or-equal priority that
come from other tasks under ELF scheduling (defined in
[prosa.analysis.definitions.workload.elf_athep_bound]) is
valid. *)
Section ATHEPWorkloadBoundIsValidForELF .
(** Consider any type of tasks, each characterized by a WCET
[task_cost], a relative deadline [task_deadline], an arrival
curve [max_arrivals], and a relative priority point, ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{PriorityPoint Task}.
(** ... and any type of jobs associated with these tasks, where each
job has a task [job_task], a cost [job_cost], and an arrival
time [job_arrival]. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor model. *)
Context `{PState : ProcessorState Job}.
(** Consider any valid arrival sequence [arr_seq] ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... with valid job costs. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** We consider an arbitrary task set [ts] ... *)
Variable ts : seq Task.
(** ... and assume that all jobs stem from tasks in this task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** We assume that [max_arrivals] is a family of valid arrival
curves that constrains the arrival sequence [arr_seq], i.e., for
any task [tsk] in [ts], [max_arrival tsk] is an arrival bound of
[tsk]. *)
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Let [tsk] be any task to be analyzed. *)
Variable tsk : Task.
(** Consider any schedule. *)
Variable sched : schedule PState.
(* Consider any fixed-priority scheduling policy. *)
Context (FP : FP_policy Task).
(** Before we prove the main result, we establish some auxiliary lemmas. *)
Section HepWorkloadBound .
(** Consider an arbitrary job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Consider the busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : duration.
Hypothesis H_busy_interval : busy_interval arr_seq sched j t1 t2.
(** Let's define [A] as a relative arrival time of job [j] (with
respect to time [t1]). *)
Let A := job_arrival j - t1.
(** Consider an arbitrary shift [delta] inside the busy interval ... *)
Variable delta : duration.
Hypothesis H_delta_in_busy : t1 + delta < t2.
(** ... and the set of all arrivals between [t1] and [t1 + delta]. *)
Let jobs := arrivals_between arr_seq t1 (t1 + delta).
(** Now, we define a predicate to identify jobs from a given task that have
priority higher than or equal to [j]. *)
Let hep_job_from_tsk (tsk_o : Task) (jo : Job) := hep_job jo j && (job_task jo == tsk_o).
Section ShortenRange .
(** Consider an arbitrary task [tsk_o ≠ tsk] from [ts]. *)
Variable tsk_o : Task.
Hypothesis H_tsko_in_ts : tsk_o \in ts.
Hypothesis H_neq : tsk_o != tsk.
(** And assume that [ep_task_interfering_interval_length tsk tsk_o A] is bounded by delta. *)
Hypothesis H_delta_ge : ((ep_task_interfering_interval_length tsk tsk_o A) <= delta%:R)%R.
(** Then we prove that the total workload of jobs with higher-or-equal priority
from task [tsk_o] over the interval [[t1, t1 + Δ]] is bounded by the workload
over the interval [[t1, t1 + ep_task_interfering_interval_length tsk tsk_o A]].
The intuition behind this inequality is that jobs that arrive after time instant
[t1 + ep_task_interfering_interval_length tsk tsk_o A] have lower priority
than job [j]. *)
Lemma total_ep_tsk_workload_shorten_range :
ep_task tsk tsk_o ->
workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 (t1 + delta))
<= workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1 `|Num.max 0 %R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R
ep_task tsk tsk_o ->
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1 (t1 + delta)) <=
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R
ep_task tsk tsk_o ->
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1 (t1 + delta)) <=
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|)
move => EP_tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1 (t1 + delta)) <=
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|)
have BOUNDED: `|Num.max 0 %R (t1%:R + (ep_task_interfering_interval_length tsk tsk_o A))%R| <= t1 + delta
by clear - H_delta_ge; lia .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1 (t1 + delta)) <=
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|)
rewrite /hep_job_from_tsk /hep_job /ELF.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta
workload_of_jobs
(fun jo : Job =>
(hp_task (job_task jo) (job_task j)
|| hep_task (job_task jo) (job_task j) &&
hep_job jo j) && (job_task jo == tsk_o))
(arrivals_between arr_seq t1 (t1 + delta)) <=
workload_of_jobs
(fun jo : Job =>
(hp_task (job_task jo) (job_task j)
|| hep_task (job_task jo) (job_task j) &&
hep_job jo j) && (job_task jo == tsk_o))
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|)
rewrite (workload_of_jobs_nil_tail _ _ BOUNDED) //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta
forall j0 : Job,
j0 \in arrivals_between arr_seq t1 (t1 + delta) ->
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk tsk_o A)%R| <=
job_arrival j0 ->
~~
((hp_task (job_task j0) (job_task j)
|| hep_task (job_task j0) (job_task j) &&
hep_job j0 j) && (job_task j0 == tsk_o))
move => j' IN' ARR'.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) ARR' : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= job_arrival j'
~~
((hp_task (job_task j') (job_task j)
|| hep_task (job_task j') (job_task j) &&
hep_job j' j) && (job_task j' == tsk_o))
apply /contraT => /negPn /andP [/orP [/negP+ | /andP [_ HEP]] /eqP TSKo].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) ARR' : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= job_arrival j' TSKo : job_task j' = tsk_o
~ ~ hp_task (job_task j') (job_task j) -> false
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) ARR' : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= job_arrival j' TSKo : job_task j' = tsk_o
~ ~ hp_task (job_task j') (job_task j) -> false
rewrite /ep_task in EP_tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) ARR' : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= job_arrival j' TSKo : job_task j' = tsk_o EP_tsk : hep_task tsk tsk_o && hep_task tsk_o tsk
~ ~ hp_task (job_task j') (job_task j) -> false
rewrite /hp_task TSKo.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) ARR' : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= job_arrival j' TSKo : job_task j' = tsk_o EP_tsk : hep_task tsk tsk_o && hep_task tsk_o tsk
~
~
hep_task tsk_o (job_task j) &&
~~ hep_task (job_task j) tsk_o -> false
move : H_job_of_tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) ARR' : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= job_arrival j' TSKo : job_task j' = tsk_o EP_tsk : hep_task tsk tsk_o && hep_task tsk_o tsk
job_of_task tsk j ->
~
~
hep_task tsk_o (job_task j) &&
~~ hep_task (job_task j) tsk_o -> false
rewrite /job_of_task => /eqP ->.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) ARR' : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= job_arrival j' TSKo : job_task j' = tsk_o EP_tsk : hep_task tsk tsk_o && hep_task tsk_o tsk
~ ~ hep_task tsk_o tsk && ~~ hep_task tsk tsk_o ->
false
by move : EP_tsk => /andP [-> ->]. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) ARR' : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= job_arrival j' HEP : hep_job j' j TSKo : job_task j' = tsk_o
false
move : ARR'; rewrite /ep_task_interfering_interval_length -TSKo.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) HEP : hep_job j' j TSKo : job_task j' = tsk_o
`|Order.Def.max 0 %R
(t1%:R +
((A + 1 )%:R + task_priority_point tsk -
task_priority_point (job_task j')))%R| <=
job_arrival j' -> false
move : H_job_of_tsk => /eqP <-.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) HEP : hep_job j' j TSKo : job_task j' = tsk_o
`|Order.Def.max 0 %R
(t1%:R +
((A + 1 )%:R + task_priority_point (job_task j) -
task_priority_point (job_task j')))%R| <=
job_arrival j' -> false
move : HEP; rewrite /hep_job /GEL /job_priority_point.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_delta_ge : (ep_task_interfering_interval_length tsk
tsk_o A <= delta%:R)%R EP_tsk : ep_task tsk tsk_o BOUNDED : `|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R| <= t1 + delta j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + delta) TSKo : job_task j' = tsk_o
((job_arrival j')%:R +
task_priority_point (job_task j') <=
(job_arrival j)%:R + task_priority_point (job_task j))%R ->
`|Order.Def.max 0 %R
(t1%:R +
((A + 1 )%:R + task_priority_point (job_task j) -
task_priority_point (job_task j')))%R| <=
job_arrival j' -> false
by clear ; lia .
Qed .
End ShortenRange .
(** Consider the jobs that have priority higher than or equal to [j] released
by any task in the same priority band as [tsk] (excluding [tsk]).
We prove that the workload of these jobs is at most [bound_on_ep_task_workload]. *)
Corollary sum_of_ep_tsk_workloads_is_at_most_bound_on_ep_task_workload :
\sum_(tsk_o <- ts | (ep_task tsk tsk_o) && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
<= bound_on_ep_task_workload ts tsk A delta.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_ep_task_workload ts tsk A delta
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_ep_task_workload ts tsk A delta
rewrite /bound_on_ep_task_workload.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
task_request_bound_function tsk_o
(minn
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| delta)
apply leq_sum_seq => tsk_o INtsko /andP [EP_tsk NEQT].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
task_request_bound_function tsk_o
(minn
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| delta)
have [LEQ|GT] := leqP delta `|Num.max 0 %R (ep_task_interfering_interval_length tsk tsk_o A)%R|; [| apply ltnW in GT].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk LEQ : delta <=
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)|
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
task_request_bound_function tsk_o delta
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk LEQ : delta <=
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)|
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
task_request_bound_function tsk_o delta
apply : leq_trans; last by apply rbf_spec with (t := t1).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk LEQ : delta <=
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)|
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
task_workload_between arr_seq tsk_o t1 (t1 + delta)
by apply : workload_of_jobs_weaken => ? /andP[]. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk GT : `|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| <= delta
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
task_request_bound_function tsk_o
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk tsk_o A)|
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk GT : `|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| <= delta
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
task_request_bound_function tsk_o
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk tsk_o A)|
eapply leq_trans; first by apply total_ep_tsk_workload_shorten_range => //; clear - GT H_delta_in_busy; lia .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk GT : `|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| <= delta
workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|) <=
task_request_bound_function tsk_o
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk tsk_o A)|
rewrite (workload_of_jobs_equiv_pred _ _ (fun jo : Job => hep_job jo j && (job_task jo == tsk_o))) => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk GT : `|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| <= delta
workload_of_jobs
(fun jo : Job =>
hep_job jo j && (job_task jo == tsk_o))
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|) <=
task_request_bound_function tsk_o
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk tsk_o A)|
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk GT : `|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| <= delta
workload_of_jobs
(fun jo : Job =>
hep_job jo j && (job_task jo == tsk_o))
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|) <=
task_request_bound_function tsk_o
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk tsk_o A)|
case : (boolP (0 <= ep_task_interfering_interval_length tsk tsk_o A)%R) => EQ;
last by rewrite arrivals_between_geq; [rewrite workload_of_jobs0 | clear - EQ; lia ].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk GT : `|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| <= delta EQ : (0 <=
ep_task_interfering_interval_length tsk tsk_o A)%R
workload_of_jobs
(fun jo : Job =>
hep_job jo j && (job_task jo == tsk_o))
(arrivals_between arr_seq t1
`|Order.Def.max 0 %R
(t1%:R +
ep_task_interfering_interval_length tsk
tsk_o A)%R|) <=
task_request_bound_function tsk_o
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk tsk_o A)|
have -> : `|Num.max 0 %R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|
= t1 + `|Num.max 0 %R (ep_task_interfering_interval_length tsk tsk_o A)| by clear -EQ; lia .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk_o : Task INtsko : tsk_o \in ts EP_tsk : ep_task tsk tsk_o NEQT : tsk_o != tsk GT : `|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)| <= delta EQ : (0 <=
ep_task_interfering_interval_length tsk tsk_o A)%R
workload_of_jobs
(fun jo : Job =>
hep_job jo j && (job_task jo == tsk_o))
(arrivals_between arr_seq t1
(t1 +
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk
tsk_o A)|)) <=
task_request_bound_function tsk_o
`|Order.Def.max 0 %R
(ep_task_interfering_interval_length tsk tsk_o A)|
by apply : rbf_spec' => // ? /andP[].
}
}
Qed .
(** Next, consider a workload of all jobs with priority higher
than [j] released by any task in higher priority band.
we establish that this workload is at most [bound_on_hp_task_workload]. *)
Corollary sum_of_hp_tsk_workloads_is_at_most_bound_on_hp_task_workload :
\sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
<= bound_on_hp_task_workload ts tsk delta.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_hp_task_workload ts tsk delta
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_hp_task_workload ts tsk delta
rewrite /bound_on_hp_task_workload.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
total_hp_request_bound_function_FP ts tsk delta
rewrite /total_hp_request_bound_function_FP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
\sum_(tsk_other <- ts | hp_task tsk_other tsk)
task_request_bound_function tsk_other delta
apply leq_sum_seq => tsk' IN' HP_TSK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task IN' : tsk' \in ts HP_TSK : hp_task tsk' tsk
workload_of_jobs (hep_job_from_tsk tsk') jobs <=
task_request_bound_function tsk' delta
by apply : rbf_spec' => // ? /andP[].
Qed .
(** To help with further analysis, we establish a useful lemma on partitioning
higher-or-equal priority workloads. *)
Lemma sum_of_hep_workloads_partitioned :
\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
= \sum_(tsk_o <- ts | (ep_task tsk tsk_o) && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
+ \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | tsk_o != tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs =
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | tsk_o != tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs =
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
rewrite (bigID (fun (tsk_o : Task) => hep_task tsk_o tsk)) //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (i != tsk) && hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs +
\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs =
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
rewrite (bigID (fun (tsk_o : Task) => hep_task tsk tsk_o)) //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (i != tsk) && hep_task i tsk &&
hep_task tsk i)
workload_of_jobs (hep_job_from_tsk i) jobs +
\sum_(i <- ts | (i != tsk) && hep_task i tsk &&
~~ hep_task tsk i)
workload_of_jobs (hep_job_from_tsk i) jobs +
\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs =
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
under eq_bigl.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
forall x : Task,
'Under[ (x != tsk) && hep_task x tsk && hep_task tsk x ]
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
forall x : Task,
'Under[ (x != tsk) && hep_task x tsk && hep_task tsk x ]
move => tsk'.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task
'Under[ (tsk' != tsk) && hep_task tsk' tsk &&
hep_task tsk tsk' ]
rewrite -andbA andbC.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task
'Under[ hep_task tsk' tsk && hep_task tsk tsk' &&
(tsk' != tsk) ]
rewrite (@andbC (hep_task tsk' tsk) (hep_task tsk tsk')).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task
'Under[ hep_task tsk tsk' && hep_task tsk' tsk &&
(tsk' != tsk) ]
over . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (fun tsk' : Task =>
hep_task tsk tsk' &&
hep_task tsk' tsk && (tsk' != tsk)) i)
workload_of_jobs (hep_job_from_tsk i) jobs +
\sum_(i <- ts | (i != tsk) && hep_task i tsk &&
~~ hep_task tsk i)
workload_of_jobs (hep_job_from_tsk i) jobs +
\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs =
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
have ->: \sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs = 0 .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs = 0
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs = 0
under eq_bigr.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
forall i : Task,
(i != tsk) && ~~ hep_task i tsk ->
'Under[ workload_of_jobs (hep_job_from_tsk i) jobs ]
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
forall i : Task,
(i != tsk) && ~~ hep_task i tsk ->
'Under[ workload_of_jobs (hep_job_from_tsk i) jobs ]
move => tsk' /andP [NEQ HEP].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk
'Under[ workload_of_jobs (hep_job_from_tsk tsk') jobs ]
rewrite /workload_of_jobs.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk
'Under[ \sum_(j <- jobs | hep_job_from_tsk tsk' j)
job_cost j ]
under big_pred0.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk
forall x : Job, hep_job_from_tsk tsk' x = false
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk
forall x : Job, hep_job_from_tsk tsk' x = false
move => j'.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk j' : Job
hep_job_from_tsk tsk' j' = false
rewrite /hep_job_from_tsk /hep_job /ELF /hp_task.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk j' : Job
(hep_task (job_task j') (job_task j) &&
~~ hep_task (job_task j) (job_task j')
|| hep_task (job_task j') (job_task j) &&
hep_job j' j) && (job_task j' == tsk') = false
elim Tsk_j' : (job_task j' == tsk'); last by rewrite andbF.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk j' : Job Tsk_j' : (job_task j' == tsk') = true
(hep_task (job_task j') (job_task j) &&
~~ hep_task (job_task j) (job_task j')
|| hep_task (job_task j') (job_task j) &&
hep_job j' j) && true = false
move : Tsk_j' => /eqP ->.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk j' : Job
(hep_task tsk' (job_task j) &&
~~ hep_task (job_task j) tsk'
|| hep_task tsk' (job_task j) && hep_job j' j) &&
true = false
move : H_job_of_tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk j' : Job
job_of_task tsk j ->
(hep_task tsk' (job_task j) &&
~~ hep_task (job_task j) tsk'
|| hep_task tsk' (job_task j) && hep_job j' j) &&
true = false
rewrite /job_of_task => /eqP ->.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk j' : Job
(hep_task tsk' tsk && ~~ hep_task tsk tsk'
|| hep_task tsk' tsk && hep_job j' j) && true = false
by move : HEP => /negbTE ->. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' != tsk HEP : ~~ hep_task tsk' tsk
'Under[ 0 ]
over . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
(fun => 0 ) i = 0
apply /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk) 0 ==
0
by rewrite big_const_idem.
} Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | hep_task tsk i && hep_task i tsk &&
(i != tsk))
workload_of_jobs (hep_job_from_tsk i) jobs +
\sum_(i <- ts | (i != tsk) && hep_task i tsk &&
~~ hep_task tsk i)
workload_of_jobs (hep_job_from_tsk i) jobs + 0 =
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
rewrite addn0 /ep_task.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | hep_task tsk i && hep_task i tsk &&
(i != tsk))
workload_of_jobs (hep_job_from_tsk i) jobs +
\sum_(i <- ts | (i != tsk) && hep_task i tsk &&
~~ hep_task tsk i)
workload_of_jobs (hep_job_from_tsk i) jobs =
\sum_(tsk_o <- ts | hep_task tsk tsk_o &&
hep_task tsk_o tsk &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
apply /eqP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | hep_task tsk i && hep_task i tsk &&
(i != tsk))
workload_of_jobs (hep_job_from_tsk i) jobs +
\sum_(i <- ts | (i != tsk) && hep_task i tsk &&
~~ hep_task tsk i)
workload_of_jobs (hep_job_from_tsk i) jobs ==
\sum_(tsk_o <- ts | hep_task tsk tsk_o &&
hep_task tsk_o tsk &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
rewrite eqn_add2l /hp_task.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(i <- ts | (i != tsk) && hep_task i tsk &&
~~ hep_task tsk i)
workload_of_jobs (hep_job_from_tsk i) jobs ==
\sum_(tsk_o <- ts | hep_task tsk_o tsk &&
~~ hep_task tsk tsk_o)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs
rewrite (eq_bigl (fun (tsk_o : Task) => hep_task tsk_o tsk && ~~ hep_task tsk tsk_o)) //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
(fun i : Task =>
(i != tsk) && hep_task i tsk && ~~ hep_task tsk i) =1
(fun tsk_o : Task =>
hep_task tsk_o tsk && ~~ hep_task tsk tsk_o)
rewrite /eqfun => tsk'.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task
(tsk' != tsk) && hep_task tsk' tsk &&
~~ hep_task tsk tsk' =
hep_task tsk' tsk && ~~ hep_task tsk tsk'
elim NEQ: (tsk' != tsk) => //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : (tsk' != tsk) = false
false = hep_task tsk' tsk && ~~ hep_task tsk tsk'
move : NEQ => /idP /idP /eqP NEQ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' = tsk
false = hep_task tsk' tsk && ~~ hep_task tsk tsk'
rewrite NEQ.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool tsk' : Task NEQ : tsk' = tsk
false = hep_task tsk tsk && ~~ hep_task tsk tsk
by rewrite andbN.
Qed .
(** Finally, we establish that the workload of jobs with priority higher than or equal to
[j] is at most [bound_on_athep_workload]. *)
Corollary sum_of_workloads_is_at_most_bound_on_total_hep_workload :
\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
<= bound_on_athep_workload ts tsk A delta.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | tsk_o != tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_athep_workload ts tsk A delta
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | tsk_o != tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_athep_workload ts tsk A delta
rewrite sum_of_hep_workloads_partitioned.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_athep_workload ts tsk A delta
rewrite /bound_on_athep_workload.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_hp_task_workload ts tsk delta +
bound_on_ep_task_workload ts tsk A delta
move : sum_of_hp_tsk_workloads_is_at_most_bound_on_hp_task_workload => LT_HP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool LT_HP : \sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o)
jobs <=
bound_on_hp_task_workload ts tsk delta
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_hp_task_workload ts tsk delta +
bound_on_ep_task_workload ts tsk A delta
move : sum_of_ep_tsk_workloads_is_at_most_bound_on_ep_task_workload => LT_EP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat delta : duration H_delta_in_busy : t1 + delta < t2 jobs := arrivals_between arr_seq t1 (t1 + delta) : seq Job hep_job_from_tsk := fun (tsk_o : Task) (jo : Job) =>
hep_job jo j &&
(job_task jo == tsk_o): Task -> Job -> bool LT_HP : \sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o)
jobs <=
bound_on_hp_task_workload ts tsk delta LT_EP : \sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o)
jobs <=
bound_on_ep_task_workload ts tsk A delta
\sum_(tsk_o <- ts | ep_task tsk tsk_o &&
(tsk_o != tsk))
workload_of_jobs (hep_job_from_tsk tsk_o) jobs +
\sum_(tsk_o <- ts | hp_task tsk_o tsk)
workload_of_jobs (hep_job_from_tsk tsk_o) jobs <=
bound_on_hp_task_workload ts tsk delta +
bound_on_ep_task_workload ts tsk A delta
by lia .
Qed .
End HepWorkloadBound .
(** The validity of [bound_on_athep_workload] then easily follows
from lemma [sum_of_workloads_is_at_most_bound_on_total_hep_workload]. *)
Corollary bound_on_athep_workload_is_valid :
athep_workload_is_bounded arr_seq sched tsk (bound_on_athep_workload ts tsk).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task
athep_workload_is_bounded arr_seq sched tsk
(bound_on_athep_workload ts tsk)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task
athep_workload_is_bounded arr_seq sched tsk
(bound_on_athep_workload ts tsk)
move => j t1 delta POS TSK QT.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job t1 : instant delta : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + delta)) <=
bound_on_athep_workload ts tsk (job_arrival j - t1)
delta
eapply leq_trans.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job t1 : instant delta : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + delta)) <= ?n
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job t1 : instant delta : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + delta)) <= ?n
eapply reorder_summation => j' IN _.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job t1 : instant delta : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1 j' : Job IN : j' \in arrivals_between arr_seq t1 (t1 + delta)
job_task j' \in ?ys
by apply H_all_jobs_from_taskset; eapply in_arrivals_implies_arrived; exact IN.
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job t1 : instant delta : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1
\sum_(y <- ts | y != job_task j)
\sum_(x <- arrivals_between arr_seq t1 (t1 + delta) |
(hep_job^~ j) x && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1)
delta
move : TSK => /eqP TSK; rewrite TSK.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : PriorityPoint Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState FP : FP_policy Task j : Job t1 : instant delta : duration POS : job_cost_positive j QT : quiet_time arr_seq sched j t1 TSK : job_task j = tsk
\sum_(y <- ts | y != tsk)
\sum_(x <- arrivals_between arr_seq t1 (t1 + delta) |
hep_job x j && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1)
delta
by apply : sum_of_workloads_is_at_most_bound_on_total_hep_workload => //; apply /eqP.
Qed .
End ATHEPWorkloadBoundIsValidForELF .