Library prosa.analysis.facts.behavior.supply

Require Export prosa.util.all.
Require Export prosa.model.processor.platform_properties.

Supply

In this file, we establish properties of the notion of supply.

We start with a few basic facts about supply.

Section BasicFacts.

Consider any type of jobs, ...

Context {Job : JobType}.

... any kind of processor state model, ...

Context `{PState : ProcessorState Job}.

... and any schedule.

Variable sched : schedule PState.

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.

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.

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.

End BasicFacts.

As a common special case, we establish facts about schedules in which supply is either 0 or 1 at all times.

Section UnitService.

Consider any type of jobs, ...

Context {Job : JobType}.

... any kind of unit-supply processor state model, ...

Context `{PState : ProcessorState Job}.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.

... and any schedule.

Variable sched : schedule PState.

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.

We note that supply is bounded at all times by 1 ...

  Remark supply_at_le_1 :
    ∀ t,
      supply_at sched t ≤ 1.

... 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.

We show that supply during an interval [t, t + δ) is bounded by δ.

  Lemma supply_during_bound :
    ∀ t δ,
      supply_during sched t (t + δ) ≤ δ.

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.

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 + δ).

End UnitService.

Lastly, we prove one lemma about supply in the case of the fully supply-consuming processor model.

Section ConsumedSupply.

Consider any type of jobs, ...

Context {Job : JobType}.

... any kind of fully supply-consuming processor state model, ...

Context `{PState : ProcessorState Job}.
Hypothesis H_supply_is_fully_consumed : fully_consuming_proc_model PState.

... and any schedule.

Variable sched : schedule PState.

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.

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.