From f3039ae5f593a64607b7bd6363f43cfd1fadede3 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:09:11 +0100
Subject: [PATCH] polish prosa.implementation.facts.ideal_uni.preemption_aware
---
.../facts/ideal_uni/preemption_aware.v | 40 +++++++++----------
1 file changed, 19 insertions(+), 21 deletions(-)
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
index e00a3f96a..de4b6ca15 100644
--- a/implementation/facts/ideal_uni/preemption_aware.v
+++ b/implementation/facts/ideal_uni/preemption_aware.v
@@ -210,39 +210,37 @@ Section NPUniprocessorScheduler.
End PreemptionTimes.
- (** In this section, we establish that the preemption-aware scheduler indeed respects
- the preemption model semantics. *)
+ (** Finally, we establish the main feature: the generated schedule respects
+ the preemption-model semantics. *)
Section PreemptionCompliance.
- (** Assuming that every job in [arr_seq] adheres by the rule that jobs must
- start execution to become nonpreemptive,... *)
- Hypothesis H_valid_preemption_function : forall j, arrives_in arr_seq j ->
- job_cannot_become_nonpreemptive_before_execution j.
+ (** As a minimal validity requirement (which is a part of
+ [valid_preemption_model]), we require that any job in [arr_seq] must
+ start execution to become nonpreemptive. *)
+ Hypothesis H_valid_preemption_function :
+ forall j,
+ arrives_in arr_seq j ->
+ job_cannot_become_nonpreemptive_before_execution j.
- (** ...we show that the generated schedule respects the preemption model semantics. *)
+ (** Given such a valid preemption model, we establish that the generated
+ schedule indeed respects the preemption model semantics. *)
Lemma np_respects_preemption_model :
schedule_respects_preemption_model arr_seq schedule.
Proof.
- rewrite /schedule_respects_preemption_model => j.
- elim => [| t' IH];
- first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR) => P; exfalso.
- move => ARR NP.
- have SCHED : scheduled_at schedule j t'.
+ move=> j; elim => [| t' IH];
+ first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR) => P; exfalso.
+ move=> ARR NP.
+ have: scheduled_at schedule j t'.
{ apply contraT => NOT_SCHED.
move: (not_scheduled_implies_no_service _ _ _ NOT_SCHED) => NO_SERVICE.
rewrite -(service_last_plus_before) NO_SERVICE addn0 in NP; apply IH in NP => //.
now move /negP in NOT_SCHED. }
- rewrite /schedule/np_uni_schedule scheduled_at_def /generic_schedule schedule_up_to_def /allocation_at /prev_job_nonpreemptive.
- rewrite /schedule /np_uni_schedule scheduled_at_def /generic_schedule /allocation_at in SCHED.
- move /eqP in SCHED; rewrite SCHED.
- rewrite (identical_prefix_service _ schedule).
- rewrite ifT => //.
- rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule.
- move => h LT; rewrite ltnS in LT.
- now rewrite (schedule_up_to_prefix_inclusion _ _ _ _ LT h).
+ rewrite !scheduled_at_def /schedule/np_uni_schedule/generic_schedule => /eqP SCHED.
+ rewrite -SCHED (schedule_up_to_prefix_inclusion _ _ t' t'.+1) // np_job_remains_scheduled //.
+ rewrite /prev_job_nonpreemptive SCHED (identical_prefix_service _ schedule) //.
+ by apply schedule_up_to_identical_prefix.
Qed.
-
End PreemptionCompliance.
End NPUniprocessorScheduler.
--
GitLab