From 37e9bdac90560a000ca9e17ad9d56c60809cbd53 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 23 Aug 2019 11:40:13 +0200
Subject: [PATCH] relate ideal progress model with job completion
---
restructuring/behavior/facts/completion.v | 21 +++++++++++++++++++--
1 file changed, 19 insertions(+), 2 deletions(-)
diff --git a/restructuring/behavior/facts/completion.v b/restructuring/behavior/facts/completion.v
index ce60f349a..7743faeb4 100644
--- a/restructuring/behavior/facts/completion.v
+++ b/restructuring/behavior/facts/completion.v
@@ -224,6 +224,7 @@ Section ServiceAndCompletionFacts.
first by apply: H_jobs_must_arrive => //.
by apply: scheduled_implies_not_completed => //.
Qed.
+
End GuaranteedService.
End ServiceAndCompletionFacts.
@@ -283,7 +284,7 @@ Section PositiveCost.
End PositiveCost.
-Section RelationToReady.
+Section CompletedJobs.
(* Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
@@ -318,4 +319,20 @@ Section RelationToReady.
by apply ready_implies_incomplete.
Qed.
-End RelationToReady.
+ (* We further observe that completed jobs don't execute if scheduled jobs
+ always receive non-zero service and cumulative service never exceeds job
+ costs. *)
+ Lemma ideal_progress_completed_jobs:
+ ideal_progress_proc_model ->
+ (forall j t, service sched j t <= job_cost j) ->
+ completed_jobs_dont_execute sched.
+ Proof.
+ move=> IDEAL SERVICE_BOUND j t SCHED.
+ have UB := SERVICE_BOUND j t.+1.
+ have POS := IDEAL _ _ SCHED.
+ apply ltn_leq_trans with (n := service sched j t.+1) => //.
+ rewrite -service_last_plus_before /service_at.
+ by rewrite -{1}(addn0 (service sched j t)) ltn_add2l.
+ Qed.
+
+End CompletedJobs.
--
GitLab