From 2f5fe6a2366a787f1d01df3036ee658a932e9e96 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 24 Mar 2022 18:37:41 +0100
Subject: [PATCH] make the limited-preemptive job model a local instance

---
 analysis/facts/preemption/job/limited.v           | 14 +++++++-------
 .../facts/preemption/rtc_threshold/floating.v     |  2 +-
 analysis/facts/preemption/rtc_threshold/limited.v |  1 +
 analysis/facts/preemption/task/floating.v         | 15 ++++++++-------
 analysis/facts/preemption/task/limited.v          | 15 +++++++--------
 model/preemption/limited_preemptive.v             |  8 ++++----
 model/task/preemption/floating_nonpreemptive.v    |  5 ++++-
 model/task/preemption/limited_preemptive.v        |  2 +-
 results/edf/rta/floating_nonpreemptive.v          |  7 +++----
 results/edf/rta/limited_preemptive.v              |  3 +++
 .../fixed_priority/rta/floating_nonpreemptive.v   |  7 +++----
 results/fixed_priority/rta/limited_preemptive.v   |  3 +++
 12 files changed, 45 insertions(+), 37 deletions(-)

diff --git a/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
index d992e4620..59ea4ec49 100644
--- a/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ -3,10 +3,7 @@ Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.analysis.facts.behavior.all.
 Require Export prosa.analysis.facts.model.sequential.
 Require Export prosa.analysis.facts.model.ideal_schedule.
-
-(** Throughout this file, we assume the job model with limited
-    preemption points. *)
-Require Import prosa.model.preemption.limited_preemptive.
+Require Export prosa.model.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of predicate
@@ -25,9 +22,12 @@ Section ModelWithLimitedPreemptions.
   Context `{JobCost Job}.
 
   (** In addition, assume the existence of a function that maps a job
-      to the sequence of its preemption points. *)
+      to the sequence of its preemption points... *)
   Context `{JobPreemptionPoints Job}.
 
+  (** ..., i.e., we assume limited-preemptive jobs. *)
+  #[local] Existing Instance limited_preemptive_job_model.
+
   (** Consider any arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
   
@@ -176,7 +176,7 @@ Section ModelWithLimitedPreemptions.
         last0 (filter (fun x => 0 < x) (distances (job_preemption_points j))).
     Proof.
       destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
-      unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
+      unfold parameter.job_preemption_points, job_preemptable, limited_preemptive_job_model.
       intros; rewrite distances_iota_filtered; eauto.
       rewrite -A2 //.
         by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
@@ -191,7 +191,7 @@ Section ModelWithLimitedPreemptions.
       max0 (distances (job_preemption_points j)).
     Proof.
       destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
-      unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
+      unfold parameter.job_preemption_points, job_preemptable, limited_preemptive_job_model.
       intros; rewrite distances_iota_filtered; eauto 2.
       rewrite max0_rem0 //.
       rewrite -A2 //.
diff --git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index b81a81011..68cc14ee5 100644
--- a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -1,6 +1,6 @@
 Require Export prosa.analysis.facts.preemption.task.floating.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
-Require Import prosa.model.task.preemption.floating_nonpreemptive.
+Require Export prosa.model.task.preemption.floating_nonpreemptive.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 54da3f195..567ce69b0 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -12,6 +12,7 @@ Require Import prosa.model.preemption.limited_preemptive.
 Section TaskRTCThresholdLimitedPreemptions.
 
   (** We assume the task model with fixed preemption points. *)
+  #[local] Existing Instance limited_preemptive_job_model.
   #[local] Existing Instance limited_preemptions_rtc_threshold.
 
   (** Consider any type of tasks ... *)
diff --git a/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
index 0171bff61..b6a9cf733 100644
--- a/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -1,9 +1,8 @@
 Require Export prosa.analysis.facts.preemption.job.limited.
-
-(** Furthermore, we assume the task model with floating non-preemptive regions. *)
 Require Import prosa.model.task.preemption.floating_nonpreemptive.
 Require Import prosa.model.preemption.limited_preemptive.
 
+
 (** * Platform for Floating Non-Preemptive Regions Model *)
 (** In this section, we prove that instantiation of functions
     [job_preemptable and task_max_nonpreemptive_segment] to the model
@@ -26,9 +25,11 @@ Section FloatingNonPreemptiveRegionsModel.
   Context `{TaskMaxNonpreemptiveSegment Task}.
 
   (** .. and the existence of functions mapping a
-      job to the sequence of its preemption points. *)
+      job to the sequence of its preemption points, ... *)
   Context `{JobPreemptionPoints Job}.
-  
+  (** ... i.e., we assume limited-preemptive jobs. *)
+  #[local] Existing Instance limited_preemptive_job_model.
+
   (** Consider any arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
   
@@ -59,19 +60,19 @@ Section FloatingNonPreemptiveRegionsModel.
     - split.
       rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
               /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
-      rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+      rewrite /job_preemptable /limited_preemptive_job_model; erewrite zero_in_preemption_points; eauto 2.
       + move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
         exists 0; rewrite LE; split; first by apply/andP; split.
           by eapply zero_in_preemption_points; eauto 2.
     - split; last (move => progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
       + by apply MAX.
-      + exists progr; split; first apply/andP; first split; rewrite ?leq_addr; by done. 
+      + by exists progr; split; first apply/andP; first split; rewrite ?leq_addr // conversion_preserves_equivalence. 
       + move: NotIN => /eqP; rewrite eqbF_neg; move => NotIN. 
         edestruct (work_belongs_to_some_nonpreemptive_segment arr_seq) as [x [SIZE2 N]]; eauto 2. move: N => /andP [N1 N2].
         set ptl := nth 0 (job_preemption_points j) x.
         set ptr := nth 0 (job_preemption_points j) x.+1.
         exists ptr; split; first last.
-        * by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
+        * by unfold job_preemptable, limited_preemptive_job_model; apply mem_nth.
         * apply/andP; split; first by apply ltnW.
           apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
           -- rewrite addn1 ltn_add2r; apply N1. 
diff --git a/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
index 80ba93c84..bb8745643 100644
--- a/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ -1,8 +1,5 @@
 Require Export prosa.analysis.facts.preemption.job.limited.
-
-(** Furthermore, we assume the task model with fixed preemption points. *)
-Require Import prosa.model.task.preemption.limited_preemptive.
-Require Import prosa.model.preemption.limited_preemptive.
+Require Export prosa.model.task.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of functions
@@ -21,10 +18,12 @@ Section LimitedPreemptionsModel.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
   
-  (** In addition, we assume the existence of functions mapping a
-      job and task to the sequence of its preemption points. *)
+  (** We assume that jobs are preemptable only at specific points during their
+      execution, ... *)
   Context `{JobPreemptionPoints Job}.
   Context `{TaskPreemptionPoints Task}.
+  (** ... i.e., we assume limited-preemptive jobs. *)
+  #[local] Existing Instance limited_preemptive_job_model.
   
   (** Consider any arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
@@ -60,7 +59,7 @@ Section LimitedPreemptionsModel.
     - split.
       rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
               /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
-      rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+      rewrite /job_preemptable /limited_preemptive_job_model; erewrite zero_in_preemption_points; eauto 2.
       + move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
         exists 0; rewrite LE; split; first by apply/andP; split.
           by eapply zero_in_preemption_points; eauto 2.
@@ -74,7 +73,7 @@ Section LimitedPreemptionsModel.
         set ptl := nth 0 (job_preemption_points j) x.
         set ptr := nth 0 (job_preemption_points j) x.+1.
         exists ptr; split; first last.
-        * by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
+        * by unfold job_preemptable, limited_preemptive_job_model; apply mem_nth.
         * apply/andP; split; first by apply ltnW.
           apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
           -- rewrite addn1 ltn_add2r; apply N1. 
diff --git a/model/preemption/limited_preemptive.v b/model/preemption/limited_preemptive.v
index e97da2ae3..32e058b71 100644
--- a/model/preemption/limited_preemptive.v
+++ b/model/preemption/limited_preemptive.v
@@ -31,10 +31,10 @@ Section LimitedPreemptions.
 
   (** ...a job [j] is preemptable at a given point of progress [ρ] iff [ρ] is
       one of the preemption points of [j]. *)
-  Global Instance limited_preemptions_model : JobPreemptable Job :=
-    {
-      job_preemptable (j : Job) (ρ : work) := ρ \in job_preemption_points j
-    }.
+  #[local] Instance limited_preemptive_job_model : JobPreemptable Job :=
+  {
+    job_preemptable (j : Job) (ρ : work) := ρ \in job_preemption_points j
+  }.
 
   (** ** Model Validity *)
 
diff --git a/model/task/preemption/floating_nonpreemptive.v b/model/task/preemption/floating_nonpreemptive.v
index c15a8cdd6..7476b2268 100644
--- a/model/task/preemption/floating_nonpreemptive.v
+++ b/model/task/preemption/floating_nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Import prosa.model.preemption.limited_preemptive.
+Require Export prosa.model.preemption.limited_preemptive.
 Require Export prosa.model.task.preemption.parameters.
 
 (** * Task Model with Floating Non-Preemptive Regions *)
@@ -27,6 +27,9 @@ Section ValidModelWithFloatingNonpreemptiveRegions.
   Context `{JobCost Job}.
   Context `{JobPreemptionPoints Job}.
 
+  (** We assume limited-preemptive jobs. *)
+  #[local] Existing Instance limited_preemptive_job_model.
+
   (** Consider any arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
 
diff --git a/model/task/preemption/limited_preemptive.v b/model/task/preemption/limited_preemptive.v
index c8e4d3b39..a6248232b 100644
--- a/model/task/preemption/limited_preemptive.v
+++ b/model/task/preemption/limited_preemptive.v
@@ -1,5 +1,5 @@
 Require Export prosa.model.task.preemption.parameters.
-Require Import prosa.model.preemption.limited_preemptive.
+Require Export prosa.model.preemption.limited_preemptive.
 
 (** * Limited-Preemptive Task Model *)
 
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index dccc43bd0..3fce23b1f 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -11,10 +11,6 @@ Require Export prosa.analysis.facts.readiness.sequential.
 (** Throughout this file, we assume the EDF priority policy. *)
 Require Import prosa.model.priority.edf.
 
-(** Furthermore, we assume the task model with floating non-preemptive regions. *)
-Require Import prosa.model.preemption.limited_preemptive.
-Require Import prosa.model.task.preemption.floating_nonpreemptive.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
@@ -34,6 +30,9 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
+
+  (** We assume that jobs are limited-preemptive. *)
+  #[local] Existing Instance limited_preemptive_job_model.
   
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 4330b2020..fbc4cd658 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -35,6 +35,9 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
+
+  (** We assume that jobs are limited-preemptive. *)
+  #[local] Existing Instance limited_preemptive_job_model.
    
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 5a5c84a21..dce02894c 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -11,10 +11,6 @@ Require Export prosa.analysis.facts.readiness.sequential.
     schedules, and the sequential readiness model. *)
 Require Import prosa.model.readiness.sequential.
 
-(** Furthermore, we assume the task model with floating non-preemptive regions. *)
-Require Import prosa.model.preemption.limited_preemptive.
-Require Import prosa.model.task.preemption.floating_nonpreemptive.
-
 (** ** Setup and Assumptions *)
 
 Section RTAforFloatingModelwithArrivalCurves.
@@ -32,6 +28,9 @@ Section RTAforFloatingModelwithArrivalCurves.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
+  (** We assume that jobs are limited-preemptive. *)
+  #[local] Existing Instance limited_preemptive_job_model.
+
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 4fc269599..482aa178b 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -32,6 +32,9 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
+
+  (** We assume that jobs are limited-preemptive. *)
+  #[local] Existing Instance limited_preemptive_job_model.
   
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
-- 
GitLab