Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.abstract .restricted_supply.iw_instantiation.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** * Helper Lemmas for Bounded Busy Interval Lemmas *)
(** In this section, we introduce a few lemmas that facilitate the
proof of an upper bound on busy intervals for various priority
policies in the context of the restricted-supply processor
model. *)
Section BoundedBusyIntervalsAux .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of fully supply-consuming unit-supply
uniprocessor model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
(** Consider a JLFP policy that indicates a higher-or-equal
priority relation, and assume that the relation is reflexive. *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
(** Consider any valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Next, consider a schedule of this arrival sequence, ... *)
Variable sched : schedule PState.
(** ... allow for any work-bearing notion of job readiness, ... *)
Context `{!JobReady Job PState}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is valid. *)
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** Furthermore, we assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** Recall that [busy_intervals_are_bounded_by] is an abstract
notion. Hence, we need to introduce interference and interfering
workload. We will use the restricted-supply instantiations. *)
(** We say that job [j] incurs interference at time [t] iff it
cannot execute due to (1) the lack of supply at time [t], (2)
service inversion (i.e., a lower-priority job receiving service
at [t]), or a higher-or-equal-priority job receiving service. *)
#[local] Instance rs_jlfp_interference : Interference Job :=
rs_jlfp_interference arr_seq sched.
(** The interfering workload, in turn, is defined as the sum of the
blackout predicate, service inversion predicate, and the
interfering workload of jobs with higher or equal priority. *)
#[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
rs_jlfp_interfering_workload arr_seq sched.
(** Consider any job [j] of task [tsk] that has a positive job cost
and is in the arrival sequence. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** First, we note that, since job [j] is pending at time
[job_arrival j], there is a (potentially unbounded) busy
interval that starts no later than with the arrival of [j]. *)
Lemma busy_interval_prefix_exists :
exists t1 ,
t1 <= job_arrival j
/\ busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j
exists t1 : nat,
t1 <= job_arrival j /\
busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j
exists t1 : nat,
t1 <= job_arrival j /\
busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1
have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j PEND : pending sched j (job_arrival j)
exists t1 : nat,
t1 <= job_arrival j /\
busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1
have PREFIX := busy_interval.exists_busy_interval_prefix ltac :(eauto ) j.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j PEND : pending sched j (job_arrival j) PREFIX : forall t_busy : instant,
pending sched j t_busy ->
exists t1 : instant,
definitions.busy_interval_prefix sched j t1
t_busy.+1 /\
t1 <= job_arrival j <= t_busy
exists t1 : nat,
t1 <= job_arrival j /\
busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1
feed (PREFIX (job_arrival j)); first by done . Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j PEND : pending sched j (job_arrival j) PREFIX : exists t1 : instant,
definitions.busy_interval_prefix sched j t1
(job_arrival j).+1 /\
t1 <= job_arrival j <= job_arrival j
exists t1 : nat,
t1 <= job_arrival j /\
busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1
move : PREFIX => [t1 [PREFIX /andP [GE1 _]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j PEND : pending sched j (job_arrival j) t1 : instant PREFIX : definitions.busy_interval_prefix sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j
exists t1 : nat,
t1 <= job_arrival j /\
busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1
by eexists ; split ; last by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
Qed .
(** Let <[t1, t2)>> be a busy-interval prefix. *)
Variable t1 t2 : instant.
Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.
(** We show that the service of higher-or-equal-priority jobs is
less than the workload of higher-or-equal-priority jobs in any
subinterval <<[t1, t)>> of the interval <<[t1, t2)>>. *)
Lemma service_lt_workload_in_busy :
forall t ,
t1 < t < t2 ->
service_of_hep_jobs arr_seq sched j t1 t < workload_of_hep_jobs arr_seq j t1 t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2
forall t : nat,
t1 < t < t2 ->
service_of_hep_jobs arr_seq sched j t1 t <
workload_of_hep_jobs arr_seq j t1 t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2
forall t : nat,
t1 < t < t2 ->
service_of_hep_jobs arr_seq sched j t1 t <
workload_of_hep_jobs arr_seq j t1 t
move => t /andP [LT1 LT2]; move : (H_busy_prefix) => PREF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
service_of_hep_jobs arr_seq sched j t1 t <
workload_of_hep_jobs arr_seq j t1 t
move_neq_up LE. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 LE : workload_of_hep_jobs arr_seq j t1 t <=
service_of_hep_jobs arr_seq sched j t1 t
False
have EQ: workload_of_hep_jobs arr_seq j t1 t = service_of_hep_jobs arr_seq sched j t1 t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 LE : workload_of_hep_jobs arr_seq j t1 t <=
service_of_hep_jobs arr_seq sched j t1 t
workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 LE : workload_of_hep_jobs arr_seq j t1 t <=
service_of_hep_jobs arr_seq sched j t1 t
workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t
apply /eqP; rewrite eqn_leq; apply /andP; split => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 LE : workload_of_hep_jobs arr_seq j t1 t <=
service_of_hep_jobs arr_seq sched j t1 t
service_of_hep_jobs arr_seq sched j t1 t <=
workload_of_hep_jobs arr_seq j t1 t
by apply service_of_jobs_le_workload => //.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 LE : workload_of_hep_jobs arr_seq j t1 t <=
service_of_hep_jobs arr_seq sched j t1 t EQ : workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t
False
clear LE; move : PREF => [LT [QT1 [NQT QT2]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 EQ : workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j tQT2 : t1 <= job_arrival j < t2
False
specialize (NQT t ltac :(lia )); apply : NQT => s ARR HEP BF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 EQ : workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
completed_by sched s t
have EQ2: workload_of_hep_jobs arr_seq j 0 t = service_of_hep_jobs arr_seq sched j 0 t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 EQ : workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
workload_of_hep_jobs arr_seq j 0 t =
service_of_hep_jobs arr_seq sched j 0 t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 EQ : workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
workload_of_hep_jobs arr_seq j 0 t =
service_of_hep_jobs arr_seq sched j 0 t
rewrite /workload_of_hep_jobs (workload_of_jobs_cat _ t1); last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 EQ : workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
workload_of_jobs (hep_job^~ j)
(arrivals_between arr_seq 0 t1) +
workload_of_jobs (hep_job^~ j)
(arrivals_between arr_seq t1 t) =
service_of_hep_jobs arr_seq sched j 0 t
rewrite /service_of_hep_jobs (service_of_jobs_cat_scheduling_interval _ _ _ _ _ 0 t t1) //; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 EQ : workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
workload_of_jobs (hep_job^~ j)
(arrivals_between arr_seq 0 t1) +
workload_of_jobs (hep_job^~ j)
(arrivals_between arr_seq t1 t) =
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) 0 t1 +
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) t1 t +
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq t1 t) t1 t
rewrite /workload_of_hep_jobs in EQ; rewrite EQ; clear EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
workload_of_jobs (hep_job^~ j)
(arrivals_between arr_seq 0 t1) +
service_of_hep_jobs arr_seq sched j t1 t =
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) 0 t1 +
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) t1 t +
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq t1 t) t1 t
apply /eqP; rewrite eqn_add2r.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
workload_of_jobs (hep_job^~ j)
(arrivals_between arr_seq 0 t1) ==
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) 0 t1 +
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) t1 t
replace (service_of_jobs sched (hep_job^~ j) (arrivals_between arr_seq 0 t1) t1 t) with 0 ; last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
0 =
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) t1 t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
0 =
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) t1 t
symmetry ; apply : big1_seq => h /andP [HEPh BWh].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1
service_during sched h t1 t = 0
apply big1_seq => t' /andP [_ IN].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1 t' : Datatypes_nat__canonical__eqtype_Equality IN : t' \in index_iota t1 t
service_at sched h t' = 0
apply not_scheduled_implies_no_service, completed_implies_not_scheduled => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1 t' : Datatypes_nat__canonical__eqtype_Equality IN : t' \in index_iota t1 t
completed_by sched h t'
apply : completion_monotonic; last apply QT1 => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1 t' : Datatypes_nat__canonical__eqtype_Equality IN : t' \in index_iota t1 t
t1 <= t'
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1 t' : Datatypes_nat__canonical__eqtype_Equality IN : t' \in index_iota t1 t
t1 <= t'
by rewrite mem_index_iota in IN; lia . } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1 t' : Datatypes_nat__canonical__eqtype_Equality IN : t' \in index_iota t1 t
arrives_in arr_seq h
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1 t' : Datatypes_nat__canonical__eqtype_Equality IN : t' \in index_iota t1 t
arrives_in arr_seq h
by apply : in_arrivals_implies_arrived. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1 t' : Datatypes_nat__canonical__eqtype_Equality IN : t' \in index_iota t1 t
arrived_before h t1
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job HEPh : hep_job h j BWh : h \in arrivals_between arr_seq 0 t1 t' : Datatypes_nat__canonical__eqtype_Equality IN : t' \in index_iota t1 t
arrived_before h t1
by apply : in_arrivals_implies_arrived_before. }
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
workload_of_jobs (hep_job^~ j)
(arrivals_between arr_seq 0 t1) ==
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) 0 t1 + 0
rewrite addn0; apply /eqP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
workload_of_jobs (hep_job^~ j)
(arrivals_between arr_seq 0 t1) =
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq 0 t1) 0 t1
apply all_jobs_have_completed_impl_workload_eq_service => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t
forall j0 : Job,
j0 \in arrivals_between arr_seq 0 t1 ->
hep_job j0 j -> completed_by sched j0 t1
move => h ARRh HEPh; apply : QT1 => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job ARRh : h \in arrivals_between arr_seq 0 t1 HEPh : hep_job h j
arrives_in arr_seq h
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job ARRh : h \in arrivals_between arr_seq 0 t1 HEPh : hep_job h j
arrives_in arr_seq h
by apply : in_arrivals_implies_arrived.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 LT : t1 < t2 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t h : Job ARRh : h \in arrivals_between arr_seq 0 t1 HEPh : hep_job h j
arrived_before h t1
by apply : in_arrivals_implies_arrived_before.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 t : nat LT1 : t1 < t LT2 : t < t2 EQ : workload_of_hep_jobs arr_seq j t1 t =
service_of_hep_jobs arr_seq sched j t1 t LT : t1 < t2 QT1 : quiet_time arr_seq sched j t1 QT2 : t1 <= job_arrival j < t2 s : Job ARR : arrives_in arr_seq s HEP : hep_job s j BF : arrived_before s t EQ2 : workload_of_hep_jobs arr_seq j 0 t =
service_of_hep_jobs arr_seq sched j 0 t
completed_by sched s t
by apply : workload_eq_service_impl_all_jobs_have_completed => //.
Qed .
(** Consider a subinterval <<[t1, t1 + Δ)>> of the interval <<[t1,
t2)>>. We show that the sum of [j]'s workload and the cumulative
workload in <<[t1, t1 + Δ)>> is strictly larger than [Δ]. *)
Lemma workload_exceeds_interval :
forall Δ ,
0 < Δ ->
t1 + Δ < t2 ->
Δ < workload_of_job arr_seq j t1 (t1 + Δ) + cumulative_interfering_workload j t1 (t1 + Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2
forall Δ : nat,
0 < Δ ->
t1 + Δ < t2 ->
Δ <
workload_of_job arr_seq j t1 (t1 + Δ) +
cumulative_interfering_workload j t1 (t1 + Δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2
forall Δ : nat,
0 < Δ ->
t1 + Δ < t2 ->
Δ <
workload_of_job arr_seq j t1 (t1 + Δ) +
cumulative_interfering_workload j t1 (t1 + Δ)
move => δ POS LE; move : (H_busy_prefix) => PREF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
δ <
workload_of_job arr_seq j t1 (t1 + δ) +
cumulative_interfering_workload j t1 (t1 + δ)
apply leq_ltn_trans with (service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
δ <=
service_during sched j t1 (t1 + δ) +
cumulative_interference j t1 (t1 + δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
δ <=
service_during sched j t1 (t1 + δ) +
cumulative_interference j t1 (t1 + δ)
rewrite /service_during /cumulative_interference /cumul_cond_interference /cond_interference /service_at.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
δ <=
\sum_(t1 <= t < t1 + δ) service_in j (sched t) +
\sum_(t1 <= t < t1 + δ) true && interference j t
rewrite -big_split //= -{1 }(sum_of_ones t1 δ) big_nat [in X in _ <= X]big_nat.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
\sum_(t1 <= i < t1 + δ | t1 <= i < t1 + δ) 1 <=
\sum_(t1 <= i < t1 + δ | t1 <= i < t1 + δ)
(service_in j (sched i) + interference j i)
apply leq_sum => x /andP[Lo Hi].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ
0 < service_in j (sched x) + interference j x
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ
0 < service_in j (sched x) + interference j x
eapply instantiated_i_and_w_are_coherent_with_schedule in H_work_conserving; eauto 2 => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched
0 < service_in j (sched x) + interference j x
move : (H_work_conserving j t1 t2 x) => Workj.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : arrives_in arr_seq j ->
0 < job_cost j ->
definitions.busy_interval_prefix sched j t1 t2 ->
t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
0 < service_in j (sched x) + interference j x
feed_n 4 Workj; try done . Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : definitions.busy_interval_prefix sched j t1 t2 ->
t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
definitions.busy_interval_prefix sched j t1 t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : definitions.busy_interval_prefix sched j t1 t2 ->
t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
definitions.busy_interval_prefix sched j t1 t2
by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
t1 <= x < t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
t1 <= x < t2
by apply /andP; split ; eapply leq_trans; eauto . } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : ~ interference j x <->
receives_service_at sched j x
0 < service_in j (sched x) + interference j x
destruct interference.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : ~ true <-> receives_service_at sched j x
0 < service_in j (sched x) + true
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : ~ true <-> receives_service_at sched j x
0 < service_in j (sched x) + true
by lia .
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2 x : nat Lo : t1 <= x Hi : x < t1 + δ H_work_conserving : definitions.work_conserving
arr_seq sched Workj : ~ false <-> receives_service_at sched j x
0 < service_in j (sched x) + false
by rewrite //= addn0; apply Workj.
}
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
service_during sched j t1 (t1 + δ) +
cumulative_interference j t1 (t1 + δ) <
workload_of_job arr_seq j t1 (t1 + δ) +
cumulative_interfering_workload j t1 (t1 + δ)
rewrite cumulative_interfering_workload_split // cumulative_interference_split //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
service_during sched j t1 (t1 + δ) +
(blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
cumulative_another_hep_job_interference arr_seq sched
j t1 (t1 + δ)) <
workload_of_job arr_seq j t1 (t1 + δ) +
(blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
cumulative_other_hep_jobs_interfering_workload
arr_seq j t1 (t1 + δ))
rewrite cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //; last by apply PREF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
service_during sched j t1 (t1 + δ) +
(blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
service_of_other_hep_jobs arr_seq sched j t1 (t1 + δ)) <
workload_of_job arr_seq j t1 (t1 + δ) +
(blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
workload_of_other_hep_jobs arr_seq j t1 (t1 + δ))
rewrite -[leqRHS]addnC -[leqRHS]addnA [(_ + workload_of_job _ _ _ _ )]addnC.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
service_during sched j t1 (t1 + δ) +
(blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
service_of_other_hep_jobs arr_seq sched j t1 (t1 + δ)) <
blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
(workload_of_job arr_seq j t1 (t1 + δ) +
workload_of_other_hep_jobs arr_seq j t1 (t1 + δ))
rewrite workload_job_and_ahep_eq_workload_hep //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
service_during sched j t1 (t1 + δ) +
(blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
service_of_other_hep_jobs arr_seq sched j t1 (t1 + δ)) <
blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
workload_of_hep_jobs arr_seq j t1 (t1 + δ)
rewrite -addnC -addnA [(_ + service_during _ _ _ _ )]addnC.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
(service_during sched j t1 (t1 + δ) +
service_of_other_hep_jobs arr_seq sched j t1 (t1 + δ)) <
blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
workload_of_hep_jobs arr_seq j t1 (t1 + δ)
rewrite service_plus_ahep_eq_service_hep //; last by move : PREF => [_ [_ [_ /andP [A B]]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
service_of_hep_jobs arr_seq sched j t1 (t1 + δ) <
blackout_during sched t1 (t1 + δ) +
cumulative_service_inversion arr_seq sched j t1
(t1 + δ) +
workload_of_hep_jobs arr_seq j t1 (t1 + δ)
rewrite ltn_add2l.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_prefix : busy_interval_prefix arr_seq sched j
t1 t2 δ : nat POS : 0 < δLE : t1 + δ < t2 PREF : busy_interval_prefix arr_seq sched j t1 t2
service_of_hep_jobs arr_seq sched j t1 (t1 + δ) <
workload_of_hep_jobs arr_seq j t1 (t1 + δ)
by apply : service_lt_workload_in_busy; eauto ; lia .
Qed .
End BoundedBusyIntervalsAux .