Library rt.restructuring.model.readiness.basic
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import completion.
We define the readiness indicator function for the classic Liu & Layland
model without jitter and no self-suspensions, where jobs are always
ready.
Consider any kind of jobs...
... and any kind of processor state.
Supose jobs have an arrival time and a cost.
In the basic Liu & Layland model, a job is ready iff it is pending.
Global Program Instance basic_ready_instance : JobReady Job PState :=
{
job_ready sched j t := pending sched j t
}.
{
job_ready sched j t := pending sched j t
}.
Under this definition, a schedule satisfies that only ready jobs execute
as long as jobs must arrive to execute and completed jobs don't execute,
which we note with the following theorem.
Theorem basic_readiness_compliance:
∀ sched,
jobs_must_arrive_to_execute sched →
completed_jobs_dont_execute sched →
jobs_must_be_ready_to_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
============================
forall sched : schedule PState,
jobs_must_arrive_to_execute sched ->
completed_jobs_dont_execute sched -> jobs_must_be_ready_to_execute sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ sched ARR COMP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
============================
jobs_must_be_ready_to_execute sched
----------------------------------------------------------------------------- *)
rewrite /jobs_must_be_ready_to_execute ⇒ j t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 88)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
job_ready sched j t
----------------------------------------------------------------------------- *)
rewrite /job_ready /basic_ready_instance /pending.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 109)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
has_arrived j t && ~~ completed_by sched j t
----------------------------------------------------------------------------- *)
apply /andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 135)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
has_arrived j t
subgoal 2 (ID 136) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- by apply ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- rewrite -less_service_than_cost_is_incomplete.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 158)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
by apply COMP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End LiuAndLaylandReadiness.
∀ sched,
jobs_must_arrive_to_execute sched →
completed_jobs_dont_execute sched →
jobs_must_be_ready_to_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
============================
forall sched : schedule PState,
jobs_must_arrive_to_execute sched ->
completed_jobs_dont_execute sched -> jobs_must_be_ready_to_execute sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ sched ARR COMP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
============================
jobs_must_be_ready_to_execute sched
----------------------------------------------------------------------------- *)
rewrite /jobs_must_be_ready_to_execute ⇒ j t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 88)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
job_ready sched j t
----------------------------------------------------------------------------- *)
rewrite /job_ready /basic_ready_instance /pending.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 109)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
has_arrived j t && ~~ completed_by sched j t
----------------------------------------------------------------------------- *)
apply /andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 135)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
has_arrived j t
subgoal 2 (ID 136) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- by apply ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- rewrite -less_service_than_cost_is_incomplete.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 158)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched : schedule PState
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
by apply COMP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End LiuAndLaylandReadiness.