ideal_uni_exceed.v

Require Import prosa.model.processor.ideal_uni_exceed.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_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.

(** In the following section, we prove some general properties about the
    ideal uniprocessor with exceedance processor state. *)
Section ExceedanceProcStateProperties.

  (** In this section, we consider any type of jobs. *)
  Context `{Job : JobType}.

  (** First we prove that the processor state provides unit supply. *)
  Lemma eps_is_unit_supply : unit_supply_proc_model (exceedance_proc_state Job).Job: JobType
unit_supply_proc_model (exceedance_proc_state Job)
  Proof.Job: JobType
unit_supply_proc_model (exceedance_proc_state Job)
    rewrite /unit_supply_proc_model.Job: JobType
forall s : exceedance_proc_state Job, supply_in s <= 1
    move => s.Job: JobType
s: exceedance_proc_state Job
supply_in s <= 1
    destruct s => //=.Job: JobType
j: Job
supply_in (NominalExecution j) <= 1
Job: JobType
j: Job
supply_in (ExceedanceExecution j) <= 1
Job: JobType
supply_in Idle <= 1
    all : by rewrite /supply_in //=;rewrite sum_unit1.
  Qed.

  (** The usually opaque predicates are made transparent for this section
      to enable us to prove some processor properties. *)
  Local Transparent scheduled_in scheduled_on service_on.

  (** A job [j] is said to be [scheduled_at] some time [t] if and only if the
      processor state at that time is [NominalExecution j] or
      [ExceedanceExecution j]. *)
   Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t:
    scheduled_at sched j t <->
      sched t = NominalExecution j \/ sched t = ExceedanceExecution j.Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
scheduled_at sched j t <->
sched t = NominalExecution j \/
sched t = ExceedanceExecution j
  Proof.Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
scheduled_at sched j t <->
sched t = NominalExecution j \/
sched t = ExceedanceExecution j
    split.Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
scheduled_at sched j t ->
sched t = NominalExecution j \/
sched t = ExceedanceExecution j
Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
sched t = NominalExecution j \/
sched t = ExceedanceExecution j ->
scheduled_at sched j t
    -Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
scheduled_at sched j t ->
sched t = NominalExecution j \/
sched t = ExceedanceExecution j move => /existsP [c SCHEDON].Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
c: Core
SCHEDON: scheduled_on j (sched t) c
sched t = NominalExecution j \/
sched t = ExceedanceExecution j
      destruct (sched t); try done.Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
c: Core
j0: Job
SCHEDON: scheduled_on j (NominalExecution j0) c
NominalExecution j0 = NominalExecution j \/
NominalExecution j0 = ExceedanceExecution j
Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
c: Core
j0: Job
SCHEDON: scheduled_on j (ExceedanceExecution j0) c
ExceedanceExecution j0 = NominalExecution j \/
ExceedanceExecution j0 = ExceedanceExecution j
      +Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
c: Core
j0: Job
SCHEDON: scheduled_on j (NominalExecution j0) c
NominalExecution j0 = NominalExecution j \/
NominalExecution j0 = ExceedanceExecution j by left; move : SCHEDON => /eqP <-.
      +Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
c: Core
j0: Job
SCHEDON: scheduled_on j (ExceedanceExecution j0) c
ExceedanceExecution j0 = NominalExecution j \/
ExceedanceExecution j0 = ExceedanceExecution j by right; move : SCHEDON => /eqP <-.
    -Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
sched t = NominalExecution j \/
sched t = ExceedanceExecution j ->
scheduled_at sched j t rewrite /scheduled_at.Job: JobType
sched: schedule (exceedance_proc_state Job)
j: Job
t: instant
sched t = NominalExecution j \/
sched t = ExceedanceExecution j ->
scheduled_in j (sched t)
      by move => [-> | -> ]; rewrite /scheduled_in /scheduled_on //=; apply /existsP.
  Qed.


  (** Next we prove that the processor model under consideration is a uniprocessor
      model i.e., only one job can be scheduled at any time instant. *)
  Lemma eps_is_uniproc : uniprocessor_model (exceedance_proc_state Job).Job: JobType
uniprocessor_model (exceedance_proc_state Job)
  Proof.Job: JobType
uniprocessor_model (exceedance_proc_state Job)
    move => j1 j2 sched t /existsP [? SCHED1] /existsP [? SCHED2].Job: JobType
j1, j2: Job
sched: schedule (exceedance_proc_state Job)
t: instant
_x_: Core
SCHED1: scheduled_on j1 (sched t) _x_
_x1_: Core
SCHED2: scheduled_on j2 (sched t) _x1_
j1 = j2
    destruct (sched t) eqn: EQ; try done.Job: JobType
j1, j2: Job
sched: schedule (exceedance_proc_state Job)
t: instant
_x_: Core
j: Job
EQ: sched t = NominalExecution j
SCHED1: scheduled_on j1 (NominalExecution j) _x_
_x1_: Core
SCHED2: scheduled_on j2 (NominalExecution j) _x1_
j1 = j2
Job: JobType
j1, j2: Job
sched: schedule (exceedance_proc_state Job)
t: instant
_x_: Core
j: Job
EQ: sched t = ExceedanceExecution j
SCHED1: scheduled_on j1 (ExceedanceExecution j) _x_
_x1_: Core
SCHED2: scheduled_on j2 (ExceedanceExecution j) _x1_
j1 = j2
    -Job: JobType
j1, j2: Job
sched: schedule (exceedance_proc_state Job)
t: instant
_x_: Core
j: Job
EQ: sched t = NominalExecution j
SCHED1: scheduled_on j1 (NominalExecution j) _x_
_x1_: Core
SCHED2: scheduled_on j2 (NominalExecution j) _x1_
j1 = j2 by move : SCHED1 => /eqP <-; move : SCHED2 => /eqP <-.
    -Job: JobType
j1, j2: Job
sched: schedule (exceedance_proc_state Job)
t: instant
_x_: Core
j: Job
EQ: sched t = ExceedanceExecution j
SCHED1: scheduled_on j1 (ExceedanceExecution j) _x_
_x1_: Core
SCHED2: scheduled_on j2 (ExceedanceExecution j) _x1_
j1 = j2 by move : SCHED1 => /eqP <-; move : SCHED2 => /eqP <-.
  Qed.

  (** Next, we prove that the processor model under consideration is fully
      consuming i.e., all the supply offered is consumed by the scheduled job. *)
  Lemma eps_is_fully_consuming :
    fully_consuming_proc_model (exceedance_proc_state Job).Job: JobType
fully_consuming_proc_model (exceedance_proc_state Job)
  Proof.Job: JobType
fully_consuming_proc_model (exceedance_proc_state Job)
    rewrite /fully_consuming_proc_model.Job: JobType
forall (j : Job)
  (s : schedule (exceedance_proc_state Job))
  (t : instant),
scheduled_at s j t -> service_at s j t = supply_at s t
    move => j sched t SCHED1.Job: JobType
j: Job
sched: schedule (exceedance_proc_state Job)
t: instant
SCHED1: scheduled_at sched j t
service_at sched j t = supply_at sched t
    rewrite /scheduled_at /scheduled_in in SCHED1.Job: JobType
j: Job
sched: schedule (exceedance_proc_state Job)
t: instant
SCHED1: [exists c, scheduled_on j (sched t) c]
service_at sched j t = supply_at sched t
    apply scheduled_at_procstate in SCHED1.Job: JobType
j: Job
sched: schedule (exceedance_proc_state Job)
t: instant
SCHED1: sched t = NominalExecution j \/
sched t = ExceedanceExecution j
service_at sched j t = supply_at sched t
    move : SCHED1 => [SCHED1 | SCHED1].Job: JobType
j: Job
sched: schedule (exceedance_proc_state Job)
t: instant
SCHED1: sched t = NominalExecution j
service_at sched j t = supply_at sched t
Job: JobType
j: Job
sched: schedule (exceedance_proc_state Job)
t: instant
SCHED1: sched t = ExceedanceExecution j
service_at sched j t = supply_at sched t
    -Job: JobType
j: Job
sched: schedule (exceedance_proc_state Job)
t: instant
SCHED1: sched t = NominalExecution j
service_at sched j t = supply_at sched t by rewrite /service_at /service_in /exceedance_service_on /supply_at /supply_in
      !/exceedance_service_on //= SCHED1 sum_unit1 // sum_unit1 //
      /exceedance_service_on /exceedance_supply_on eq_refl.
    -Job: JobType
j: Job
sched: schedule (exceedance_proc_state Job)
t: instant
SCHED1: sched t = ExceedanceExecution j
service_at sched j t = supply_at sched t by rewrite /service_at /service_in /exceedance_service_on /supply_at /supply_in
        !/exceedance_service_on //= SCHED1 sum_unit1 // sum_unit1 //
        /exceedance_service_on /exceedance_supply_on eq_refl.
  Qed.

  (** Finally we prove that the processor model under consideration is unit
      service i.e., it provides at most one unit of service at any time instant. *)
  Lemma eps_is_unit_service : unit_service_proc_model (exceedance_proc_state Job).Job: JobType
unit_service_proc_model (exceedance_proc_state Job)
  Proof.Job: JobType
unit_service_proc_model (exceedance_proc_state Job)
    move => j pstate.Job: JobType
j: Job
pstate: exceedance_proc_state Job
service_in j pstate <= 1
    rewrite /service_in /service_on //= sum_unit1 /exceedance_service_on.Job: JobType
j: Job
pstate: exceedance_proc_state Job
match pstate with
| NominalExecution j' => j' == j
| _ => 0
end <= 1
    destruct pstate =>//=.Job: JobType
j, j0: Job
(j0 == j) <= 1
    by apply leq_b1.
  Qed.

End ExceedanceProcStateProperties.

(** Next, we prove some general properties specific to the
    ideal uniprocessor with exceedance processor state. *)
Section ExceedanceProcStateProperties1.

  (** In this section we consider any type of jobs. *)
  Context `{Job : JobType}.

  (** First let us define the notion of exceedance execution. A processor state
      is said to be an exceedance execution state if is equal to
      [ExceedanceExecution j] for some [j]. *)
  Definition is_exceedance_exec (pstate : (exceedance_proc_state Job)) :=
    match pstate with
    | ExceedanceExecution _ => true
    | _ => false
    end.

  (** Next, let us consider any schedule of the [exceedance_proc_state]. *)
  Variable sched : schedule (exceedance_proc_state Job).

  (** We prove that the schedule being in blackout at any time [t] is equivalent
      to the processor state at [t] being an exceedance execution state. *)
  Lemma blackout_implies_exceedance_execution t :
    is_blackout sched t = is_exceedance_exec (sched t).Job: JobType
sched: schedule (exceedance_proc_state Job)
t: instant
is_blackout sched t = is_exceedance_exec (sched t)
  Proof.Job: JobType
sched: schedule (exceedance_proc_state Job)
t: instant
is_blackout sched t = is_exceedance_exec (sched t)
    rewrite /is_blackout /has_supply /supply_at /supply_in
    /is_exceedance_exec //= sum_unit1 /exceedance_supply_on.Job: JobType
sched: schedule (exceedance_proc_state Job)
t: instant
~~
(0 <
 match sched t with
 | ExceedanceExecution _ => 0
 | _ => 1
 end) =
match sched t with
| ExceedanceExecution _ => true
| _ => false
end
    destruct (sched t) eqn : PSTATE; try done.
  Qed.

End ExceedanceProcStateProperties1.

Global Hint Resolve
  eps_is_uniproc
  eps_is_unit_supply
  eps_is_fully_consuming
  : basic_rt_facts.