From 04af1bb46c2b069c90d7b4b3910bde3b0cd9a527 Mon Sep 17 00:00:00 2001
From: kimaya <f20171026@goa.bits-pilani.ac.in>
Date: Mon, 25 Oct 2021 16:37:30 +0200
Subject: [PATCH] add a stronger notion of priority policy compliance
The existing notion of priority policy compliance is silent on preemptions
that exchange jobs of equal priority. A real scheduler would not engage
in such superfluous preemptions. For some intuitively true properties, it
is natural and necessary to assume the absence of superfluous preemptions.
This patch introduces a definition for this purpose.
---
model/preemption/parameter.v | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/model/preemption/parameter.v b/model/preemption/parameter.v
index 210792017..be3211a50 100644
--- a/model/preemption/parameter.v
+++ b/model/preemption/parameter.v
@@ -1,5 +1,6 @@
Require Export prosa.util.all.
Require Export prosa.behavior.all.
+Require Export prosa.model.priority.classes.
(** * Job-Level Preemption Model *)
(** There are many equivalent ways to represent at which points in time a job
@@ -95,6 +96,9 @@ Section PreemptionModel.
(** ... and any preemption model. *)
Context `{JobPreemptable Job}.
+ (** Consider any JLDP policy. *)
+ Context `{JLDP_policy Job}.
+
(** Consider any kind of processor model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
@@ -146,5 +150,13 @@ Section PreemptionModel.
/\ job_cannot_be_nonpreemptive_after_completion j
/\ not_preemptive_implies_scheduled j
/\ execution_starts_with_preemption_point j.
+
+ (** We say that there are no superfluous preemptions if a job can
+ only be preempted by another job having strictly higher priority. *)
+ Definition no_superfluous_preemptions :=
+ forall t j j_hp,
+ preempted_at j t ->
+ scheduled_at sched j_hp t ->
+ ~~ hep_job_at t j j_hp.
End PreemptionModel.
--
GitLab