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.util.all .[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.behavior.all .
Require Export prosa.analysis.definitions.schedule_prefix.
Require Export prosa.analysis.facts.behavior.supply.
Require Export prosa.analysis.facts.model.scheduled.
(** * Service *)
(** In this file, we establish basic facts about the service received by
jobs. *)
(** To begin with, we provide some simple but handy rewriting rules for
[service] and [service_during]. *)
Section Composition .
(** Consider any job type and any processor state. *)
Context {Job : JobType}.
Context {PState : ProcessorState Job}.
(** For any given schedule... *)
Variable sched : schedule PState.
(** ...and any given job... *)
Variable j : Job.
(** ...we establish a number of useful rewriting rules that decompose
the service received during an interval into smaller intervals. *)
(** As a trivial base case, no job receives any service during an empty
interval. *)
Lemma service_during_geq :
forall t1 t2 ,
t1 >= t2 -> service_during sched j t1 t2 = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t2 <= t1 -> service_during sched j t1 t2 = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t2 <= t1 -> service_during sched j t1 t2 = 0
by move => ? ? ?; rewrite /service_during big_geq. Qed .
(** Conversely, if a job receives some service in some interval, then the
interval is not empty. *)
Corollary service_during_ge :
forall t1 t2 k ,
service_during sched j t1 t2 > k ->
t1 < t2.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall (t1 t2 : instant) (k : nat),
k < service_during sched j t1 t2 -> t1 < t2
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall (t1 t2 : instant) (k : nat),
k < service_during sched j t1 t2 -> t1 < t2
move => t1 t2 k GT.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant k : nat GT : k < service_during sched j t1 t2
t1 < t2
apply : (contraPltn _ GT) => LEQ.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant k : nat GT : k < service_during sched j t1 t2 LEQ : t2 <= t1
~ k < service_during sched j t1 t2
by move : (service_during_geq _ _ LEQ) => ->.
Qed .
(** Equally trivially, no job has received service prior to time zero. *)
Corollary service0 :
service sched j 0 = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
service sched j 0 = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
service sched j 0 = 0
by rewrite /service service_during_geq. Qed .
(** Trivially, an interval consisting of one time unit is equivalent to
[service_at]. *)
Lemma service_during_instant :
forall t ,
service_during sched j t t.+1 = service_at sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
service_during sched j t t.+1 = service_at sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
service_during sched j t t.+1 = service_at sched j t
by move => ?; rewrite /service_during big_nat_recr// big_geq. Qed .
(** Next, we observe that we can look at the service received during an
interval <<[t1, t3)>> as the sum of the service during [t1, t2) and [t2, t3)
for any t2 \in [t1, t3]. (The "_cat" suffix denotes the concatenation of
the two intervals.) *)
Lemma service_during_cat :
forall t1 t2 t3 ,
t1 <= t2 <= t3 ->
(service_during sched j t1 t2) + (service_during sched j t2 t3)
= service_during sched j t1 t3.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 t3 : nat,
t1 <= t2 <= t3 ->
service_during sched j t1 t2 +
service_during sched j t2 t3 =
service_during sched j t1 t3
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 t3 : nat,
t1 <= t2 <= t3 ->
service_during sched j t1 t2 +
service_during sched j t2 t3 =
service_during sched j t1 t3
by move => ? ? ? /andP[? ?]; rewrite -big_cat_nat. Qed .
(** Since [service] is just a special case of [service_during], the same holds
for [service]. *)
Lemma service_cat :
forall t1 t2 ,
t1 <= t2 ->
(service sched j t1) + (service_during sched j t1 t2)
= service sched j t2.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 ->
service sched j t1 + service_during sched j t1 t2 =
service sched j t2
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 ->
service sched j t1 + service_during sched j t1 t2 =
service sched j t2
move => ? ? ?; exact : service_during_cat. Qed .
(** As a special case, we observe that the service during an interval can be
decomposed into the first instant and the rest of the interval. *)
Lemma service_during_first_plus_later :
forall t1 t2 ,
t1 < t2 ->
(service_at sched j t1) + (service_during sched j t1.+1 t2)
= service_during sched j t1 t2.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t1 < t2 ->
service_at sched j t1 +
service_during sched j t1.+1 t2 =
service_during sched j t1 t2
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t1 < t2 ->
service_at sched j t1 +
service_during sched j t1.+1 t2 =
service_during sched j t1 t2
by move => ? ? ?; rewrite -service_during_instant service_during_cat// leqnSn.
Qed .
(** Symmetrically, we have the same for the end of the interval. *)
Lemma service_during_last_plus_before :
forall t1 t2 ,
t1 <= t2 ->
(service_during sched j t1 t2) + (service_at sched j t2)
= service_during sched j t1 t2.+1 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 ->
service_during sched j t1 t2 + service_at sched j t2 =
service_during sched j t1 t2.+1
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 ->
service_during sched j t1 t2 + service_at sched j t2 =
service_during sched j t1 t2.+1
move => t1 t2 ?; rewrite -(service_during_cat t1 t2 t2.+1 ) ?leqnSn ?andbT //.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : nat _Hyp_ : t1 <= t2
service_during sched j t1 t2 + service_at sched j t2 =
service_during sched j t1 t2 +
service_during sched j t2 t2.+1
by rewrite service_during_instant.
Qed .
(** And hence also for [service]. *)
Corollary service_last_plus_before :
forall t ,
(service sched j t) + (service_at sched j t)
= service sched j t.+1 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
service sched j t + service_at sched j t =
service sched j t.+1
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
service sched j t + service_at sched j t =
service sched j t.+1
move => ?; exact : service_during_last_plus_before. Qed .
(** Finally, we deconstruct the service received during an interval <<[t1, t3)>>
into the service at a midpoint t2 and the service in the intervals before
and after. *)
Lemma service_split_at_point :
forall t1 t2 t3 ,
t1 <= t2 < t3 ->
(service_during sched j t1 t2) + (service_at sched j t2) + (service_during sched j t2.+1 t3)
= service_during sched j t1 t3.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 t3 : nat,
t1 <= t2 < t3 ->
service_during sched j t1 t2 + service_at sched j t2 +
service_during sched j t2.+1 t3 =
service_during sched j t1 t3
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 t3 : nat,
t1 <= t2 < t3 ->
service_during sched j t1 t2 + service_at sched j t2 +
service_during sched j t2.+1 t3 =
service_during sched j t1 t3
move => t1 t2 t3 /andP[t1t2 t2t3].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2, t3 : nat t1t2 : t1 <= t2 t2t3 : t2 < t3
service_during sched j t1 t2 + service_at sched j t2 +
service_during sched j t2.+1 t3 =
service_during sched j t1 t3
rewrite -addnA service_during_first_plus_later// service_during_cat//.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2, t3 : nat t1t2 : t1 <= t2 t2t3 : t2 < t3
t1 <= t2 <= t3
by rewrite t1t2 ltnW.
Qed .
End Composition .
(** As a common special case, we establish facts about schedules in which a
job receives either 1 or 0 service units at all times. *)
Section UnitService .
(** Consider any job type and any processor state. *)
Context {Job : JobType}.
Context {PState : ProcessorState Job}.
(** Let's consider a unit-service model... *)
Hypothesis H_unit_service : unit_service_proc_model PState.
(** ...and a given schedule. *)
Variable sched : schedule PState.
(** Let [j] be any job that is to be scheduled. *)
Variable j : Job.
(** First, we prove that the instantaneous service cannot be greater than 1, ... *)
Lemma service_at_most_one :
forall t , service_at sched j t <= 1 .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t : instant, service_at sched j t <= 1
Proof .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t : instant, service_at sched j t <= 1
by rewrite /service_at. Qed .
(** ... which implies that the instantaneous service always equals to 0 or 1. *)
Corollary service_is_zero_or_one :
forall t , service_at sched j t = 0 \/ service_at sched j t = 1 .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t : instant,
service_at sched j t = 0 \/ service_at sched j t = 1
Proof .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t : instant,
service_at sched j t = 0 \/ service_at sched j t = 1
move => t.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant
service_at sched j t = 0 \/ service_at sched j t = 1
by case : service_at (service_at_most_one t) => [|[|//]] _; [left |right ].
Qed .
(** Next we prove that the cumulative service received by job [j] in
any interval of length [delta] is at most [delta]. *)
Lemma cumulative_service_le_delta :
forall t delta , service_during sched j t (t + delta) <= delta.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall (t : instant) (delta : nat),
service_during sched j t (t + delta) <= delta
Proof .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall (t : instant) (delta : nat),
service_during sched j t (t + delta) <= delta
move => t delta; rewrite -[X in _ <= X](sum_of_ones t).Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat
service_during sched j t (t + delta) <=
\sum_(t <= x < t + delta) 1
apply : leq_sum => t' _; exact : service_at_most_one.
Qed .
(** Conversely, we prove that if the cumulative service received by
job [j] in an interval of length [delta] is greater than or
equal to [ρ], then [ρ ≤ delta]. *)
Lemma cumulative_service_ge_delta :
forall t delta ρ ,
ρ <= service_during sched j t (t + delta) ->
ρ <= delta.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall (t : instant) (delta ρ : nat),
ρ <= service_during sched j t (t + delta) ->
ρ <= delta
Proof .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall (t : instant) (delta ρ : nat),
ρ <= service_during sched j t (t + delta) ->
ρ <= delta
move => ??? /leq_trans; apply ; exact : cumulative_service_le_delta. Qed .
Section ServiceIsUnitGrowthFunction .
(** We show that the service received by any job [j] during any interval is
a unit growth function... *)
Lemma service_during_is_unit_growth_function :
forall t0 ,
unit_growth_function (service_during sched j t0).Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t0 : instant,
unit_growth_function (service_during sched j t0)
Proof .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t0 : instant,
unit_growth_function (service_during sched j t0)
move => t0 t1.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t0 : instant t1 : nat
service_during sched j t0 (t1 + 1 ) <=
service_during sched j t0 t1 + 1
have [LEQ|LT]:= leqP t0 t1; last by rewrite service_during_geq; lia .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t0 : instant t1 : nat LEQ : t0 <= t1
service_during sched j t0 (t1 + 1 ) <=
service_during sched j t0 t1 + 1
rewrite addn1 -service_during_last_plus_before // leq_add2l.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t0 : instant t1 : nat LEQ : t0 <= t1
service_at sched j t1 <= 1
exact : service_at_most_one.
Qed .
(** ... and restate the same observation in terms of [service]. *)
Corollary service_is_unit_growth_function :
unit_growth_function (service sched j).Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
unit_growth_function (service sched j)
Proof .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
unit_growth_function (service sched j)
by apply : service_during_is_unit_growth_function. Qed .
(** It follows that [service_during] does not skip over any values. *)
Corollary exists_intermediate_service_during :
forall t0 t1 t2 s ,
t0 <= t1 <= t2 ->
service_during sched j t0 t1 <= s < service_during sched j t0 t2 ->
exists t ,
t1 <= t < t2 /\
service_during sched j t0 t = s.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t0 t1 t2 s : nat,
t0 <= t1 <= t2 ->
service_during sched j t0 t1 <= s <
service_during sched j t0 t2 ->
exists t : nat,
t1 <= t < t2 /\ service_during sched j t0 t = s
Proof .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t0 t1 t2 s : nat,
t0 <= t1 <= t2 ->
service_during sched j t0 t1 <= s <
service_during sched j t0 t2 ->
exists t : nat,
t1 <= t < t2 /\ service_during sched j t0 t = s
move => t0 t1 t2 s /andP [t0t1 t1t2] SERV.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t0, t1, t2, s : nat t0t1 : t0 <= t1 t1t2 : t1 <= t2 SERV : service_during sched j t0 t1 <= s <
service_during sched j t0 t2
exists t : nat,
t1 <= t < t2 /\ service_during sched j t0 t = s
apply : exists_intermediate_point => //.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t0, t1, t2, s : nat t0t1 : t0 <= t1 t1t2 : t1 <= t2 SERV : service_during sched j t0 t1 <= s <
service_during sched j t0 t2
unit_growth_function (service_during sched j t0)
exact : service_during_is_unit_growth_function.
Qed .
(** To restate this observation in terms of [service], let [s] be any value
less than the service received by job [j] by time [t]. *)
Variable t : instant.
Variable s : duration.
Hypothesis H_less_than_s : s < service sched j t.
(** There necessarily exists an earlier time [t'] where job [j] had [s]
units of service. *)
Corollary exists_intermediate_service :
exists t' ,
t' < t /\
service sched j t' = s.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant s : duration H_less_than_s : s < service sched j t
exists t' : nat, t' < t /\ service sched j t' = s
Proof .Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant s : duration H_less_than_s : s < service sched j t
exists t' : nat, t' < t /\ service sched j t' = s
apply : (exists_intermediate_point _ service_is_unit_growth_function 0 ) => //.Job : JobType PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant s : duration H_less_than_s : s < service sched j t
service sched j 0 <= s < service sched j t
by rewrite service0.
Qed .
End ServiceIsUnitGrowthFunction .
End UnitService .
(** In this section we prove a lemma about the service received by a
job in a fully-consuming processor schedule. *)
Section FullyConsumingProcessor .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
(** Consider any kind of fully-supply-consuming processor state model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** We show that, given that the processor provides supply at a time
instant [t], the fact that a job [j] is scheduled at time [t]
implies that the job receives service at time [t]. Intuitively,
this lemma states that "inside a supply" the model is equivalent
to the ideal uniprocessor model. *)
Lemma ideal_progress_inside_supplies :
forall j t ,
has_supply sched t ->
scheduled_at sched j t ->
receives_service_at sched j t.Task : TaskType Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobTask Job Task PState : ProcessorState Job H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job sched : schedule PState
forall (j : Job) (t : instant),
has_supply sched t ->
scheduled_at sched j t ->
receives_service_at sched j t
Proof .Task : TaskType Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobTask Job Task PState : ProcessorState Job H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job sched : schedule PState
forall (j : Job) (t : instant),
has_supply sched t ->
scheduled_at sched j t ->
receives_service_at sched j t
by move => jo to SUP SCHED; rewrite /receives_service_at H_consumed_supply_proc_model //.
Qed .
End FullyConsumingProcessor .
(** We establish a basic fact about the monotonicity of service. *)
Section Monotonicity .
(** Consider any job type and any processor model. *)
Context {Job : JobType}.
Context {PState : ProcessorState Job}.
(** Consider any given schedule... *)
Variable sched : schedule PState.
(** ...and a given job that is to be scheduled. *)
Variable j : Job.
(** We observe that the amount of service received is monotonic by definition. *)
Lemma service_monotonic :
forall t1 t2 ,
t1 <= t2 ->
service sched j t1 <= service sched j t2.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 -> service sched j t1 <= service sched j t2
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 -> service sched j t1 <= service sched j t2
by move => t1 t2 ?; rewrite -(service_cat _ _ t1 t2)// leq_addr. Qed .
End Monotonicity .
(** In the following, we establish a collection of facts relating
service with predicates [scheduled_in] and [scheduled_at]. *)
Section RelationToScheduled .
(** Consider any job type and any processor model. *)
Context {Job : JobType}.
Context {PState : ProcessorState Job}.
(** Consider any given schedule... *)
Variable sched : schedule PState.
(** ...and a given job that is to be scheduled. *)
Variable j : Job.
(** We observe that a job that isn't scheduled in a given processor
state cannot possibly receive service in that state. *)
Lemma service_in_implies_scheduled_in :
forall s ,
~~ scheduled_in j s -> service_in j s = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall s : PState,
~~ scheduled_in j s -> service_in j s = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall s : PState,
~~ scheduled_in j s -> service_in j s = 0
move => s.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job s : PState
~~ scheduled_in j s -> service_in j s = 0
move => /existsP Hsched; apply /eqP; rewrite sum_nat_eq0; apply /forallP => c.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job s : PState Hsched : ~ (exists x : Core, scheduled_on j s x) c : Core
true ==> (service_on j s c == 0 )
rewrite service_on_implies_scheduled_on//.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job s : PState Hsched : ~ (exists x : Core, scheduled_on j s x) c : Core
~~ scheduled_on j s c
by apply /negP => ?; apply : Hsched; exists c .
Qed .
(** In particular, it cannot receive service at any given time. *)
Corollary not_scheduled_implies_no_service :
forall t ,
~~ scheduled_at sched j t -> service_at sched j t = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
~~ scheduled_at sched j t -> service_at sched j t = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
~~ scheduled_at sched j t -> service_at sched j t = 0
move => ?; exact : service_in_implies_scheduled_in. Qed .
(** Similarly, if a job is not scheduled during an interval, then it
does not receive any service in that interval. *)
Lemma not_scheduled_during_implies_zero_service :
forall t1 t2 ,
(forall t , t1 <= t < t2 -> ~~ scheduled_at sched j t) ->
service_during sched j t1 t2 = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
(forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t) ->
service_during sched j t1 t2 = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : nat,
(forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t) ->
service_during sched j t1 t2 = 0
move => t1 t2; rewrite big_nat_eq0 => + t titv => /(_ t titv).Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2, t : nat titv : t1 <= t < t2
~~ scheduled_at sched j t -> service_at sched j t = 0
by apply not_scheduled_implies_no_service.
Qed .
(** Conversely, if the job's instantaneous received service is
positive, then it must be scheduled. *)
Lemma service_at_implies_scheduled_at :
forall t ,
service_at sched j t > 0 -> scheduled_at sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
0 < service_at sched j t -> scheduled_at sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
0 < service_at sched j t -> scheduled_at sched j t
move => t; case SCHEDULED: scheduled_at => //.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t : instant SCHEDULED : scheduled_at sched j t = false
0 < service_at sched j t -> false
by rewrite not_scheduled_implies_no_service// negbT.
Qed .
(** Thus, if the cumulative amount of service changes, then it must
be scheduled, too. *)
Lemma service_delta_implies_scheduled :
forall t ,
service sched j t < service sched j t.+1 -> scheduled_at sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
service sched j t < service sched j t.+1 ->
scheduled_at sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
service sched j t < service sched j t.+1 ->
scheduled_at sched j t
move => t; rewrite -service_last_plus_before -ltn_subLR// subnn.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t : instant
0 < service_at sched j t -> scheduled_at sched j t
exact : service_at_implies_scheduled_at.
Qed .
(** We observe that a job receives cumulative service during some interval iff
it receives services at some specific time in the interval. *)
Lemma service_during_service_at :
forall t1 t2 ,
service_during sched j t1 t2 > 0
<->
exists t ,
t1 <= t < t2 /\
service_at sched j t > 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 <->
(exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t)
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 <->
(exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t)
move => t1 t2.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant
0 < service_during sched j t1 t2 <->
(exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t)
split => [|[t [titv nz_serv]]].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
- Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
rewrite sum_nat_gt0 filter_predT => /hasP [t IN GT0].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : Datatypes_nat__canonical__eqtype_Equality IN : t \in index_iota t1 t2 GT0 : 0 < service_at sched j t
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
by exists t ; split ; [rewrite -mem_index_iota|].
- Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat titv : t1 <= t < t2 nz_serv : 0 < service_at sched j t
0 < service_during sched j t1 t2
rewrite sum_nat_gt0; apply /hasP.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat titv : t1 <= t < t2 nz_serv : 0 < service_at sched j t
exists2 x : Datatypes_nat__canonical__eqtype_Equality,
x \in [seq _ <- index_iota t1 t2 | true] &
0 < service_at sched j x
by exists t ; [rewrite filter_predT mem_index_iota|].
Qed .
(** Thus, any job that receives some service during an interval must be
scheduled at some point during the interval... *)
Corollary cumulative_service_implies_scheduled :
forall t1 t2 ,
service_during sched j t1 t2 > 0 ->
exists t ,
t1 <= t < t2 /\
scheduled_at sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 ->
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 ->
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t
move => t1 t2; rewrite service_during_service_at => -[t' [TIMES SERVICED]].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t' : nat TIMES : t1 <= t' < t2 SERVICED : 0 < service_at sched j t'
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t
exists t' ; split => //; exact : service_at_implies_scheduled_at.
Qed .
(** ...which implies that any job with positive cumulative service must have
been scheduled at some point. *)
Corollary positive_service_implies_scheduled_before :
forall t ,
service sched j t > 0 -> exists t' , (t' < t /\ scheduled_at sched j t').Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
0 < service sched j t ->
exists t' : nat, t' < t /\ scheduled_at sched j t'
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t : instant,
0 < service sched j t ->
exists t' : nat, t' < t /\ scheduled_at sched j t'
by move => t /cumulative_service_implies_scheduled[t' ?]; exists t' .
Qed .
(** We can further strengthen [service_during_service_at] to yield the
earliest point in time at which a job receives service in an interval... *)
Corollary service_during_service_at_earliest :
forall t1 t2 ,
service_during sched j t1 t2 > 0 ->
exists t ,
t1 <= t < t2
/\ service_at sched j t > 0
/\ service_during sched j t1 t = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\
0 < service_at sched j t /\
service_during sched j t1 t = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\
0 < service_at sched j t /\
service_during sched j t1 t = 0
move => t1 t2.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\
0 < service_at sched j t /\
service_during sched j t1 t = 0
rewrite service_during_service_at => [[t [IN SAT]]].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j t
exists t : nat,
t1 <= t < t2 /\
0 < service_at sched j t /\
service_during sched j t1 t = 0
set P := fun t' => (service_at sched j t' > 0 ) && (t1 <= t' < t2).Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tP := fun t' : instant =>
[&& 0 < service_at sched j t', t1 <= t' & t' < t2]: instant -> bool
exists t : nat,
t1 <= t < t2 /\
0 < service_at sched j t /\
service_during sched j t1 t = 0
have WITNESS: exists t' , P t' by exists t ; apply /andP.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tP := fun t' : instant =>
[&& 0 < service_at sched j t', t1 <= t' & t' < t2]: instant -> bool WITNESS : exists t' : instant, P t'
exists t : nat,
t1 <= t < t2 /\
0 < service_at sched j t /\
service_during sched j t1 t = 0
have [t' /andP [SCHED' IN'] LEAST] := ex_minnP WITNESS.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tP := fun t' : instant =>
[&& 0 < service_at sched j t', t1 <= t' & t' < t2]: instant -> bool WITNESS : exists t' : instant, P t't' : nat SCHED' : 0 < service_at sched j t'IN' : t1 <= t' < t2 LEAST : forall n : nat, P n -> t' <= n
exists t : nat,
t1 <= t < t2 /\
0 < service_at sched j t /\
service_during sched j t1 t = 0
exists t' ; repeat (split => //).Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tP := fun t' : instant =>
[&& 0 < service_at sched j t', t1 <= t' & t' < t2]: instant -> bool WITNESS : exists t' : instant, P t't' : nat SCHED' : 0 < service_at sched j t'IN' : t1 <= t' < t2 LEAST : forall n : nat, P n -> t' <= n
service_during sched j t1 t' = 0
apply /eqP/contraT.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tP := fun t' : instant =>
[&& 0 < service_at sched j t', t1 <= t' & t' < t2]: instant -> bool WITNESS : exists t' : instant, P t't' : nat SCHED' : 0 < service_at sched j t'IN' : t1 <= t' < t2 LEAST : forall n : nat, P n -> t' <= n
service_during sched j t1 t' != 0 -> false
rewrite -lt0n service_during_service_at => [[t'' [IN'' SAT'']]].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tP := fun t' : instant =>
[&& 0 < service_at sched j t', t1 <= t' & t' < t2]: instant -> bool WITNESS : exists t' : instant, P t't' : nat SCHED' : 0 < service_at sched j t'IN' : t1 <= t' < t2 LEAST : forall n : nat, P n -> t' <= nt'' : nat IN'' : t1 <= t'' < t' SAT'' : 0 < service_at sched j t''
false
have : t' <= t''; last by lia .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tP := fun t' : instant =>
[&& 0 < service_at sched j t', t1 <= t' & t' < t2]: instant -> bool WITNESS : exists t' : instant, P t't' : nat SCHED' : 0 < service_at sched j t'IN' : t1 <= t' < t2 LEAST : forall n : nat, P n -> t' <= nt'' : nat IN'' : t1 <= t'' < t' SAT'' : 0 < service_at sched j t''
t' <= t''
apply /LEAST/andP; split => //.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tP := fun t' : instant =>
[&& 0 < service_at sched j t', t1 <= t' & t' < t2]: instant -> bool WITNESS : exists t' : instant, P t't' : nat SCHED' : 0 < service_at sched j t'IN' : t1 <= t' < t2 LEAST : forall n : nat, P n -> t' <= nt'' : nat IN'' : t1 <= t'' < t' SAT'' : 0 < service_at sched j t''
t1 <= t'' < t2
by lia .
Qed .
(** ... and make a similar observation about the same point in time
w.r.t. [scheduled_at]. *)
Corollary service_during_scheduled_at_earliest :
forall t1 t2 ,
service_during sched j t1 t2 > 0 ->
exists t ,
t1 <= t < t2
/\ scheduled_at sched j t
/\ service_during sched j t1 t = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = 0
move => t1 t2 SERVICED.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant SERVICED : 0 < service_during sched j t1 t2
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = 0
have [t [IN [SAT NONE]]] := service_during_service_at_earliest t1 t2 SERVICED.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant SERVICED : 0 < service_during sched j t1 t2t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tNONE : service_during sched j t1 t = 0
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = 0
exists t ; repeat (split => //).Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant SERVICED : 0 < service_during sched j t1 t2t : nat IN : t1 <= t < t2 SAT : 0 < service_at sched j tNONE : service_during sched j t1 t = 0
scheduled_at sched j t
exact : service_at_implies_scheduled_at.
Qed .
(** If we can assume that a scheduled job always receives service, then we can
further relate above observations to [scheduled_at]. *)
Section GuaranteedService .
(** Assume [j] always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced : ideal_progress_proc_model PState.
(** In other words, not being scheduled is equivalent to receiving zero
service. *)
Lemma no_service_not_scheduled :
forall t ,
~~ scheduled_at sched j t <-> service_at sched j t = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
~~ scheduled_at sched j t <-> service_at sched j t = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
~~ scheduled_at sched j t <-> service_at sched j t = 0
move => t.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant
~~ scheduled_at sched j t <-> service_at sched j t = 0
split => [|NO_SERVICE]; first exact : service_in_implies_scheduled_in.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant NO_SERVICE : service_at sched j t = 0
~~ scheduled_at sched j t
apply : (contra (H_scheduled_implies_serviced j (sched t))).Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant NO_SERVICE : service_at sched j t = 0
~~ (0 < service_in j (sched t))
by rewrite -eqn0Ngt -NO_SERVICE.
Qed .
(** Then, if a job does not receive any service during an interval, it
is not scheduled. *)
Lemma no_service_during_implies_not_scheduled :
forall t1 t2 ,
service_during sched j t1 t2 = 0 ->
forall t ,
t1 <= t < t2 -> ~~ scheduled_at sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : instant,
service_during sched j t1 t2 = 0 ->
forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : instant,
service_during sched j t1 t2 = 0 ->
forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t
move => t1 t2.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2 : instant
service_during sched j t1 t2 = 0 ->
forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t
by move => + t titv; rewrite no_service_not_scheduled big_nat_eq0; apply .
Qed .
(** If a job is scheduled at some point in an interval, it receives
positive cumulative service during the interval... *)
Lemma scheduled_implies_cumulative_service :
forall t1 t2 ,
(exists t ,
t1 <= t < t2 /\
scheduled_at sched j t) ->
service_during sched j t1 t2 > 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : nat,
(exists t : nat,
t1 <= t < t2 /\ scheduled_at sched j t) ->
0 < service_during sched j t1 t2
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : nat,
(exists t : nat,
t1 <= t < t2 /\ scheduled_at sched j t) ->
0 < service_during sched j t1 t2
move => t1 t2 [t [titv sch]]; rewrite service_during_service_at.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2, t : nat titv : t1 <= t < t2 sch : scheduled_at sched j t
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
exists t ; split => //; exact : H_scheduled_implies_serviced.
Qed .
(** ...which again applies to total service, too. *)
Corollary scheduled_implies_nonzero_service :
forall t ,
(exists t' ,
t' < t /\
scheduled_at sched j t') ->
service sched j t > 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : nat,
(exists t' : nat, t' < t /\ scheduled_at sched j t') ->
0 < service sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : nat,
(exists t' : nat, t' < t /\ scheduled_at sched j t') ->
0 < service sched j t
move => t.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : nat
(exists t' : nat, t' < t /\ scheduled_at sched j t') ->
0 < service sched j t
by move => [t' ?]; apply : scheduled_implies_cumulative_service; exists t' .
Qed .
End GuaranteedService .
(** Furthermore, if we know that jobs are not released early, then we can
narrow the interval during which they must have been scheduled. *)
Section AfterArrival .
Context `{JobArrival Job}.
(** Assume that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive :
jobs_must_arrive_to_execute sched.
(** We prove that any job with positive cumulative service at time [t] must
have been scheduled some time since its arrival and before time [t]. *)
Lemma positive_service_implies_scheduled_since_arrival :
forall t ,
service sched j t > 0 ->
exists t' , (job_arrival j <= t' < t /\ scheduled_at sched j t').Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
0 < service sched j t ->
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
0 < service sched j t ->
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
move => t /positive_service_implies_scheduled_before[t' [t't sch]].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant t' : nat t't : t' < t sch : scheduled_at sched j t'
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
exists t' ; split => //; rewrite t't andbT; exact : H_jobs_must_arrive.
Qed .
Lemma not_scheduled_before_arrival :
forall t , t < job_arrival j -> ~~ scheduled_at sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t < job_arrival j -> ~~ scheduled_at sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t < job_arrival j -> ~~ scheduled_at sched j t
by move => t ?; apply : (contra (H_jobs_must_arrive j t)); rewrite -ltnNge.
Qed .
(** We show that job [j] does not receive service at any time [t] prior to its
arrival. *)
Lemma service_before_job_arrival_zero :
forall t ,
t < job_arrival j ->
service_at sched j t = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t < job_arrival j -> service_at sched j t = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t < job_arrival j -> service_at sched j t = 0
move => t NOT_ARR; rewrite not_scheduled_implies_no_service//.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : nat NOT_ARR : t < job_arrival j
~~ scheduled_at sched j t
exact : not_scheduled_before_arrival.
Qed .
(** Note that the same property applies to the cumulative service. *)
Lemma cumulative_service_before_job_arrival_zero :
forall t1 t2 : instant,
t2 <= job_arrival j ->
service_during sched j t1 t2 = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t1 t2 : instant,
t2 <= job_arrival j ->
service_during sched j t1 t2 = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t1 t2 : instant,
t2 <= job_arrival j ->
service_during sched j t1 t2 = 0
move => t1 t2 early; rewrite big_nat_eq0 => t /andP[_ t_lt_t2].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : instant early : t2 <= job_arrival j t : nat t_lt_t2 : t < t2
service_at sched j t = 0
apply : service_before_job_arrival_zero; exact : leq_trans early.
Qed .
(** Hence, one can ignore the service received by a job before its arrival
time... *)
Lemma ignore_service_before_arrival :
forall t1 t2 ,
t1 <= job_arrival j ->
t2 >= job_arrival j ->
service_during sched j t1 t2 = service_during sched j (job_arrival j) t2.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t1 t2 : nat,
t1 <= job_arrival j ->
job_arrival j <= t2 ->
service_during sched j t1 t2 =
service_during sched j (job_arrival j) t2
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t1 t2 : nat,
t1 <= job_arrival j ->
job_arrival j <= t2 ->
service_during sched j t1 t2 =
service_during sched j (job_arrival j) t2
move => t1 t2 t1_le t2_ge.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : nat t1_le : t1 <= job_arrival j t2_ge : job_arrival j <= t2
service_during sched j t1 t2 =
service_during sched j (job_arrival j) t2
rewrite -(service_during_cat sched _ _ (job_arrival j)); last exact /andP.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : nat t1_le : t1 <= job_arrival j t2_ge : job_arrival j <= t2
service_during sched j t1 (job_arrival j) +
service_during sched j (job_arrival j) t2 =
service_during sched j (job_arrival j) t2
by rewrite cumulative_service_before_job_arrival_zero.
Qed .
(** ... which we can also state in terms of cumulative service. *)
Corollary no_service_before_arrival :
forall t ,
t <= job_arrival j -> service sched j t = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t <= job_arrival j -> service sched j t = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job H : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t <= job_arrival j -> service sched j t = 0
exact : cumulative_service_before_job_arrival_zero. Qed .
End AfterArrival .
(** In this section, we prove some lemmas about time instants with same
service. *)
Section TimesWithSameService .
(** Consider any time instants [t1] and [t2]... *)
Variable t1 t2 : instant.
(** ...where [t1] is no later than [t2]... *)
Hypothesis H_t1_le_t2 : t1 <= t2.
(** ...and where job [j] has received the same amount of service. *)
Hypothesis H_same_service : service sched j t1 = service sched j t2.
(** First, we observe that this means that the job receives no service
during <<[t1, t2)>>... *)
Lemma constant_service_implies_no_service_during :
service_during sched j t1 t2 = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
service_during sched j t1 t2 = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
service_during sched j t1 t2 = 0
move : H_same_service; rewrite -(service_cat _ _ t1 t2)// => /eqP.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
service sched j t1 ==
service sched j t1 + service_during sched j t1 t2 ->
service_during sched j t1 t2 = 0
by rewrite -[X in X == _]addn0 eqn_add2l => /eqP.
Qed .
(** ...which of course implies that it does not receive service at any
point, either. *)
Lemma constant_service_implies_not_scheduled :
forall t ,
t1 <= t < t2 -> service_at sched j t = 0 .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
forall t : nat,
t1 <= t < t2 -> service_at sched j t = 0
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
forall t : nat,
t1 <= t < t2 -> service_at sched j t = 0
move => t titv.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : nat titv : t1 <= t < t2
service_at sched j t = 0
have := constant_service_implies_no_service_during.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : nat titv : t1 <= t < t2
service_during sched j t1 t2 = 0 ->
service_at sched j t = 0
rewrite big_nat_eq0; exact .
Qed .
(** We show that job [j] receives service at some point [t < t1]
iff [j] receives service at some point [t' < t2]. *)
Lemma same_service_implies_serviced_at_earlier_times :
[exists t : 'I_t1, service_at sched j t > 0 ] =
[exists t' : 'I_t2, service_at sched j t' > 0 ].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
[exists t , 0 < service_at sched j t] =
[exists t' , 0 < service_at sched j t']
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
[exists t , 0 < service_at sched j t] =
[exists t' , 0 < service_at sched j t']
apply /idP/idP => /existsP[t serv].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : fintype_ordinal__canonical__fintype_Finite t1 serv : 0 < service_at sched j t
[exists t' , 0 < service_at sched j t']
{ Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : fintype_ordinal__canonical__fintype_Finite t1 serv : 0 < service_at sched j t
[exists t' , 0 < service_at sched j t']
by apply /existsP; exists (widen_ord H_t1_le_t2 t ). } Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : fintype_ordinal__canonical__fintype_Finite t2 serv : 0 < service_at sched j t
[exists t , 0 < service_at sched j t]
have [t_lt_t1|t1_le_t] := ltnP t t1.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : fintype_ordinal__canonical__fintype_Finite t2 serv : 0 < service_at sched j tt_lt_t1 : t < t1
[exists t , 0 < service_at sched j t]
{ Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : fintype_ordinal__canonical__fintype_Finite t2 serv : 0 < service_at sched j tt_lt_t1 : t < t1
[exists t , 0 < service_at sched j t]
by apply /existsP; exists (Ordinal t_lt_t1 ). } Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : fintype_ordinal__canonical__fintype_Finite t2 serv : 0 < service_at sched j tt1_le_t : t1 <= t
[exists t , 0 < service_at sched j t]
exfalso ; move : serv; apply /negP; rewrite -eqn0Ngt.Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : fintype_ordinal__canonical__fintype_Finite t2 t1_le_t : t1 <= t
service_at sched j t == 0
by apply /eqP/constant_service_implies_not_scheduled; rewrite t1_le_t /=.
Qed .
(** Then, under the assumption that scheduled jobs receives service,
we can translate this into a claim about scheduled_at. *)
(** Assume [j] always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced : ideal_progress_proc_model PState.
(** We show that job [j] is scheduled at some point [t < t1] iff [j] is scheduled
at some point [t' < t2]. *)
Lemma same_service_implies_scheduled_at_earlier_times :
[exists t : 'I_t1, scheduled_at sched j t] =
[exists t' : 'I_t2, scheduled_at sched j t'].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState
[exists t , scheduled_at sched j t] =
[exists t' , scheduled_at sched j t']
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState
[exists t , scheduled_at sched j t] =
[exists t' , scheduled_at sched j t']
have CONV B : [exists b : 'I_B, scheduled_at sched j b]
= [exists b : 'I_B, service_at sched j b > 0 ].Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat
[exists b , scheduled_at sched j b] =
[exists b , 0 < service_at sched j b]
{ Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat
[exists b , scheduled_at sched j b] =
[exists b , 0 < service_at sched j b]
apply /idP/idP => /existsP[b P]; apply /existsP; exists b .Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat b : fintype_ordinal__canonical__fintype_Finite B P : scheduled_at sched j b
0 < service_at sched j b
- Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat b : fintype_ordinal__canonical__fintype_Finite B P : scheduled_at sched j b
0 < service_at sched j b
exact : H_scheduled_implies_serviced.
- Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat b : fintype_ordinal__canonical__fintype_Finite B P : 0 < service_at sched j b
scheduled_at sched j b
exact : service_at_implies_scheduled_at. } Job : JobType PState : ProcessorState Job sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState CONV : forall B : nat,
[exists b , scheduled_at sched j b] =
[exists b , 0 < service_at sched j b]
[exists t , scheduled_at sched j t] =
[exists t' , scheduled_at sched j t']
by rewrite !CONV same_service_implies_serviced_at_earlier_times.
Qed .
End TimesWithSameService .
End RelationToScheduled .
(** In this section we prove a few auxiliary lemmas about the service
received by a job. *)
Section GenericProcessor .
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
Context `{PState : ProcessorState Job}.
(** Consider any valid arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and 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.
(** If a job [j] receives service at time [t], then [j] is in the
set of served jobs at time [t] ... *)
Lemma receives_service_and_served_at_consistent :
forall j t ,
receives_service_at sched j t ->
j \in served_jobs_at arr_seq sched t.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
receives_service_at sched j t ->
j \in served_jobs_at arr_seq sched t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
receives_service_at sched j t ->
j \in served_jobs_at arr_seq sched t
move => jo t RSERV; rewrite mem_filter; apply /andP; split => //.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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 jo : Job t : instant RSERV : receives_service_at sched jo t
jo \in arrivals_up_to arr_seq t
apply service_at_implies_scheduled_at in RSERV.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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 jo : Job t : instant RSERV : scheduled_at sched jo t
jo \in arrivals_up_to arr_seq t
by apply : arrivals_before_scheduled_at.
Qed .
(** ... and vice versa, if [j] is in the set of jobs receiving
service at time [t], then [j] receives service at time [t]. *)
Lemma served_at_and_receives_service_consistent :
forall j t ,
j \in served_jobs_at arr_seq sched t ->
receives_service_at sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
j \in served_jobs_at arr_seq sched t ->
receives_service_at sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
j \in served_jobs_at arr_seq sched t ->
receives_service_at sched j t
by move => jo t; rewrite mem_filter => /andP [RSERV _].
Qed .
(** If the processor is idle at time [t], then no job receives
service at time [t]. *)
Lemma no_service_received_when_idle :
forall j t ,
is_idle arr_seq sched t ->
~~ receives_service_at sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
is_idle arr_seq sched t ->
~~ receives_service_at sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
is_idle arr_seq sched t ->
~~ receives_service_at sched j t
move => j t IDLE; apply /negP => SERV.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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 j : Job t : instant IDLE : is_idle arr_seq sched t SERV : receives_service_at sched j t
False
eapply not_scheduled_when_idle with (j := j) in IDLE => //.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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 j : Job t : instant IDLE : ~~ scheduled_at sched j t SERV : receives_service_at sched j t
False
apply service_at_implies_scheduled_at in SERV.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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 j : Job t : instant IDLE : ~~ scheduled_at sched j t SERV : scheduled_at sched j t
False
by rewrite SERV in IDLE.
Qed .
(** Next, if a job [j] receives service at time [t],
then the processor has supply at time [t]. *)
Lemma receives_service_implies_has_supply :
forall j t ,
receives_service_at sched j t ->
has_supply sched t.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
receives_service_at sched j t -> has_supply sched t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
receives_service_at sched j t -> has_supply sched t
by move => j SERV; apply : pos_service_impl_pos_supply.
Qed .
(** Similarly, if a job [j] receives service at time [t], then time
[t] is not a blackout time. *)
Lemma no_blackout_when_service_received :
forall j t ,
receives_service_at sched j t ->
~~ is_blackout sched t.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
receives_service_at sched j t ->
~~ is_blackout sched t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
receives_service_at sched j t ->
~~ is_blackout sched t
by move => j t RSERV; apply pos_service_impl_pos_supply in RSERV; rewrite negbK.
Qed .
(** Finally, if time [t] is a blackout time, then no job receives
service at time [t]. *)
Lemma no_service_during_blackout :
forall j t ,
is_blackout sched t ->
service_at sched j t = 0 .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
is_blackout sched t -> service_at sched j t = 0
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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
forall (j : Job) (t : instant),
is_blackout sched t -> service_at sched j t = 0
move => j t BL; apply /eqP; rewrite -leqn0; move_neq_up GE.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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 j : Job t : instant BL : is_blackout sched t GE : 0 < service_at sched j t
False
apply pos_service_impl_pos_supply in GE.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job 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 j : Job t : instant BL : is_blackout sched t GE : 0 < supply_at sched t
False
by rewrite /is_blackout /has_supply GE in BL.
Qed .
End GenericProcessor .
(** In this section we prove a lemma about the service received by a
job in a uniprocessor schedule. *)
Section UniProcessor .
(** Consider any type of jobs. *)
Context {Job : JobType}.
(** Consider any kind of uniprocessor state model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
(** Consider any schedule. *)
Variable sched : schedule PState.
(** If two jobs [j1] and [j2] receive service at the same instant
then [j1] is equal to [j2]. *)
Lemma only_one_job_receives_service_at_uni :
forall j1 j2 t ,
receives_service_at sched j1 t ->
receives_service_at sched j2 t ->
j1 = j2.Job : JobType PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState sched : schedule PState
forall (j1 j2 : Job) (t : instant),
receives_service_at sched j1 t ->
receives_service_at sched j2 t -> j1 = j2
Proof .Job : JobType PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState sched : schedule PState
forall (j1 j2 : Job) (t : instant),
receives_service_at sched j1 t ->
receives_service_at sched j2 t -> j1 = j2
move => j1 j2 t SERV1 SERV2.Job : JobType PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState sched : schedule PState j1, j2 : Job t : instant SERV1 : receives_service_at sched j1 t SERV2 : receives_service_at sched j2 t
j1 = j2
apply service_at_implies_scheduled_at in SERV1.Job : JobType PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState sched : schedule PState j1, j2 : Job t : instant SERV1 : scheduled_at sched j1 t SERV2 : receives_service_at sched j2 t
j1 = j2
apply service_at_implies_scheduled_at in SERV2.Job : JobType PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState sched : schedule PState j1, j2 : Job t : instant SERV1 : scheduled_at sched j1 t SERV2 : scheduled_at sched j2 t
j1 = j2
by apply (H_uniprocessor_proc_model j1 j2 sched t).
Qed .
End UniProcessor .
(** * Incremental Service in Unit-Service Schedules *)
(** In unit-service schedules, any job gains at most one unit of service at any
time. Hence, no job "skips" an service values, which we note with the lemma
[incremental_service_during] below. *)
Section IncrementalService .
(** Consider any job type, ... *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** ... any arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and any unit-service schedule of this arrival sequence. *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_unit_service : unit_service_proc_model PState.
(** We prove that if in some time interval <<[t1,t2)>> a job [j] receives [k]
units of service, then there exists a time instant <<t ∈ [t1,t2)>> such
that [j] is scheduled at time [t] and service of job [j] within interval
<<[t1,t)>> is equal to [k]. *)
Lemma incremental_service_during :
forall j t1 t2 k ,
service_during sched j t1 t2 > k ->
exists t , t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState
forall (j : Job) (t1 t2 : instant) (k : nat),
k < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState
forall (j : Job) (t1 t2 : instant) (k : nat),
k < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k
move => j t1 t2 k SERV.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant k : nat SERV : k < service_during sched j t1 t2
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k
have LE: t1 < t2 by move : (service_during_ge _ _ _ _ _ SERV).Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant k : nat SERV : k < service_during sched j t1 t2 LE : t1 < t2
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k
case : k SERV => [|k] SERV; first by apply service_during_scheduled_at_earliest in SERV.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k.+1
set P := fun t' => service_during sched j t1 t' >= k.+1 .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 P := fun t' : instant =>
k < service_during sched j t1 t': instant -> bool
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k.+1
have : exists t' : nat, t1 < t' <= t2 /\ (forall x : nat, t1 <= x < t' -> ~~ P x) /\ P t'.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 P := fun t' : instant =>
k < service_during sched j t1 t': instant -> bool
exists t' : nat,
t1 < t' <= t2 /\
(forall x : nat, t1 <= x < t' -> ~~ P x) /\ P t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 P := fun t' : instant =>
k < service_during sched j t1 t': instant -> bool
exists t' : nat,
t1 < t' <= t2 /\
(forall x : nat, t1 <= x < t' -> ~~ P x) /\ P t'
apply : (exists_first_intermediate_point P t1 t2); first by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 P := fun t' : instant =>
k < service_during sched j t1 t': instant -> bool
~~ P t1
- Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 P := fun t' : instant =>
k < service_during sched j t1 t': instant -> bool
~~ P t1
by rewrite /P service_during_geq //.
- Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 P := fun t' : instant =>
k < service_during sched j t1 t': instant -> bool
P t2
by rewrite /P; lia . } Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 P := fun t' : instant =>
k < service_during sched j t1 t': instant -> bool
(exists t' : nat,
t1 < t' <= t2 /\
(forall x : nat, t1 <= x < t' -> ~~ P x) /\ P t') ->
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k.+1
rewrite /P; move => [t' [IN' [LIMIT Pt']]]; clear P.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t'
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k.+1
set P'' := fun t'' => (t' <= t'' < t2) && (service_at sched j t'' > 0 ).Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k.+1
have WITNESS: exists t'' , P'' t''.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool
exists t'' : nat, P'' t''
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool
exists t'' : nat, P'' t''
have : 0 < service_during sched j t' t2;
last by rewrite service_during_service_at => [[t'' [IN'' SERVICED]]]
; exists t'' ; apply /andP; split .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool
0 < service_during sched j t' t2
move : SERV; rewrite -(service_during_cat _ _ t1 t'.-1 t2); last by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k, t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool
k.+1 <
service_during sched j t1 t'.-1 +
service_during sched j t'.-1 t2 ->
0 < service_during sched j t' t2
move => SERV.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k, t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool SERV : k.+1 <
service_during sched j t1 t'.-1 +
service_during sched j t'.-1 t2
0 < service_during sched j t' t2
have SERV2: service_during sched j t1 t'.-1 <= k
by rewrite leqNgt; apply (LIMIT t'.-1 ); lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k, t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool SERV : k.+1 <
service_during sched j t1 t'.-1 +
service_during sched j t'.-1 t2 SERV2 : service_during sched j t1 t'.-1 <= k
0 < service_during sched j t' t2
have : service_during sched j t'.-1 t2 >= 2 by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k, t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool SERV : k.+1 <
service_during sched j t1 t'.-1 +
service_during sched j t'.-1 t2 SERV2 : service_during sched j t1 t'.-1 <= k
1 < service_during sched j t'.-1 t2 ->
0 < service_during sched j t' t2
rewrite -service_during_first_plus_later; last by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k, t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool SERV : k.+1 <
service_during sched j t1 t'.-1 +
service_during sched j t'.-1 t2 SERV2 : service_during sched j t1 t'.-1 <= k
1 <
service_at sched j t'.-1 +
service_during sched j t'.-1 .+1 t2 ->
0 < service_during sched j t' t2
move : (IN') => /andP [LE' _]; rewrite (ltn_predK LE').Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k, t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool SERV : k.+1 <
service_during sched j t1 t'.-1 +
service_during sched j t'.-1 t2 SERV2 : service_during sched j t1 t'.-1 <= k LE' : t1 < t'
1 <
service_at sched j t'.-1 +
service_during sched j t' t2 ->
0 < service_during sched j t' t2
by case : (service_is_zero_or_one _ sched j t'.-1 ) => [//|->|->]; try lia . } Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k.+1
have [t''' /andP [IN''' SCHED'''] MIN] := ex_minnP WITNESS.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
exists t : nat,
t1 <= t < t2 /\
scheduled_at sched j t /\
service_during sched j t1 t = k.+1
exists t''' ; repeat split ; [by lia |by apply : service_at_implies_scheduled_at|].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
service_during sched j t1 t''' = k.+1
have ->: service_during sched j t1 t''' = service_during sched j t1 t'.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
service_during sched j t1 t''' =
service_during sched j t1 t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
service_during sched j t1 t''' =
service_during sched j t1 t'
rewrite -(service_during_cat _ _ t1 t' t'''); last by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
service_during sched j t1 t' +
service_during sched j t' t''' =
service_during sched j t1 t'
have [Z|POS] := leqP (service_during sched j t' t''') 0 ; first by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nPOS : 0 < service_during sched j t' t'''
service_during sched j t1 t' +
service_during sched j t' t''' =
service_during sched j t1 t'
exfalso .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nPOS : 0 < service_during sched j t' t'''
False
move : POS; rewrite service_during_service_at => [[x [xIN xSERV]]].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nx : nat xIN : t' <= x < t''' xSERV : 0 < service_at sched j x
False
have xP'': P'' x by apply /andP;split ; [by lia | by []].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nx : nat xIN : t' <= x < t''' xSERV : 0 < service_at sched j xxP'' : P'' x
False
by move : (MIN x xP''); lia . } Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)Pt' : k < service_during sched j t1 t' P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
service_during sched j t1 t' = k.+1
move : Pt'; rewrite leq_eqVlt => /orP [/eqP -> //|XL].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nXL : k.+1 < service_during sched j t1 t'
service_during sched j t1 t' = k.+1
exfalso .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nXL : k.+1 < service_during sched j t1 t'
False
move : XL.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
k.+1 < service_during sched j t1 t' -> False
have ->: service_during sched j t1 t' = service_during sched j t1 t'.-1 .+1
by move : (IN') => /andP [LE' _]; rewrite (ltn_predK LE').Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
k.+1 < service_during sched j t1 t'.-1 .+1 -> False
rewrite -service_during_last_plus_before; last by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= n
k.+1 <
service_during sched j t1 t'.-1 +
service_at sched j t'.-1 -> False
move => ABOVE.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nABOVE : k.+1 <
service_during sched j t1 t'.-1 +
service_at sched j t'.-1
False
have BELOW: service_during sched j t1 t'.-1 <= k
by rewrite leqNgt; apply (LIMIT t'.-1 ); lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nABOVE : k.+1 <
service_during sched j t1 t'.-1 +
service_at sched j t'.-1 BELOW : service_during sched j t1 t'.-1 <= k
False
have : service_at sched j t'.-1 > 1 by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nABOVE : k.+1 <
service_during sched j t1 t'.-1 +
service_at sched j t'.-1 BELOW : service_during sched j t1 t'.-1 <= k
1 < service_at sched j t'.-1 -> False
have : service_at sched j t'.-1 <= 1 by apply /service_at_most_one.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t1, t2 : instant LE : t1 < t2 k : nat SERV : k.+1 < service_during sched j t1 t2 t' : nat IN' : t1 < t' <= t2 LIMIT : forall x : nat,
t1 <= x < t' ->
~~ (k < service_during sched j t1 x)P'' := fun t'' : nat =>
(t' <= t'' < t2) && (0 < service_at sched j t''): nat -> bool WITNESS : exists t'' : nat, P'' t''t''' : nat IN''' : t' <= t''' < t2 SCHED''' : 0 < service_at sched j t'''MIN : forall n : nat, P'' n -> t''' <= nABOVE : k.+1 <
service_during sched j t1 t'.-1 +
service_at sched j t'.-1 BELOW : service_during sched j t1 t'.-1 <= k
service_at sched j t'.-1 <= 1 ->
1 < service_at sched j t'.-1 -> False
by lia .
Qed .
(** An implication of the above lemma is that for any job [j] that
has [k] units of service at time [t] and more than [k] units of
service at time [t'], there exists a time instant [st] such that
[t <= st < t'] and the job is scheduled but still has [k] units
of service. *)
Lemma kth_scheduling_time :
forall j t t' k ,
service sched j t = k ->
k < service sched j t' ->
exists st ,
t <= st < t'
/\ service sched j st = k
/\ scheduled_at sched j st.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState
forall (j : Job) (t t' : instant) (k : nat),
service sched j t = k ->
k < service sched j t' ->
exists st : nat,
t <= st < t' /\
service sched j st = k /\ scheduled_at sched j st
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState
forall (j : Job) (t t' : instant) (k : nat),
service sched j t = k ->
k < service sched j t' ->
exists st : nat,
t <= st < t' /\
service sched j st = k /\ scheduled_at sched j st
move => j t t' σ SERVEQ GT.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t'
exists st : nat,
t <= st < t' /\
service sched j st = σ /\ scheduled_at sched j st
have LT : t <= t'.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t'
t <= t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t'
t <= t'
move_neq_up LT. Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t' < t
False
rewrite -(service_cat _ _ t') in SERVEQ; last by lia .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat GT : σ < service sched j t' LT : t' < t SERVEQ : service sched j t' +
service_during sched j t' t = σ
False
move_neq_down GT. Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat LT : t' < t SERVEQ : service sched j t' +
service_during sched j t' t = σ
service sched j t' <= σ
by rewrite -SERVEQ leq_addr. } Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t'
exists st : nat,
t <= st < t' /\
service sched j st = σ /\ scheduled_at sched j st
have POS : service_during sched j t t' > 0 .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t'
0 < service_during sched j t t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t'
0 < service_during sched j t t'
rewrite -(service_cat _ _ t) in GT; last by done .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ LT : t <= t' GT : σ <
service sched j t + service_during sched j t t'
0 < service_during sched j t t'
by rewrite SERVEQ -addn1 leq_add2l in GT. } Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t' POS : 0 < service_during sched j t t'
exists st : nat,
t <= st < t' /\
service sched j st = σ /\ scheduled_at sched j st
apply service_during_service_at_earliest in POS.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t' POS : exists t0 : nat,
t <= t0 < t' /\
0 < service_at sched j t0 /\
service_during sched j t t0 = 0
exists st : nat,
t <= st < t' /\
service sched j st = σ /\ scheduled_at sched j st
move : POS => [st [/andP [NEQ1 NEQ2 ] [SERV SDZ]]].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t' st : nat NEQ1 : t <= st NEQ2 : st < t' SERV : 0 < service_at sched j stSDZ : service_during sched j t st = 0
exists st : nat,
t <= st < t' /\
service sched j st = σ /\ scheduled_at sched j st
exists st ; split ; [by lia | split ].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t' st : nat NEQ1 : t <= st NEQ2 : st < t' SERV : 0 < service_at sched j stSDZ : service_during sched j t st = 0
service sched j st = σ
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t' st : nat NEQ1 : t <= st NEQ2 : st < t' SERV : 0 < service_at sched j stSDZ : service_during sched j t st = 0
service sched j st = σ
erewrite <-service_cat; last by apply : NEQ1.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t' st : nat NEQ1 : t <= st NEQ2 : st < t' SERV : 0 < service_at sched j stSDZ : service_during sched j t st = 0
service sched j t + service_during sched j t st = σ
by rewrite SERVEQ SDZ addn0. } Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t' st : nat NEQ1 : t <= st NEQ2 : st < t' SERV : 0 < service_at sched j stSDZ : service_during sched j t st = 0
scheduled_at sched j st
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_unit_service : unit_service_proc_model PState j : Job t, t' : instant σ : nat SERVEQ : service sched j t = σ GT : σ < service sched j t' LT : t <= t' st : nat NEQ1 : t <= st NEQ2 : st < t' SERV : 0 < service_at sched j stSDZ : service_during sched j t st = 0
scheduled_at sched j st
by apply service_at_implies_scheduled_at. }
Qed .
End IncrementalService .
Section ServiceInTwoSchedules .
(** Consider any job type and any processor model. *)
Context {Job : JobType}.
Context {PState : ProcessorState Job}.
(** Consider any two given schedules... *)
Variable sched1 sched2 : schedule PState.
(** Given an interval in which the schedules provide the same service
to a job at each instant, we can prove that the cumulative service
received during the interval has to be the same. *)
Section ServiceDuringEquivalentInterval .
(** Consider two time instants... *)
Variable t1 t2 : instant.
(** ...and a given job that is to be scheduled. *)
Variable j : Job.
(** Assume that, in any instant between [t1] and [t2] the service
provided to [j] from the two schedules is the same. *)
Hypothesis H_sched1_sched2_same_service_at :
forall t , t1 <= t < t2 ->
service_at sched1 j t = service_at sched2 j t.
(** It follows that the service provided during [t1] and [t2]
is also the same. *)
Lemma same_service_during :
service_during sched1 j t1 t2 = service_during sched2 j t1 t2.Job : JobType PState : ProcessorState Job sched1, sched2 : schedule PState t1, t2 : instant j : Job H_sched1_sched2_same_service_at : forall t : nat,
t1 <= t < t2 ->
service_at sched1 j
t =
service_at sched2 j
t
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
Proof .Job : JobType PState : ProcessorState Job sched1, sched2 : schedule PState t1, t2 : instant j : Job H_sched1_sched2_same_service_at : forall t : nat,
t1 <= t < t2 ->
service_at sched1 j
t =
service_at sched2 j
t
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
exact /eq_big_nat/H_sched1_sched2_same_service_at. Qed .
End ServiceDuringEquivalentInterval .
(** We can leverage the previous lemma to conclude that two schedules
that match in a given interval will also have the same cumulative
service across the interval. *)
Corollary equal_prefix_implies_same_service_during :
forall t1 t2 ,
(forall t , t1 <= t < t2 -> sched1 t = sched2 t) ->
forall j , service_during sched1 j t1 t2 = service_during sched2 j t1 t2.Job : JobType PState : ProcessorState Job sched1, sched2 : schedule PState
forall t1 t2 : nat,
(forall t : nat, t1 <= t < t2 -> sched1 t = sched2 t) ->
forall j : Job,
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
Proof .Job : JobType PState : ProcessorState Job sched1, sched2 : schedule PState
forall t1 t2 : nat,
(forall t : nat, t1 <= t < t2 -> sched1 t = sched2 t) ->
forall j : Job,
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
move => t1 t2 sch j; apply : same_service_during => t' t'itv.Job : JobType PState : ProcessorState Job sched1, sched2 : schedule PState t1, t2 : nat sch : forall t : nat,
t1 <= t < t2 -> sched1 t = sched2 tj : Job t' : nat t'itv : t1 <= t' < t2
service_at sched1 j t' = service_at sched2 j t'
by rewrite /service_at sch.
Qed .
(** For convenience, we restate the corollary also at the level of
[service] for identical prefixes. *)
Corollary identical_prefix_service :
forall h ,
identical_prefix sched1 sched2 h ->
forall j , service sched1 j h = service sched2 j h.Job : JobType PState : ProcessorState Job sched1, sched2 : schedule PState
forall h : instant,
identical_prefix sched1 sched2 h ->
forall j : Job,
service sched1 j h = service sched2 j h
Proof .Job : JobType PState : ProcessorState Job sched1, sched2 : schedule PState
forall h : instant,
identical_prefix sched1 sched2 h ->
forall j : Job,
service sched1 j h = service sched2 j h
move => ? ? ?; exact : equal_prefix_implies_same_service_during. Qed .
End ServiceInTwoSchedules .
(** We add some facts into the "Hint Database" basic_rt_facts, so
Coq will be able to apply them automatically where needed. *)
Global Hint Resolve
served_at_and_receives_service_consistent
: basic_rt_facts.