From 0ceae79188d121032cdc32e5db4d20268bb97baf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 20 Aug 2019 23:01:41 +0200
Subject: [PATCH] note equivalence of assumptions in case of basic readiness
---
restructuring/model/readiness/basic.v | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index c8125ed34..d9fd6d860 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -1,4 +1,5 @@
From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior.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
@@ -22,4 +23,24 @@ Section LiuAndLaylandReadiness.
}.
Proof. trivial. Defined.
+
+ (* 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:
+ forall 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.
+
--
GitLab