supply.v

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]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.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 :
    forall j t,
      service_at sched j t <= supply_at sched t.Job: JobType
PState: ProcessorState Job
sched: schedule PState
forall (j : Job) (t : instant),
service_at sched j t <= supply_at sched t
  Proof.Job: JobType
PState: ProcessorState Job
sched: schedule PState
forall (j : Job) (t : instant),
service_at sched j t <= supply_at sched t
    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 :
    forall j t,
      0 < service_at sched j t ->
      0 < supply_at sched t.Job: JobType
PState: ProcessorState Job
sched: schedule PState
forall (j : Job) (t : instant),
0 < service_at sched j t -> 0 < supply_at sched t
  Proof.Job: JobType
PState: ProcessorState Job
sched: schedule PState
forall (j : Job) (t : instant),
0 < service_at sched j t -> 0 < supply_at sched t
    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 :
    forall t,
      is_blackout sched t \/ has_supply sched t.Job: JobType
PState: ProcessorState Job
sched: schedule PState
forall t : instant,
is_blackout sched t \/ has_supply sched t
  Proof.Job: JobType
PState: ProcessorState Job
sched: schedule PState
forall t : instant,
is_blackout sched t \/ has_supply sched t
    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. *)
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 :
    forall t,
      supply_at sched t = 1 - is_blackout sched t.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall t : instant,
supply_at sched t = 1 - is_blackout sched t
  Proof.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall t : instant,
supply_at sched t = 1 - is_blackout sched t
    move=> t; have := H_unit_supply_proc_model (sched t).Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
t: instant
supply_in (sched t) <= 1 ->
supply_at sched t = 1 - is_blackout 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 :
    forall t,
      supply_at sched t <= 1.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall t : instant, supply_at sched t <= 1
  Proof.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall t : instant, supply_at sched t <= 1 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 :
    forall j t,
      service_at sched j t = 0 \/ service_at sched j t = 1.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall (j : Job) (t : instant),
service_at sched j t = 0 \/ service_at sched j t = 1
  Proof.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall (j : Job) (t : instant),
service_at sched j t = 0 \/ service_at sched j t = 1
    move=> j t.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
j: Job
t: instant
service_at sched j t = 0 \/ service_at sched j t = 1
    have SER := service_at_le_supply_at sched j t.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
j: Job
t: instant
SER: service_at sched j t <= supply_at sched t
service_at sched j t = 0 \/ service_at sched j t = 1
    have SUP := supply_at_le_1 t.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
j: Job
t: instant
SER: service_at sched j t <= supply_at sched t
SUP: supply_at sched t <= 1
service_at sched j t = 0 \/ service_at sched j t = 1
    by lia.
  Qed.

  (** We show that supply during an interval <<[t, t + δ)>> is bounded by [δ]. *)
  Lemma supply_during_bound :
    forall t δ,
      supply_during sched t (t + δ) <= δ.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall (t : instant) (δ : nat),
supply_during sched t (t + δ) <= δ
  Proof.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall (t : instant) (δ : nat),
supply_during sched t (t + δ) <= δ
    move=> t d; rewrite -[leqRHS](addKn t) -[leqRHS]muln1 -sum_nat_const_nat.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
t: instant
d: nat
supply_during sched t (t + d) <=
\sum_(t <= i < t + d) 1
    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 :
    forall t1 t2,
      t1 <= t2 ->
      supply_during sched t1 t2.+1 = supply_during sched t1 t2 + supply_at sched t2.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall t1 t2 : nat,
t1 <= t2 ->
supply_during sched t1 t2.+1 =
supply_during sched t1 t2 + supply_at sched t2
  Proof.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall t1 t2 : nat,
t1 <= t2 ->
supply_during sched t1 t2.+1 =
supply_during sched t1 t2 + supply_at sched t2 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 :
    forall t δ,
      blackout_during sched t (t + δ) = δ - supply_during sched t (t + δ).Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall (t : instant) (δ : nat),
blackout_during sched t (t + δ) =
δ - supply_during sched t (t + δ)
  Proof.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
forall (t : instant) (δ : nat),
blackout_during sched t (t + δ) =
δ - supply_during sched t (t + δ)
    move=> t; elim=> [|δ IHδ]; first by rewrite addn0 [LHS]big_geq.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
t: instant
δ: nat
IHδ: blackout_during sched t (t + δ) =
δ - supply_during sched t (t + δ)
blackout_during sched t (t + δ.+1) =
δ.+1 - supply_during sched t (t + δ.+1)
    rewrite addnS [LHS]big_nat_recr ?leq_addr//= [X in X + _]IHδ.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
t: instant
δ: nat
IHδ: blackout_during sched t (t + δ) =
δ - supply_during sched t (t + δ)
δ - supply_during sched t (t + δ) +
is_blackout sched (t + δ) =
δ.+1 - supply_during sched t (t + δ).+1
    rewrite supply_during_last_plus_before ?leq_addr// supply_at_complement.Job: JobType
PState: ProcessorState Job
H_unit_supply_proc_model: unit_supply_proc_model
  PState
sched: schedule PState
t: instant
δ: nat
IHδ: blackout_during sched t (t + δ) =
δ - supply_during sched t (t + δ)
δ - supply_during sched t (t + δ) +
is_blackout sched (t + δ) =
δ.+1 -
(supply_during sched t (t + δ) +
 (1 - is_blackout sched (t + δ)))
    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. *)
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 :
    forall (j : Job) (t : instant),
      has_supply sched t ->
      scheduled_at sched j t ->
      0 < service_at sched j t.Job: JobType
PState: ProcessorState Job
H_supply_is_fully_consumed: fully_consuming_proc_model
  PState
sched: schedule PState
forall (j : Job) (t : instant),
has_supply sched t ->
scheduled_at sched j t -> 0 < service_at sched j t
  Proof.Job: JobType
PState: ProcessorState Job
H_supply_is_fully_consumed: fully_consuming_proc_model
  PState
sched: schedule PState
forall (j : Job) (t : instant),
has_supply sched t ->
scheduled_at sched j t -> 0 < service_at sched j t
    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.