README.md

@@ -6,7 +6,7 @@ This repository contains the main Coq specification & proof development of the [
 
 ## Documentation
 
-Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homeage:
+Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:
 
 - <https://prosa.mpi-sws.org/branches>
 

analysis/abstract/abstract_rta.v

@@ -58,10 +58,9 @@ Section Abstract_RTA.
   Hypothesis H_valid_preemption_model:
     valid_preemption_model arr_seq sched.
   
-  (** ...and a valid task run-to-completion threshold function. That is, 
-     [task_run_to_completion_threshold tsk] is (1) no bigger than [tsk]'s 
-     cost, (2) for any job of task [tsk] job_run_to_completion_threshold 
-     is bounded by task_run_to_completion_threshold. *)
+  (** ...and a valid task run-to-completion threshold function. That
+     is, [task_rtct tsk] is (1) no bigger than [tsk]'s cost, (2) for
+     any job of task [tsk] [job_rtct] is bounded by [task_rtct]. *)
   Hypothesis H_valid_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
 
@@ -100,15 +99,15 @@ Section Abstract_RTA.
 
   (** 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_run_to_completion_threshold tsk) <= R]. *)
+     solution [F] such that [F + (task_cost tsk - task_rtct tsk) <= R]. *)
   Variable R: nat.
   Hypothesis H_R_is_maximum:
     forall A,
       is_in_search_space A -> 
       exists F,
-        A + F = task_run_to_completion_threshold tsk
+        A + F = task_rtct tsk
                 + interference_bound_function tsk A (A + F) /\
-        F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R.
+        F + (task_cost tsk - task_rtct tsk) <= R.
 
   (** In this section we show a detailed proof of the main theorem 
      that establishes that R is a response-time bound of task [tsk]. *) 
@@ -153,10 +152,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_run_to_completion_threshold 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_run_to_completion_threshold tsk) <= R.
+    Hypothesis H_R_gt_Fsp : F_sp + (task_cost tsk - task_rtct tsk) <= R.
 
     (** 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. 
@@ -178,7 +177,7 @@ Section Abstract_RTA.
         { by rewrite !addnA leq_add2r leq_add2l. }
         rewrite /A subnKC; last by done.
         rewrite leq_add2l.
-          by apply leq_trans with (F_sp + (task_cost tsk - task_run_to_completion_threshold tsk));
+          by apply leq_trans with (F_sp + (task_cost tsk - task_rtct tsk));
             first rewrite leq_addr.
       Qed.
       
@@ -226,39 +225,44 @@ 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_run_to_completion_threshold 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).
 
-          (** Some additional reasoning is required since the term [task_cost tsk - task_run_to_completion_threshold tsk]
-             does not necessarily bound the term [job_cost j - job_run_to_completion_threshold j]. That is, a job can 
+          (** Some additional reasoning is required since the term [task_cost tsk - task_rtct tsk]
+             does not necessarily bound the term [job_cost j - job_rtct j]. That is, a job can 
              have a small run-to-completion threshold, thereby becoming non-preemptive much earlier than guaranteed 
              according to task run-to-completion threshold, while simultaneously executing the last non-preemptive 
-             segment that is longer than [task_cost tsk - task_run_to_completion_threshold tsk] (e.g., this is possible 
+             segment that is longer than [task_cost tsk - task_rtct tsk] (e.g., this is possible 
              in the case of floating non-preemptive sections). 
 
              In this case we cannot directly apply lemma "j_receives_at_least_run_to_completion_threshold". Therefore
              we introduce two temporal notions of the last non-preemptive region of job j and an execution 
              optimism. We use these notions inside this proof, so we define them only locally. *)
 
-          (** Let the last non-preemptive region of job [j] (last) be the difference between the cost of the job 
-             and the [j]'s run-to-completion threshold (i.e. [job_cost j - job_run_to_completion_threshold j]). 
-             We know that after j has reached its run-to-completion threshold, it will additionally be executed
-             [job_last j] units of time. *)          
-          Let job_last := job_cost j - job_run_to_completion_threshold j.
-
-          (** And let execution optimism (optimism) be the difference between the [tsk]'s 
-             run-to-completion threshold and the [j]'s run-to-completion threshold (i.e. 
-             [task_run_to_completion_threshold -  job_run_to_completion_threshold]).
-             Intuitively, optimism is how much earlier job j has received its 
-             run-to-completion threshold than it could at worst.  *)
-          Let optimism := task_run_to_completion_threshold tsk - job_run_to_completion_threshold j.
+          (** Let the last non-preemptive region of job [j] (last) be
+             the difference between the cost of the job and the [j]'s
+             run-to-completion threshold (i.e. [job_cost j - job_rtct j]). 
+             We know that after j has reached its
+             run-to-completion threshold, it will additionally be
+             executed [job_last j] units of time. *)          
+          Let job_last := job_cost j - job_rtct j.
+
+          (** And let execution optimism (optimism) be the difference
+             between the [tsk]'s run-to-completion threshold and the
+             [j]'s run-to-completion threshold (i.e.  [task_rtct -
+             job_rtct]).  Intuitively, optimism is how much earlier
+             job j has received its run-to-completion threshold than
+             it could at worst.  *)
+          Let optimism := task_rtct tsk - job_rtct j.
           
-          (** From lemma "j_receives_at_least_run_to_completion_threshold" with parameters [progress_of_job :=
-             job_run_to_completion_threshold j] and [delta := (A + F) - optimism)] we know that service of [j]
-             by time [t1 + (A + F) - optimism] is no less than [job_run_to_completion_threshold j]. Hence, job [j]
-             is completed by time [t1 + (A + F) - optimism + last]. *)
+          (** From lemma "j_receives_at_least_run_to_completion_threshold" 
+              with parameters [progress_of_job := job_rtct j] and [delta :=
+              (A + F) - optimism)] we know that service of [j] by time
+              [t1 + (A + F) - optimism] is no less than [job_rtct
+              j]. Hence, job [j] is completed by time [t1 + (A + F) -
+              optimism + last]. *)
           Lemma j_is_completed_by_t1_A_F_optimist_last :
             completed_by sched j (t1 + (A + F - optimism) + job_last).
           Proof.
@@ -267,7 +271,7 @@ Section Abstract_RTA.
             have ESERV :=
               @j_receives_at_least_run_to_completion_threshold
                 _ _ H1 H2 H3 PState H5 _ _  arr_seq sched tsk interference interfering_workload
-                _ j _ _ _ t1 t2 _ (job_run_to_completion_threshold j) _ ((A + F) - optimism). 
+                _ j _ _ _ t1 t2 _ (job_rtct j) _ ((A + F) - optimism). 
             feed_n 7 ESERV; eauto 2.
             specialize (ESERV H3 H4).
             feed_n 2 ESERV.
@@ -289,7 +293,7 @@ Section Abstract_RTA.
                   apply completion_monotonic with (t1 + (A + F)); try done.
                   rewrite addnA subnKC // leq_add2l.
                   apply leq_trans with F_sp; first by done.
-                    by apply leq_trans with (F_sp + (task_cost tsk - task_run_to_completion_threshold tsk)).
+                    by apply leq_trans with (F_sp + (task_cost tsk - task_rtct tsk)).
               }
             }
             eapply job_completes_after_reaching_run_to_completion_threshold with (arr_seq0 := arr_seq); eauto 2.
@@ -343,16 +347,16 @@ Section Abstract_RTA.
                   apply completion_monotonic with (t1 + (A + F)); last by done. 
                   rewrite !addnA subnKC // leq_add2l.
                   apply leq_trans with F_sp; first by done.
-                    by apply leq_trans with (F_sp + (task_cost tsk - task_run_to_completion_threshold tsk)).
+                    by apply leq_trans with (F_sp + (task_cost tsk - task_rtct tsk)).
               }
             Qed.
             
             (** As two trivial corollaries, we show that 
                [tsk]'s run-to-completion threshold is at most [F_sp]... *)
             Corollary tsk_run_to_completion_threshold_le_Fsp :
-              task_run_to_completion_threshold tsk <= F_sp.
+              task_rtct tsk <= F_sp.
             Proof.
-              have HH : task_run_to_completion_threshold tsk <= F.
+              have HH : task_rtct tsk <= F.
               { move: H_A_F_fixpoint => EQ.
                 have L1 := relative_arrival_le_interference_bound.
                 ssrlia.
@@ -364,12 +368,12 @@ Section Abstract_RTA.
             Corollary optimism_le_F :
               optimism <= F.
             Proof.
-              have HH : task_run_to_completion_threshold tsk <= F.
+              have HH : task_rtct tsk <= F.
               { move: H_A_F_fixpoint => EQ.
                 have L1 := relative_arrival_le_interference_bound.
                 ssrlia.
               }
-                by apply leq_trans with (task_run_to_completion_threshold tsk); first rewrite /optimism leq_subr.
+                by apply leq_trans with (task_rtct tsk); first rewrite /optimism leq_subr.
             Qed.
             
           End AuxiliaryInequalities.
@@ -381,8 +385,8 @@ Section Abstract_RTA.
              [≤ job_arrival j + (F - optimism) + job_last]
              [≤ job_arrival j + (F_sp - optimism) + job_last]
              [≤ job_arrival j + F_sp + (job_last - optimism)]
-             [≤ job_arrival j + F_sp + job_cost j - task_run_to_completion_threshold tsk]
-             [≤ job_arrival j + F_sp + task_cost tsk - task_run_to_completion_threshold tsk]
+             [≤ job_arrival j + F_sp + job_cost j - task_rtct tsk]
+             [≤ job_arrival j + F_sp + task_cost tsk - task_rtct tsk]
              [≤ job_arrival j + R]. *)
           Lemma t1_A_F_optimist_last_le_arrival_R :
             t1 + (A + F - optimism) + job_last <= job_arrival j + R.
@@ -398,7 +402,7 @@ Section Abstract_RTA.
             { move: H_valid_run_to_completion_threshold => [PRT1 PRT2]. 
               rewrite -addnA leq_add2l.
               apply leq_trans with (F_sp - optimism + job_last ); first by rewrite leq_add2r leq_sub2r. 
-              apply leq_trans with (F_sp + (task_cost tsk - task_run_to_completion_threshold tsk)); last by done. 
+              apply leq_trans with (F_sp + (task_cost tsk - task_rtct tsk)); last by done. 
               rewrite /optimism subnBA; last by apply PRT2.
               rewrite -subh1 //.
               rewrite /job_last.
@@ -430,7 +434,7 @@ Section Abstract_RTA.
           have HelpAuto: forall m n, n <= n + m; first by intros; rewrite leq_addr.
           move: H_busy_interval => [[/andP [GT LT] _] _].
           have L1 := solution_for_A_exists
-                       tsk L (fun tsk A R => task_run_to_completion_threshold tsk
+                       tsk L (fun tsk A R => task_rtct tsk
                                           + interference_bound_function tsk A R) A_sp F_sp.
           specialize (L1 H0).
           feed_n 2 L1; try done.
@@ -474,7 +478,7 @@ Section Abstract_RTA.
         (** We can use [j_receives_at_least_run_to_completion_threshold] to prove that the service 
            received by j by time [t1 + (A_sp + F_sp)] is no less than run-to-completion threshold. *)
         Lemma service_of_job_ge_run_to_completion_threshold:
-          service sched j (t1 + (A_sp + F_sp)) >= job_run_to_completion_threshold j.
+          service sched j (t1 + (A_sp + F_sp)) >= job_rtct j.
         Proof.
           move: (H_busy_interval) => [[NEQ [QT1 NTQ]] QT2].
           move: (NEQ) => /andP [GT LT]. 
@@ -496,7 +500,7 @@ Section Abstract_RTA.
           have ESERV :=
             @j_receives_at_least_run_to_completion_threshold
               _ _ H1 H2 H3 PState H5 _ _ arr_seq sched tsk
-              interference interfering_workload _ j _ _ _ t1 t2 _ (job_run_to_completion_threshold j) _ (A_sp + F_sp). 
+              interference interfering_workload _ j _ _ _ t1 t2 _ (job_rtct j) _ (A_sp + F_sp). 
           feed_n 7 ESERV; eauto 2.
           specialize (ESERV H3 H4).
           feed_n 2 ESERV; eauto using job_run_to_completion_threshold_le_job_cost.

analysis/abstract/abstract_seq_rta.v

@@ -57,10 +57,9 @@ Section Sequential_Abstract_RTA.
   Hypothesis H_valid_preemption_model:
     valid_preemption_model arr_seq sched.
 
-  (** ...and a valid task run-to-completion threshold function. That is,
-     [task_run_to_completion_threshold tsk] is (1) no bigger than [tsk]'s
-     cost, (2) for any job of task [tsk] [job_run_to_completion_threshold]
-     is bounded by [task_run_to_completion_threshold]. *)
+  (** ...and a valid task run-to-completion threshold function. That
+     is, [task_rtct tsk] is (1) no bigger than [tsk]'s cost, (2) for
+     any job of task [tsk] [job_rtct] is bounded by [task_rtct]. *)
   Hypothesis H_valid_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
 
@@ -160,7 +159,7 @@ Section Sequential_Abstract_RTA.
     (** Unlike the previous theorem [uniprocessor_response_time_bound], we assume
        that (1) tasks are sequential, moreover (2) functions interference and
        interfering_workload are consistent with the hypothesis of sequential tasks. *)
-    Hypothesis H_sequential_tasks : sequential_tasks sched.
+    Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
     Hypothesis H_interference_and_workload_consistent_with_sequential_tasks:
       interference_and_workload_consistent_with_sequential_tasks.
 
@@ -205,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_run_to_completion_threshold 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_run_to_completion_threshold tsk) <= R.
+          F + (task_cost tsk - task_rtct tsk) <= R.
 
     (** 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. *)
@@ -429,7 +428,7 @@ Section Sequential_Abstract_RTA.
                 { exfalso.
                   apply negbT in ARRNEQ; rewrite -ltnNge in ARRNEQ.
                   move: (H_sequential_tasks j j' t) => CONTR.
-                  feed_n 3 CONTR; try done.
+                  feed_n 5 CONTR; try done.
                   { by rewrite /same_task eq_sym H_job_of_tsk. }
                   { by move: H_sched => /eqP SCHEDt; rewrite scheduled_at_def. }
                   move: H_job_j_is_not_completed => /negP T; apply: T.
@@ -649,9 +648,9 @@ Section Sequential_Abstract_RTA.
         forall (A : duration),
           is_in_search_space A ->
           exists (F : duration),
-            A + F = task_run_to_completion_threshold 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_run_to_completion_threshold tsk) <= R.
+            F + (task_cost tsk - task_rtct tsk) <= R.
       Proof.
         move: H_valid_run_to_completion_threshold => [PRT1 PRT2].
         intros A INSP.

analysis/abstract/ideal_jlfp_rta.v

@@ -42,7 +42,7 @@ Section JLFPInstantiation.
 
   (** Assume we have sequential tasks, i.e., jobs of the 
      same task execute in the order of their arrival. *)
-  Hypothesis H_sequential_tasks : sequential_tasks sched.
+  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
 
   (** Consider a JLFP-policy that indicates a higher-or-equal priority relation,
      and assume that this relation is reflexive and transitive. *)             
@@ -218,7 +218,8 @@ Section JLFPInstantiation.
        is equal to the sum of the cumulative priority inversion of job [j] and the cumulative interference
        incurred by task [tsk] due to other tasks. *)
     Lemma cumulative_task_interference_split: 
-      forall j t1 t2 upp_t, 
+      forall j t1 t2 upp_t,
+        arrives_in arr_seq j -> 
         job_task j = tsk ->
         j \in arrivals_before arr_seq upp_t ->
         ~~ job_completed_by j t2 ->
@@ -227,7 +228,7 @@ Section JLFPInstantiation.
         cumulative_interference_from_hep_jobs_from_other_tasks j t1 t2.
     Proof.
       rewrite /cumulative_task_interference /cumul_task_interference.
-      intros j t1 R upp TSK ARR NCOMPL.
+      intros j t1 R upp ARRin TSK ARR NCOMPL.
       rewrite -big_split //= big_nat_cond [X in _ = X]big_nat_cond. 
       apply/eqP; rewrite eqn_leq; apply/andP; split.
       all: rewrite /interference /is_priority_inversion /priority_inversion.is_priority_inversion.
@@ -253,7 +254,7 @@ Section JLFPInstantiation.
           apply completion_monotonic with t; [ by apply ltnW | ].
           apply/negP; intros NCOMPL; move: NCOMPL => /negP NCOMPL.
           move: NEQ => /negP NEQ; apply: NEQ; apply H_JLFP_respects_sequential_tasks; eauto 2. 
-            by eapply scheduler_executes_job_with_earliest_arrival; eauto 2.
+          by eapply scheduler_executes_job_with_earliest_arrival; eauto 2.
         + have NEQ: s != j.
           { apply/negP; intros EQ2; move: EQ2 => /eqP EQ2.
               by move: TSKEQ => /eqP TSKEQ; apply: TSKEQ; rewrite EQ2. } 

analysis/abstract/run_to_completion.v

@@ -171,15 +171,15 @@ Section AbstractRTARunToCompletionThreshold.
     Hypothesis H_valid_preemption_model:
       valid_preemption_model arr_seq sched.
 
-    (** Then, job [j] must complete in [job_cost j - job_run_to_completion_threshold j] time
+    (** Then, job [j] must complete in [job_cost j - job_rtct j] time
        units after it reaches run-to-completion threshold. *)
     Lemma job_completes_after_reaching_run_to_completion_threshold:
       forall t,
-        job_run_to_completion_threshold j <= service sched j t ->
-        completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j)).
+        job_rtct j <= service sched j t ->
+        completed_by sched j (t + (job_cost j - job_rtct j)).
     Proof.
       move => t ES.
-      set (job_cost j - job_run_to_completion_threshold j) as job_last.
+      set (job_cost j - job_rtct j) as job_last.
       have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
                      Job H2 H3 _ _ arr_seq sched _ j _ t.
       apply negbNE; apply/negP; intros CONTR.
@@ -204,9 +204,9 @@ Section AbstractRTARunToCompletionThreshold.
       eapply service_at_most_cost with (j0 := j) (t0 := t + job_last.+1) in H_completed_jobs_dont_execute; auto.
       move: H_completed_jobs_dont_execute; rewrite leqNgt; move => /negP T; apply: T.
       rewrite /service -(service_during_cat _ _ _ t); last by (apply/andP; split; last rewrite leq_addr).
-      apply leq_trans with (job_run_to_completion_threshold j + service_during sched j t (t + job_last.+1));
+      apply leq_trans with (job_rtct j + service_during sched j t (t + job_last.+1));
         last by rewrite leq_add2r.
-      apply leq_trans with  (job_run_to_completion_threshold j + job_last.+1); last by rewrite leq_add2l /service_during -addn1.
+      apply leq_trans with  (job_rtct j + job_last.+1); last by rewrite leq_add2l /service_during -addn1.
         by rewrite addnS ltnS subnKC //; eapply job_run_to_completion_threshold_le_job_cost; eauto.
     Qed.
 

analysis/definitions/busy_interval.v

@@ -13,12 +13,16 @@ Section BusyIntervalJLFP.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.    
 
-  (** Consider any arrival sequence with consistent arrivals. *)
+  (** Consider any kind of processor state model. *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.  
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
-  Variable sched : schedule (ideal.processor_state Job).
+  (** ... and a schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
   
   (** Assume a given JLFP policy. *)
   Context `{JLFP_policy Job}. 
@@ -89,4 +93,4 @@ Section BusyIntervalJLFP.
 
   End DecidableQuietTime.
 
-End BusyIntervalJLFP.
\ No newline at end of file
+End BusyIntervalJLFP.

analysis/facts/model/rbf.v

@@ -252,7 +252,7 @@ Section RequestBoundFunctions.
      [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function
      that equals 0 for the empty interval delta = 0. *)
   Context `{MaxArrivals Task}.
-  Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
+  Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
   Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
 
   (** Let's define some local names for clarity. *)

analysis/facts/model/sequential.v

@@ -15,28 +15,33 @@ Section ExecutionOrder.
   Context {PState: Type}.
   Context `{ProcessorState Job PState}.
 
-  (** Assume a schedule ... *)
-  Variable sched: schedule PState.
-
-  (** in which the sequential tasks hypothesis holds. *)
-  Hypothesis H_sequential_tasks: sequential_tasks sched.
 
+  (** Consider any arrival sequence ... *) 
+  Variable arr_seq : arrival_sequence Job.
+  
+  (** ... and any schedule of this arrival sequence ... *)
+  Variable sched : schedule PState.  
+  
+  (** ... in which the sequential tasks hypothesis holds. *)
+  Hypothesis H_sequential_tasks: sequential_tasks arr_seq sched.
 
   (** A simple corollary of this hypothesis is that the scheduler
       executes a job with the earliest arrival time. *)
   Corollary scheduler_executes_job_with_earliest_arrival:
     forall j1 j2 t,
+      arrives_in arr_seq j1 -> 
+      arrives_in arr_seq j2 ->
       same_task j1 j2 ->
       ~~ completed_by sched j2 t ->
       scheduled_at sched j1 t ->
       job_arrival j1 <= job_arrival j2.
   Proof.
-    intros ? ? t TSK NCOMPL SCHED.
+    intros ? ? t ARR1 ARR2 TSK NCOMPL SCHED.
     rewrite /same_task eq_sym in TSK.
-    have SEQ := H_sequential_tasks j2 j1 t TSK.
+    have SEQ := H_sequential_tasks j2 j1 t ARR2 ARR1 TSK.
     rewrite leqNgt; apply/negP; intros ARR.
     move: NCOMPL => /negP NCOMPL; apply: NCOMPL.
-      by apply SEQ.
+    by apply SEQ.
   Qed.
 
 End ExecutionOrder.

analysis/facts/model/service_of_jobs.v

@@ -312,7 +312,7 @@ Section IdealModelLemmas.
       { unfold workload_of_jobs, service_of_jobs in EQ; unfold completed_by, service.completed_by.
         rewrite /service -(service_during_cat _ _ _ t1); last by apply/andP; split.
         rewrite cumulative_service_before_job_arrival_zero // add0n.
-        rewrite <- sum_majorant_eqn with (F1 := fun j => service_during sched j t1 t_compl)
+        rewrite <- sum_majorant_eqn with (E1 := fun j => service_during sched j t1 t_compl)
                                         (xs := arrivals_between t1 t2) (P := P); try done.
         intros; apply cumulative_service_le_job_cost; auto using ideal_proc_model_provides_unit_service.
       }

analysis/facts/model/task_arrivals.v

@@ -230,7 +230,7 @@ Section TaskArrivals.
   Proof.
     intros *.
     rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.
-    now apply cat_filter_eq_filter_cat.
+    now apply bigcat_nat_filter_eq_filter_bigcat_nat.
   Qed.
 
   (** The number of jobs of a task [tsk] in the interval <<[t1, t2)>> is the same 
@@ -242,7 +242,7 @@ Section TaskArrivals.
   Proof.
     intros *.
     rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.
-    now rewrite size_big_nat cat_filter_eq_filter_cat.
+    now rewrite size_big_nat bigcat_nat_filter_eq_filter_bigcat_nat.
   Qed.
     
 End TaskArrivals.

analysis/facts/preemption/rtc_threshold/floating.v

@@ -27,7 +27,7 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
   Hypothesis H_valid_job_cost:
     arrivals_have_valid_job_costs arr_seq.
 
-  (** Then, we prove that [task_run_to_completion_threshold] function
+  (** Then, we prove that [task_rtct] function
       defines a valid task's run to completion threshold. *)   
   Lemma floating_preemptive_valid_task_run_to_completion_threshold:
     forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.

analysis/facts/preemption/rtc_threshold/job_preemptable.v

@@ -195,9 +195,9 @@ Section RunToCompletionThreshold.
         service. *)
   Lemma job_run_to_completion_threshold_positive:
     job_cost_positive j ->
-    0 < job_run_to_completion_threshold j.
+    0 < job_rtct j.
   Proof.
-    intros COST; unfold job_run_to_completion_threshold, ε.
+    intros COST; unfold job_rtct, ε.
     have N1 := job_last_nonpreemptive_segment_positive COST.
     have N2 := job_last_nonpreemptive_segment_le_job_cost.
     ssrlia.
@@ -206,7 +206,7 @@ Section RunToCompletionThreshold.
   (** Next we show that the run-to-completion threshold is at most
         the cost of a job. *)
   Lemma job_run_to_completion_threshold_le_job_cost:
-    job_run_to_completion_threshold j <= job_cost j.
+    job_rtct j <= job_cost j.
   Proof. by apply leq_subr. Qed.
 
   
@@ -214,13 +214,13 @@ Section RunToCompletionThreshold.
         during execution of the last segment. *)
   Lemma job_cannot_be_preempted_within_last_segment:
     forall (ρ : duration), 
-      job_run_to_completion_threshold j <= ρ < job_cost j ->
+      job_rtct j <= ρ < job_cost j ->
       ~~ job_preemptable j ρ.
   Proof.
     move => ρ /andP [GE LT].
     apply/negP; intros C.
     have POS : 0 < job_cost j; first by ssrlia.
-    rewrite /job_run_to_completion_threshold subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
+    rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
     rewrite -subh1 in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost]. 
     rewrite job_cost_is_last_element_of_preemption_points in LT, GE.
     rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.
@@ -246,7 +246,7 @@ Section RunToCompletionThreshold.
   Lemma job_nonpreemptive_after_run_to_completion_threshold: 
     forall t t',
       t <= t' ->
-      job_run_to_completion_threshold j <= service sched j t ->
+      job_rtct j <= service sched j t ->
       ~~ completed_by sched j t' ->
       scheduled_at sched j t'.
   Proof.

analysis/facts/preemption/rtc_threshold/limited.v

@@ -93,7 +93,7 @@ Section TaskRTCThresholdLimitedPreemptions.
     }
   Qed.
     
-  (** Then, we prove that [task_run_to_completion_threshold] function
+  (** Then, we prove that [task_rtct] function
       defines a valid task's run to completion threshold. *)   
   Lemma limited_valid_task_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
@@ -101,7 +101,7 @@ Section TaskRTCThresholdLimitedPreemptions.
     split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
     intros ? ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) => [LJ LT].
     move: (LJ) (LT) => [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
-    rewrite /job_run_to_completion_threshold /task_run_to_completion_threshold /limited_preemptions
+    rewrite /job_rtct /task_rtct /limited_preemptions
             /job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
     case: (posnP (job_cost j)) => [Z|POS]; first by rewrite Z; compute.
     have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j

analysis/facts/preemption/rtc_threshold/nonpreemptive.v

@@ -33,16 +33,15 @@ Section TaskRTCThresholdFullyNonPreemptive.
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
   Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
-  (** First we prove that if the cost of a job j is equal to 0, then 
-      [job_run_to_completion_threshold j = 0] ...  *)
+  (** First we prove that if the cost of a job j is equal to 0, then [job_rtct j = 0] ...  *)
   Fact job_rtc_threshold_is_0:
     forall j,
       job_cost j = 0 -> 
-      job_run_to_completion_threshold j = 0.
+      job_rtct j = 0.
   Proof.
     intros.
     apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
-    unfold job_run_to_completion_threshold.
+    unfold job_rtct.
       by rewrite H3; compute.
   Qed.
   
@@ -51,10 +50,10 @@ Section TaskRTCThresholdFullyNonPreemptive.
     forall j,
       job_cost j > 0 ->
       arrives_in arr_seq j ->
-      job_run_to_completion_threshold j = ε.
+      job_rtct j = ε.
   Proof.
     intros ? ARRj POSj; unfold ε in *.
-    unfold job_run_to_completion_threshold.
+    unfold job_rtct.
     rewrite job_last_nps_is_job_cost.
       by rewrite subKn.
   Qed.
@@ -63,15 +62,15 @@ Section TaskRTCThresholdFullyNonPreemptive.
   Variable tsk : Task.
   Hypothesis H_positive_cost : 0 < task_cost tsk.
                 
-  (** Then, we prove that [task_run_to_completion_threshold] function
-      defines a valid task's run to completion threshold. *)     
+  (** Then, we prove that [task_rtct] function defines a valid task's
+      run to completion threshold. *)     
   Lemma fully_nonpreemptive_valid_task_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
   Proof.
     intros; split.
     - by unfold task_rtc_bounded_by_cost.
     - intros j ARR TSK.
-      rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.
+      rewrite -TSK /fully_nonpreemptive.
       edestruct (posnP (job_cost j)) as [ZERO|POS].
       + by rewrite job_rtc_threshold_is_0.
       + by erewrite job_rtc_threshold_is_ε; eauto 2. 

analysis/facts/preemption/rtc_threshold/preemptive.v

@@ -25,7 +25,7 @@ Section TaskRTCThresholdFullyPreemptiveModel.
   Hypothesis H_valid_job_cost:
     arrivals_have_valid_job_costs arr_seq.
 
-  (** Then, we prove that [task_run_to_completion_threshold] function
+  (** Then, we prove that [task_rtct] function
       defines a valid task's run to completion threshold. *)     
   Lemma fully_preemptive_valid_task_run_to_completion_threshold:
     forall tsk, valid_task_run_to_completion_threshold arr_seq tsk.

classic/model/schedule/uni/service.v

@@ -504,7 +504,7 @@ Module Service.
           rewrite /service /service_during (@big_cat_nat _ _ _ t1) //=.
           rewrite (cumulative_service_before_job_arrival_zero
                      job_arrival sched _ j 0 t1) // add0n.
-          rewrite <- sum_majorant_eqn with (F1 := fun j => service_during sched j t1 t_compl)
+          rewrite <- sum_majorant_eqn with (E1 := fun j => service_during sched j t1 t_compl)
                                       (xs := arrivals_between t1 t2) (P := P); try done.
             by intros; apply cumulative_service_le_job_cost.
         } 

doc/guidelines.md

@@ -31,7 +31,7 @@ This project targets Coq *non*-experts. Accordingly, great emphasis is placed on
 ```
 - When commenting, be careful not to leave any misspelled words: Prosa's CI system comprises a spell-checker that will signal errors.
 - When comments have to contain variable names or mathematical notation, use square brackets (e.g. `[job_cost j]`). You can nest square brackets _only if they are balanced_: `[[t1,t2)]` will not work. In this case, use `<<[t1,t2)>>`.
-- The vocabulary of the spell-checker is extended with the words contained in `scripts/wordlist.pws`. Add new words only if strictly necessary.
+- The vocabulary of the spell-checker is extended with the words contained in [`scripts/wordlist.pws`](../scripts/wordlist.pws). Add new words only if strictly necessary.
 - Document the sources of lemmas and theorems in the comments. For example, say something like "Theorem XXX in (Foo & Bar, 2007)", and document at the beginning of the file what "(Foo & Bar, 2007)" refers to.
 
 

doc/tactics.md

@@ -19,19 +19,19 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 
 - `desf_asm`: same as `desf`, but only applied to the assumptions in the local context.
 
-- `exploit H`: When applied to a hypothesis/lemma H, converts pre-conditions into goals in order to infer the post-condition of H, which is then added to the local context.
+- `exploit H`: When applied to a hypothesis/lemma `H`, converts pre-conditions into goals in order to infer the post-condition of `H`, which is then added to the local context.
 
-- `feed H`: Same as exploit, but only generates a goal for the first pre-condition. That is, applying exploit to (H: P1 -> P2 -> P3) produces (H: P2 -> P3) and converts P1 into a goal. This is useful for cleaning up induction hypotheses.
+- `feed H`: Same as exploit, but only generates a goal for the first pre-condition. That is, applying exploit to `H: P1 -> P2 -> P3` produces `H: P2 -> P3` and converts `P1` into a goal. This is useful for cleaning up induction hypotheses.
 
-- `feed_n k H`: Same as feed, but generates goals up to the k-th pre-condition.
+- `feed_n k H`: Same as feed, but generates goals up to the `k`-th pre-condition.
 
-- `specialize (H x1 x2 x3)`: instantiates hypothesis H in place with values x1, x2, x3.
+- `specialize (H x1 x2 x3)`: instantiates hypothesis `H` in place with values `x1`, `x2`, and `x3`.
 
 *To be continued… please help out.*
 
 ## Tactics from `ssreflect`
 
-- `have y := f x1 x2 x3`: Creates an alias to (f x1 x2 x3) called y (in the local context). Note that f can be a function or a proposition/lemma.
+- `have y := f x1 x2 x3`: Creates an alias to `f x1 x2 x3` called `y` (in the local context). Note that `f` can be a function or a proposition/lemma. It's usually easier to read than `move: (f x1 x2 x3) => y`.
 
 *To be written… please feel free to start.*
 
@@ -40,3 +40,7 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 
 *To be written… please feel free to start.*
 
+## Miscellaneous
+
+- `ssrlia`: Solves arithmetic goals, including ones with `ssreflect`'s definitions.
+

model/preemption/parameter.v

@@ -72,10 +72,11 @@ Section MaxAndLastNonpreemptiveSegment.
 
   (** * Run-to-Completion Threshold of a Job *)
 
-  (** Finally, we define the notion of a job's run-to-completion threshold: the
-      run-to-completion threshold is the amount of service after which a job
-      cannot be preempted until its completion. *)
-  Definition job_run_to_completion_threshold (j : Job) :=
+  (** Finally, we define the notion of a job's run-to-completion
+      threshold (RTCT): the run-to-completion threshold is the amount
+      of service after which a job cannot be preempted until its
+      completion. *)
+  Definition job_rtct (j : Job) :=
     job_cost j - (job_last_nonpreemptive_segment j - ε).
 
 End MaxAndLastNonpreemptiveSegment.

model/task/arrival/arrival_curve_to_rbf.v

+Require Export prosa.util.all.
+Require Export prosa.model.task.arrival.request_bound_functions.
+Require Export prosa.model.task.arrival.curves.
+
+(** * Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF) *)
+
+(** Consider any type of tasks with a given cost ... *)
+Context {Task : TaskType} `{TaskCost Task} `{TaskMinCost Task}.
+
+(**  ... and any type of jobs associated with these tasks. *)
+Context {Job : JobType} `{JobTask Job Task} `{JobCost Job}.
+
+(** In the following, we show a way to convert a given arrival curve, 
+    paired with a worst-case/best-case execution time, to a request-bound function. 
+    Definitions and proofs will handle both lower-bounding and upper-bounding arrival 
+    curves. *)
+Section ArrivalCurveToRBF.
+
+  (** Let [MaxArr] and [MinArr] represent two arrivals curves. [MaxArr] upper-bounds 
+      the possible number or arrivals for a given task, whereas [MinArr] lower-bounds it. *)
+  Context `{MaxArr : MaxArrivals Task} `{MinArr : MinArrivals Task}. 
+
+  (** We define the conversion to a request-bound function as the product of the task cost and the 
+      number of arrivals during [Δ]. In the upper-bounding case, the cost of a task will represent 
+      the WCET of its jobs. Symmetrically, in the lower-bounding case, the cost of a task will 
+      represent the BCET of its jobs. *)
+  Definition task_max_rbf (arrivals :  Task -> duration -> nat) task Δ := task_cost task * arrivals task Δ.
+  Definition task_min_rbf (arrivals :  Task -> duration -> nat) task Δ := task_min_cost task * arrivals task Δ.
+  
+  (** Finally, we show that the newly defined functions are indeed request-bound functions. *)
+  Global Program Instance MaxArrivalsRBF : MaxRequestBound Task := task_max_rbf max_arrivals.
+  Global Program Instance MinArrivalsRBF : MinRequestBound Task := task_min_rbf min_arrivals.
+
+  (** In the following section, we prove that the transformation yields a request-bound 
+      function that conserves correctness properties in both the upper-bounding 
+      and lower-bounding cases. *)     
+  Section Facts.
+
+    (** First, we establish the validity of the transformation for a single, given task. *)
+    Section SingleTask.
+
+      (** Consider an arbitrary task [tsk] ... *)
+      Variable tsk : Task.
+      
+      (** ... and any job arrival sequence. *)
+      Variable arr_seq : arrival_sequence Job.
+
+      (** First, note that any valid upper-bounding arrival curve, after being 
+          converted, is a valid request-bound function. *)
+      Theorem valid_arrival_curve_to_max_rbf:
+        forall (arrivals : Task -> duration -> nat),
+        valid_arrival_curve (arrivals tsk) ->
+        valid_request_bound_function ((task_max_rbf arrivals) tsk).
+      Proof.
+        move => ARR [ZERO MONO].
+        split.
+        - by rewrite /task_max_rbf ZERO muln0.
+        - move => x y LEQ.
+          rewrite /task_max_rbf.
+          destruct (task_cost tsk); first by rewrite mul0n.
+          by rewrite leq_pmul2l //; apply MONO.
+      Qed.
+
+      (** The same idea can be applied in the lower-bounding case. *)
+      Theorem valid_arrival_curve_to_min_rbf:
+        forall (arrivals : Task -> duration -> nat),
+          valid_arrival_curve (arrivals tsk) ->
+          valid_request_bound_function ((task_min_rbf arrivals) tsk).
+      Proof.
+        move => ARR [ZERO MONO].
+        split.
+        - by rewrite /task_min_rbf ZERO muln0.
+        - move => x y LEQ.
+          rewrite /task_min_rbf.
+          destruct (task_min_cost tsk); first by rewrite mul0n.
+          by rewrite leq_pmul2l //; apply MONO.
+      Qed.
+      
+      (** Next, we prove that the task respects the request-bound function in 
+          the upper-bounding case. Note that, for this to work, we assume that the 
+          cost of tasks upper-bounds the cost of the jobs belonging to them (i.e., 
+          the task cost is the worst-case). *)
+      Theorem respects_arrival_curve_to_max_rbf:
+        jobs_have_valid_job_costs ->
+        respects_max_arrivals arr_seq tsk (MaxArr tsk) ->
+        respects_max_request_bound arr_seq tsk ((task_max_rbf MaxArr) tsk).
+      Proof.
+        move=> TASK_COST RESPECT t1 t2 LEQ.
+        specialize (RESPECT t1 t2 LEQ).
+        apply leq_trans with (n := task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.
+        - rewrite /max_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.
+          rewrite mem_filter => /andP [/eqP TSK _] _.
+          rewrite -TSK.
+          by apply TASK_COST.
+        - by destruct (task_cost tsk) eqn:C; rewrite /task_max_rbf C // leq_pmul2l.
+      Qed.
+      
+      (** Finally, we prove that the task respects the request-bound function also in 
+          the lower-bounding case. This time, we assume that the cost of tasks lower-bounds 
+          the cost of the jobs belonging to them. (i.e., the task cost is the best-case). *)
+      Theorem respects_arrival_curve_to_min_rbf:
+        jobs_have_valid_min_job_costs ->
+        respects_min_arrivals arr_seq tsk (MinArr tsk) ->
+        respects_min_request_bound arr_seq tsk ((task_min_rbf MinArr) tsk).
+      Proof.
+        move=> TASK_COST RESPECT t1 t2 LEQ.
+        specialize (RESPECT t1 t2 LEQ).
+        apply leq_trans with (n := task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.
+        - by destruct (task_min_cost tsk) eqn:C; rewrite /task_min_rbf C // leq_pmul2l.
+        - rewrite /min_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.
+          rewrite mem_filter => /andP [/eqP TSK _] _.
+          rewrite -TSK.
+          by apply TASK_COST.
+      Qed.
+      
+    End SingleTask.
+
+    (** Next, we lift the results to the previous section to an arbitrary task set. *)
+    Section TaskSet.
+      
+      (** Let [ts] be an arbitrary task set... *)
+      Variable ts : TaskSet Task.
+      
+      (** ... and consider any job arrival sequence. *)
+      Variable arr_seq : arrival_sequence Job.
+
+      (** First, we generalize the validity of the transformation to a task set both in
+          the upper-bounding case ... *)
+      Corollary valid_taskset_arrival_curve_to_max_rbf:
+        valid_taskset_arrival_curve ts MaxArr ->
+        valid_taskset_request_bound_function ts MaxArrivalsRBF.
+      Proof.
+        move=> VALID tsk IN.
+        specialize (VALID tsk IN).
+        by apply valid_arrival_curve_to_max_rbf.
+      Qed.
+      
+      (** ... and in the lower-bounding case. *)
+      Corollary valid_taskset_arrival_curve_to_min_rbf:
+        valid_taskset_arrival_curve ts MinArr ->
+        valid_taskset_request_bound_function ts MinArrivalsRBF.
+      Proof.
+        move=> VALID tsk IN.
+        specialize (VALID tsk IN).
+        by apply valid_arrival_curve_to_min_rbf.
+      Qed.
+      
+      (** Second, we show that a task set that respects a given arrival curve also respects 
+          the produced request-bound function, lifting the result obtained in the single-task 
+          case. The result is valid in the upper-bounding case... *) 
+      Corollary taskset_respects_arrival_curve_to_max_rbf:
+        jobs_have_valid_job_costs ->
+        taskset_respects_max_arrivals arr_seq ts ->
+        taskset_respects_max_request_bound arr_seq ts.
+      Proof.
+        move=> TASK_COST SET_RESPECTS tsk IN.
+        by apply respects_arrival_curve_to_max_rbf, SET_RESPECTS.
+      Qed.
+      
+      (** ...as well as in the lower-bounding case. *)
+      Corollary taskset_respects_arrival_curve_to_min_rbf:
+        jobs_have_valid_min_job_costs ->
+        taskset_respects_min_arrivals arr_seq ts ->
+        taskset_respects_min_request_bound arr_seq ts.
+      Proof.
+        move=> TASK_COST SET_RESPECTS tsk IN.
+        by apply respects_arrival_curve_to_min_rbf, SET_RESPECTS.
+      Qed.
+      
+    End TaskSet.
+
+  End Facts.
+  
+End ArrivalCurveToRBF.