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]

Require Export prosa.analysis.definitions.progress.
Require Export prosa.util.nat.

(** * Job Model Parameter for Jobs Exhibiting Self-Suspensions *)

(** We define a job's self-suspension parameter as follows: after having
    received a given number of units of service [rho], a job [j] may either
    self-suspend for a given duration [d], in which case [job_suspension j rho
    = d], or it may remain ready, in which case [job_suspension j rho =
    0]. Note that a job may self-suspend before having received any service,
    which is equivalent to release jitter. (Suspensions after a job has
    completed are meaningless and irrelevant.) *)
Class JobSuspension (Job : JobType) := job_suspension : Job -> work -> duration.

(** * Readiness of Self-Suspending Jobs *)

(** In the following section, we define the notion of "readiness" for
    self-suspending jobs based on the just-defined job-model parameter. *)
Section ReadinessOfSelfSuspendingJobs.
  (** Consider any kind of jobs... *)
  Context {Job : JobType}.

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

  (** Suppose jobs have an arrival time, a cost, and that they exhibit
      self-suspensions. *)
  Context `{JobArrival Job} `{JobCost Job} `{JobSuspension Job}.

  (** We say that a job's last suspension (if any) of length [delay] "has
      passed" at a given time [t] (i.e., the job is ready again at time [t]) if
      the job arrived at least [delay] time units ago and has not progressed
      within the last [delay] time units. In other words, since a
      self-suspension can start only when a job progresses (i.e., when it
      receives some service), if a job has not been making progress in the last
      [delay] time units, then a self-suspension of length [delay] has
      necessarily ended at time [t]. *)
  Definition suspension_has_passed (sched : schedule PState) (j : Job) (t : instant) :=
    let delay := job_suspension j (service sched j t) in
    (job_arrival j + delay <= t) && no_progress_for sched j t delay.

  (** Based on [suspension_has_passed], we state the notion of readiness for
      self-suspending jobs: a job [t] is ready at time [t] in a schedule
      [sched] only if it is not self-suspended or complete at time [t]. *)
  #[local,program] Instance suspension_ready_instance : JobReady Job PState :=
  {
    job_ready sched j t := suspension_has_passed sched j t
                             && ~~ completed_by sched j t
  }.
  
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
forall (sched : schedule PState) (j : Job)
  (t : instant),
(fun (sched0 : schedule PState) (j0 : Job)
   (t0 : instant) =>
 suspension_has_passed sched0 j0 t0 &&
 ~~ completed_by sched0 j0 t0) sched j t ->
pending sched j t

    
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
sched: schedule PState
j: Job
t: instant
PASSED: suspension_has_passed sched j t
UNFINISHED: ~~ completed_by sched j t
pending sched j t

    
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
sched: schedule PState
j: Job
t: instant
PASSED: suspension_has_passed sched j t
UNFINISHED: ~~ completed_by sched j t
has_arrived j t && ~~ completed_by sched j t
 
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
sched: schedule PState
j: Job
t: instant
PASSED: suspension_has_passed sched j t
UNFINISHED: ~~ completed_by sched j t
has_arrived j t /\ ~~ completed_by sched j t
 
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
sched: schedule PState
j: Job
t: instant
PASSED: suspension_has_passed sched j t
UNFINISHED: ~~ completed_by sched j t
has_arrived j t

    
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
sched: schedule PState
j: Job
t: instant
UNFINISHED: ~~ completed_by sched j t
suspension_has_passed sched j t -> has_arrived j t
 
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobSuspension Job
sched: schedule PState
j: Job
t: instant
UNFINISHED: ~~ completed_by sched j t
ARR: job_arrival j +
job_suspension j (service sched j t) <= t
job_arrival j <= t

    by apply: leq_trans ARR; rewrite leq_addr.
  Qed.

End ReadinessOfSelfSuspendingJobs.


(** * Total Suspension Time of a Job *)

(** Next, we define the notion of a job's cumulative and total suspension times. *)

Section TotalSuspensionTime.

  (** Consider any kind of jobs... *)
  Context {Job : JobType}.

  (** ...where each job has a cost and may exhibit self-suspensions. *)
  Context `{JobCost Job} `{JobSuspension Job}.

  (** A job's total self-suspension length is simply the sum of the lengths of
     all its suspensions. *)
  Definition total_suspension (j : Job) := \sum_(0 <= ρ < job_cost j) job_suspension j ρ.

End TotalSuspensionTime.