From f925eeee3e81dba90efde213fa2ca6d767384919 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 28 Mar 2022 15:55:03 +0200
Subject: [PATCH] fix the `job_preemption_points` name clash

Rename the type-class parameter to `job_preemptive_points` to avoid a
name clash with the the definition of the same name.

Keep `JobPreemptionPoints` to match `TaskPreemptionPoints`. This does
not  result in a name clash.
---
 analysis/facts/preemption/job/limited.v       | 66 +++++++++----------
 .../facts/preemption/rtc_threshold/limited.v  |  4 +-
 analysis/facts/preemption/task/floating.v     | 12 ++--
 analysis/facts/preemption/task/limited.v      |  8 +--
 model/preemption/limited_preemptive.v         | 24 ++++---
 model/task/preemption/limited_preemptive.v    |  4 +-
 6 files changed, 59 insertions(+), 59 deletions(-)

diff --git a/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
index 59ea4ec49..1c02cea30 100644
--- a/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ -52,13 +52,13 @@ Section ModelWithLimitedPreemptions.
     Hypothesis H_j_arrives : arrives_in arr_seq j.
 
     (** Recall that 0 is a preemption point. *)
-    Remark zero_in_preemption_points: 0 \in job_preemption_points j.
+    Remark zero_in_preemption_points: 0 \in job_preemptive_points j.
     Proof. by apply H_valid_limited_preemptions_job_model. Qed.                
     
-    (** Using the fact that [job_preemption_points] is a
+    (** Using the fact that [job_preemptive_points] is a
         non-decreasing sequence, we prove that the first element of
-        [job_preemption_points] is 0. *)
-    Lemma zero_is_first_element: first0 (job_preemption_points j) = 0.
+        [job_preemptive_points] is 0. *)
+    Lemma zero_is_first_element: first0 (job_preemptive_points j) = 0.
     Proof.
       have F := zero_in_preemption_points.
       destruct H_valid_limited_preemptions_job_model as [_ [_ C]]; specialize (C j H_j_arrives).
@@ -67,7 +67,7 @@ Section ModelWithLimitedPreemptions.
     
     (** We prove that the list of preemption points is not empty. *)
     Lemma list_of_preemption_point_is_not_empty:
-      0 < size (job_preemption_points j).
+      0 < size (job_preemptive_points j).
     Proof.
       move: H_valid_limited_preemptions_job_model => [BEG [END _]].
       apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; rewrite size_eq0 in CONTR.
@@ -76,14 +76,14 @@ Section ModelWithLimitedPreemptions.
     Qed.
 
     (** Next, we prove that the cost of a job is a preemption point. *)
-    Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemption_points j.
+    Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemptive_points j.
     Proof.
       move: H_valid_limited_preemptions_job_model => [BEG [END _]].
       move: (END _ H_j_arrives) => EQ.
       rewrite -EQ; clear EQ.
       rewrite /last0 -nth_last.
       apply/(nthP 0).
-      exists ((size (job_preemption_points j)).-1); last by done. 
+      exists ((size (job_preemptive_points j)).-1); last by done.
       rewrite -(leq_add2r 1) !addn1 prednK //.
         by apply list_of_preemption_point_is_not_empty.
     Qed.
@@ -93,7 +93,7 @@ Section ModelWithLimitedPreemptions.
         points. *)
     Corollary number_of_preemption_points_at_least_two:
       job_cost_positive j ->
-      2 <= size (job_preemption_points j).
+      2 <= size (job_preemptive_points j).
     Proof.
       intros POS.
       move: H_valid_limited_preemptions_job_model => [BEG [END _]]. 
@@ -116,8 +116,8 @@ Section ModelWithLimitedPreemptions.
     Lemma antidensity_of_preemption_points:
       forall (ρ : work),
         ρ <= job_cost j -> 
-        ~~ (ρ \in job_preemption_points j) -> 
-        first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j). 
+        ~~ (ρ \in job_preemptive_points j) ->
+        first0 (job_preemptive_points j) <= ρ < last0 (job_preemptive_points j).
     Proof.
       intros ρ LE NotIN.
       move: H_valid_limited_preemptions_job_model => [BEG [END NDEC]].
@@ -137,10 +137,10 @@ Section ModelWithLimitedPreemptions.
     Lemma work_belongs_to_some_nonpreemptive_segment:
       forall (ρ : work),
         ρ <= job_cost j ->
-        ~~ (ρ \in job_preemption_points j)-> 
+        ~~ (ρ \in job_preemptive_points j) ->
         exists n,
-          n.+1 < size (job_preemption_points j) /\
-          nth 0 (job_preemption_points j) n < ρ < nth 0 (job_preemption_points j) n.+1.
+          n.+1 < size (job_preemptive_points j) /\
+          nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1.
     Proof.
       intros ρ LE NotIN.
       case: (posnP (job_cost j)) => [ZERO|POS].
@@ -148,7 +148,7 @@ Section ModelWithLimitedPreemptions.
         move: LE. rewrite ZERO leqn0; move => /eqP ->.
           by apply zero_in_preemption_points. }
       move: (belonging_to_segment_of_seq_is_total
-               (job_preemption_points j) ρ (number_of_preemption_points_at_least_two POS)
+               (job_preemptive_points j) ρ (number_of_preemption_points_at_least_two POS)
                (antidensity_of_preemption_points _ LE NotIN)) => [n [SIZE2 /andP [N1 N2]]].
       exists n; split; first by done.
       apply/andP; split; last by done.
@@ -160,38 +160,34 @@ Section ModelWithLimitedPreemptions.
         by apply ltnW. 
     Qed.
 
-    (** Recall that file [job.parameters] also defines notion of
-        preemption points.  And note that
-        [job.parameter.job_preemption_points] cannot have a
-        duplicating preemption points. Therefore, we need additional
-        lemmas to relate [job.parameter.job_preemption_points] and
-        [limited.job_preemption_points]]. *)
-
-    (** First we show that the length of the last non-preemptive
-        segment of [job.parameter.job_preemption_points] is equal to
-        the length of the last non-empty non-preemptive segment of
-        [limited.job_preemption_points]. *)
+    (** Recall that the module [prosa.model.preemption.parameters] also defines
+        a notion of preemption points, namely [job_preemption_points], which
+        cannot have duplicated preemption points. Therefore, we need additional
+        lemmas to relate [job_preemption_points] and [job_preemptive_points]. *)
+
+    (** First we show that the length of the last non-preemptive segment in
+        [job_preemption_points] is equal to the length of the last non-empty
+        non-preemptive segment of [job_preemptive_points]. *)
     Lemma job_parameters_last_np_to_job_limited:
-        last0 (distances (parameter.job_preemption_points j)) =
-        last0 (filter (fun x => 0 < x) (distances (job_preemption_points j))).
+        last0 (distances (job_preemption_points j)) =
+        last0 (filter (fun x => 0 < x) (distances (job_preemptive_points j))).
     Proof.
       destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
-      unfold parameter.job_preemption_points, job_preemptable, limited_preemptive_job_model.
+      unfold 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.
     Qed.
 
-    (** Next we show that the length of the max non-preemptive
-        segment of [job.parameter.job_preemption_points] is equal to
-        the length of the max non-preemptive segment of
-        [limited.job_preemption_points]. *)
+    (** Next we show that the length of the max non-preemptive segment of
+        [job_preemption_points] is equal to the length of the max non-preemptive
+        segment of [job_preemptive_points]. *)
     Lemma job_parameters_max_np_to_job_limited:
-      max0 (distances (parameter.job_preemption_points j)) =
-      max0 (distances (job_preemption_points j)).
+      max0 (distances (job_preemption_points j)) =
+      max0 (distances (job_preemptive_points j)).
     Proof.
       destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
-      unfold parameter.job_preemption_points, job_preemptable, limited_preemptive_job_model.
+      unfold 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/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 2ff20119d..39edeba09 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -126,9 +126,9 @@ Section TaskRTCThresholdLimitedPreemptions.
     rewrite subnBA // subnBA // -addnBAC // -addnBAC // !addn1 ltnS.
     erewrite job_parameters_last_np_to_job_limited; eauto 2.
     rewrite distances_positive_undup //; last by apply SORT__job. 
-    have -> : job_cost j = last0 (undup (job_preemption_points j)) by rewrite last0_undup; [rewrite -COST__job | apply SORT__job].
+    have -> : job_cost j = last0 (undup (job_preemptive_points j)) by rewrite last0_undup; [rewrite -COST__job | apply SORT__job].
     rewrite last_seq_minus_last_distance_seq; last by apply nondecreasing_sequence_undup, SORT__job. 
-    apply leq_trans with( nth 0 (job_preemption_points j) ((size (job_preemption_points j)).-2)); first by apply undup_nth_le; eauto 2.
+    apply leq_trans with( nth 0 (job_preemptive_points j) ((size (job_preemptive_points j)).-2)); first by apply undup_nth_le; eauto 2.
     have -> : task_cost tsk = last0 (task_preemption_points tsk) by rewrite COST__task. 
     rewrite last_seq_minus_last_distance_seq; last by apply SORT__task.
     move: TSK__j => /eqP TSK__j; rewrite -TSK__j.
diff --git a/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
index 4b3b8d282..4849be03f 100644
--- a/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -1,6 +1,6 @@
-Require Export prosa.analysis.facts.preemption.job.limited.
-Require Export prosa.model.task.preemption.floating_nonpreemptive.
 Require Export prosa.model.preemption.limited_preemptive.
+Require Export prosa.model.task.preemption.floating_nonpreemptive.
+Require Export prosa.analysis.facts.preemption.job.limited.
 
 (** * Platform for Floating Non-Preemptive Regions Model *)
 
@@ -59,18 +59,18 @@ Section FloatingNonPreemptiveRegionsModel.
     case: (posnP (job_cost j)) => [ZERO|POS].
     - split.
       rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
-              /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
+              /lengths_of_segments /job_preemption_points; rewrite ZERO; simpl.
       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).
+    - split; last (move => progr /andP [_ LE]; destruct (progr \in job_preemptive_points j) eqn:NotIN).
       + by apply MAX.
       + 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.
+        set ptl := nth 0 (job_preemptive_points j) x.
+        set ptr := nth 0 (job_preemptive_points j) x.+1.
         exists ptr; split; first last.
         * by unfold job_preemptable, limited_preemptive_job_model; apply mem_nth.
         * apply/andP; split; first by apply ltnW.
diff --git a/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
index bb8745643..07ba4d876 100644
--- a/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ -58,20 +58,20 @@ Section LimitedPreemptionsModel.
     case: (posnP (job_cost j)) => [ZERO|POS].
     - split.
       rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
-              /lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
+              /lengths_of_segments /job_preemption_points; rewrite ZERO; simpl.
       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).
+    - split; last (move => progr /andP [_ LE]; destruct (progr \in job_preemptive_points j) eqn:NotIN).
       + rewrite /job_respects_max_nonpreemptive_segment
                 /job_max_nonpreemptive_segment /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
           by apply max_of_dominating_seq; intros; apply A5.
       + exists progr; split; first apply/andP; first split; rewrite ?leq_addr; by done. 
       + 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.
+        set ptl := nth 0 (job_preemptive_points j) x.
+        set ptr := nth 0 (job_preemptive_points j) x.+1.
         exists ptr; split; first last.
         * by unfold job_preemptable, limited_preemptive_job_model; apply mem_nth.
         * apply/andP; split; first by apply ltnW.
diff --git a/model/preemption/limited_preemptive.v b/model/preemption/limited_preemptive.v
index 32e058b71..80976de6d 100644
--- a/model/preemption/limited_preemptive.v
+++ b/model/preemption/limited_preemptive.v
@@ -5,18 +5,22 @@ Require Export prosa.model.preemption.parameter.
 (** Under the limited-preemptive preemption model, jobs can be preempted only
     at a precise set of points during their execution. To allow such fixed,
     progress-dependent preemption points to be specified, we introduce a new
-    job parameter [job_preemption_points] that, for each job, yields the set of
-    progress values at which the job can be preempted by the scheduler. *)
+    job parameter [job_preemptive_points] that, for each job, yields the set of
+    progress values at which the job can be preempted by the scheduler.
+
+    NB: the job parameter is called [job_preemptive_points], rather than
+    [job_preemption_points], to avoid a name clash with the definition of the
+    same name. *)
 Class JobPreemptionPoints (Job : JobType) :=
   {
-    job_preemption_points : Job -> seq work
+    job_preemptive_points : Job -> seq work
   }.
 
 (** * Preemption Model: Limited-Preemptive Jobs *)
 
-(** Based on the above definition of [job_preemption_points], in the following
+(** Based on the above definition of [job_preemptive_points], in the following
     we instantiate [job_preemptable] for limited-preemptive jobs and introduce
-    requirements that the function [job_preemption_points] should satisfy to be
+    requirements that the function [job_preemptive_points] should satisfy to be
     coherent with the limited-preemptive preemption model. *)
 Section LimitedPreemptions.
 
@@ -26,14 +30,14 @@ Section LimitedPreemptions.
   Context `{JobCost Job}.
 
   (** Given each job's preemption points, as determined by
-      [job_preemption_points], ...*)
+      [job_preemptive_points], ...*)
   Context `{JobPreemptionPoints Job}.
 
   (** ...a job [j] is preemptable at a given point of progress [ρ] iff [ρ] is
       one of the preemption points of [j]. *)
   #[local] Instance limited_preemptive_job_model : JobPreemptable Job :=
   {
-    job_preemptable (j : Job) (ρ : work) := ρ \in job_preemption_points j
+    job_preemptable (j : Job) (ρ : work) := ρ \in job_preemptive_points j
   }.
 
   (** ** Model Validity *)
@@ -47,17 +51,17 @@ Section LimitedPreemptions.
 
     (** We require the sequence of preemption points to contain the beginning ... *)
     Definition beginning_of_execution_in_preemption_points :=
-      forall j, arrives_in arr_seq j -> 0 \in job_preemption_points j.
+      forall j, arrives_in arr_seq j -> 0 \in job_preemptive_points j.
 
     (** ... and the end of execution for any job [j] that arrives in the given
         arrival sequence [arr_seq]. *)
     Definition end_of_execution_in_preemption_points :=
-      forall j, arrives_in arr_seq j -> last0 (job_preemption_points j) = job_cost j.
+      forall j, arrives_in arr_seq j -> last0 (job_preemptive_points j) = job_cost j.
 
     (** We further require the sequence of preemption points to be a
         non-decreasing sequence. *)
     Definition preemption_points_is_nondecreasing_sequence :=
-      forall j, arrives_in arr_seq j -> nondecreasing_sequence (job_preemption_points j).
+      forall j, arrives_in arr_seq j -> nondecreasing_sequence (job_preemptive_points j).
 
     (** A job model is considered valid w.r.t. limited-preemptive preemption
         model if it satisfies each of the preceding definitions. *)
diff --git a/model/task/preemption/limited_preemptive.v b/model/task/preemption/limited_preemptive.v
index a6248232b..42d7393ef 100644
--- a/model/task/preemption/limited_preemptive.v
+++ b/model/task/preemption/limited_preemptive.v
@@ -56,14 +56,14 @@ Section ValidModelWithFixedPreemptionPoints.
   Definition consistent_job_segment_count :=
     forall j,
       arrives_in arr_seq j ->
-      size (job_preemption_points j) = size (task_preemption_points (job_task j)).
+      size (job_preemptive_points j) = size (task_preemption_points (job_task j)).
 
   (** (5) We require the lengths of the nonpreemptive segments of a job to be
           bounded by the lengths of the corresponding segments of its task.  *)
   Definition job_respects_segment_lengths :=
     forall j n,
       arrives_in arr_seq j ->
-      nth 0 (distances (job_preemption_points j)) n
+      nth 0 (distances (job_preemptive_points j)) n
       <= nth 0 (distances (task_preemption_points (job_task j))) n.
 
   (** (6) Lastly, we ban empty nonpreemptive segments at the task level. *)
-- 
GitLab