make the limited-preemptive job model a local instance

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

analysis/facts/preemption/rtc_threshold/floating.v

 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

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 ... *)

analysis/facts/preemption/task/floating.v

 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. 

analysis/facts/preemption/task/limited.v

 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. 

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 *)
 

model/task/preemption/floating_nonpreemptive.v

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

model/task/preemption/limited_preemptive.v

 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 *)
 

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.

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.

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.

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.