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]
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 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
sched: schedule PState
j: Job
t: instant
H2: suspension_has_passed sched j t && ~~ 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

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.