Library prosa.analysis.facts.readiness.basic
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.
Proof.
move⇒ sched ARR COMP.
rewrite /jobs_must_be_ready_to_execute ⇒ j t SCHED.
rewrite /job_ready /basic_ready_instance /pending.
apply /andP; split.
- by apply ARR.
- rewrite -less_service_than_cost_is_incomplete.
by apply COMP.
Qed.
End LiuAndLaylandReadiness.
∀ sched,
jobs_must_arrive_to_execute sched →
completed_jobs_dont_execute sched →
jobs_must_be_ready_to_execute sched.
Proof.
move⇒ sched ARR COMP.
rewrite /jobs_must_be_ready_to_execute ⇒ j t SCHED.
rewrite /job_ready /basic_ready_instance /pending.
apply /andP; split.
- by apply ARR.
- rewrite -less_service_than_cost_is_incomplete.
by apply COMP.
Qed.
End LiuAndLaylandReadiness.