disambiguate preemption model and RTC threshold instances

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}.

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

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. 

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}.

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}.

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}.

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.

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.

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.

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.

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.

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.