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]

(** * The Ideal Uniprocessor Model *)


(** In this module, we define a central piece of the Prosa model: the notion of
    an ideal uniprocessor state. The word "ideal" here refers to the complete
    absence of runtime overheads or any other complications. In an ideal
    uniprocessor schedule, there are only two possible cases: at a given time,
    either a specific job is scheduled and makes unit-progress, or the
    processor is idle. To model this, we simply reuse the standard [option]
    type from the Coq standard library. *)

Section State.

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

  (** We connect the notion of an ideal processor state with
      the generic interface for the processor-state abstraction in Prosa by
      declaring a so-called instance of the [ProcessorState] typeclass. *)
  Program Definition processor_state : ProcessorState Job :=
    {|
      (** We define the ideal "processor state" as an [option Job],
          which means that it is either [Some j] (where [j] is a
          [Job]) or [None] (which we use to indicate an idle
          instant). *)
      State := option Job;
      (** As this is a uniprocessor model, cores are implicitly defined
          as the [unit] type containing a single element as a placeholder. *)
      (** We say that a given job [j] is scheduled in a
          given state [s] iff [s] is [Some j]. *)
      scheduled_on j s (_ : unit) := s == Some j;
      (** Any state of an ideal processor provides exactly one unit of
          supply. *)
      supply_on s (_ : unit) := 1;
      (** We say that a given job [j] receives service in a given
          state [s] iff [s] is [Some j]. *)
      service_on j s (_ : unit) := if s == Some j then 1 else 0;
    |}.
  Next Obligation.
Job: JobType
forall (j : Job) (s : option Job)
  (r : Datatypes_unit__canonical__fintype_Finite),
(fun (j0 : Job) (s0 : option Job) =>
 fun=> (if s0 == Some j0 then 1 else 0)) j s r <=
(fun=> (fun=> 1)) s r
    by move=> j s ?; rewrite /nat_of_bool; case: ifP => // ? /negP[].
  Qed.
  Next Obligation.
Job: JobType
forall (j : Job) (s : option Job)
  (r : Datatypes_unit__canonical__fintype_Finite),
~~
(fun (j0 : Job) (s0 : option Job) =>
 fun=> s0 == Some j0) j s r ->
(fun (j0 : Job) (s0 : option Job) =>
 fun=> (if s0 == Some j0 then 1 else 0)) j s r = 0
    by move=> j s ?; rewrite /nat_of_bool; case: ifP => // ? /negP[].
  Qed.

End State.

(** ** Idle Instants *)

(** In this section, we define the notion of idleness for ideal uniprocessor
    schedules. *)
Section IsIdle.

  (** Consider any type of jobs... *)
  Context {Job : JobType}.
  Variable arr_seq : arrival_sequence Job.

  (** ... and any ideal uniprocessor schedule of such jobs. *)
  Variable sched : schedule ((*ideal*)processor_state Job).

  (** We say that the processor is idle at time [t] iff there is no job being scheduled. *)
  Definition ideal_is_idle (t : instant) := sched t == None.

End IsIdle.