improve the bound on arrival blocking under EDF

Modify the EDF blocking bound so that the arrival offset of the
job under analysis is taken into account when considering from
which task a lower-priority job that is causing arrival-blocking
may stem.

With contributions by Kimaya Bedarkar, Sergey Bozhko,
and Björn Brandenburg.

analysis/definitions/priority_inversion.v

@@ -45,19 +45,31 @@ Section CumulativePriorityInversion.
       if sched t is Some jlp then
         ~~ hep_job jlp j
       else false.
-    
+
     (** Then we compute the cumulative priority inversion incurred by
          a job within some time interval <<[t1, t2)>>. *)
     Definition cumulative_priority_inversion (t1 t2 : instant) :=
       \sum_(t1 <= t < t2) is_priority_inversion t.
 
-    (** We say that priority inversion of job [j] is bounded by a constant [B] iff cumulative 
-         priority inversion within any busy interval prefix is bounded by [B]. *)
-    Definition priority_inversion_of_job_is_bounded_by (B : duration) :=
+    (** We say that the priority inversion experienced by a job [j] is bounded
+        by a constant [B] if the cumulative priority inversion within any busy
+        interval prefix is bounded by [B]. *)
+    Definition priority_inversion_of_job_is_bounded_by_constant (B : duration) :=
       forall (t1 t2 : instant),
         busy_interval_prefix arr_seq sched j t1 t2 ->
         cumulative_priority_inversion t1 t2 <= B.
 
+    (** More generally, if the priority inversion experienced by a job [j]
+        depends on its relative arrival time w.r.t. the beginning of its busy
+        interval at a time [t1], we say that the priority inversion of job [j]
+        is bounded by a function [B : duration -> duration] if the cumulative
+        priority inversion within any busy interval prefix is bounded by [B
+        (job_arrival j - t1)] *)
+    Definition priority_inversion_of_job_is_bounded_by (B : duration -> duration) :=
+      forall (t1 t2 : instant),
+        busy_interval_prefix arr_seq sched j t1 t2 ->
+        cumulative_priority_inversion t1 t2 <= B (job_arrival j - t1).
+
   End JobPriorityInversionBound.
 
   (** In this section, we define a notion of the bounded priority inversion for task. *)
@@ -66,13 +78,24 @@ Section CumulativePriorityInversion.
     (** Consider an arbitrary task [tsk]. *)
     Variable tsk : Task.
 
-    (** We say that task [tsk] has bounded priority inversion if all 
-         its jobs have bounded cumulative priority inversion. *)
-    Definition priority_inversion_is_bounded_by (B : duration) :=
+    (** We say that priority inversion of task [tsk] is bounded by a constant
+        [B] if all jobs released by the task have cumulative priority inversion
+        bounded by [B] *)
+    Definition priority_inversion_is_bounded_by_constant (B : duration) :=
+      forall (j : Job),
+        arrives_in arr_seq j ->
+        job_of_task tsk j ->
+        job_cost j > 0 ->
+        priority_inversion_of_job_is_bounded_by_constant j B.
+
+    (** We say that task [tsk] has bounded priority inversion if all its jobs
+        have bounded cumulative priority inversion that depends on its relative
+        arrival time w.r.t.  the beginning of the busy interval. *)
+    Definition priority_inversion_is_bounded_by (B : duration -> duration) :=
       forall (j : Job),
         arrives_in arr_seq j ->
         job_of_task tsk j ->
-        job_cost j > 0 -> 
+        job_cost j > 0 ->
         priority_inversion_of_job_is_bounded_by j B.
 
   End TaskPriorityInversionBound.

analysis/facts/busy_interval/busy_interval.v

@@ -62,7 +62,7 @@ Section ExistsBusyIntervalJLFP.
   Let quiet_time_dec t1 := quiet_time_dec arr_seq sched j t1.
   Let busy_interval_prefix t1 t2 := busy_interval_prefix arr_seq sched j t1 t2.
   Let busy_interval t1 t2 := busy_interval arr_seq sched j t1 t2.
-  Let is_priority_inversion_bounded_by K := priority_inversion_of_job_is_bounded_by arr_seq sched j K.
+  Let is_priority_inversion_bounded_by K := priority_inversion_of_job_is_bounded_by_constant arr_seq sched j K.
   
   (** We begin by proving a basic lemma about busy intervals. *)
   Section BasicLemma.

analysis/facts/busy_interval/priority_inversion.v

@@ -77,10 +77,7 @@ Section PriorityInversionIsBounded.
   (** Finally, we introduce the notion of the maximal length of
        (potential) priority inversion at a time instant [t], which is
        defined as the maximum length of nonpreemptive segments among
-       all jobs that arrived so far. Note that the value
-       [job_max_nonpreemptive_segment j_lp] is at least [ε] for any job
-       [j_lp], so the maximal length of priority inversion cannot be
-       negative. *)
+       all jobs that arrived so far. *)
   Definition max_length_of_priority_inversion (j : Job) (t : instant) :=
     \max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j)
      (job_max_nonpreemptive_segment j_lp - ε).

classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v

@@ -69,10 +69,8 @@ Module PriorityInversionIsBounded.
     Let job_completed_by := completed_by job_cost sched.
 
     (* Finally, we introduce the notion of the maximal length of (potential) priority 
-       inversion at a time instant t, which is defined as the maximum length of 
-       nonpreemptive segments among all jobs that arrived so far. Note that 
-       the value [job_max_nps j_lp] is at least ε for any job j_lp, so the maximal
-       length of priority inversion cannot be negative. *)
+       inversion at a time instant [t], which is defined as the maximum length of 
+       nonpreemptive segments among all jobs that arrived so far. *)
     Definition max_length_of_priority_inversion (j: Job) (t: time) :=
       \max_(j_lp <- jobs_arrived_before arr_seq t | ~~ higher_eq_priority j_lp j)
        (job_max_nps j_lp - ε).

results/edf/rta/bounded_nps.v

@@ -130,12 +130,13 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     bound_on_total_hep_workload_changes_at ts tsk.
   Let response_time_bounded_by := task_response_time_bound arr_seq sched.
   Let is_in_search_space := is_in_search_space ts tsk.
-                         
-  (** We also define a bound for the priority inversion caused by jobs with lower priority. *)
-  Definition blocking_bound :=
-    \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
-     (task_max_nonpreemptive_segment tsk_o - ε).
-  
+
+  (** For a job with the relative arrival offset [A] within its busy window, we define
+      the following blocking bound. *)
+   Definition blocking_bound (A : duration)  :=
+     \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk_o > D tsk + A))
+       (task_max_nonpreemptive_segment tsk_o - ε).
+
   (** ** Priority inversion is bounded *)
   (** In this section, we prove that a priority inversion for task [tsk] is bounded by 
       the maximum length of non-preemptive segments among the tasks with lower priority. *)
@@ -146,15 +147,16 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         non-preemptive section of a task with lower-priority task
         (i.e., the blocking term). *)
     Lemma priority_inversion_is_bounded_by_blocking:
-      forall j t,
+      forall j t1 t2,
         arrives_in arr_seq j ->
         job_of_task tsk j ->
-        t <= job_arrival j ->
-        max_length_of_priority_inversion j t <= blocking_bound.
+        busy_interval_prefix  arr_seq sched j t1 t2 ->
+        max_length_of_priority_inversion j t1 <= blocking_bound (job_arrival j - t1).
     Proof.
-      intros j t ARR TSK LE; unfold max_length_of_priority_inversion, blocking_bound. 
+      intros j t1 t2 ARR TSK BUSY; unfold max_length_of_priority_inversion, blocking_bound.
+      destruct BUSY as [TT [QT [_ LE]]]; move: LE => /andP [GE LT].
       apply leq_trans with
-          (\max_(j_lp <- arrivals_between arr_seq 0 t | ~~ EDF j_lp j)
+          (\max_(j_lp <- arrivals_between arr_seq 0 t1 | ~~ EDF j_lp j)
             (task_max_nonpreemptive_segment (job_task j_lp) - ε)).
       - apply leq_big_max.
         intros j' JINB NOTHEP.        
@@ -166,30 +168,30 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1). 
         { apply H_all_jobs_from_taskset.
           apply mem_bigcat_nat_exists in JINB.
-            by inversion JINB as [ta' [JIN' _]]; exists ta'. }
+           by inversion JINB as [ta' [JIN' _]]; exists ta'. }
+        eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
+        move: JINB; move => /andP [_ TJ'].
         { have NINTSK: job_task j' != tsk.
           { apply/eqP; intros TSKj'.
             rewrite /EDF -ltnNge in NOTHEP.
             rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
-            move: TSK => /eqP -> in NOTHEP; rewrite TSKj' ltn_add2r in NOTHEP.
-            move: NOTHEP; rewrite ltnNge; move => /negP T; apply: T.
-            apply leq_trans with t; last by done.
-            eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
-            move: JINB; move => /andP [_ T].
-              by apply ltnW.
+            move: TSK => /eqP -> in NOTHEP. rewrite TSKj' ltn_add2r in NOTHEP.
+            move: NOTHEP; rewrite ltnNge. move => /negP T. apply: T.
+            apply leq_trans with t1; [by apply ltnW | done]. 
           }
           apply/andP; split; first by done.
           rewrite /EDF -ltnNge in NOTHEP.
           move: TSK => /eqP <-.
-          have ARRLE: job_arrival j' < job_arrival j.
-          { apply leq_trans with t; last by done.
-            eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
-              by move: JINB; move => /andP [_ T].
-          }
+          have ARRLE: job_arrival j' < job_arrival j by apply leq_trans with t1.
           rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
-          rewrite /D; lia.
+          rewrite /D.
+          have EQ1: task_deadline (job_task j)
+                    < job_arrival j' + task_deadline (job_task j') - job_arrival j
+            by lia.
+          have EQ2: job_arrival j - job_arrival j' >  (job_arrival j - t1) by lia.
+          by lia.
         }
-    Qed.
+      Qed.
 
     (** Using the lemma above, we prove that the priority inversion of the task is bounded by 
        the maximum length of a nonpreemptive section of lower-priority tasks. *)
@@ -198,7 +200,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Proof.
       move => j ARR TSK POS t1 t2 PREF; move: (PREF) => [_ [_ [_ /andP [T _]]]].
       move: H_sched_valid => [COARR MBR].
-      destruct (leqP (t2 - t1) blocking_bound) as [NEQ|NEQ].
+      destruct (leqP (t2 - t1) (blocking_bound (job_arrival j - t1))) as [NEQ|NEQ].
       { apply leq_trans with (t2 - t1); last by done. 
         rewrite /cumulative_priority_inversion /is_priority_inversion. 
         rewrite -[X in _ <= X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat. 
@@ -213,7 +215,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
       - rewrite /cumulative_priority_inversion /is_priority_inversion. 
         rewrite (@big_cat_nat _ _ _ ppt) //=; last first.
         { rewrite ltn_subRL in NEQ.
-          apply leq_trans with (t1 + blocking_bound); last by apply ltnW. 
+          apply leq_trans with (t1 + blocking_bound (job_arrival j - t1)); last by apply ltnW. 
           apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
             by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2. }
         rewrite -[X in _ <= X]addn0 leq_add2l leqn0.
@@ -255,9 +257,9 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Variable R : duration.
     Hypothesis H_R_is_maximum:
       forall (A : duration),
-        is_in_search_space L A -> 
+        is_in_search_space blocking_bound L A -> 
         exists (F : duration),
-          A + F >= blocking_bound
+          A + F >= blocking_bound A
                   + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                   + bound_on_total_hep_workload  A (A + F) /\
           R >= F + (task_cost tsk - task_rtct tsk).

results/edf/rta/bounded_pi.v

@@ -34,6 +34,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
   Context `{TaskCost Task}.
   Context `{TaskDeadline Task}.
   Context `{TaskRunToCompletionThreshold Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
 
   (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
@@ -122,18 +124,13 @@ Section AbstractRTAforEDFwithArrivalCurves.
        function of all tasks (total request bound function). *)
   Let total_rbf := total_request_bound_function ts.
 
-  (** For simplicity, let's define some local names. *)
-  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
-  Let number_of_task_arrivals := number_of_task_arrivals arr_seq.
-
-  (** Assume that there exists a constant priority_inversion_bound that bounds 
-     the length of any priority inversion experienced by any job of [tsk]. 
-     Since we analyze only task [tsk], we ignore the lengths of priority 
-     inversions incurred by any other tasks. *)
-  Variable priority_inversion_bound : duration.
+  (** Assume that there exists a bound on the length of any priority inversion experienced 
+     by any job of task [tsk]. Since we analyze only task [tsk], we ignore the lengths of priority 
+     inversions incurred by any other tasks.*)
+  Variable priority_inversion_bound: duration -> duration.
   Hypothesis H_priority_inversion_is_bounded:
     priority_inversion_is_bounded_by
-      arr_seq sched tsk priority_inversion_bound.
+     arr_seq sched tsk priority_inversion_bound.
 
   (** Let L be any positive fixed point of the busy interval recurrence. *)
   Variable L : duration.
@@ -150,25 +147,33 @@ Section AbstractRTAforEDFwithArrivalCurves.
      Intuitively, this corresponds to all "interesting" arrival offsets that the job under
      analysis might have with regard to the beginning of its busy-window. *) 
 
-  (** In case of search space for EDF we ask whether [task_rbf A ≠ task_rbf (A + ε)]... *)
+  (** In the case of the search space for EDF, we consider three conditions.
+      First, we ask whether [task_rbf A ≠ task_rbf (A + ε)]. *)
   Definition task_rbf_changes_at (A : duration) := task_rbf A != task_rbf (A + ε).
 
-  (** ...or there exists a task [tsko] from ts such that [tsko ≠ tsk] and 
-     [rbf(tsko, A + D tsk - D tsko) ≠ rbf(tsko, A + ε + D tsk - D tsko)].
-     Note that we use a slightly uncommon notation [has (λ tsko ⇒ P tskₒ) ts] 
-     which can be interpreted as follows: task-set ts contains a task [tsko] such 
-     that a predicate [P] holds for [tsko]. *)
+  (** Second, we ask whether there exists a task [tsko] from ts such that [tsko
+      ≠ tsk] and [rbf(tsko, A + D tsk - D tsko) ≠ rbf(tsko, A + ε + D tsk - D
+      tsko)].  Note that we use a slightly uncommon notation [has (λ tsko ⇒ P
+      tskₒ) ts], which can be interpreted as follows: the task set [ts] contains
+      a task [tsko] such that a predicate [P] holds for [tsko]. *)
   Definition bound_on_total_hep_workload_changes_at A :=
     has (fun tsko =>
            (tsk != tsko)
              && (rbf tsko (A + D tsk - D tsko)
                      != rbf tsko ((A + ε) + D tsk - D tsko))) ts.
-  
-  (** The final search space for EDF is a set of offsets that are less than [L] 
-     and where [task_rbf] or [bound_on_total_hep_workload] changes. *)
+
+  (** Third, we ask whether [priority_inversion_bound (A - ε) ≠ priority_inversion_bound A]. *)
+  Definition priority_inversion_changes_at (A : duration) :=
+    priority_inversion_bound (A - ε) != priority_inversion_bound A.
+
+  (** The final search space for EDF is a set of offsets that are less than [L]
+      and where [priority_inversion_bound], [task_rbf], or
+      [bound_on_total_hep_workload] changes in value. *)
   Definition is_in_search_space (A : duration) :=
-    (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
-  
+    (A < L) && (priority_inversion_changes_at A
+                || 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]
@@ -178,7 +183,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F >= priority_inversion_bound
+        A + F >= priority_inversion_bound A
                 + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                 + bound_on_total_hep_workload  A (A + F) /\
         R >= F + (task_cost tsk - task_rtct tsk).
@@ -202,7 +207,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
       the interference if tasks are sequential. Since tasks are sequential, we exclude 
       interference from other jobs of the same task. For EDF, we define [IBF_other] as 
       the sum of the priority interference bound and the higher-or-equal-priority workload. *)
-  Let IBF_other (A R : duration) := priority_inversion_bound + bound_on_total_hep_workload A R.
+  Let IBF_other (A R : duration) := priority_inversion_bound A + bound_on_total_hep_workload A R.
 
   (** ** Filling Out Hypothesis Of Abstract RTA Theorem *)
   (** In this section we prove that all hypotheses necessary 
@@ -334,7 +339,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
             [priority_inversion_bound] bounds cumulative priority inversion 
             follows from assumption [H_priority_inversion_is_bounded]. *)
         Lemma cumulative_priority_inversion_is_bounded:
-          cumulative_priority_inversion sched j t1 (t1 + Δ) <= priority_inversion_bound.
+          cumulative_priority_inversion sched j t1 (t1 + Δ) <= priority_inversion_bound (job_arrival j - t1).
         Proof.
           unfold priority_inversion_is_bounded_by, EDF in *.
           move: H_sched_valid => [CARR MBR].
@@ -425,7 +430,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
             workload_of_jobs (EDF_from tsk_o) jobs <= rbf tsk_o Δ.
           Proof.
             unfold workload_of_jobs, EDF_from.
-            apply leq_trans with (task_cost tsk_o * number_of_task_arrivals tsk_o t1 (t1 + Δ)).
+            apply leq_trans with (task_cost tsk_o * number_of_task_arrivals arr_seq tsk_o t1 (t1 + Δ)).
             { apply leq_trans with (\sum_(j0 <- arrivals_between arr_seq t1 (t1 + Δ) | job_task j0 == tsk_o)
                                      job_cost j0).
               { rewrite big_mkcond [X in _ <= X]big_mkcond //= leq_sum //.
@@ -513,7 +518,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
             move: (H_busy_interval) => [[/andP [JINBI JINBI2] [QT _]] _].
             set (V := A + ε + D tsk - D tsk_o) in *.
             apply leq_trans with
-                (task_cost tsk_o * number_of_task_arrivals tsk_o t1 (t1 + (A + ε + D tsk - D tsk_o))).
+                (task_cost tsk_o * number_of_task_arrivals arr_seq tsk_o t1 (t1 + (A + ε + D tsk - D tsk_o))).
             -  apply leq_trans with
                    (\sum_(jo <- arrivals_between arr_seq t1 (t1 + V) | job_task jo == tsk_o) job_cost jo).
                + rewrite big_mkcond [X in _ <= X]big_mkcond //=.
@@ -601,8 +606,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
          the busy interval, the bound of the total interference incurred by j within an 
          interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other(A, Δ)]. *)
       Let total_interference_bound tsk (A Δ : duration) :=
-        task_rbf (A + ε) - task_cost tsk + IBF_other A Δ.
-      
+            task_rbf (A + ε) - task_cost tsk + IBF_other A Δ.
+
       (** Next, consider any A from the search space (in abstract sense). *)
       Variable A : duration.
       Hypothesis H_A_is_in_abstract_search_space:
@@ -611,42 +616,36 @@ Section AbstractRTAforEDFwithArrivalCurves.
       (** We prove that A is also in the concrete search space. *)
       Lemma A_is_in_concrete_search_space:
         is_in_search_space A.
-      Proof. 
-        move: H_A_is_in_abstract_search_space => [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]].
-        { subst A. 
-          apply/andP; split; [by done | apply/orP; left].
-          rewrite /task_rbf_changes_at neq_ltn; apply/orP; left.
-          rewrite /task_rbf /rbf; erewrite task_rbf_0_zero; eauto 2.
-          rewrite add0n /task_rbf; apply leq_trans with (task_cost tsk).
-          - by eapply leq_trans; eauto 2; move: H_job_of_tsk => /eqP <-; apply H_valid_job_cost. 
-          - by eapply task_rbf_1_ge_task_cost; eauto 2; apply/eqP.
-        }
-        { apply/andP; split; first by done.
-          rewrite -[_ || _ ]Bool.negb_involutive negb_or; apply/negP; move => /andP [/negPn/eqP EQ1 /hasPn EQ2].
-          unfold total_interference_bound in * ;apply INSP2. 
-          rewrite subn1 addn1 prednK // -EQ1. 
-          apply/eqP; rewrite eqn_add2l eqn_add2l.
-          apply: eq_sum_seq; intros tsk_o IN NEQ.
-          rewrite addn1 prednK //.
-          move: (EQ2 tsk_o IN); clear EQ2;
-            rewrite eq_sym NEQ Bool.andb_true_l Bool.negb_involutive; move => /eqP EQ2.
-          edestruct (leqP (A + ε + D tsk - D tsk_o) x) as [CASE|CASE]. 
-          - have ->: minn (A + D tsk - D tsk_o) x = A + D tsk - D tsk_o.
-            { rewrite minnE.
-              have CASE2: A + D tsk - D tsk_o <= x
-                by apply leq_trans with (A + ε + D tsk - D tsk_o);
-                  first (apply leq_sub2r; rewrite leq_add2r leq_addr).
-                now move: CASE2; rewrite -subn_eq0; move => /eqP CASE2; rewrite CASE2 subn0.
-            } 
-            by apply/eqP.
-          - have ->: minn (A + D tsk - D tsk_o) x = x.
-            { rewrite minnE; rewrite subKn //; rewrite -(leq_add2r 1) !addn1 -subSn.
-              + now rewrite -[in X in _ <= X]addn1 -addnA [_ + 1]addnC addnA.
-              + enough (POS: 0 < A + ε + D tsk - D tsk_o); last eapply leq_ltn_trans with x; eauto 2.
-                now rewrite subn_gt0 -addnA [1 + _]addnC addnA addn1 ltnS in POS.
-            }
-            by apply/eqP.
-        }
+      Proof.
+        move: H_A_is_in_abstract_search_space  => [-> | [/andP [POSA LTL] [x [LTx INSP2]]]];
+          apply/andP; split => //.
+        { apply/orP; left; apply/orP; right.
+          rewrite /task_rbf_changes_at /task_rbf /rbf task_rbf_0_zero //; eauto 2.
+          apply contraT => /negPn /eqP ZERO.
+          rewrite -(ltnn 0) {2}ZERO add0n.
+          apply: (@leq_trans (task_cost tsk));
+            last by apply: task_rbf_1_ge_task_cost; eauto.
+          apply: (@leq_trans (job_cost j)) => //.
+          move: (H_job_of_tsk) => /eqP <-.
+          by apply: (H_valid_job_cost _ H_j_arrives). }
+        { apply contraT; rewrite !negb_or => /andP [/andP [/negPn/eqP PI /negPn/eqP RBF]  WL].
+          exfalso; apply INSP2.
+          rewrite /total_interference_bound subnK // RBF.
+          apply /eqP; rewrite eqn_add2l /IBF_other PI eqn_add2l.
+          rewrite /bound_on_total_hep_workload subnK //.
+          apply /eqP; rewrite big_seq_cond [RHS]big_seq_cond.
+          apply eq_big => // tsk_i /andP [TS OTHER].
+          move: WL; rewrite /bound_on_total_hep_workload_changes_at => /hasPn WL.
+          move: {WL} (WL tsk_i TS) =>  /nandP [/negPn/eqP EQ|/negPn/eqP WL];
+            first by move: OTHER; rewrite EQ => /neqP.
+          case: (ltngtP (A + ε + D tsk - D tsk_i) x) => [ltn_x|gtn_x|eq_x];
+            rewrite /minn.
+          { by rewrite ifT //; lia. }
+          { rewrite ifF //.
+            by move: gtn_x; rewrite leq_eqVlt /ε => /orP [/eqP EQ|LEQ]; lia. }
+          { case: (A + D tsk - D tsk_i < x).
+            - by rewrite WL.
+            - by rewrite eq_x. } }
       Qed.
 
       (** Then, there exists solution for response-time recurrence (in the abstract sense). *)
@@ -659,7 +658,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
         - by apply A_is_in_concrete_search_space.
         - exists F; split; last by done.
           rewrite -{2}(leqRW FIX).
-          by rewrite addnA [_ + priority_inversion_bound]addnC -!addnA.
+          by rewrite addnA [_ + priority_inversion_bound A]addnC -!addnA.
       Qed.
          
       End SolutionOfResponseTimeReccurenceExists.       
@@ -670,7 +669,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
   (** Based on the properties established above, we apply the abstract analysis 
      framework to infer that R is a response-time bound for [tsk]. *)
   Theorem uniprocessor_response_time_bound_edf:
-    response_time_bounded_by tsk R.
+    task_response_time_bound arr_seq sched tsk R.
   Proof.
     intros js ARRs TSKs.
     move: H_sched_valid => [CARR MBR].
@@ -686,7 +685,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.
-    - by eapply correct_search_space; eauto 2; apply/eqP.
+    - by eapply correct_search_space; eauto 2.
   Qed.
   
 End AbstractRTAforEDFwithArrivalCurves. 

results/edf/rta/floating_nonpreemptive.v

@@ -98,8 +98,8 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Let total_rbf := total_request_bound_function ts.
   
   (** We define a bound for the priority inversion caused by jobs with lower priority. *)
-  Definition blocking_bound :=
-    \max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk))
+  Definition blocking_bound A :=
+    \max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk + A))
      (task_max_nonpreemptive_segment tsk_other - ε).
   
   (** Next, we define an upper bound on interfering workload received from jobs 
@@ -116,7 +116,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   (** ** Response-Time Bound *)
   
   (** 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.
+  Let is_in_search_space := is_in_search_space ts tsk blocking_bound L.
   
   (** Consider any value [R], and assume that for any given arrival
       offset [A] in the search space, there is a solution of the
@@ -126,7 +126,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
     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) /\
+        A + F >= blocking_bound A + task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
         R >= F.
 
   (** Now, we can leverage the results for the abstract model with

results/edf/rta/fully_nonpreemptive.v

@@ -75,7 +75,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
       job_preemptable function (i.e., jobs have bounded nonpreemptive
       segments). *)
   Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
-
+   
   (** ** Total Workload and Length of Busy Interval *)
 
   (** We introduce the abbreviation [rbf] for the task request bound function,
@@ -91,8 +91,8 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   Let total_rbf := total_request_bound_function ts.
   
   (** We also define a bound for the priority inversion caused by jobs with lower priority. *)
-  Let blocking_bound :=
-    \max_(tsk_o <- ts | (tsk_o != tsk) && (task_deadline tsk_o > task_deadline tsk))
+  Let blocking_bound A :=
+    \max_(tsk_o <- ts | (tsk_o != tsk) && (task_deadline tsk_o > task_deadline tsk + A))
      (task_cost tsk_o - ε).
   
   (** Next, we define an upper bound on interfering workload received from jobs 
@@ -109,7 +109,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   (** ** Response-Time Bound *)
     
   (** 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.
+  Let is_in_search_space := is_in_search_space ts tsk blocking_bound L.
   
   (** Consider any value [R], and assume that for any given arrival
       offset [A] in the search space, there is a solution of the
@@ -119,7 +119,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
     forall A,
       is_in_search_space A -> 
       exists F,
-        A + F >= blocking_bound + (task_rbf (A + ε) - (task_cost tsk - ε))
+        A + F >= blocking_bound A + (task_rbf (A + ε) - (task_cost tsk - ε))
                 + bound_on_total_hep_workload A (A + F) /\
         R >= F + (task_cost tsk - ε).
 

results/edf/rta/fully_preemptive.v

@@ -91,6 +91,10 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
       function of all tasks (total request bound function). *)
   Let total_rbf := total_request_bound_function ts.
 
+  (** If jobs are fully preemptive, lower priority jobs do not cause priority inversion. 
+      Hence, the blocking bound is always 0 for any [A]. *)
+  Let blocking_bound (A : duration) := 0.
+
   (** Next, we define an upper bound on interfering workload received from jobs 
       of other tasks with higher-than-or-equal priority. *)
   Let bound_on_total_hep_workload A Δ :=
@@ -105,7 +109,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   (** ** Response-Time Bound *)
   
   (** 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.
+  Let is_in_search_space := is_in_search_space ts tsk blocking_bound L.
   
   (** Consider any value [R], and assume that for any given arrival
       offset [A] in the search space, there is a solution of the
@@ -128,19 +132,19 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Theorem uniprocessor_response_time_bound_fully_preemptive_edf:
     response_time_bounded_by tsk R.
   Proof.
-    have BLOCK: blocking_bound  ts tsk = 0.
-    { by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
-                 /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.
-    - move => A /andP [LT NEQ].
-      specialize (H_R_is_maximum A); feed H_R_is_maximum.
-      { by apply/andP; split. }
-      move: H_R_is_maximum => [F [FIX BOUND]].
-      exists F; split.
-      + by rewrite BLOCK add0n subnn subn0. 
-      + by rewrite subnn addn0.
+    eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L); rt_eauto.
+    move => A /andP [LT CHANGE].
+    have BLOCK: forall A', bounded_nps.blocking_bound ts tsk A' = blocking_bound A'.
+    { by move=> A'; rewrite /bounded_nps.blocking_bound /parameters.task_max_nonpreemptive_segment
+         /fully_preemptive_task_model subnn big1_eq. }
+    specialize (H_R_is_maximum A); feed H_R_is_maximum.
+    { apply/andP; split; first by done.
+      by move: CHANGE; rewrite /priority_inversion_changes_at /is_in_search_space !BLOCK. }
+    move: H_R_is_maximum => [F [FIX BOUND]].
+    exists F; split.
+    + by rewrite BLOCK add0n subnn subn0.
+    + by rewrite subnn addn0.
   Qed.
-    
+
 End RTAforFullyPreemptiveEDFModelwithArrivalCurves.

results/edf/rta/limited_preemptive.v

@@ -99,8 +99,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Let total_rbf := total_request_bound_function ts.
 
   (** We define a bound for the priority inversion caused by jobs with lower priority. *)
-  Let blocking_bound :=
-    \max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk))
+  Let blocking_bound A :=
+    \max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk + A))
      (task_max_nonpreemptive_segment tsk_other - ε).
   
   (** Next, we define an upper bound on interfering workload received from jobs 
@@ -117,7 +117,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** ** Response-Time Bound *)
   
   (** 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.
+  Let is_in_search_space := is_in_search_space ts tsk blocking_bound L.
   
   (** Consider any value [R], and assume that for any given arrival
       offset [A] in the search space, there is a solution of the
@@ -127,7 +127,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
     forall (A : duration),
       is_in_search_space A -> 
       exists (F : duration),
-        A + F >= blocking_bound
+        A + F >= blocking_bound A
                 + (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε)) 
                 + bound_on_total_hep_workload A (A + F) /\
         R >= F + (task_last_nonpr_segment tsk - ε).

results/fixed_priority/rta/bounded_nps.v

@@ -157,7 +157,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
 
     (** Using the above lemma, we prove that the priority inversion of the task is bounded by blocking_bound. *) 
     Lemma priority_inversion_is_bounded:
-      priority_inversion_is_bounded_by
+      priority_inversion_is_bounded_by_constant
         arr_seq sched tsk blocking_bound.
     Proof.
       intros j ARR TSK POS t1 t2 PREF.

results/fixed_priority/rta/bounded_pi.v

@@ -128,7 +128,7 @@ Section AbstractRTAforFPwithArrivalCurves.
      inversions incurred by any other tasks. *)
   Variable priority_inversion_bound : duration.
   Hypothesis H_priority_inversion_is_bounded:
-    priority_inversion_is_bounded_by
+    priority_inversion_is_bounded_by_constant
       arr_seq sched tsk priority_inversion_bound.
 
   (** Let L be any positive fixed point of the busy interval recurrence. *)