relax assumption in aRTA

Currently, aRTA required [F] to be solution of equation
[A + F = task_rtct + IBF A (A + F)], this commit relaxes
this assumption to [A + F >= task_rtct + IBF A (A + F)]

analysis/abstract/abstract_rta.v

@@ -97,17 +97,18 @@ Section Abstract_RTA.
   (** For simplicity, let's define a local name for the search space. *)
   Let is_in_search_space A := is_in_search_space tsk L interference_bound_function A.
 
-  (** Consider any value [R] that upper-bounds the solution of each response-time recurrence, 
-     i.e., for any relative arrival time A in the search space, there exists a corresponding 
-     solution [F] such that [F + (task_cost tsk - task_rtct tsk) <= R]. *)
+  (** Consider any value [R] that upper-bounds the solution of each
+      response-time recurrence, i.e., for any relative arrival time [A]
+      in the search space, there exists a corresponding solution [F]
+      such that [R >= F + (task_cost tsk - task_rtct tsk)]. *)
   Variable R: nat.
   Hypothesis H_R_is_maximum:
     forall A,
       is_in_search_space A -> 
       exists F,
-        A + F = task_rtct tsk
+        A + F >= task_rtct tsk
                 + interference_bound_function tsk A (A + F) /\
-        F + (task_cost tsk - task_rtct tsk) <= R.
+        R >= F + (task_cost tsk - task_rtct tsk).
 
   (** In this section we show a detailed proof of the main theorem 
      that establishes that R is a response-time bound of task [tsk]. *) 
@@ -152,10 +153,10 @@ Section Abstract_RTA.
    
     (** (d) [A_sp + F_sp] is a solution of the response time recurrence... *)
     Hypothesis H_Asp_Fsp_fixpoint :
-      A_sp + F_sp = task_rtct tsk + interference_bound_function tsk A_sp (A_sp + F_sp).
+      A_sp + F_sp >= task_rtct tsk + interference_bound_function tsk A_sp (A_sp + F_sp).
 
     (** (e) and finally, [F_sp + (task_last - ε)] is no greater than R. *)
-    Hypothesis H_R_gt_Fsp : F_sp + (task_cost tsk - task_rtct tsk) <= R.
+    Hypothesis H_R_gt_Fsp : R >= F_sp + (task_cost tsk - task_rtct tsk).
 
     (** In this section, we consider the case where the solution is so large 
        that the value of [t1 + A_sp + F_sp] goes beyond the busy interval. 
@@ -225,7 +226,7 @@ Section Abstract_RTA.
           Hypothesis H_F_le_Fsp : F <= F_sp.
           (** (c) and [A + F] is a solution for the response-time recurrence for [A]. *)
           Hypothesis H_A_F_fixpoint:
-            A + F = task_rtct tsk + interference_bound_function tsk A (A + F).
+            A + F >= task_rtct tsk + interference_bound_function tsk A (A + F).
  
           (** Next, we assume that job [j] is not completed by time [job_arrival j + R]. *)
           Hypothesis H_j_not_completed : ~~ completed_by sched j (job_arrival j + R).
@@ -276,7 +277,7 @@ Section Abstract_RTA.
             specialize (ESERV H3 H4).
             feed_n 2 ESERV.
             { eapply job_run_to_completion_threshold_le_job_cost; eauto. }
-            { rewrite {2}H_A_F_fixpoint.
+            { rewrite -{2}(leqRW H_A_F_fixpoint).
               rewrite /definitions.cumul_interference.
               rewrite -[in X in _ <= X]addnBAC; last by rewrite leq_subr.
               rewrite {2}/optimism.
@@ -504,7 +505,7 @@ Section Abstract_RTA.
           feed_n 7 ESERV; eauto 2.
           specialize (ESERV H3 H4).
           feed_n 2 ESERV; eauto using job_run_to_completion_threshold_le_job_cost.
-            by rewrite {2}H_Asp_Fsp_fixpoint leq_add //; apply H_valid_run_to_completion_threshold.
+          by rewrite -{2}(leqRW H_Asp_Fsp_fixpoint) leq_add //; apply H_valid_run_to_completion_threshold.
         Qed.
 
         (** However, this is a contradiction. Since job [j] has not yet arrived, its service 

analysis/abstract/abstract_seq_rta.v

@@ -204,9 +204,9 @@ Section Sequential_Abstract_RTA.
       forall (A : duration),
         is_in_search_space_seq A ->
         exists (F : duration),
-          A + F = (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
+          A + F >= (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                   + task_interference_bound_function tsk A (A + F) /\
-          F + (task_cost tsk - task_rtct tsk) <= R.
+          R >= F + (task_cost tsk - task_rtct tsk).
 
     (** In this section we prove a few simple lemmas about the completion of jobs from the task
        considering the busy interval of the job under consideration. *)
@@ -648,18 +648,17 @@ Section Sequential_Abstract_RTA.
         forall (A : duration),
           is_in_search_space A ->
           exists (F : duration),
-            A + F = task_rtct tsk +
+            A + F >= task_rtct tsk +
                     (task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A (A + F)) /\
-            F + (task_cost tsk - task_rtct tsk) <= R.
+            R >= F + (task_cost tsk - task_rtct tsk).
       Proof.
         move: H_valid_run_to_completion_threshold => [PRT1 PRT2].
         intros A INSP.
         clear H_sequential_tasks H_interference_and_workload_consistent_with_sequential_tasks.
         move: (H_R_is_maximum_seq _ INSP) => [F [FIX LE]].
         exists F; split; last by done.
-        rewrite {1}FIX.
-        apply/eqP.
-        rewrite addnA eqn_add2r.
+        rewrite -{2}(leqRW FIX).
+        rewrite addnA leq_add2r.
         rewrite addnBA; last first.
         { apply leq_trans with (task_rbf 1).
           eapply task_rbf_1_ge_task_cost; eauto 2.

analysis/abstract/search_space.v

@@ -132,7 +132,7 @@ Section AbstractRTAReduction.
     (** Suppose [A_sp + F_sp] is a "small" solution (i.e. less than [B]) of the response-time recurrence. *)
     Variables A_sp F_sp : duration.
     Hypothesis H_less_than : A_sp + F_sp < B.
-    Hypothesis H_fixpoint : A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).
+    Hypothesis H_fixpoint : A_sp + F_sp >= interference_bound_function tsk A_sp (A_sp + F_sp).
 
     (** Next, let [A] be any point such that: (a) [A_sp <= A <= A_sp + F_sp] and 
        (b) [interference_bound_function(A, x)] is equal to 
@@ -150,7 +150,7 @@ Section AbstractRTAReduction.
       exists F,
         A_sp + F_sp = A + F /\
         F <= F_sp /\
-        A + F = interference_bound_function tsk A (A + F).
+        A + F >= interference_bound_function tsk A (A + F).
     Proof.  
       move: H_bounds_for_A => /andP [NEQ1 NEQ2].
       set (X := A_sp + F_sp) in *.
@@ -162,4 +162,4 @@ Section AbstractRTAReduction.
 
   End FixpointSolutionForAnotherA.
   
-End AbstractRTAReduction. 
\ No newline at end of file
+End AbstractRTAReduction. 

results/edf/rta/bounded_nps.v

@@ -259,10 +259,10 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
       forall (A : duration),
         is_in_search_space L A -> 
         exists (F : duration),
-          A + F = blocking_bound
+          A + F >= blocking_bound
                   + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                   + bound_on_total_hep_workload  A (A + F) /\
-          F + (task_cost tsk - task_rtct tsk) <= R.
+          R >= F + (task_cost tsk - task_rtct tsk).
 
     (** Then, using the results for the general RTA for EDF-schedulers, we establish a 
          response-time bound for the more concrete model of bounded nonpreemptive segments.

results/edf/rta/bounded_pi.v

@@ -171,18 +171,19 @@ Section AbstractRTAforEDFwithArrivalCurves.
   Definition is_in_search_space (A : duration) :=
     (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
   
-  (** Let R be a value that upper-bounds the solution of each response-time recurrence, 
-     i.e., for any relative arrival time A in the search space, there exists a corresponding 
-     solution F such that [F + (task cost - task lock-in service) <= R]. *)
+  (** Let [R] be a value that upper-bounds the solution of each
+      response-time recurrence, i.e., for any relative arrival time [A]
+      in the search space, there exists a corresponding solution [F]
+      such that [R >= F + (task cost - task lock-in service)]. *)
   Variable R : duration.
   Hypothesis H_R_is_maximum: 
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F = priority_inversion_bound
+        A + F >= priority_inversion_bound
                 + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                 + bound_on_total_hep_workload  A (A + F) /\
-        F + (task_cost tsk - task_rtct tsk) <= R.
+        R >= F + (task_cost tsk - task_rtct tsk).
   
   (** To use the theorem uniprocessor_response_time_bound_seq from the Abstract RTA module, 
      we need to specify functions of interference, interfering workload and IBF.  *)
@@ -657,14 +658,14 @@ Section AbstractRTAforEDFwithArrivalCurves.
       (** Then, there exists solution for response-time recurrence (in the abstract sense). *)
       Corollary correct_search_space:
         exists F,
-          A + F = task_rbf (A + ε) - (task_cost tsk - task_rtct tsk) + IBF A (A + F) /\
-          F + (task_cost tsk - task_rtct tsk) <= R.
+          A + F >= task_rbf (A + ε) - (task_cost tsk - task_rtct tsk) + IBF A (A + F) /\
+          R >= F + (task_cost tsk - task_rtct tsk).
       Proof.
         edestruct H_R_is_maximum as [F [FIX NEQ]].
         - by apply A_is_in_concrete_search_space.
         - exists F; split; last by done.
-          apply/eqP; rewrite {1}FIX.
-            by rewrite addnA [_ + priority_inversion_bound]addnC -!addnA.
+          rewrite -{2}(leqRW FIX).
+          by rewrite addnA [_ + priority_inversion_bound]addnC -!addnA.
       Qed.
          
       End SolutionOfResponseTimeReccurenceExists.       
@@ -688,7 +689,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
     - by apply instantiated_interference_and_workload_consistent_with_sequential_tasks.
     - by apply instantiated_busy_intervals_are_bounded.
     - by apply instantiated_task_interference_is_bounded.
-    - eapply correct_search_space; eauto 2. by apply/eqP.
+    - by eapply correct_search_space; eauto 2; apply/eqP.
   Qed.
   
 End AbstractRTAforEDFwithArrivalCurves. 

results/edf/rta/floating_nonpreemptive.v

@@ -118,15 +118,16 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
   Let is_in_search_space := is_in_search_space ts tsk L.
   
-  (** Consider any value R, and assume that for any given arrival offset A in the search space,
-      there is a solution of the response-time bound recurrence which is bounded by R. *)
+  (** Consider any value [R], and assume that for any given arrival
+      offset [A] in the search space, there is a solution of the
+      response-time bound recurrence which is bounded by [R]. *)
   Variable R : duration.
   Hypothesis H_R_is_maximum:
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F = blocking_bound + task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
-        F <= R.
+        A + F >= blocking_bound + task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
+        R >= F.
 
   (** Now, we can leverage the results for the abstract model with
       bounded nonpreemptive segments to establish a response-time

results/edf/rta/fully_nonpreemptive.v

@@ -108,16 +108,17 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
   Let is_in_search_space := is_in_search_space ts tsk L.
   
-  (** Consider any value R, and assume that for any given arrival offset A in the search space,
-      there is a solution of the response-time bound recurrence which is bounded by R. *)
+  (** Consider any value [R], and assume that for any given arrival
+      offset [A] in the search space, there is a solution of the
+      response-time bound recurrence which is bounded by [R]. *)
   Variable R: nat.
   Hypothesis H_R_is_maximum:
     forall A,
       is_in_search_space A -> 
       exists F,
-        A + F = blocking_bound + (task_rbf (A + ε) - (task_cost tsk - ε))
+        A + F >= blocking_bound + (task_rbf (A + ε) - (task_cost tsk - ε))
                 + bound_on_total_hep_workload A (A + F) /\
-        F + (task_cost tsk - ε) <= R.
+        R >= F + (task_cost tsk - ε).
 
   (** Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
      to establish a response-time bound for the more concrete model of fully nonpreemptive scheduling. *)

results/edf/rta/fully_preemptive.v

@@ -103,15 +103,16 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)      
   Let is_in_search_space := is_in_search_space ts tsk L.
   
-  (** Consider any value R, and assume that for any given arrival offset A in the search space,
-      there is a solution of the response-time bound recurrence which is bounded by R. *)
+  (** Consider any value [R], and assume that for any given arrival
+      offset [A] in the search space, there is a solution of the
+      response-time bound recurrence which is bounded by [R]. *)
   Variable R : duration.
   Hypothesis H_R_is_maximum:
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F = task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
-        F <= R.
+        A + F >= task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
+        R >= F.
 
   (** Now, we can leverage the results for the abstract model with
       bounded non-preemptive segments to establish a response-time

results/edf/rta/limited_preemptive.v

@@ -119,17 +119,18 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
   Let is_in_search_space := is_in_search_space ts tsk L.
   
-  (** Consider any value R, and assume that for any given arrival offset A in the search space,
-     there is a solution of the response-time bound recurrence which is bounded by R. *)
+  (** Consider any value [R], and assume that for any given arrival
+      offset [A] in the search space, there is a solution of the
+      response-time bound recurrence which is bounded by [R]. *)
   Variable R : duration.
   Hypothesis H_R_is_maximum:
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F = blocking_bound
+        A + F >= blocking_bound
                 + (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) 
                 + bound_on_total_hep_workload A (A + F) /\
-        F + (task_last_nonpr_segment tsk - ε) <= R.
+        R >= F + (task_last_nonpr_segment tsk - ε).
   
   (** Now, we can leverage the results for the abstract model with bounded non-preemptive segments
       to establish a response-time bound for the more concrete model of fixed preemption points.  *)

results/fixed_priority/rta/bounded_nps.v

@@ -227,7 +227,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
       forall (A : duration), 
         is_in_search_space A -> 
         exists (F : duration),
-          A + F = blocking_bound
+          A + F >= blocking_bound
                   + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                   + total_ohep_rbf (A + F) /\
           F + (task_cost tsk - task_rtct tsk) <= R.

results/fixed_priority/rta/bounded_pi.v

@@ -145,18 +145,18 @@ Section AbstractRTAforFPwithArrivalCurves.
      analysis might have with regard to the beginning of its busy-window. *)
   Definition is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
 
-  (** Let R be a value that upper-bounds the solution of each response-time recurrence, 
+  (** Let [R] be a value that upper-bounds the solution of each response-time recurrence, 
      i.e., for any relative arrival time A in the search space, there exists a corresponding 
-     solution F such that [F + (task cost - task lock-in service) <= R]. *)
+     solution [F] such that [R >= F + (task cost - task lock-in service)]. *)
   Variable R : duration.
   Hypothesis H_R_is_maximum : 
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F = priority_inversion_bound
+        A + F >= priority_inversion_bound
                 + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                 + total_ohep_rbf (A + F) /\
-        F + (task_cost tsk - task_rtct tsk) <= R.
+        R >= F + (task_cost tsk - task_rtct tsk).
 
   (** Instantiation of Interference *)
   (** We say that job j incurs interference at time t iff it cannot execute due to 
@@ -342,14 +342,14 @@ Section AbstractRTAforFPwithArrivalCurves.
       (** Then, there exists a solution for the response-time recurrence (in the abstract sense). *)
       Corollary correct_search_space:
         exists (F : duration),
-          A + F = task_rbf (A + ε) - (task_cost tsk - task_rtct tsk) + IBF (A + F) /\
-          F + (task_cost tsk - task_rtct tsk) <= R.
+          A + F >= task_rbf (A + ε) - (task_cost tsk - task_rtct tsk) + IBF (A + F) /\
+          R >= F + (task_cost tsk - task_rtct tsk).
       Proof.
         move: (H_R_is_maximum A) => FIX.
         feed FIX; first by apply A_is_in_concrete_search_space. 
         move: FIX => [F [FIX NEQ]].
         exists F; split; last by done.
-        apply/eqP; rewrite {1}FIX.
+        rewrite -{2}(leqRW FIX).
           by rewrite addnA [_ + priority_inversion_bound]addnC -!addnA.
       Qed.
 

results/fixed_priority/rta/floating_nonpreemptive.v

@@ -132,8 +132,8 @@ Section RTAforFloatingModelwithArrivalCurves.
     forall (A : duration),
       is_in_search_space A ->
       exists  (F : duration),
-        A + F = blocking_bound + task_rbf (A + ε) + total_ohep_rbf (A + F) /\
-        F <= R.
+        A + F >= blocking_bound + task_rbf (A + ε) + total_ohep_rbf (A + F) /\
+        R >= F.
   
   (** Now, we can reuse the results for the abstract model with
       bounded nonpreemptive segments to establish a response-time

results/fixed_priority/rta/fully_nonpreemptive.v

@@ -116,17 +116,18 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
   Let is_in_search_space := is_in_search_space tsk L.
 
-  (** Next, consider any value R, and assume that for any given arrival A from search space
-      there is a solution of the response-time bound recurrence which is bounded by R. *)
+  (** Next, consider any value [R], and assume that for any given
+      arrival [A] from search space there is a solution of the
+      response-time bound recurrence which is bounded by [R]. *)
   Variable R : duration.
   Hypothesis H_R_is_maximum:
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F = blocking_bound
+        A + F >= blocking_bound
                 + (task_rbf (A + ε) - (task_cost tsk - ε))
                 + total_ohep_rbf (A + F) /\
-        F + (task_cost tsk - ε) <= R.
+        R >= F + (task_cost tsk - ε).
   
   (** Now, we can leverage the results for the abstract model with
       bounded nonpreemptive segments to establish a response-time

results/fixed_priority/rta/fully_preemptive.v

@@ -111,16 +111,16 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
   Let is_in_search_space := is_in_search_space tsk L.
   
-  (** Next, consider any value R, and assume that for any given
-       arrival A from search space there is a solution of the
-       response-time bound recurrence which is bounded by R. *)
+  (** Next, consider any value [R], and assume that for any given
+       arrival [A] from search space there is a solution of the
+       response-time bound recurrence which is bounded by [R]. *)
   Variable R : duration.
   Hypothesis H_R_is_maximum:
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F = task_rbf (A + ε) + total_ohep_rbf (A + F) /\
-        F <= R.
+        A + F >= task_rbf (A + ε) + total_ohep_rbf (A + F) /\
+        R >= F.
 
   (** Now, we can leverage the results for the abstract model with
       bounded non-preemptive segments to establish a response-time

results/fixed_priority/rta/limited_preemptive.v

@@ -124,17 +124,18 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
   Let is_in_search_space := is_in_search_space tsk L.
   
-  (** Next, consider any value R, and assume that for any given arrival A from search space
-      there is a solution of the response-time bound recurrence which is bounded by R. *)    
+  (** Next, consider any value [R], and assume that for any given
+      arrival [A] from search space there is a solution of the
+      response-time bound recurrence which is bounded by [R]. *)    
   Variable R: nat.
   Hypothesis H_R_is_maximum:
     forall (A : duration),
       is_in_search_space A ->
       exists (F : duration),
-        A + F = blocking_bound
+        A + F >= blocking_bound
                 + (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε))
                 + total_ohep_rbf (A + F) /\
-        F + (task_last_nonpr_segment tsk - ε) <= R.
+        R >= F + (task_last_nonpr_segment tsk - ε).
         
   (** Now, we can reuse the results for the abstract model with
       bounded non-preemptive segments to establish a response-time