From 41a542a85c7d8edcca16522b8414ab87aab93569 Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <f20171026@goa.bits-pilani.ac.in>
Date: Fri, 6 May 2022 07:45:52 +0000
Subject: [PATCH] modify definitions of priority policy compliance
The current definitions of `respects_JLFP_policy_at_preemption_time`
and `respects_FP_policy_at_preemption_time` use the predicate
`hep_job_at`. This predicate does not make sense for `JLFP`
and `FP` policies. To avoid this, these definitions should
instead use the definition `respects_JLDP_policy_at_preemption_point`.
Doing this requires coercions from `JLFP` to `JLDP` and from
`FP` to `JLFP`. This patch also introduces these coercions.
---
model/priority/classes.v | 5 +++++
model/schedule/priority_driven.v | 18 +++++-------------
scripts/wordlist.pws | 1 +
3 files changed, 11 insertions(+), 13 deletions(-)
diff --git a/model/priority/classes.v b/model/priority/classes.v
index c7766865b..a6e953a81 100644
--- a/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -49,6 +49,11 @@ Instance FP_to_JLFP (Job: JobType) (Task: TaskType)
Instance JLFP_to_JLDP (Job: JobType) `{JLFP_policy Job} : JLDP_policy Job :=
fun _ j1 j2 => hep_job j1 j2.
+(** We add coercions to enable automatic conversion from [JLFP] to [JLDP]... *)
+Coercion JLFP_to_JLDP : JLFP_policy >-> JLDP_policy.
+(** ...and from [FP] to [JLFP]. *)
+Coercion FP_to_JLFP : FP_policy >-> JLFP_policy.
+
(** ** Properties of Priority Policies *)
(** In the following section, we define key properties of common priority
diff --git a/model/schedule/priority_driven.v b/model/schedule/priority_driven.v
index 49357bead..a8c23380d 100644
--- a/model/schedule/priority_driven.v
+++ b/model/schedule/priority_driven.v
@@ -46,22 +46,14 @@ Section Priority.
preemption_time sched t ->
backlogged sched j t ->
scheduled_at sched j_hp t ->
- hep_job_at t j_hp j.
+ hep_job_at t j_hp j.
+
(** ... [JLFP], and... *)
Definition respects_JLFP_policy_at_preemption_point (policy: JLFP_policy Job) :=
- forall j j_hp t,
- arrives_in arr_seq j ->
- preemption_time sched t ->
- backlogged sched j t ->
- scheduled_at sched j_hp t ->
- hep_job_at t j_hp j.
+ respects_JLDP_policy_at_preemption_point policy.
+
(** [FP]. *)
Definition respects_FP_policy_at_preemption_point (policy: FP_policy Task) :=
- forall j j_hp t,
- arrives_in arr_seq j ->
- preemption_time sched t ->
- backlogged sched j t ->
- scheduled_at sched j_hp t ->
- hep_job_at t j_hp j.
+ respects_JLDP_policy_at_preemption_point (FP_to_JLFP Job Task ).
End Priority.
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index 3de0d0f0d..208f1bb0f 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -77,3 +77,4 @@ et
al
discoverable
formedness
+coercions
--
GitLab