From 8b22505b7af91c78c4248983d78a776d024aff84 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 11 Mar 2021 15:05:07 +0100
Subject: [PATCH] extract schedule_up_to_identical_prefix corollary for reuse
---
implementation/facts/generic_schedule.v | 15 ++++++++++++++-
implementation/facts/ideal_uni/preemption_aware.v | 3 +--
2 files changed, 15 insertions(+), 3 deletions(-)
diff --git a/implementation/facts/generic_schedule.v b/implementation/facts/generic_schedule.v
index 142075708..7c092d4a9 100644
--- a/implementation/facts/generic_schedule.v
+++ b/implementation/facts/generic_schedule.v
@@ -68,7 +68,7 @@ Section GenericScheduleProperties.
Qed.
(** A crucial fact is that a prefix up to horizon [h1] is identical to a
- prefix up to a later horizon [h2] at times up to [h1]. *)
+ prefix up to a later horizon [h2] at times up to [h1]. *)
Lemma schedule_up_to_prefix_inclusion:
forall h1 h2,
h1 <= h2 ->
@@ -84,4 +84,17 @@ Section GenericScheduleProperties.
now apply (leq_trans t_H1).
Qed.
+ (** It follows that [generic_schedule] and [schedule_up_to] for a given
+ horizon [h] share an identical prefix. *)
+ Corollary schedule_up_to_identical_prefix:
+ forall h t,
+ t <= h.+1 ->
+ identical_prefix (schedule_up_to policy idle_state h) (generic_schedule policy idle_state) t.
+ Proof.
+ move=> h t LE.
+ rewrite /identical_prefix /generic_schedule => t' LT.
+ rewrite (schedule_up_to_prefix_inclusion t' h) //.
+ by move: (leq_trans LT LE); rewrite ltnS.
+ Qed.
+
End GenericScheduleProperties.
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
index fa50d0604..e00a3f96a 100644
--- a/implementation/facts/ideal_uni/preemption_aware.v
+++ b/implementation/facts/ideal_uni/preemption_aware.v
@@ -150,8 +150,7 @@ Section NPUniprocessorScheduler.
move: (H_chooses_from_set _ _ _ IN).
rewrite mem_filter /backlogged => /andP [/andP [READY _] _].
rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t') schedule j t'.+1) //.
- rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule => t'' LT.
- now rewrite (schedule_up_to_prefix_inclusion _ _ t'' t') //. }
+ by apply schedule_up_to_identical_prefix. }
case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply JOB.
destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply JOB.
apply H_valid_preemption_behavior.
--
GitLab