Require Export prosa.behavior.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]

(** In the following, we define a model of processors with variable execution
    speeds.

    NB: For now, the definition serves only to document how this can be done;
        it is not actually used anywhere in the library.  *)

Section State.

  (** Consider any type of jobs. *)
  Variable Job: JobType.

  (** We define the state of a variable-speed processor at a given
      time to be one of two possible cases: either a specific job is
      scheduled and progresses with a specific speed, or the processor
      is idle.  Here, [Idle k] denotes a scenario where the processor
      could have generated [k] units of service, but there is no job
      being scheduled at that time instant. *)
  Inductive processor_state :=
  | Idle (speed : nat)
  | Progress (j : Job) (speed : nat).

  (** Next, we define the semantics of the variable-speed processor state. *)
  Section Service.

    (** Consider any job [j]. *)
    Variable j : Job.

    (** Job [j] is scheduled in a given state [s] if [s] is not idle
        and [j] matches the job recorded in [s]. *)
    Definition varspeed_scheduled_on (s : processor_state) (_ : unit) : bool :=
      match s with
      | Idle _ => false
      | Progress j' _  => j' == j
      end.

    (** The processor state [Idle k] indicates that the processor is
        ready to produce [k] units of supply; however, no job is
        scheduled. If the processor is in state [Progress j k], it
        produces [k] unit of work at a given time instant. *)
    Definition varspeed_supply_on (s : processor_state) (_ : unit) : work :=
      match s with
      | Idle k => k
      | Progress j' k => k
      end.

    (** If it is scheduled in state [s], job [j] receives service
        proportional to the speed recorded in the state. *)
    Definition varspeed_service_on (s : processor_state) (_ : unit) : work :=
      match s with
      | Idle _ => 0
      | Progress j' speed => if j' == j then speed else 0
      end.

  End Service.

  (** Finally, we connect the above definitions to the generic Prosa
      interface for processor states. *)
  Program Definition pstate_instance : ProcessorState Job :=
    {|
      State        := processor_state;
      scheduled_on := varspeed_scheduled_on;
      supply_on    := varspeed_supply_on;
      service_on   := varspeed_service_on
    |}.
  Next Obligation.
Job: JobType
forall (j : Job) (s : processor_state)
  (r : Datatypes_unit__canonical__fintype_Finite),
varspeed_service_on j s r <= varspeed_supply_on s r by move=> j [] //= s ; case: eqP. Qed.
  Next Obligation.
Job: JobType
forall (j : Job) (s : processor_state)
  (r : Datatypes_unit__canonical__fintype_Finite),
~~ varspeed_scheduled_on j s r ->
varspeed_service_on j s r = 0 by move=> j [] //= j' v _; case: ifP. Qed.

End State.