Library prosa.model.readiness.suspension
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.behavior.all.
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].
Global Program Instance suspension_ready_instance : JobReady Job PState :=
{
job_ready sched j t := suspension_has_passed sched j t && ~~ completed_by sched j t
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 381)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobSuspension Job
sched : schedule PState
j : Job
t : instant
H3 : suspension_has_passed sched j t && ~~ completed_by sched j t
============================
pending sched j t
----------------------------------------------------------------------------- *)
move: H3 ⇒ /andP [PASSED UNFINISHED].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 438)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
rewrite /pending.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 445)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 469)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 471)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
move: PASSED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 496)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
rewrite /suspension_has_passed /has_arrived ⇒ /andP [ARR _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 542)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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 move: ARR; apply leq_addk.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End ReadinessOfSelfSuspendingJobs.
{
job_ready sched j t := suspension_has_passed sched j t && ~~ completed_by sched j t
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 381)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobSuspension Job
sched : schedule PState
j : Job
t : instant
H3 : suspension_has_passed sched j t && ~~ completed_by sched j t
============================
pending sched j t
----------------------------------------------------------------------------- *)
move: H3 ⇒ /andP [PASSED UNFINISHED].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 438)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
rewrite /pending.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 445)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 469)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 471)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
move: PASSED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 496)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
rewrite /suspension_has_passed /has_arrived ⇒ /andP [ARR _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 542)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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 move: ARR; apply leq_addk.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
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.
Definition total_suspension (j : Job) := \sum_(0 ≤ ρ < job_cost j) job_suspension j ρ.
End TotalSuspensionTime.
End TotalSuspensionTime.