Library prosa.model.readiness.jitter
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.behavior.all.
Require Import prosa.util.nat.
Job Model Parameter for Jobs Exhibiting Release Jitter
Readiness of Jobs with Release Jitter
Consider any kind of jobs...
... and any kind of processor state.
Suppose jobs have an arrival time, a cost, and exhibit release jitter.
We say that a job is released at a time [t] after its arrival if the
job's release jitter has passed.
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.
Global Program Instance jitter_ready_instance : JobReady Job PState :=
{
job_ready sched j t := is_released j t && ~~ completed_by sched j t
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobJitter Job
sched : schedule PState
j : Job
t : instant
H3 : is_released j t && ~~ completed_by sched j t
============================
pending sched j t
----------------------------------------------------------------------------- *)
move: H3 ⇒ /andP [REL UNFINISHED].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 111)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobJitter Job
sched : schedule PState
j : Job
t : instant
REL : is_released j t
UNFINISHED : ~~ completed_by sched j t
============================
pending sched j t
----------------------------------------------------------------------------- *)
rewrite /pending.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 118)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 142)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 144)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobJitter Job
sched : schedule PState
j : Job
t : instant
REL : is_released j t
UNFINISHED : ~~ completed_by sched j t
============================
has_arrived j t
----------------------------------------------------------------------------- *)
move: REL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 168)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobJitter Job
sched : schedule PState
j : Job
t : instant
UNFINISHED : ~~ completed_by sched j t
============================
is_released j t -> has_arrived j t
----------------------------------------------------------------------------- *)
rewrite /is_released /has_arrived.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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_addk.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End ReadinessOfJitteryJobs.
{
job_ready sched j t := is_released j t && ~~ completed_by sched j t
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobJitter Job
sched : schedule PState
j : Job
t : instant
H3 : is_released j t && ~~ completed_by sched j t
============================
pending sched j t
----------------------------------------------------------------------------- *)
move: H3 ⇒ /andP [REL UNFINISHED].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 111)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobJitter Job
sched : schedule PState
j : Job
t : instant
REL : is_released j t
UNFINISHED : ~~ completed_by sched j t
============================
pending sched j t
----------------------------------------------------------------------------- *)
rewrite /pending.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 118)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 142)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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
----------------------------------------------------------------------------- *)
split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 144)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobJitter Job
sched : schedule PState
j : Job
t : instant
REL : is_released j t
UNFINISHED : ~~ completed_by sched j t
============================
has_arrived j t
----------------------------------------------------------------------------- *)
move: REL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 168)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobJitter Job
sched : schedule PState
j : Job
t : instant
UNFINISHED : ~~ completed_by sched j t
============================
is_released j t -> has_arrived j t
----------------------------------------------------------------------------- *)
rewrite /is_released /has_arrived.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
H2 : 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_addk.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End ReadinessOfJitteryJobs.