Library prosa.analysis.facts.readiness.basic
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Import prosa.analysis.facts.behavior.completion.
Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model.
Consider any kind of jobs...
... and any kind of processor state.
Suppose jobs have an arrival time and a cost.
In the basic Liu & Layland model, 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.
Lemma 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 346)
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 349)
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 357)
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 388)
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 414)
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 415) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- by apply ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 415)
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 437)
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 346)
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 349)
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 357)
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 388)
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 414)
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 415) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- by apply ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 415)
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 437)
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.