From fb1dbaae93861dadf06b94ee020d215bf19b20e3 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Sat, 5 Apr 2025 18:26:26 +0200
Subject: [PATCH] make fully-preemptive policy explicit

---
 rt/analysis/completion_time.v             |  3 ++-
 rt/analysis/pRTA/pRTA.v                   |  2 +-
 rt/analysis/scheduler_properties.v        |  4 +++-
 rt/model/assumptions/pr_respects_policy.v | 10 ++++------
 4 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/rt/analysis/completion_time.v b/rt/analysis/completion_time.v
index 398b435..dc10879 100644
--- a/rt/analysis/completion_time.v
+++ b/rt/analysis/completion_time.v
@@ -1,5 +1,6 @@
 (* --------------------------------- Prosa ---------------------------------- *)
 From prosa.analysis Require Export facts.model.service_of_jobs.
+From prosa Require Export model.preemption.fully_preemptive.
 
 (* --------------------------------- ProBsa --------------------------------- *)
 From probsa.rt.model Require Export abort_readiness.
@@ -30,7 +31,7 @@ Section CompletionTimeExists.
   Variable sched : pr_schedule μ (ideal.processor_state Job).
   Hypothesis H_work_conserving : pr_work_conserving sched pr_abort_ready_instance.
   Hypothesis H_respects_policy_at_preemption_point :
-    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance.
+    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.
   Hypothesis H_pr_jobs_must_be_ready_to_execute :
     pr_jobs_must_be_ready_to_execute sched pr_abort_ready_instance.
 
diff --git a/rt/analysis/pRTA/pRTA.v b/rt/analysis/pRTA/pRTA.v
index fca5a2e..9537a70 100644
--- a/rt/analysis/pRTA/pRTA.v
+++ b/rt/analysis/pRTA/pRTA.v
@@ -165,7 +165,7 @@ Section WCDFPIsBounded.
   (** ... and assume that it is work conserving and respects the FP-FP policy. *)
   Hypothesis H_work_conserving : pr_work_conserving sched pr_abort_ready_instance.
   Hypothesis H_respects_policy_at_preemption_point :
-    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance.
+    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.
 
   Hypothesis H_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence sched.
   Hypothesis H_completed_jobs_dont_execute : pr_completed_jobs_dont_execute sched.
diff --git a/rt/analysis/scheduler_properties.v b/rt/analysis/scheduler_properties.v
index 75ecfd9..839bc88 100644
--- a/rt/analysis/scheduler_properties.v
+++ b/rt/analysis/scheduler_properties.v
@@ -1,4 +1,5 @@
 (* --------------------------------- Prosa ---------------------------------- *)
+From prosa Require Export model.preemption.fully_preemptive.
 From prosa.implementation Require Import facts.ideal_uni.prio_aware.
 
 (* --------------------------------- ProBsa --------------------------------- *)
@@ -297,7 +298,8 @@ Section SchedulerProperties.
   Qed.
 
   Lemma FP_FP_sched_respects_policy_at_preemption_point :
-    pr_respects_policy_at_preemption_point pr_sched pr_abort_ready_instance.
+    pr_respects_policy_at_preemption_point
+      pr_sched pr_abort_ready_instance fully_preemptive_model.
   Proof.
     intros ω; apply schedule_respects_policy => //.
     { by apply pr_consistent_arrival_times. }
diff --git a/rt/model/assumptions/pr_respects_policy.v b/rt/model/assumptions/pr_respects_policy.v
index 32ff5f7..ad412ba 100644
--- a/rt/model/assumptions/pr_respects_policy.v
+++ b/rt/model/assumptions/pr_respects_policy.v
@@ -1,8 +1,4 @@
 (* --------------------------------- Prosa ---------------------------------- *)
-(* TODO: switch to generic preemption policy *)
-(* From prosa Require Export model.preemption.parameter. *)
-From prosa Require Export model.preemption.fully_preemptive.
-
 From prosa.model Require Export schedule.priority_driven.
 
 (* --------------------------------- ProBsa --------------------------------- *)
@@ -29,8 +25,10 @@ Section PrRespectsPolicyAtPreemptionPoint.
         Job (ideal.processor_state Job)
         (fun j => odflt0 (job_cost j) ω) (fun j => odflt0 (job_arrival j) ω).
 
-  Definition pr_respects_policy_at_preemption_point (job_ready : JobReadyRV) :=
+  Definition pr_respects_policy_at_preemption_point
+             (job_ready : JobReadyRV) (job_preemptable : JobPreemptable Job) :=
     forall (ω : Ω),
-      @respects_policy_at_preemption_point _ _ _ _ (job_ready ω) (arr_seq ω) (sched ω) _.
+      @respects_policy_at_preemption_point
+        _ _ _ job_preemptable (job_ready ω) (arr_seq ω) (sched ω) _.
 
 End PrRespectsPolicyAtPreemptionPoint.
-- 
GitLab