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.classes.[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 ] 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 ] 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.aggregate.service_of_jobs.
Require Export prosa.analysis.facts.behavior.service.
(** * Service Received by Sets of Jobs in Uniprocessor Schedules *)
(** In this section, we establish a fact about the service received by
_sets_ of jobs in the presence of idle times on a fully-consuming
uniprocessor model. *)
Section FullyConsumingModelLemmas .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Allow for any fully-consuming uniprocessor model. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
Hypothesis H_fully_consuming_proc_model : fully_consuming_proc_model PState.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Next, consider any schedule of this arrival sequence ... *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Let [P] be any predicate over jobs. *)
Variable P : pred Job.
(** We prove that, if the sum of the total blackout and the total
service within some time interval <<[t1,t2)>> is smaller than
[t2 - t1], then there is an idle time instant <<t ∈ [t1,t2)>>. *)
Lemma low_service_implies_existence_of_idle_time_rs :
forall t1 t2 ,
blackout_during sched t1 t2
+ service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t ,
t1 <= t < t2 /\ is_idle arr_seq sched t.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 : instant,
blackout_during sched t1 t2 +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 : instant,
blackout_during sched t1 t2 +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move => t1 t2 SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : blackout_during sched t1 t2 +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
destruct (t1 <= t2) eqn :LE; last first .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : blackout_during sched t1 t2 +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = false
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : blackout_during sched t1 t2 +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = false
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move : LE => /negP/negP; rewrite -ltnNge.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : blackout_during sched t1 t2 +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
t2 < t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : blackout_during sched t1 t2 +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LT : t2 - t1 == 0
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
by move : LT => /eqP -> in SERV; rewrite ltn0 in SERV.
} Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : blackout_during sched t1 t2 +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
interval_to_duration t1 t2 δ. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : blackout_during sched t1 (t1 + δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t1 + δ)) t1
(t1 + δ) <
t1 + δ - t1
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
rewrite {4 }[t1 + δ]addnC -addnBA // subnn addn0 in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : blackout_during sched t1 (t1 + δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t1 + δ)) t1
(t1 + δ) < δ
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
rewrite /service_of_jobs exchange_big //= in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : blackout_during sched t1 (t1 + δ) +
\sum_(t1 <= j <
t1 + δ)
\sum_(i <-
arrivals_between arr_seq 0
(t1 + δ))
service_at sched i j < δ
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
rewrite -big_split //= in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : \sum_(t1 <= i <
t1 + δ)
(is_blackout sched i +
\sum_(i0 <-
arrivals_between arr_seq 0
(t1 + δ))
service_at sched i0 i) < δ
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
apply sum_le_summation_range in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : exists x : nat,
t1 <= x < t1 + δ /\
is_blackout sched x +
\sum_(i <-
arrivals_between arr_seq 0
(t1 + δ))
service_at sched i x = 0
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
move : SERV => [x [/andP [GEx LEx] L]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : is_blackout sched x +
\sum_(i <-
arrivals_between arr_seq 0 (t1 + δ))
service_at sched i x = 0
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
exists x ; split ; first by apply /andP; split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : is_blackout sched x +
\sum_(i <-
arrivals_between arr_seq 0 (t1 + δ))
service_at sched i x = 0
is_idle arr_seq sched x
move : L => /eqP; rewrite addn_eq0 eqb0 sum_nat_eq0_nat filter_predT => /andP [SUP /allP L].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ SUP : ~~ is_blackout sched x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
is_idle arr_seq sched x
apply /negPn/negP; rewrite is_nonidle_iff //= => [[j SCHED]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ SUP : ~~ is_blackout sched x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x
False
have /eqP: service_at sched j x == 0 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ SUP : ~~ is_blackout sched x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x
service_at sched j x == 0
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ SUP : ~~ is_blackout sched x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x
service_at sched j x == 0
apply /L/arrived_between_implies_in_arrivals => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ SUP : ~~ is_blackout sched x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x
arrived_between j 0 (t1 + δ)
rewrite /arrived_between; apply /andP; split => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ SUP : ~~ is_blackout sched x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x
job_arrival j < t1 + δ
have : job_arrival j <= x by apply : H_jobs_must_arrive_to_execute.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ SUP : ~~ is_blackout sched x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x
job_arrival j <= x -> job_arrival j < t1 + δ
lia . } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ SUP : ~~ is_blackout sched x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x
service_at sched j x = 0 -> False
move : SUP; rewrite negbK => SUP SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x SUP : has_supply sched x SERV : service_at sched j x = 0
False
eapply ideal_progress_inside_supplies in SUP => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 } j : Job SCHED : scheduled_at sched j x SERV : service_at sched j x = 0 SUP : receives_service_at sched j x
False
by move : SUP; rewrite /receives_service_at SERV.
Qed .
End FullyConsumingModelLemmas .
(** * Service Received by Sets of Jobs in Uniprocessor Ideal-Progress Schedules *)
(** Next, we establish a fact about the service received by sets of
jobs in the presence of idle times on a uniprocessor under the
ideal-progress assumption (i.e., that a scheduled job necessarily
receives nonzero service). *)
Section IdealModelLemmas .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Allow for any uniprocessor model that ensures ideal progress. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
(** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Let [P] be any predicate over jobs. *)
Variable P : pred Job.
(** We prove that if the total service within some time interval <<[t1,t2)>>
is smaller than <<[t2 - t1]>>, then there is an idle time instant [t ∈ [t1,t2)]. *)
Lemma low_service_implies_existence_of_idle_time :
forall t1 t2 ,
service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t ,
t1 <= t < t2 /\ is_idle arr_seq sched t.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 : instant,
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 : instant,
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move => t1 t2 SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
destruct (t1 <= t2) eqn :LE; last first .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = false
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = false
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move : LE => /negP/negP; rewrite -ltnNge.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
t2 < t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LT : t2 - t1 == 0
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
by move : LT => /eqP -> in SERV; rewrite ltn0 in SERV.
} Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
interval_to_duration t1 t2 δ. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 (t1 + δ)) t1
(t1 + δ) <
t1 + δ - t1
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
rewrite {3 }[t1 + δ]addnC -addnBA // subnn addn0 in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 (t1 + δ)) t1
(t1 + δ) < δ
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
rewrite /service_of_jobs exchange_big //= in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : \sum_(t1 <= j <
t1 + δ)
\sum_(i <-
arrivals_between arr_seq 0
(t1 + δ))
service_at sched i j < δ
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
apply sum_le_summation_range in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : exists x : nat,
t1 <= x < t1 + δ /\
\sum_(i <-
arrivals_between arr_seq 0
(t1 + δ))
service_at sched i x = 0
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
move : SERV => [x [/andP [GEx LEx] L]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <-
arrivals_between arr_seq 0 (t1 + δ))
service_at sched i x = 0
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
exists x ; split ; first by apply /andP; split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <-
arrivals_between arr_seq 0 (t1 + δ))
service_at sched i x = 0
is_idle arr_seq sched x
apply /negPn/negP; rewrite is_nonidle_iff //= => [[j SCHED]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <-
arrivals_between arr_seq 0 (t1 + δ))
service_at sched i x = 0 j : Job SCHED : scheduled_at sched j x
False
move : L => /eqP; rewrite sum_nat_eq0_nat filter_predT => /allP L.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
False
have /eqP: service_at sched j x == 0 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
service_at sched j x == 0
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
service_at sched j x == 0
apply /L/arrived_between_implies_in_arrivals => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
arrived_between j 0 (t1 + δ)
rewrite /arrived_between; apply /andP; split => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
job_arrival j < t1 + δ
have : job_arrival j <= x by apply : H_jobs_must_arrive_to_execute.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
job_arrival j <= x -> job_arrival j < t1 + δ
lia . } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_ideal_progress_proc_model : ideal_progress_proc_model
PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
service_at sched j x = 0 -> False
by rewrite -no_service_not_scheduled // => /negP.
Qed .
End IdealModelLemmas .