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 "_ + _" 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]
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 "[ 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 "[ 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]

Require Import prosa.util.nat.


(** * Job Model Parameter for Jobs Exhibiting Release Jitter *)

(** If a job exhibits release jitter, it is not immediately available for
    execution upon arrival, and can be scheduled only after its release, which
    occurs some (bounded) time after its arrival. We model this with the
    [job_jitter] parameter, which maps each job to its jitter duration. *)

Class JobJitter (Job : JobType) := job_jitter : Job -> duration.

(** * Readiness of Jobs with Release Jitter *)

(** Based on the job model's jitter parameter, we define the readiness
   predicate for jogs with release jitter (and no self-suspensions). *)

Section ReadinessOfJitteryJobs.
  (** 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 exhibit release jitter. *)
  Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.

  (** We say that a job is released at a time [t] after its arrival if the
      job's release jitter has passed. *)
  Definition is_released (j : Job) (t : instant) := job_arrival j + job_jitter j <= t.

  (** Based on the predicate [is_released], it is easy to state the notion of
      readiness for jobs subject to release jitter: a job is ready only if it
      is released and not yet complete. *)
  #[local,program] Instance jitter_ready_instance : JobReady Job PState :=
  {
    job_ready sched j t := is_released j t && ~~ completed_by sched j t
  }.
  
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobJitter Job
sched: schedule PState
j: Job
t: instant
H2: is_released j t && ~~ completed_by sched j t
pending sched j t

    
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobJitter Job
sched: schedule PState
j: Job
t: instant
REL: is_released j t
UNFINISHED: ~~ completed_by sched j t
pending sched j t

    
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobJitter Job
sched: schedule PState
j: Job
t: instant
REL: is_released 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: JobJitter Job
sched: schedule PState
j: Job
t: instant
REL: is_released 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: JobJitter Job
sched: schedule PState
j: Job
t: instant
REL: is_released j t
UNFINISHED: ~~ completed_by sched j t
has_arrived j t

    
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobJitter Job
sched: schedule PState
j: Job
t: instant
UNFINISHED: ~~ completed_by sched j t
is_released j t -> has_arrived j t
 
Job: JobType
PState: ProcessorState Job
H: JobArrival Job
H0: JobCost Job
H1: JobJitter Job
sched: schedule PState
j: Job
t: instant
UNFINISHED: ~~ completed_by sched j t
job_arrival j + job_jitter j <= t ->
job_arrival j <= t

    by apply: leq_trans; rewrite leq_addr.
  Qed.

End ReadinessOfJitteryJobs.