Library prosa.analysis.facts.readiness.basic
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.definitions.readiness.
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 646)
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 649)
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 657)
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 688)
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 714)
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 715) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- by apply ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 715)
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 737)
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.
∀ sched,
jobs_must_arrive_to_execute sched →
completed_jobs_dont_execute sched →
jobs_must_be_ready_to_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 646)
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 649)
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 657)
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 688)
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 714)
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 715) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- by apply ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 715)
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 737)
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.
The Liu & Layland readiness model is trivially non-clairvoyant.
Fact basic_readiness_nonclairvoyance:
nonclairvoyant_readiness basic_ready_instance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 657)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
============================
nonclairvoyant_readiness basic_ready_instance
----------------------------------------------------------------------------- *)
Proof.
move⇒ sched sched' j h PREFIX t IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 665)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched, sched' : schedule PState
j : Job
h : instant
PREFIX : identical_prefix sched sched' h
t : nat
IN : t <= h
============================
job_ready sched j t = job_ready sched' j t
----------------------------------------------------------------------------- *)
rewrite /job_ready /basic_ready_instance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 689)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched, sched' : schedule PState
j : Job
h : instant
PREFIX : identical_prefix sched sched' h
t : nat
IN : t <= h
============================
pending sched j t = pending sched' j t
----------------------------------------------------------------------------- *)
now apply (identical_prefix_pending _ _ h).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End LiuAndLaylandReadiness.
nonclairvoyant_readiness basic_ready_instance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 657)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
============================
nonclairvoyant_readiness basic_ready_instance
----------------------------------------------------------------------------- *)
Proof.
move⇒ sched sched' j h PREFIX t IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 665)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched, sched' : schedule PState
j : Job
h : instant
PREFIX : identical_prefix sched sched' h
t : nat
IN : t <= h
============================
job_ready sched j t = job_ready sched' j t
----------------------------------------------------------------------------- *)
rewrite /job_ready /basic_ready_instance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 689)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
sched, sched' : schedule PState
j : Job
h : instant
PREFIX : identical_prefix sched sched' h
t : nat
IN : t <= h
============================
pending sched j t = pending sched' j t
----------------------------------------------------------------------------- *)
now apply (identical_prefix_pending _ _ h).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End LiuAndLaylandReadiness.