Library prosa.analysis.facts.readiness.basic
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.definitions.readiness.
Require Export prosa.analysis.definitions.work_bearing_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.
The Liu & Layland readiness model is trivially non-clairvoyant.
Fact basic_readiness_nonclairvoyance :
nonclairvoyant_readiness basic_ready_instance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
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 36)
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 60)
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.
nonclairvoyant_readiness basic_ready_instance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
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 36)
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 60)
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.
Consider any job arrival sequence ...
... and any schedule of these jobs.
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 :
jobs_must_arrive_to_execute sched →
completed_jobs_dont_execute sched →
jobs_must_be_ready_to_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence Job
sched : schedule PState
============================
jobs_must_arrive_to_execute sched ->
completed_jobs_dont_execute sched -> jobs_must_be_ready_to_execute sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ ARR COMP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 53)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 84)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 110)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 111) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- by apply ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 111)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 133)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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.
jobs_must_arrive_to_execute sched →
completed_jobs_dont_execute sched →
jobs_must_be_ready_to_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence Job
sched : schedule PState
============================
jobs_must_arrive_to_execute sched ->
completed_jobs_dont_execute sched -> jobs_must_be_ready_to_execute sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ ARR COMP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 53)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 84)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 110)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 111) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
- by apply ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 111)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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 133)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence 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.
Consider a JLFP policy that indicates a reflexive
higher-or-equal priority relation.
We show that the basic readiness model is a work-bearing
readiness model. That is, at any time instant [t], if a job [j]
is pending, then there exists a job (namely [j] itself) with
higher-or-equal priority that is ready at time [t].
Fact basic_readiness_is_work_bearing_readiness :
work_bearing_readiness arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 54)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence Job
sched : schedule PState
H2 : JLFP_policy Job
H_priority_is_reflexive : reflexive_priorities
============================
work_bearing_readiness arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
intros ? ? ARR PEND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence Job
sched : schedule PState
H2 : JLFP_policy Job
H_priority_is_reflexive : reflexive_priorities
j : Job
t : instant
ARR : arrives_in arr_seq j
PEND : pending sched j t
============================
exists j_hp : Job,
arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
----------------------------------------------------------------------------- *)
∃ j; repeat split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 114)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence Job
sched : schedule PState
H2 : JLFP_policy Job
H_priority_is_reflexive : reflexive_priorities
j : Job
t : instant
ARR : arrives_in arr_seq j
PEND : pending sched j t
============================
hep_job j j
----------------------------------------------------------------------------- *)
by eapply (H_priority_is_reflexive 0).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End LiuAndLaylandReadiness.
work_bearing_readiness arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 54)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence Job
sched : schedule PState
H2 : JLFP_policy Job
H_priority_is_reflexive : reflexive_priorities
============================
work_bearing_readiness arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
intros ? ? ARR PEND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence Job
sched : schedule PState
H2 : JLFP_policy Job
H_priority_is_reflexive : reflexive_priorities
j : Job
t : instant
ARR : arrives_in arr_seq j
PEND : pending sched j t
============================
exists j_hp : Job,
arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
----------------------------------------------------------------------------- *)
∃ j; repeat split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 114)
Job : JobType
PState : Type
H : ProcessorState Job PState
H0 : JobArrival Job
H1 : JobCost Job
arr_seq : arrival_sequence Job
sched : schedule PState
H2 : JLFP_policy Job
H_priority_is_reflexive : reflexive_priorities
j : Job
t : instant
ARR : arrives_in arr_seq j
PEND : pending sched j t
============================
hep_job j j
----------------------------------------------------------------------------- *)
by eapply (H_priority_is_reflexive 0).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End LiuAndLaylandReadiness.