From 35ed3fa3dbe37abf8b9997134b5d90aba420d0ec Mon Sep 17 00:00:00 2001
From: Marco Maida <mmaida@mpi-sws.org>
Date: Fri, 12 Mar 2021 10:35:54 +0100
Subject: [PATCH] Shortened, restructured, polished proofs
---
.../facts/ideal_uni/preemption_aware.v | 45 ++++++++++---------
1 file changed, 25 insertions(+), 20 deletions(-)
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
index d1373f7a6..9298cd7ef 100644
--- a/implementation/facts/ideal_uni/preemption_aware.v
+++ b/implementation/facts/ideal_uni/preemption_aware.v
@@ -123,11 +123,24 @@ Section NPUniprocessorScheduler.
Hypothesis H_valid_preemption_behavior:
valid_nonpreemptive_readiness RM.
- (** Under this natural assumption, the generated schedule is valid. *)
+ (** First, we show that if a job is chosen from the list of backlogged jobs, then it must be ready. *)
+ Lemma choose_job_implies_job_ready:
+ forall t j,
+ choose_job t.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t) t.+1) = Some j
+ -> job_ready schedule j t.+1.
+ Proof.
+ move=> t j IN.
+ 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) //.
+ by apply schedule_up_to_identical_prefix.
+ Qed.
+
+ (** Next, we show that, under these natural assumptions, the generated schedule is valid. *)
Theorem np_schedule_valid:
valid_schedule schedule arr_seq.
Proof.
- rewrite /valid_schedule; split; move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
+ split; move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
{ elim: t => [/eqP | t' IH /eqP].
- rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => IN.
move: (H_chooses_from_set _ _ _ IN).
@@ -143,16 +156,8 @@ Section NPUniprocessorScheduler.
rewrite mem_filter /backlogged => /andP [/andP [READY _] _].
by rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0).
- rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive.
- have JOB: choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t') t'.+1)
- = Some j
- -> job_ready schedule j t'.+1.
- { move=> IN.
- 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) //.
- 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.
+ case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply choose_job_implies_job_ready.
+ destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply choose_job_implies_job_ready.
apply H_valid_preemption_behavior.
injection EQ => <-.
move: NP.
@@ -196,13 +201,13 @@ Section NPUniprocessorScheduler.
~~ preemption_time schedule t.
Proof.
elim => [|t _]; first by rewrite /prev_job_nonpreemptive.
- rewrite /schedule /np_uni_schedule /generic_schedule /preemption_time schedule_up_to_def /prefix /allocation_at => NP.
- rewrite ifT //.
- rewrite -pred_Sn.
- move: NP. rewrite /prev_job_nonpreemptive.
+ rewrite /schedule /np_uni_schedule /generic_schedule /preemption_time
+ schedule_up_to_def /prefix /allocation_at => NP.
+ rewrite ifT // -pred_Sn.
+ move: NP; rewrite /prev_job_nonpreemptive.
elim: (schedule_up_to policy idle_state t t) => // j.
- have <-: service (schedule_up_to policy idle_state t) j t.+1
- = service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 => //.
+ have ->: (service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 =
+ service (schedule_up_to policy idle_state t) j t.+1) => //.
rewrite /service.
apply equal_prefix_implies_same_service_during => t' /andP [_ BOUND].
by rewrite (schedule_up_to_prefix_inclusion _ _ t' t).
@@ -227,8 +232,8 @@ Section NPUniprocessorScheduler.
Lemma np_respects_preemption_model :
schedule_respects_preemption_model arr_seq schedule.
Proof.
- move=> j; elim => [| t' IH];
- first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR) => P; exfalso.
+ move=> j.
+ elim => [| t' IH]; first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR).
move=> ARR NP.
have: scheduled_at schedule j t'.
{ apply contraT => NOT_SCHED.
--
GitLab