From ff88d776e5b8eb0721a4203d90f203ff1c0b110a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 24 Mar 2022 16:57:37 +0100
Subject: [PATCH] disambiguate preemption model and RTC threshold instances

---
 analysis/facts/preemption/rtc_threshold/floating.v      | 2 +-
 analysis/facts/preemption/rtc_threshold/limited.v       | 4 ++--
 analysis/facts/preemption/rtc_threshold/nonpreemptive.v | 8 ++++----
 analysis/facts/preemption/rtc_threshold/preemptive.v    | 4 ++--
 analysis/facts/preemption/task/nonpreemptive.v          | 4 ++--
 analysis/facts/preemption/task/preemptive.v             | 4 ++--
 model/task/preemption/floating_nonpreemptive.v          | 2 +-
 model/task/preemption/fully_nonpreemptive.v             | 4 ++--
 model/task/preemption/fully_preemptive.v                | 4 ++--
 model/task/preemption/limited_preemptive.v              | 2 +-
 results/edf/rta/fully_preemptive.v                      | 6 +++---
 results/fixed_priority/rta/fully_preemptive.v           | 6 +++---
 12 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index 53d2804df..b81a81011 100644
--- a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -8,7 +8,7 @@ Require Import prosa.model.task.preemption.floating_nonpreemptive.
 Section TaskRTCThresholdFloatingNonPreemptiveRegions.
 
   (** Furthermore, we assume the task model with floating non-preemptive regions. *)
-  #[local] Existing Instance floating_preemptive.
+  #[local] Existing Instance floating_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 36f5e40f3..54da3f195 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -12,7 +12,7 @@ Require Import prosa.model.preemption.limited_preemptive.
 Section TaskRTCThresholdLimitedPreemptions.
 
   (** We assume the task model with fixed preemption points. *)
-  #[local] Existing Instance limited_preemptions.
+  #[local] Existing Instance limited_preemptions_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
@@ -104,7 +104,7 @@ Section TaskRTCThresholdLimitedPreemptions.
     split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
     intros ? ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) => [LJ LT].
     move: (LJ) (LT) => [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
-    rewrite /job_rtct /task_rtct /limited_preemptions
+    rewrite /job_rtct /task_rtct /limited_preemptions_rtc_threshold
             /job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
     case: (posnP (job_cost j)) => [Z|POS]; first by rewrite Z; compute.
     have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
diff --git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index ce67a5b82..0982fbacc 100644
--- a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -9,9 +9,9 @@ Require Import prosa.model.task.preemption.fully_nonpreemptive.
 Section TaskRTCThresholdFullyNonPreemptive.
 
   (** We assume the fully non-preemptive task model. *)
-  #[local] Existing Instance fully_nonpreemptive_model.
-  #[local] Existing Instance fully_nonpreemptive.
-
+  #[local] Existing Instance fully_nonpreemptive_task_model.
+  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
+  
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}. 
   Context `{TaskCost Task}.
@@ -72,7 +72,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
     intros; split.
     - by unfold task_rtc_bounded_by_cost.
     - intros j ARR TSK.
-      move: TSK => /eqP <-; rewrite /fully_nonpreemptive.
+      move: TSK => /eqP <-; rewrite /fully_nonpreemptive_rtc_threshold.
       edestruct (posnP (job_cost j)) as [ZERO|POS].
       + by rewrite job_rtc_threshold_is_0.
       + by erewrite job_rtc_threshold_is_ε; eauto 2. 
diff --git a/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
index d8cbbeb4c..04ad48fff 100644
--- a/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -12,8 +12,8 @@ Section TaskRTCThresholdFullyPreemptiveModel.
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance
     model.preemption.fully_preemptive.fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
diff --git a/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
index 810081e55..1e9a62ee8 100644
--- a/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ -10,8 +10,8 @@ Require Import prosa.model.task.preemption.fully_nonpreemptive.
 Section FullyNonPreemptiveModel.
 
   (** We assume the fully non-preemptive task model. *)
-  #[local] Existing Instance fully_nonpreemptive_model.
-  #[local] Existing Instance fully_nonpreemptive.
+  #[local] Existing Instance fully_nonpreemptive_task_model.
+  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
diff --git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index c5a8f4bf8..5dd416eb1 100644
--- a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -12,8 +12,8 @@ Section FullyPreemptiveModel.
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance
     model.preemption.fully_preemptive.fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
diff --git a/model/task/preemption/floating_nonpreemptive.v b/model/task/preemption/floating_nonpreemptive.v
index 60d621e7f..c15a8cdd6 100644
--- a/model/task/preemption/floating_nonpreemptive.v
+++ b/model/task/preemption/floating_nonpreemptive.v
@@ -59,7 +59,7 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
       information about the placement of preemption points in all jobs, i.e.,
       it is impossible to predict when exactly a job will be preemptable. Thus,
       the only safe run-to-completion threshold is [task cost]. *)
-  Definition floating_preemptive : TaskRunToCompletionThreshold Task :=
+  Definition floating_preemptive_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => task_cost tsk.
 
 End TaskRTCThresholdFloatingNonPreemptiveRegions.
diff --git a/model/task/preemption/fully_nonpreemptive.v b/model/task/preemption/fully_nonpreemptive.v
index ca541512c..249dc0685 100644
--- a/model/task/preemption/fully_nonpreemptive.v
+++ b/model/task/preemption/fully_nonpreemptive.v
@@ -13,7 +13,7 @@ Section FullyNonPreemptiveModel.
   (** In the fully non-preemptive model, no job can be preempted until its
       completion. The maximal non-preemptive segment of a job [j] has length
       [job_cost j], which is bounded by [task_cost tsk].*)
-  Definition fully_nonpreemptive_model : TaskMaxNonpreemptiveSegment Task :=
+  Definition fully_nonpreemptive_task_model : TaskMaxNonpreemptiveSegment Task :=
     fun tsk : Task => task_cost tsk.
 
 End FullyNonPreemptiveModel.
@@ -31,7 +31,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
       completion. In other words, once a job starts running, it is guaranteed
       to finish. Thus, we can set the task-level run-to-completion threshold
       to ε. *)
-  Definition fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
+  Definition fully_nonpreemptive_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => ε.
 
 End TaskRTCThresholdFullyNonPreemptive.
diff --git a/model/task/preemption/fully_preemptive.v b/model/task/preemption/fully_preemptive.v
index a6eea1288..f3d48b5fe 100644
--- a/model/task/preemption/fully_preemptive.v
+++ b/model/task/preemption/fully_preemptive.v
@@ -13,7 +13,7 @@ Section FullyPreemptiveModel.
   (** In the fully preemptive model, any job can be preempted at any
       time. Thus, the maximal non-preemptive segment has length at most ε
       (i.e., one time unit such as a processor cycle). *)
-  Definition fully_preemptive_model : TaskMaxNonpreemptiveSegment Task :=
+  Definition fully_preemptive_task_model : TaskMaxNonpreemptiveSegment Task :=
     fun tsk : Task => ε.
 
 End FullyPreemptiveModel.
@@ -32,7 +32,7 @@ Section TaskRTCThresholdFullyPreemptiveModel.
   (** In the fully preemptive model, any job can be preempted at any
       time. Thus, the only safe run-to-completion threshold for a task
       is its WCET. *)
-  Definition fully_preemptive : TaskRunToCompletionThreshold Task :=
+  Definition fully_preemptive_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => task_cost tsk.
 
 End TaskRTCThresholdFullyPreemptiveModel.
diff --git a/model/task/preemption/limited_preemptive.v b/model/task/preemption/limited_preemptive.v
index b0719ed11..c8e4d3b39 100644
--- a/model/task/preemption/limited_preemptive.v
+++ b/model/task/preemption/limited_preemptive.v
@@ -106,7 +106,7 @@ Section TaskRTCThresholdLimitedPreemptions.
       reaches its last non-preemptive segment. Thus, we can set the task-level
       run-to-completion threshold to [task_cost tsk - (task_last_nonpr_seg tsk - ε)],
       which safely bounds [job_cost j - (job_last_nonpr_seg j - ε)]. *)
-  Definition limited_preemptions : TaskRunToCompletionThreshold Task :=
+  Definition limited_preemptions_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => task_cost tsk - (task_last_nonpr_segment tsk - ε).
 
 End TaskRTCThresholdLimitedPreemptions.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index dcf9f74c1..79ed6a0fe 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -25,8 +25,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance
     model.preemption.fully_preemptive.fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
@@ -133,7 +133,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Proof.
     have BLOCK: blocking_bound  ts tsk = 0.
     { by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
-                 /fully_preemptive.fully_preemptive_model subnn big1_eq. } 
+                 /fully_preemptive_task_model subnn big1_eq. } 
     try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L) .
     all: rt_eauto.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 96df76702..f061dfadb 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -23,8 +23,8 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance
     model.preemption.fully_preemptive.fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
@@ -139,7 +139,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   Proof.
     have BLOCK: blocking_bound ts tsk = 0.
     { by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
-               /fully_preemptive.fully_preemptive_model subnn big1_eq. } 
+               /fully_preemptive_task_model subnn big1_eq. } 
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.      
     all: rt_eauto.
     rewrite /work_bearing_readiness.
-- 
GitLab