Library prosa.analysis.facts.behavior.supply
Supply
In this file, we establish properties of the notion of supply.
Consider any type of jobs, ...
... any kind of processor state model, ...
... and any schedule.
First, we leverage the property service_on_le_supply_on to
show that service_at j t is always bounded by supply_at
t.
Lemma service_at_le_supply_at :
∀ j t,
service_at sched j t ≤ supply_at sched t.
Proof.
by move⇒ j t; apply: leq_sum ⇒ c _; apply service_on_le_supply_on.
Qed.
∀ j t,
service_at sched j t ≤ supply_at sched t.
Proof.
by move⇒ j t; apply: leq_sum ⇒ c _; apply service_on_le_supply_on.
Qed.
As a corollary, it is easy to show that if a job receives
service at a time instant t, then the supply at this time
instant is positive.
Corollary pos_service_impl_pos_supply :
∀ j t,
0 < service_at sched j t →
0 < supply_at sched t.
Proof.
by move⇒ j t; rewrite (leqRW (service_at_le_supply_at _ _)).
Qed.
∀ j t,
0 < service_at sched j t →
0 < supply_at sched t.
Proof.
by move⇒ j t; rewrite (leqRW (service_at_le_supply_at _ _)).
Qed.
Next, we show that, at any time instant t, either there is
some supply available or it is a blackout time.
Lemma blackout_or_supply :
∀ t,
is_blackout sched t ∨ has_supply sched t.
Proof.
by rewrite /is_blackout; move⇒ t; case: (has_supply).
Qed.
End BasicFacts.
∀ t,
is_blackout sched t ∨ has_supply sched t.
Proof.
by rewrite /is_blackout; move⇒ t; case: (has_supply).
Qed.
End BasicFacts.
As a common special case, we establish facts about schedules in
which supply is either 0 or 1 at all times.
Consider any type of jobs, ...
... any kind of unit-supply processor state model, ...
Context `{PState : ProcessorState Job}.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
... and any schedule.
We show that, under the unit-supply assumption, supply_at t is
equal to 1 - is_blackout t for any time instant t.
Lemma supply_at_complement :
∀ t,
supply_at sched t = 1 - is_blackout sched t.
Proof.
move⇒ t; have := H_unit_supply_proc_model (sched t).
by rewrite /is_blackout /has_supply /supply_at; case: supply_in ⇒ [|[]].
Qed.
∀ t,
supply_at sched t = 1 - is_blackout sched t.
Proof.
move⇒ t; have := H_unit_supply_proc_model (sched t).
by rewrite /is_blackout /has_supply /supply_at; case: supply_in ⇒ [|[]].
Qed.
Lemma is_blackout_complement :
∀ t,
nat_of_bool (is_blackout sched t) = 1 - supply_at sched t.
Proof.
move⇒ t; have := H_unit_supply_proc_model (sched t).
by rewrite /is_blackout /has_supply /supply_at; case: supply_in ⇒ [|[]].
Qed.
∀ t,
nat_of_bool (is_blackout sched t) = 1 - supply_at sched t.
Proof.
move⇒ t; have := H_unit_supply_proc_model (sched t).
by rewrite /is_blackout /has_supply /supply_at; case: supply_in ⇒ [|[]].
Qed.
We note that supply is bounded at all times by 1 ...
Remark supply_at_le_1 :
∀ t,
supply_at sched t ≤ 1.
Proof. by move⇒ t; apply H_unit_supply_proc_model. Qed.
∀ t,
supply_at sched t ≤ 1.
Proof. by move⇒ t; apply H_unit_supply_proc_model. Qed.
... and as a trivial consequence, we show that the service of
any job is either 0 or 1.
Corollary unit_supply_proc_service_case :
∀ j t,
service_at sched j t = 0 ∨ service_at sched j t = 1.
Proof.
move⇒ j t.
have SER := service_at_le_supply_at sched j t.
have SUP := supply_at_le_1 t.
by lia.
Qed.
∀ j t,
service_at sched j t = 0 ∨ service_at sched j t = 1.
Proof.
move⇒ j t.
have SER := service_at_le_supply_at sched j t.
have SUP := supply_at_le_1 t.
by lia.
Qed.
We show that supply during an interval
[t, t + δ) is bounded by δ.
Lemma supply_during_bound :
∀ t δ,
supply_during sched t (t + δ) ≤ δ.
Proof.
move⇒ t d; rewrite -[leqRHS](addKn t) -[leqRHS]muln1 -sum_nat_const_nat.
by apply: leq_sum ⇒ t0 _; apply supply_at_le_1.
Qed.
∀ t δ,
supply_during sched t (t + δ) ≤ δ.
Proof.
move⇒ t d; rewrite -[leqRHS](addKn t) -[leqRHS]muln1 -sum_nat_const_nat.
by apply: leq_sum ⇒ t0 _; apply supply_at_le_1.
Qed.
We show that blackout during an interval
[t, t + δ) is bounded by δ.
Lemma blackout_during_bound :
∀ t δ,
blackout_during sched t (t + δ) ≤ δ.
Proof.
move⇒ t d; rewrite -[leqRHS](addKn t) -[leqRHS]muln1 -sum_nat_const_nat.
by apply: leq_sum ⇒ t0 _; destruct is_blackout.
Qed.
∀ t δ,
blackout_during sched t (t + δ) ≤ δ.
Proof.
move⇒ t d; rewrite -[leqRHS](addKn t) -[leqRHS]muln1 -sum_nat_const_nat.
by apply: leq_sum ⇒ t0 _; destruct is_blackout.
Qed.
We observe that the supply during an interval can be decomposed
into the last instant and the rest of the interval.
Lemma supply_during_last_plus_before :
∀ t1 t2,
t1 ≤ t2 →
supply_during sched t1 t2.+1 = supply_during sched t1 t2 + supply_at sched t2.
Proof. by move ⇒ t1 t2 LEQ; rewrite /supply_during big_nat_recr //=. Qed.
∀ t1 t2,
t1 ≤ t2 →
supply_during sched t1 t2.+1 = supply_during sched t1 t2 + supply_at sched t2.
Proof. by move ⇒ t1 t2 LEQ; rewrite /supply_during big_nat_recr //=. Qed.
We show a similar lemma for blackout_during.
Lemma blackout_during_last_plus_before :
∀ t1 t2,
t1 ≤ t2 →
blackout_during sched t1 t2.+1 = blackout_during sched t1 t2 + is_blackout sched t2.
Proof. by move ⇒ t1 t2 LEQ; rewrite /blackout_during big_nat_recr //=. Qed.
∀ t1 t2,
t1 ≤ t2 →
blackout_during sched t1 t2.+1 = blackout_during sched t1 t2 + is_blackout sched t2.
Proof. by move ⇒ t1 t2 LEQ; rewrite /blackout_during big_nat_recr //=. Qed.
We show that the service during a time interval
[t, t + δ)
is equal to the difference between δ and the blackout during
[t, t + δ).
Lemma supply_during_complement :
∀ t δ,
supply_during sched t (t + δ) = δ - blackout_during sched t (t + δ).
Proof.
move⇒ t; elim⇒ [|δ IHδ]; first by rewrite addn0 [LHS]big_geq.
rewrite addnS [LHS]big_nat_recr ?leq_addr//= [X in X + _]IHδ.
rewrite blackout_during_last_plus_before ?leq_addr// is_blackout_complement.
have B := supply_at_le_1 (t + δ).
by rewrite -addn1 subnACA ?blackout_during_bound; lia.
Qed.
∀ t δ,
supply_during sched t (t + δ) = δ - blackout_during sched t (t + δ).
Proof.
move⇒ t; elim⇒ [|δ IHδ]; first by rewrite addn0 [LHS]big_geq.
rewrite addnS [LHS]big_nat_recr ?leq_addr//= [X in X + _]IHδ.
rewrite blackout_during_last_plus_before ?leq_addr// is_blackout_complement.
have B := supply_at_le_1 (t + δ).
by rewrite -addn1 subnACA ?blackout_during_bound; lia.
Qed.
Similarly, we show that the blackout during a time interval
[t, t + δ) is equal to the difference between δ and the
supply during [t, t + δ).
Lemma blackout_during_complement :
∀ t δ,
blackout_during sched t (t + δ) = δ - supply_during sched t (t + δ).
Proof.
move⇒ t; elim⇒ [|δ IHδ]; first by rewrite addn0 [LHS]big_geq.
rewrite addnS [LHS]big_nat_recr ?leq_addr//= [X in X + _]IHδ.
rewrite supply_during_last_plus_before ?leq_addr// supply_at_complement.
by rewrite -addn1 subnACA ?supply_during_bound; lia.
Qed.
∀ t δ,
blackout_during sched t (t + δ) = δ - supply_during sched t (t + δ).
Proof.
move⇒ t; elim⇒ [|δ IHδ]; first by rewrite addn0 [LHS]big_geq.
rewrite addnS [LHS]big_nat_recr ?leq_addr//= [X in X + _]IHδ.
rewrite supply_during_last_plus_before ?leq_addr// supply_at_complement.
by rewrite -addn1 subnACA ?supply_during_bound; lia.
Qed.
The number of blackout time instants in
[t1, t2) is equal to
the sum of blackout time instants in [t1, t) and [t, t2).
Lemma blackout_during_cat :
∀ (t1 t2 t : instant),
t1 ≤ t ≤ t2 →
blackout_during sched t1 t + blackout_during sched t t2 = blackout_during sched t1 t2.
Proof.
move⇒ t1 t2 t NEQ; rewrite /blackout_during.
rewrite (index_iota_cat t t1 t2) ⇒ //.
by rewrite big_cat //=.
Qed.
∀ (t1 t2 t : instant),
t1 ≤ t ≤ t2 →
blackout_during sched t1 t + blackout_during sched t t2 = blackout_during sched t1 t2.
Proof.
move⇒ t1 t2 t NEQ; rewrite /blackout_during.
rewrite (index_iota_cat t t1 t2) ⇒ //.
by rewrite big_cat //=.
Qed.
The number of blackout time instants can increase by at most 1
when extending the interval by one unit.
Lemma blackout_during_unit_growth :
∀ (t : instant),
unit_growth_function (blackout_during sched t).
Proof.
move⇒ t1 t2.
have UNIT :
∀ (f : nat → nat) (t1 t2 : instant),
(f t2 ≤ 1) →
\sum_(t1 ≤ t < t2 + 1) f t ≤ \sum_(t1 ≤ t < t2) f t + 1.
{ clear; intros f t1 t2; have [LE|LT] := leqP t1 t2.
{ by rewrite addn1 big_nat_recr //= leq_add2l. }
{ by rewrite big_geq // addn1. }
}
by apply UNIT; destruct is_blackout.
Qed.
End UnitService.
∀ (t : instant),
unit_growth_function (blackout_during sched t).
Proof.
move⇒ t1 t2.
have UNIT :
∀ (f : nat → nat) (t1 t2 : instant),
(f t2 ≤ 1) →
\sum_(t1 ≤ t < t2 + 1) f t ≤ \sum_(t1 ≤ t < t2) f t + 1.
{ clear; intros f t1 t2; have [LE|LT] := leqP t1 t2.
{ by rewrite addn1 big_nat_recr //= leq_add2l. }
{ by rewrite big_geq // addn1. }
}
by apply UNIT; destruct is_blackout.
Qed.
End UnitService.
Lastly, we prove one lemma about supply in the case of the fully
supply-consuming processor model.
Consider any type of jobs, ...
... any kind of fully supply-consuming processor state model, ...
Context `{PState : ProcessorState Job}.
Hypothesis H_supply_is_fully_consumed : fully_consuming_proc_model PState.
Hypothesis H_supply_is_fully_consumed : fully_consuming_proc_model PState.
... and any schedule.
The fact that a job j is scheduled at a time instant t and
there is a supply at t implies that the job receives service
at time t.
Lemma progress_inside_supplies :
∀ (j : Job) (t : instant),
has_supply sched t →
scheduled_at sched j t →
0 < service_at sched j t.
Proof.
by move ⇒ j t SUP SCHED; rewrite H_supply_is_fully_consumed.
Qed.
End ConsumedSupply.
∀ (j : Job) (t : instant),
has_supply sched t →
scheduled_at sched j t →
0 < service_at sched j t.
Proof.
by move ⇒ j t SUP SCHED; rewrite H_supply_is_fully_consumed.
Qed.
End ConsumedSupply.
We add some of the above lemmas to the "Hint Database"
basic_rt_facts, so the auto tactic will be able to use
them.
Global Hint Resolve
supply_at_le_1
: basic_rt_facts.
supply_at_le_1
: basic_rt_facts.