Port instantiations

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited_preemptions.v

@@ -14,7 +14,7 @@ From rt.restructuring Require Import analysis.arrival.rbf.
 From rt.restructuring Require Import analysis.fixed_priority.rta.response_time_bound.
 From rt.restructuring Require Import analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
 
-From rt.restructuring.model.preemption Require Import preemption_model job_preemptable.limited rtct.limited.
+From rt.restructuring.model.preemption Require Import job_preemptable.util preemption_model job_preemptable.limited rtct.limited.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
@@ -158,25 +158,20 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
         A + F = blocking_bound
                 + (task_rbf (A + ε) - (task_last_nps tsk - ε))
                 + total_ohep_rbf (A + F) /\
-        F + (task_last_nps tsk - ε) <= R.      
-
-  (* Now, we can reuse the results for the abstract model with bounded nonpreemptive segments
-     to establish a response-time bound for the more concrete model of fixed preemption points. *)
-  Theorem uniprocessor_response_time_bound_fp_with_fixed_preemption_points:
-    response_time_bounded_by tsk R.  
-  Proof. 
+        F + (task_last_nps tsk - ε) <= R.
+
+  (* TODO: name *)
+  (* TODO: comment*)
+  (* TODO: move *)
+  Lemma Fact2:
+    task_cost tsk > 0 ->
+    1 < size (task_preemption_points tsk).
+  Proof.
+    intros POSt.
     move: (H_model_with_fixed_preemption_points) => [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
     move: (MLP) => [EMPTj [LSMj [BEGj [ENDj HH]]]].
-    move: (posnP (@task_cost _ H tsk)) => [ZERO|POSt].
-    { intros j ARR TSK.
-      move: (H_job_cost_le_task_cost _ ARR) => POSt.
-      move: POSt; rewrite /job_cost_le_task_cost TSK ZERO leqn0; move => /eqP Z.
-        by rewrite /job_response_time_bound /completed_by Z.
-    } 
-
-    have Fact2: 1 < size (task_preemption_points tsk).
-    { have Fact2: 0 < size (task_preemption_points tsk).
-      { apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
+    have Fact2: 0 < size (task_preemption_points tsk).
+    { apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
         move: (END _ H_tsk_in_ts) => EQ.
         move: EQ; rewrite /util.last0 -nth_last nth_default; last by rewrite CONTR.
           by intros; rewrite -EQ in POSt.
@@ -206,34 +201,38 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
         exists ((size (task_preemption_points tsk)).-1); last by done. 
           by rewrite -(leq_add2r 1) !addn1 prednK //.
       }
-    }
+  Qed.
+
+  (* Now, we can reuse the results for the abstract model with bounded nonpreemptive segments
+     to establish a response-time bound for the more concrete model of fixed preemption points. *)
+  Theorem uniprocessor_response_time_bound_fp_with_fixed_preemption_points:
+    response_time_bounded_by tsk R.  
+  Proof.
+    move: (H_model_with_fixed_preemption_points) => [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
+    move: (MLP) => [EMPTj [LSMj [BEGj [ENDj HH]]]].
+    move: (posnP (@task_cost _ H tsk)) => [ZERO|POSt].
+    { intros j ARR TSK.
+      move: (H_job_cost_le_task_cost _ ARR) => POSt.
+      move: POSt; rewrite /job_cost_le_task_cost TSK ZERO leqn0; move => /eqP Z.
+        by rewrite /job_response_time_bound /completed_by Z.
+    } 
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
         (L0 := L).
     all: eauto 3.
-
-    intros ? HHh.
-
-    apply H_R_is_maximum in HHh.
-
-    destruct HHh as [FF [EQ1 EQ2]].
-
-    exists FF. rewrite subKn; first by done. 
-    
+    intros A SP.
+    destruct (H_R_is_maximum _ SP) as[FF [EQ1 EQ2]].
+    exists FF; rewrite subKn; first by done. 
     rewrite /task_last_nps  -(leq_add2r 1) subn1 !addn1 prednK; last first.
-    { rewrite /util.last0 -nth_last.
+    - rewrite /util.last0 -nth_last.
       apply HYP3; try by done. 
       rewrite -(ltn_add2r 1) !addn1 prednK //.
-      move: (Fact2) => Fact3.
-      (* by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2. *)
-      admit.
-    }        
-    { apply leq_trans with (task_max_nonpreemptive_segment tsk).
-      - admit. (* by apply last_of_seq_le_max_of_seq.  *)
-      - rewrite -END; last by done.
+      move: (Fact2 POSt) (Fact2 POSt) => Fact2 Fact3.
+        by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2. 
+    - apply leq_trans with (task_max_nonpreemptive_segment tsk).
+      + by apply last_of_seq_le_max_of_seq.
+      + rewrite -END; last by done.
         apply ltnW; rewrite ltnS; try done.
-        (* by apply max_distance_in_seq_le_last_element_of_seq; eauto 2. *)
-        admit.
-    }
-  Admitted.
+          by apply max_distance_in_seq_le_last_element_of_seq; eauto 2. 
+  Qed.
     
 End RTAforFixedPreemptionPointsModelwithArrivalCurves.