Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[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]


(** * Generic Reference Scheduler *)

(** In this file, we provide a generic procedure that produces a schedule by
    making a decision on what to schedule at each point in time. *)

(** To begin with, we define the notion of a pointwise scheduling policy that
    makes a decision at a given time [t] based on given prefix up to time
    [t.-1]. *)
Section PointwisePolicy.
  (** Consider any type of jobs and type of schedule. *)
  Context {Job : JobType}.
  Variable PState : ProcessorState Job.

  (** A pointwise scheduling policy is a function that, given a schedule prefix
      that is valid up to time [t - 1], decides what to schedule at time
      [t]. *)
  Definition PointwisePolicy := schedule PState -> instant -> PState.
End PointwisePolicy.

Section GenericSchedule.
  (** Consider any type of jobs and type of schedule. *)
  Context {Job : JobType} {PState : ProcessorState Job}.

  (** Suppose we are given a policy function that, given a schedule prefix that
      is valid up to time [t - 1], decides what to schedule at time [t]. *)
  Variable policy : PointwisePolicy PState.

  (** Let [idle_state] denote the processor state that indicates that the
      entire system is idle. *)
  Variable idle_state : PState.

  (** We construct the schedule step by step starting from an "empty" schedule
      that is idle at all times as a base case. *)
  Definition empty_schedule: schedule PState := fun _ => idle_state.

  (** Next, we define a function that computes a schedule prefix up to a given
      time horizon [h]. *)
  Fixpoint schedule_up_to (h : instant)  :=
    let
      prefix := if h is h'.+1 then schedule_up_to h' else empty_schedule
    in
      replace_at prefix h (policy prefix h).

  (** Finally, we define the generic schedule as follows: for a
      given point in time [t], we compute the finite prefix up to and including
      [t], namely [schedule_up_to t], and then return the job scheduled at time
      [t] in that prefix. *)
  Definition generic_schedule (t : instant) : PState :=
    schedule_up_to t t.

End GenericSchedule.