From 1a52af28fdd517be128179b774cef71196bc0287 Mon Sep 17 00:00:00 2001
From: LailaElbeheiry <osslaila@gmail.com>
Date: Tue, 1 Sep 2020 00:08:13 +0300
Subject: [PATCH] added the np_respect_preemption_model lemma
Proved that np_uni_schedule respects the preemption model
Proved priority compliance of uni_schedule.
---
.../facts/ideal_uni/preemption_aware.v | 36 +++++++++++++++++++
implementation/facts/ideal_uni/prio_aware.v | 18 ++++++++++
2 files changed, 54 insertions(+)
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
index 4a7160f9b..fa50d0604 100644
--- a/implementation/facts/ideal_uni/preemption_aware.v
+++ b/implementation/facts/ideal_uni/preemption_aware.v
@@ -1,6 +1,7 @@
Require Export prosa.implementation.facts.generic_schedule.
Require Export prosa.implementation.definitions.ideal_uni_scheduler.
Require Export prosa.analysis.facts.model.ideal_schedule.
+Require Export prosa.model.schedule.limited_preemptive.
(** * Properties of the Preemption-Aware Ideal Uniprocessor Scheduler *)
@@ -210,6 +211,41 @@ Section NPUniprocessorScheduler.
End PreemptionTimes.
+ (** In this section, we establish that the preemption-aware scheduler indeed 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.
+
+ (** ...we show that the generated schedule 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'.
+ { 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).
+ Qed.
+
+
+ End PreemptionCompliance.
+
End NPUniprocessorScheduler.
diff --git a/implementation/facts/ideal_uni/prio_aware.v b/implementation/facts/ideal_uni/prio_aware.v
index b1df2e0ee..2a3369c30 100644
--- a/implementation/facts/ideal_uni/prio_aware.v
+++ b/implementation/facts/ideal_uni/prio_aware.v
@@ -119,4 +119,22 @@ Section PrioAwareUniprocessorScheduler.
End Priority.
+ (** In this section, we show that [uni_schedule arr_seq] respects the preemption model semantics. *)
+ Section PreemptionCompliance.
+
+ (** Suppose 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.
+
+ (** Since [uni_schedule arr_seq] is an instance of [np_uni_schedule], then the compliance of
+ [schedule] to the preemption model follows trivially from the compliance of [np_uni_schedule]. *)
+ Lemma schedule_respects_preemption_model :
+ schedule_respects_preemption_model arr_seq schedule.
+ Proof.
+ by apply np_respects_preemption_model .
+ Qed.
+
+ End PreemptionCompliance.
+
End PrioAwareUniprocessorScheduler.
--
GitLab