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 processor state that includes the possibility
    of spinning, where spinning jobs do not progress (= don't get any service).

    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 processor at a given time to be one of three
      possible cases: either a specific job is scheduled and makes progress
      [Progress j], a specific job is scheduled but makes not useful progress
      [Spin j], or the processor is idle [Idle]. *)
  Inductive processor_state :=
    Idle
  | Spin (j : Job)
  | Progress (j : Job).

  (** Next, we define the semantics of the processor state with spinning. *)
  Section Service.

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

    (** It is scheduled in a given state [s] iff the state is not idle and [j]
        is the job mentioned in the state. *)
    Definition spin_scheduled_on (s : processor_state) (_ : unit) : bool :=
      match s with
      | Idle        => false
      | Spin j'     => j' == j
      | Progress j' => j' == j
      end.

    (** If the processor is idle, we assume that the supply equals 1,
        indicating that the processor is ready to perform work. If the
        processor is in the state [Spin j], then the job does not make
        any progress, so effectively the supply is equal to
        0. Finally, the processor being in the state [Progress j]
        indicates that the processor carries out 1 unit of useful work. *)
    Definition spin_supply_on (s : processor_state) (_ : unit) : work :=
      match s with
      | Idle       => 1
      | Spin j     => 0
      | Progress j => 1
      end.

    (** A job [j] receives service only if the given state [s] is
        [Progress j]. *)
    Definition spin_service_on (s : processor_state) (_ : unit) : work :=
      match s with
      | Idle        => 0
      | Spin j'     => 0
      | Progress j' => j' == j
      end.

  End Service.
  
  (** Finally, we connect the above definitions with the generic Prosa
      interface for abstract processor states. *)
  Program Definition pstate_instance : ProcessorState Job :=
    {|
      State        := processor_state;
      scheduled_on := spin_scheduled_on;
      supply_on    := spin_supply_on;
      service_on   := spin_service_on
    |}.
  Next Obligation.
Job: JobType
forall (j : Job) (s : processor_state)
  (r : Datatypes_unit__canonical__fintype_Finite),
spin_service_on j s r <= spin_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),
~~ spin_scheduled_on j s r ->
spin_service_on j s r = 0 by move => j [] // s [] /=; case: eqP. Qed.

End State.