Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]


(** * Definition of Work Conservation *)

(** In this module, we introduce a restrictive definition of work-conserving
    schedules. The definition is restrictive because it does not yet cover
    multiprocessor scheduling (there are plans to address this in future
    work). The definition does however cover effects such as jitter or
    self-suspensions that affect whether a job can be scheduled at a given
    point in time because it is based on the general notion of a job being
    [backlogged] (i.e., ready and not executing), which is parametric in any
    given job readiness model. *)

Section WorkConserving.
  (** Consider any type of jobs... *)
  Context {Job: JobType}.

  (** ... with arrival times and costs ... *)
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** ... and any kind of processor model. *)
  Context {PState: ProcessorState Job}.

  (** Further, allow for any notion of job readiness. *)
  Context {jr : JobReady Job PState}.

  (** Given an arrival sequence and a schedule ... *)
  Variable arr_seq : arrival_sequence Job.
  Variable sched: schedule PState.

  (** ... we say that a scheduler is _work-conserving_ iff whenever a job [j]
     is backlogged, the processor is always busy executing another job
     [j_other]. Note that this definition is intentionally silent on matters of
     priority. *)
  Definition work_conserving :=
    forall j t,
      arrives_in arr_seq j ->
      backlogged sched j t ->
      exists j_other, scheduled_at sched j_other t.

  (** Related to this, we define the set of all jobs that are backlogged at a
      given time [t], i.e., the set of jobs that could be scheduled, and which
      a work-conserving scheduler must hence consider. *)
  Definition jobs_backlogged_at (t : instant): seq Job :=
    [seq j <- arrivals_up_to arr_seq t | backlogged sched j t].

End WorkConserving.