.gitlab-ci.yml

@@ -11,7 +11,7 @@ stages:
     - opam install -y -v -j ${NJOBS} coq-prosa
 
 .preferred-stable-version:
-    image: mathcomp/mathcomp:1.10.0-coq-8.11
+    image: mathcomp/mathcomp:1.12.0-coq-8.13
 
 .build:
   image: mathcomp/mathcomp:${CI_JOB_NAME}
@@ -23,14 +23,14 @@ stages:
 
 .build-for-process:
   stage: build
-  image: mathcomp/mathcomp:1.10.0-coq-8.11
+  image: mathcomp/mathcomp:1.12.0-coq-8.13
   script:
     - ./create_makefile.sh --without-classic
     - make -j ${NJOBS}
 
 .build-for-process-classic:
   stage: build
-  image: mathcomp/mathcomp:1.10.0-coq-8.11
+  image: mathcomp/mathcomp:1.12.0-coq-8.13
   script:
     - ./create_makefile.sh --only-classic
     - make -j ${NJOBS}
@@ -72,6 +72,9 @@ stages:
 1.11.0-coq-8.12:
   extends: .build
 
+1.12.0-coq-8.13:
+  extends: .build
+
 build-for-process:
   extends:
     - .build-for-process
@@ -94,7 +97,7 @@ spell-check:
   script:
     - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`
 
-coq-8.12:
+coq-8.13:
   extends:
     - .build-dev
   # it's ok to fail with an unreleased version of ssreflect

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/definitions/completion_sequence.v

+From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
+Require Import prosa.behavior.service.
+
+(** This module contains basic definitions and properties of job
+    completion sequences. *)
+
+(** * Notion of a Completion Sequence *)
+
+(** We begin by defining a job completion sequence. *)
+Section CompletionSequence.
+
+  (** Consider any kind of jobs with a cost
+     and any kind of processor state. *)
+  Context {Job : JobType} `{JobCost Job} {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** For each instant [t], the completion sequence returns all
+     arrived jobs that have completed at [t]. *)
+  Definition completion_sequence : arrival_sequence Job :=
+    fun t => [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
+
+End CompletionSequence.

analysis/facts/behavior/arrivals.v

@@ -93,6 +93,19 @@ Section Arrived.
     now apply ready_implies_arrived.
   Qed.
 
+  (** Similarly, since backlogged jobs are by definition pending, any
+      backlogged job must be incomplete. *)
+  Lemma backlogged_implies_incomplete:
+    forall j t,
+      backlogged sched j t -> ~~ completed_by sched j t.
+  Proof.
+    move=> j t BACK.
+    have suff: pending sched j t.
+    - by move /andP => [_ INCOMP].
+    - apply; move: BACK => /andP [READY _].
+      by apply any_ready_job_is_pending.
+  Qed.
+
 End Arrived.
 
 (** In this section, we establish useful facts about arrival sequence prefixes. *)

analysis/facts/behavior/completion.v

 Require Export prosa.analysis.facts.behavior.service.
 Require Export prosa.analysis.facts.behavior.arrivals.
 Require Export prosa.analysis.definitions.schedule_prefix.
+Require Export prosa.analysis.definitions.job_properties.
 
 (** * Completion *)
 
 (** In this file, we establish basic facts about job completions. *)
 Section CompletionFacts.
-  
+
   (** Consider any job type,...*)
   Context {Job: JobType}.
   Context `{JobCost Job}.
@@ -18,10 +19,10 @@ Section CompletionFacts.
   (** ...and a given schedule. *)
   Variable sched: schedule PState.
 
-  (** Let j be any job that is to be scheduled. *)
+  (** Let [j] be any job that is to be scheduled. *)
   Variable j: Job.
 
-  (** We prove that after job j completes, it remains completed. *)
+  (** We prove that after job [j] completes, it remains completed. *)
   Lemma completion_monotonic:
     forall t t',
       t <= t' ->
@@ -33,6 +34,19 @@ Section CompletionFacts.
       by apply service_monotonic.
   Qed.
 
+  (** We prove that if [j] is not completed by [t'], then it's also not
+      completed by any earlier instant. *)
+  Lemma incompletion_monotonic:
+    forall t t',
+      t <= t' ->
+      ~~ completed_by sched j t' ->
+      ~~ completed_by sched j t.
+  Proof.
+    move => t t' LE.
+    apply contra.
+    by apply completion_monotonic.
+  Qed.
+
   (** We observe that being incomplete is the same as not having received
      sufficient service yet... *)
   Lemma less_service_than_cost_is_incomplete:
@@ -52,6 +66,19 @@ Section CompletionFacts.
     move=> t. by split; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //.
   Qed.
 
+  (** Trivially, it follows that an incomplete job has a positive cost. *)
+  Corollary incomplete_implies_positive_cost:
+    forall t,
+      ~~ completed_by sched j t ->
+      job_cost_positive j.
+  Proof.
+    move=> t INCOMP.
+    apply: (ltn_leq_trans _);
+      last by apply leq_subr.
+    apply incomplete_is_positive_remaining_cost.
+    exact INCOMP.
+  Qed.
+
   (** Assume that completed jobs do not execute. *)
   Hypothesis H_completed_jobs:
     completed_jobs_dont_execute sched.

analysis/facts/behavior/deadlines.v

@@ -5,7 +5,7 @@ Require Export prosa.analysis.facts.behavior.completion.
 (** In this file, we observe basic properties of the behavioral job
     model w.r.t. deadlines. *)
 Section DeadlineFacts.
-  
+
   (** Consider any given type of jobs with costs and deadlines... *)
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
 
@@ -13,8 +13,51 @@ Section DeadlineFacts.
   Context {PState: eqType}.
   Context `{ProcessorState Job PState}.
 
-  (** We begin with schedules / processor models in which scheduled jobs
-    always receive service. *)
+  (** First, we derive two properties from the fact that a job is incomplete at
+      some point in time. *)
+  Section Incompletion.
+
+    (** Consider any given schedule. *)
+    Variable sched: schedule PState.
+
+    (** Trivially, a job that both meets its deadline and is incomplete at a
+        time [t] must have a deadline later than [t]. *)
+    Lemma incomplete_implies_later_deadline:
+      forall j t,
+        job_meets_deadline sched j ->
+        ~~ completed_by sched j t ->
+        t < job_deadline j.
+    Proof.
+      move=> j t MET INCOMP.
+      apply contraT; rewrite -leqNgt => PAST_DL.
+      have DL_MISS: ~~ completed_by sched j (job_deadline j)
+        by apply incompletion_monotonic with (t' := t) => //.
+      by move: DL_MISS => /negP.
+    Qed.
+
+    (** Furthermore, a job that both meets its deadline and is incomplete at a
+        time [t] must be scheduled at some point between [t] and its
+        deadline. *)
+    Lemma incomplete_implies_scheduled_later:
+      forall j t,
+        job_meets_deadline sched j ->
+        ~~ completed_by sched j t ->
+        exists t', t <= t' < job_deadline j /\ scheduled_at sched j t'.
+    Proof.
+      move=> j t MET INCOMP.
+      apply: cumulative_service_implies_scheduled.
+      rewrite -(ltn_add2l (service sched j t)) addn0.
+      rewrite service_cat;
+        last by (apply ltnW; apply incomplete_implies_later_deadline).
+      apply ltn_leq_trans with (n := job_cost j);
+        first by rewrite less_service_than_cost_is_incomplete.
+      by apply MET.
+    Qed.
+
+  End Incompletion.
+
+  (** Next, we look at schedules / processor models in which scheduled jobs
+      always receive service. *)
   Section IdealProgressSchedules.
 
     (** Consider a given reference schedule... *)
@@ -26,26 +69,19 @@ Section DeadlineFacts.
     (** ...and scheduled jobs always receive service. *)
     Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
 
-    (** We observe that, if a job is known to meet its deadline, then
-       its deadline must be later than any point at which it is
-       scheduled. That is, if a job that meets its deadline is
-       scheduled at time t, we may conclude that its deadline is at a
-       time later than t. *)
+    (** We observe that if a job meets its deadline and is scheduled at time
+        [t], then then its deadline is at a time later than t. *)
     Lemma scheduled_at_implies_later_deadline:
       forall j t,
         job_meets_deadline sched j ->
         scheduled_at sched j t ->
         t < job_deadline j.
     Proof.
-      move=> j t.
-      rewrite /job_meets_deadline => COMP SCHED.
-      case: (boolP (t < job_deadline j)) => //.
-      rewrite -leqNgt => AFTER_DL.
-      apply completion_monotonic with (t' := t) in COMP => //.
-      apply scheduled_implies_not_completed in SCHED => //.
-      move/negP in SCHED. contradiction.
+      move=> j t MET SCHED_AT.
+      apply (incomplete_implies_later_deadline sched) => //.
+      by apply scheduled_implies_not_completed.
     Qed.
-    
+
   End IdealProgressSchedules.
 
   (** In the following section, we observe that it is sufficient to

analysis/facts/edf_definitions.v

+Require Export prosa.analysis.facts.model.ideal_schedule.
+Require Export prosa.analysis.facts.behavior.deadlines.
+Require Export prosa.analysis.definitions.schedulability.
+Require Export prosa.model.priority.edf.
+Require Export prosa.model.schedule.edf.
+Require Export prosa.model.schedule.priority_driven.
+
+(** * Equivalence of EDF Definitions *)
+
+(** Recall that we have defined "EDF schedules" in two ways.
+
+    The generic way to define an EDF schedule is by using the EDF priority
+    policy defined in [model.priority.edf] and the general notion of
+    priority-compliant schedules defined in [model.schedule.priority_driven].
+
+    Another, more straight-forward way to define an EDF schedule is the standalone
+    definition given in [model.schedule.edf], which is less general but simpler
+    and used in the EDF optimality proof.
+
+    In this file, we show that both definitions are equivalent assuming:
+
+    (1) ideal uniprocessor schedules, ... *)
+Require Import prosa.model.processor.ideal.
+
+(** ... (2) the classic Liu & Layland model of readiness without jitter and
+    without self-suspensions, where pending jobs are always ready, and ... *)
+Require Import prosa.model.readiness.basic.
+
+(** ... (3) that jobs are fully preemptive. *)
+Require Import prosa.model.preemption.fully_preemptive.
+
+Section Equivalence.
+
+  (** For any given type of jobs, each characterized by an arrival time,
+      an execution cost, and an absolute deadline, ... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (** ...consider a given valid job arrival sequence ... *)
+  Variable arr_seq: arrival_sequence Job.
+  Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
+
+  (** ...and a corresponding schedule. *)
+  Variable sched : schedule (ideal.processor_state Job).
+
+  (** Suppose jobs don't execute after their completion, ... *)
+  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
+
+  (** ...all jobs come from the arrival sequence [arr_seq], ...*)
+  Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ...and jobs from [arr_seq] don't miss their deadlines. *)
+  Hypothesis H_no_deadline_misses: all_deadlines_of_arrivals_met arr_seq sched.
+
+  (** We first show that a schedule that satisfies the standalone
+      [EDF_schedule] predicate is also compliant with the generic notion of EDF
+      policy defined in Prosa, namely the [respects_policy_at_preemption_point]
+      predicate. *)
+  Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
+    EDF_schedule sched ->
+    respects_policy_at_preemption_point arr_seq sched.
+  Proof.
+    move=> EDF j' j t ARR PREEMPTION BL SCHED.
+    have suff: exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t'.
+    { move=> [t' [/andP [LE _] SCHED']].
+      apply: (EDF t); [done | exact LE | exact SCHED' |].
+      by apply: (backlogged_implies_arrived sched j' t). }
+    apply; apply: incomplete_implies_scheduled_later;
+      first by apply: H_no_deadline_misses => //.
+    by apply: (backlogged_implies_incomplete sched j' t).
+  Qed.
+
+  (** Conversely, the reverse direction also holds: a schedule that satisfies
+      the [respects_policy_at_preemption_point] predicate is also an EDF
+      schedule in the sense of [EDF_schedule]. *)
+  Lemma respects_policy_at_preemption_point_implies_EDF_schedule :
+    respects_policy_at_preemption_point arr_seq sched ->
+    EDF_schedule sched.
+  Proof.
+    move=> H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.
+    case (boolP (j == j_hp)); first by move /eqP => EQ; subst.
+    move /neqP => NEQ.
+    exploit (H_priority_driven j j_hp t) => //.
+    { by apply (H_from_arr_seq _ _ SCHED'). }
+    { by rewrite /preemption_time; destruct (sched t). }
+    { apply /andP; split => //.
+      - apply /andP; split => //.
+        apply (incompletion_monotonic _ j _ _ LEQ).
+        apply scheduled_implies_not_completed => //.
+        by apply ideal_proc_model_ensures_ideal_progress.
+      - apply /negP; move => SCHED''.
+        by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }
+  Qed.
+
+  (** From the two preceding lemmas, it follows immediately that the two EDF
+      definitions are indeed equivalent, which we note with the following
+      corollary. *)
+  Corollary EDF_schedule_equiv:
+    EDF_schedule sched <-> respects_policy_at_preemption_point arr_seq sched.
+  Proof.
+    split.
+    - by apply EDF_schedule_implies_respects_policy_at_preemption_point.
+    - by apply respects_policy_at_preemption_point_implies_EDF_schedule.
+  Qed.
+
+End Equivalence.

analysis/facts/hyperperiod.v

@@ -210,7 +210,7 @@ Section PeriodicLemmas.
       now apply leq_trunc_div.
     + specialize (div_floor_add_g (job_arrival j1 - O_max) HP) => AB.
       feed_n 1 AB; first by apply valid_periods_imply_pos_hp => //.
-      apply ltn_subLR in AB.
+      rewrite ltn_subLR // in AB.
       now rewrite -/(HP); ssrlia.
   Qed.
 

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