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

(** * Readiness of a Job *)

(** We define a general notion of readiness of a job: a job can be
   scheduled only when it is ready, as determined by the predicate
   [job_ready]. This notion of readiness is a general concept that is
   used to model jitter, self-suspensions, etc.  Crucially, we require
   that any sensible notion of readiness is a refinement of the notion
   of a pending job, i.e., any ready job must also be pending. *)
Class JobReady (Job : JobType) (PState : ProcessorState Job)
      {jc : JobCost Job} {ja : JobArrival Job} :=
  {
    job_ready : schedule PState -> Job -> instant -> bool;

    (** What follows is the consistency requirement: We require any
        reasonable readiness model to consider only pending jobs to be
        ready. *)
    _ : forall sched j t, job_ready sched j t -> pending sched j t;
  }.

(** * Backlogged Jobs *)

(** Based on the general notion of readiness, we define what it means to be
   backlogged, i.e., ready to run but not executing. *)
Section Backlogged.
  (** Consider any kinds of jobs and any kind of processor state. *)
  Context {Job : JobType} {PState : ProcessorState Job}.

  (** Allow for any notion of readiness. *)
  Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.

  (** Job j is backlogged at time t iff it is ready and not scheduled. *)
  Definition backlogged (sched : schedule PState) (j : Job) (t : instant) :=
    job_ready sched j t && ~~ scheduled_at sched j t.

End Backlogged.


(** * Validity of a Schedule *)

(** With the readiness concept in place, we define the notion of valid schedules. *)
Section ValidSchedule.
  (** Consider any kind of jobs and any kind of processor state. *)
  Context {Job : JobType} {PState : ProcessorState Job}.

  (** Consider any schedule. *)
  Variable sched : schedule PState.

  Context `{JobArrival Job}.

  (** We define whether jobs come from some arrival sequence... *)
  Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
    forall j t, scheduled_at sched j t -> arrives_in arr_seq j.

  (** ..., whether a job can only be scheduled if it has arrived ... *)
  Definition jobs_must_arrive_to_execute :=
    forall j t, scheduled_at sched j t -> has_arrived j t.

  Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.

  (** ..., whether a job can only be scheduled if it is ready ... *)
  Definition jobs_must_be_ready_to_execute :=
    forall j t, scheduled_at sched j t -> job_ready sched j t.

  (** ... and whether a job cannot be scheduled after it completes. *)
  Definition completed_jobs_dont_execute :=
    forall j t, scheduled_at sched j t -> service sched j t < job_cost j.

  (** We say that the schedule is valid iff
     - jobs come from some arrival sequence
     - a job is scheduled if it is ready *)
  Definition valid_schedule (arr_seq : arrival_sequence Job) :=
    jobs_come_from_arrival_sequence arr_seq /\
    jobs_must_be_ready_to_execute.

  (** Note that we do not explicitly require that a valid schedule satisfies
     [jobs_must_arrive_to_execute] or [completed_jobs_dont_execute] because these
     properties are implied by jobs_must_be_ready_to_execute. *)

End ValidSchedule.