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.
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 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.
Finally, 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.
End UnitService.
∀ 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.
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.