Library prosa.model.readiness.suspension
Require Export prosa.behavior.all.
Require Export prosa.analysis.definitions.progress.
Require Export prosa.util.nat.
Require Export prosa.analysis.definitions.progress.
Require Export prosa.util.nat.
Job Model Parameter for Jobs Exhibiting Self-Suspensions
Readiness of Self-Suspending Jobs
Consider any kind of jobs...
... and any kind of processor state.
Suppose jobs have an arrival time, a cost, and that they exhibit
self-suspensions.
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.
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
}.
End ReadinessOfSelfSuspendingJobs.
{
job_ready sched j t := suspension_has_passed sched j t
&& ~~ completed_by sched j t
}.
End ReadinessOfSelfSuspendingJobs.
Total Suspension Time of a Job
Consider any kind of jobs...
...where each job has a cost and may exhibit self-suspensions.
A job's total self-suspension length is simply the sum of the lengths of
all its suspensions.