Major Changes in RTA and Directory Structure

- Removed unnecessary assumption in RTA about task precedence/no intra-task parallelism.
- Scheduler models and analyses are organized in separate modules/folders.
- Added RTA for FP and EDF for schedulers with release jitter.
- The scheduling invariants were split into more fine-grained assumptions:
  (a) scheduler is work-conserving
  (b) scheduler enforces FP/JLDP priority X
- New helper lemmas about counting, and sorted/uniq lists
- Inclusion of tactics feed and feed_n (see documentation).
- Added a Makefile generator

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile arrival_sequence.v bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_theory.v interference_bound_edf.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_bound.v workload.v 
+# coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./model/basic/schedulability.v ./model/basic/interference_bound_edf.v ./model/basic/task.v ./model/basic/interference_bound_fp.v ./model/basic/task_arrival.v ./model/basic/interference_bound.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/basic/workload_bound.v ./model/jitter/schedulability.v ./model/jitter/interference_bound_edf.v ./model/jitter/task.v ./model/jitter/interference_bound_fp.v ./model/jitter/task_arrival.v ./model/jitter/interference_bound.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v ./model/jitter/workload_bound.v -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
 #                        #
 ##########################
 
-COQLIBS?=-I . 
-COQDOCLIBS?=
+COQLIBS?= -R . rt
+COQDOCLIBS?=-R . rt
 
 ##########################
 #                        #
@@ -80,35 +80,57 @@ endif
 #                    #
 ######################
 
-VFILES:=arrival_sequence.v\
-  bertogna_edf_comp.v\
-  bertogna_edf_theory.v\
-  bertogna_fp_comp.v\
-  bertogna_fp_theory.v\
-  interference_bound_edf.v\
-  interference.v\
-  interference_edf.v\
-  job.v\
-  platform.v\
-  platform_edf.v\
-  priority.v\
-  response_time.v\
-  schedulability.v\
-  schedule.v\
-  ssromega.v\
-  task_arrival.v\
-  task.v\
-  util_divround.v\
-  util_lemmas.v\
-  Vbase.v\
-  workload_bound.v\
-  workload.v
+VFILES:=util/ssromega.v\
+  util/lemmas.v\
+  util/Vbase.v\
+  util/divround.v\
+  analysis/basic/bertogna_fp_theory.v\
+  analysis/basic/bertogna_edf_comp.v\
+  analysis/basic/bertogna_fp_comp.v\
+  analysis/basic/bertogna_edf_theory.v\
+  analysis/jitter/bertogna_fp_theory.v\
+  analysis/jitter/bertogna_edf_comp.v\
+  analysis/jitter/bertogna_fp_comp.v\
+  analysis/jitter/bertogna_edf_theory.v\
+  model/basic/schedulability.v\
+  model/basic/interference_bound_edf.v\
+  model/basic/task.v\
+  model/basic/interference_bound_fp.v\
+  model/basic/task_arrival.v\
+  model/basic/interference_bound.v\
+  model/basic/platform.v\
+  model/basic/schedule.v\
+  model/basic/priority.v\
+  model/basic/interference_edf.v\
+  model/basic/interference.v\
+  model/basic/workload.v\
+  model/basic/job.v\
+  model/basic/arrival_sequence.v\
+  model/basic/response_time.v\
+  model/basic/platform_fp.v\
+  model/basic/workload_bound.v\
+  model/jitter/schedulability.v\
+  model/jitter/interference_bound_edf.v\
+  model/jitter/task.v\
+  model/jitter/interference_bound_fp.v\
+  model/jitter/task_arrival.v\
+  model/jitter/interference_bound.v\
+  model/jitter/platform.v\
+  model/jitter/schedule.v\
+  model/jitter/priority.v\
+  model/jitter/interference_edf.v\
+  model/jitter/interference.v\
+  model/jitter/workload.v\
+  model/jitter/job.v\
+  model/jitter/arrival_sequence.v\
+  model/jitter/response_time.v\
+  model/jitter/platform_fp.v\
+  model/jitter/workload_bound.v
 
 -include $(addsuffix .d,$(VFILES))
 .SECONDARY: $(addsuffix .d,$(VFILES))
 
 VOFILES:=$(VFILES:.v=.vo)
-VOFILESINC=$(filter $(wildcard ./*),$(VOFILES)) 
 GLOBFILES:=$(VFILES:.v=.glob)
 VIFILES:=$(VFILES:.v=.vi)
 GFILES:=$(VFILES:.v=.g)
@@ -178,15 +200,15 @@ userinstall:
 	+$(MAKE) USERINSTALL=true install
 
 install:
-	install -d $(DSTROOT)$(COQLIBINSTALL)/$(INSTALLDEFAULTROOT); \
-	for i in $(VOFILESINC); do \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/$(INSTALLDEFAULTROOT)/`basename $$i`; \
+	for i in $(VOFILES); do \
+	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/rt/$$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/rt/$$i; \
 	done
 
 install-doc:
-	install -d $(DSTROOT)$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/html
+	install -d $(DSTROOT)$(COQDOCINSTALL)/rt/html
 	for i in html/*; do \
-	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/$$i;\
+	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/rt/$$i;\
 	done
 
 clean:

bertogna_edf_theory.v → analysis/basic/bertogna_edf_theory.v

-Require Import Vbase task job task_arrival schedule platform interference
-        workload workload_bound schedulability priority platform
-        platform_edf response_time
-        bertogna_fp_theory interference_bound_edf util_divround util_lemmas
-        ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+Add LoadPath "../.." as rt.
+Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
+Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
+               rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
+               rt.model.basic.workload rt.model.basic.workload_bound rt.model.basic.schedulability
+               rt.model.basic.priority rt.model.basic.platform rt.model.basic.response_time
+               rt.model.basic.interference_bound_edf.
+Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
 
-  Import Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime
-         Priority SporadicTaskArrival WorkloadBound EDFSpecificBound ResponseTimeAnalysisFP
-         PlatformEDF.
-
-  (* In the following section, we define Bertogna and Cirinei's
-     interference bound for EDF scheduling. *)
-  Section TotalInterferenceBoundEDF.
-
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> nat.
-    Variable task_period: sporadic_task -> nat.
-    Variable task_deadline: sporadic_task -> nat.
-    
-    (* Let tsk be the task to be analyzed. *)
-    Variable tsk: sporadic_task.
-
-    Let task_with_response_time := (sporadic_task * time)%type.
-    
-    (* Assume a known response-time bound for each interfering task ... *)
-    Variable R_prev: seq task_with_response_time.
-
-    (* ... and an interval length delta. *)
-    Variable delta: time.
-
-    Section PerTask.
-
-      Variable tsk_R: task_with_response_time.
-      Let tsk_other := fst tsk_R.
-      Let R_other := snd tsk_R.
-
-      (* By combining Bertogna's interference bound for a work-conserving
-         scheduler ... *)
-      Let basic_interference_bound := interference_bound_fp task_cost task_period tsk delta tsk_R.
-
-      (* ... with and EDF-specific interference bound, ... *)
-      Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
-
-      (* Bertogna and Cirinei define the following interference bound
-         under EDF scheduling. *)
-      Definition interference_bound_edf :=
-        minn basic_interference_bound edf_specific_bound.
-
-    End PerTask.
-
-    Section AllTasks.
-
-      Let interferes_with_tsk := is_interfering_task_jlfp tsk.
-      
-      (* The total interference incurred by tsk is bounded by the sum
-         of individual task interferences. *)
-      Definition total_interference_bound_edf :=
-        \sum_((tsk_other, R_other) <- R_prev | interferes_with_tsk tsk_other)
-           interference_bound_edf (tsk_other, R_other).
-
-    End AllTasks.
-
-  End TotalInterferenceBoundEDF.
+  Export Job SporadicTaskset Schedule ScheduleOfSporadicTask Workload Schedulability ResponseTime
+         Priority SporadicTaskArrival WorkloadBound InterferenceBoundEDF
+         Interference Platform.
 
   (* In this section, we prove that Bertogna and Cirinei's RTA yields
      safe response-time bounds. *)
@@ -106,16 +55,6 @@ Module ResponseTimeAnalysisEDF.
     Hypothesis H_at_least_one_cpu :
       num_cpus > 0.
 
-    (* In order not to overcount job interference, we assume that
-       jobs of the same task do not execute in parallel.
-       Note that under EDF, this is equivalent to task precedence
-       constraints.
-       This is required because our proof uses a definition of
-       interference based on the sum of the individual contributions
-       of each job: I_total = I_j1 + I_j2 + ... *)
-    Hypothesis H_no_intra_task_parallelism:
-      jobs_of_same_task_dont_execute_in_parallel job_task sched.
-
     (* Assume that we have a task set where all tasks have valid
        parameters and restricted deadlines. *)
     Variable ts: taskset_of sporadic_task.
@@ -151,14 +90,9 @@ Module ResponseTimeAnalysisEDF.
       forall tsk_other R,
         (tsk_other, R) \in rt_bounds -> R <= task_deadline tsk_other.
 
-    Let higher_eq_priority := @EDF Job arr_seq job_deadline. (* TODO: implicit params broken *)
-
-    (* Assume that the schedule satisfies the global scheduling invariant
-       for EDF, i.e., if any job of tsk is backlogged, every processor
-       must be busy with jobs with no larger absolute deadline. *)
-    Hypothesis H_global_scheduling_invariant:
-      JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus sched higher_eq_priority.
-
+    (* Assume that we have a work-conserving EDF scheduler. *)
+    Hypothesis H_work_conserving: work_conserving job_cost sched.
+    Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
     
     (* Assume that the task set has no duplicates. Otherwise, counting
        the number of tasks that have some property does not make sense
@@ -210,7 +144,7 @@ Module ResponseTimeAnalysisEDF.
         interference_bound_edf task_cost task_period task_deadline tsk R (tsk_other, R_other). 
       
       (* Also, let ts_interf be the subset of tasks that interfere with tsk. *)
-      Let ts_interf := [seq tsk_other <- ts | is_interfering_task_jlfp tsk tsk_other].
+      Let ts_interf := [seq tsk_other <- ts | jldp_can_interfere_with tsk tsk_other].
 
       Section LemmasAboutInterferingTasks.
         
@@ -276,7 +210,8 @@ Module ResponseTimeAnalysisEDF.
       (* Next we prove some lemmas that help to derive a contradiction.*)
       Section DerivingContradiction.
 
-      (* 1) Since job j did not complete by its response time bound, it follows that
+        
+      (* 0) Since job j did not complete by its response time bound, it follows that
             the total interference X >= R - e_k + 1. *)
       Lemma bertogna_edf_too_much_interference : X >= R - task_cost tsk + 1.
       Proof.
@@ -323,60 +258,87 @@ Module ResponseTimeAnalysisEDF.
         }
       Qed.
 
+      Let scheduled_task_other_than_tsk (t: time) (tsk_other: sporadic_task) :=
+        task_is_scheduled job_task sched tsk_other t &&
+        jldp_can_interfere_with tsk tsk_other.
+      
+      (* 1) At all times that j is backlogged, all processors are busy with other tasks. *)
+      Lemma bertogna_edf_scheduling_invariant:
+        forall t,
+          job_arrival j <= t < job_arrival j + R ->
+          backlogged job_cost sched j t ->
+          count (scheduled_task_other_than_tsk t) ts = num_cpus.
+      Proof.
+        rename H_all_jobs_from_taskset into FROMTS,
+               H_valid_task_parameters into PARAMS,
+               H_job_of_tsk into JOBtsk,
+               H_sporadic_tasks into SPO,
+               H_tsk_R_in_rt_bounds into INbounds,
+               H_all_previous_jobs_completed_on_time into BEFOREok,
+               H_tasks_miss_no_deadlines into NOMISS,
+               H_rt_bounds_contains_all_tasks into UNZIP,
+               H_restricted_deadlines into RESTR,
+               H_work_conserving into WORK.
+        unfold x, X, total_interference, task_interference.
+        move => t /andP [LEt LTt] BACK.
+        unfold scheduled_task_other_than_tsk in *.
+        eapply platform_cpus_busy_with_interfering_tasks; try (by done);
+          [ by apply WORK | by apply SPO 
+          | apply PARAMS; rewrite -JOBtsk; apply FROMTS
+          | by apply JOBtsk | by apply BACK | ].
+        {
+          intros j0 tsk0 TSK0 LE.
+          cut (tsk0 \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP -TSK0 FROMTS].
+          move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
+          apply completion_monotonic with (t0 := job_arrival j0 + R0); try (by done).
+          {
+            rewrite leq_add2l TSK0.
+            apply leq_trans with (n := task_deadline tsk0); first by apply NOMISS.
+            by apply RESTR; rewrite -TSK0 FROMTS.
+          }
+          {
+            apply BEFOREok with (tsk_other := tsk0); try (by done).
+            apply leq_ltn_trans with (n := t); last by done.
+            apply leq_trans with (n := job_arrival j0 + task_period tsk0); last by done.
+            rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk0); first by apply NOMISS.
+            by apply RESTR; rewrite -TSK0 FROMTS.
+          }
+        }
+      Qed.
+      
       (* 2) Next, we prove that the sum of the interference of each task is equal
             to the total interference multiplied by the number of processors. This
             holds because interference only occurs when all processors are busy. *)
       Lemma bertogna_edf_all_cpus_busy :
         \sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
       Proof.
-        rename H_global_scheduling_invariant into INV,
-               H_all_jobs_from_taskset into FROMTS,
+        rename H_all_jobs_from_taskset into FROMTS,
                H_valid_task_parameters into PARAMS,
                H_job_of_tsk into JOBtsk,
                H_sporadic_tasks into SPO,
                H_tsk_R_in_rt_bounds into INbounds,
                H_all_previous_jobs_completed_on_time into BEFOREok,
                H_tasks_miss_no_deadlines into NOMISS,
+               H_rt_bounds_contains_all_tasks into UNZIP,
                H_restricted_deadlines into RESTR.
         unfold sporadic_task_model in *.
         unfold x, X, total_interference, task_interference.
         rewrite -big_mkcond -exchange_big big_distrl /=.
         rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _) _]big_mkcond.
-        apply eq_big_nat; move => t /andP [LEt LTt].
+        apply eq_big_nat; move => t LEt.
         destruct (backlogged job_cost sched j t) eqn:BACK;
           last by rewrite (eq_bigr (fun i => 0));
             [by rewrite big_const_seq iter_addn mul0n addn0 | by done].
         rewrite big_mkcond mul1n /=.
         rewrite big_filter big_mkcond.
-        rewrite (eq_bigr (fun i => if (is_interfering_task_jlfp tsk i &&
-                    task_is_scheduled job_task sched i t) then 1 else 0));
-          last by intro i; clear -i; desf.
-        rewrite -big_mkcond sum1_count.
-        eapply cpus_busy_with_interfering_tasks; try (by done);
-          [ by apply INV
-          | by red; apply SPO
-          | by apply PARAMS; rewrite -JOBtsk FROMTS
-          | by apply JOBtsk
-          | by apply BACK | ].
+        rewrite (eq_bigr (fun i => if (scheduled_task_other_than_tsk t i) then 1 else 0));
+          last first.
         {
-          intros j0 TSK0 LT0.
-          unfold pending in *.
-          apply completion_monotonic with (t0 := job_arrival j0 + R);
-            try (by done).
-          {
-            apply leq_trans with (n := job_arrival j); last by done.
-            apply leq_trans with (n := job_arrival j0 + task_period tsk).
-            {
-              rewrite leq_add2l.
-              apply leq_trans with (n := task_deadline tsk);
-                [by apply NOMISS | by apply RESTR; rewrite -JOBtsk FROMTS].
-            }
-            rewrite -TSK0; apply SPO;
-              [| by rewrite JOBtsk TSK0 | by apply ltnW ].
-            by unfold not; intro BUG; rewrite BUG ltnn in LT0.
-          }
-          by apply BEFOREok with (tsk_other := tsk); rewrite ?ltn_add2r.
+          unfold scheduled_task_other_than_tsk; intros i _; clear -i.
+          by destruct (task_is_scheduled job_task sched i t); rewrite ?andFb ?andTb ?andbT //; desf.
         }
+        rewrite -big_mkcond sum1_count.
+        by apply bertogna_edf_scheduling_invariant.
       Qed.
 
       (* Let (cardGE delta) be the number of interfering tasks whose interference
@@ -391,8 +353,7 @@ Module ResponseTimeAnalysisEDF.
           cardGE delta > 0 ->
           \sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
       Proof.
-        rename H_global_scheduling_invariant into INV,
-               H_all_jobs_from_taskset into FROMTS,
+        rename H_all_jobs_from_taskset into FROMTS,
                H_valid_task_parameters into PARAMS,
                H_job_of_tsk into JOBtsk,
                H_sporadic_tasks into SPO,
@@ -431,7 +392,8 @@ Module ResponseTimeAnalysisEDF.
                                    total_interference_B t).
         {
           rewrite big_distrl /=.
-          apply leq_sum; intros t _.
+          rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
+          apply leq_sum; move => t /andP [LEt _].
           unfold some_interference_A, total_interference_B. 
           destruct (backlogged job_cost sched j t) eqn:BACK;
             [rewrite andTb mul1n | by done].
@@ -441,33 +403,8 @@ Module ResponseTimeAnalysisEDF.
           rewrite mul1n; move: HAS => /hasP HAS.
           destruct HAS as [tsk_k INk LEk].
 
-          generalize INV; intro COUNT.
-          apply cpus_busy_with_interfering_tasks with
-            (job_task0:=job_task) (ts0:=ts) (j0:=j) (tsk0:=tsk) (t0:=t)
-            (task_cost0 := task_cost) (task_period0 := task_period)
-            (task_deadline0 := task_deadline) in COUNT; try (by done);
-          [| by apply PARAMS; rewrite -JOBtsk FROMTS | ]; last first.
-          {
-            intros j0 TSK0 LT0.
-            unfold pending in *.
-            apply completion_monotonic with (t0 := job_arrival j0 + R);
-              try (by done).
-            {
-              move: BACK => /andP [/andP [ARRIVED NOTCOMP] NOTSCHED].
-              apply leq_trans with (n := job_arrival j); last by done.
-              apply leq_trans with (n := job_arrival j0 + task_period tsk).
-              {
-                rewrite leq_add2l.
-                apply leq_trans with (n := task_deadline tsk);
-                  [by apply NOMISS | by apply RESTR; rewrite -JOBtsk FROMTS].
-              }
-              rewrite -TSK0; apply SPO;
-                [| by rewrite JOBtsk TSK0 | by apply ltnW ].
-              by unfold not; intro BUG; rewrite BUG ltnn in LT0.
-            }
-            by apply BEFOREok with (tsk_other := tsk); rewrite ?ltn_add2r.
-          }
-        
+          have COUNT := bertogna_edf_scheduling_invariant t LEt BACK.
+               
           unfold cardGE.
           set interfering_tasks_at_t :=
             [seq tsk_k <- ts_interf | task_is_scheduled job_task
@@ -578,7 +515,7 @@ Module ResponseTimeAnalysisEDF.
             is not enough to cover the sum of the "minimum" term over
             all tasks (artifact of the proof by contradiction). *)
       Lemma bertogna_edf_sum_exceeds_total_interference:
-        \sum_((tsk_other, R_other) <- rt_bounds | is_interfering_task_jlfp tsk tsk_other)
+        \sum_((tsk_other, R_other) <- rt_bounds | jldp_can_interfere_with tsk tsk_other)
           minn (x tsk_other) (R - task_cost tsk + 1) > I tsk R.
       Proof.
         rename H_rt_bounds_contains_all_tasks into UNZIP,
@@ -590,15 +527,15 @@ Module ResponseTimeAnalysisEDF.
           rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
             last by ins; destruct i.
           move: UNZIP => UNZIP.
-          assert (FILTER: filter (is_interfering_task_jlfp tsk) (unzip1 rt_bounds) =
-                          filter (is_interfering_task_jlfp tsk) ts).
+          assert (FILTER: filter (jldp_can_interfere_with tsk) (unzip1 rt_bounds) =
+                          filter (jldp_can_interfere_with tsk) ts).
             by f_equal.
           unfold ts_interf; rewrite -FILTER; clear FILTER.
           rewrite -[\sum_(_ <- rt_bounds | _)_]big_filter.
           assert (SUBST: [seq i <- rt_bounds
                  | let '(tsk_other, _) := i in
-                        is_interfering_task_jlfp tsk tsk_other] = [seq i <- rt_bounds
-                           | is_interfering_task_jlfp tsk (fst i)]).
+                        jldp_can_interfere_with tsk tsk_other] = [seq i <- rt_bounds
+                           | jldp_can_interfere_with tsk (fst i)]).
           {
             by apply eq_filter; red; intro i; destruct i.
           } rewrite SUBST; clear SUBST.         
@@ -629,7 +566,7 @@ Module ResponseTimeAnalysisEDF.
         rename H_rt_bounds_contains_all_tasks into UNZIP.
         assert (HAS: has (fun tup : task_with_response_time =>
                             let (tsk_other, R_other) := tup in
-                            (tsk_other \in ts) && is_interfering_task_jlfp tsk tsk_other &&
+                            (tsk_other \in ts) && jldp_can_interfere_with tsk tsk_other &&
                               (minn (x tsk_other) (R - task_cost tsk + 1)  >
                               interference_bound tsk_other R_other))
                          rt_bounds).
@@ -713,7 +650,7 @@ Module ResponseTimeAnalysisEDF.
           by ins; apply IH with (tsk := tsk_other) (R := R_other).
         } 
         intro EX; destruct EX as [tsk_other [R_other [HP LTmin]]].
-        unfold interference_bound_edf, interference_bound_fp in LTmin.
+        unfold interference_bound_edf, interference_bound_generic in LTmin.
         rewrite minnAC in LTmin; apply min_lt_same in LTmin.
         have BASICBOUND := bertogna_edf_workload_bounds_interference R' j BEFOREok tsk_other R_other HP.
         have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' INbounds j JOBtsk BEFOREok tsk_other R_other HP).

bertogna_edf_comp.v → analysis/jitter/bertogna_edf_comp.v

-Require Import Vbase task job task_arrival schedule platform interference
-        workload workload_bound schedulability priority response_time
-        bertogna_fp_theory bertogna_edf_theory interference_bound_edf util_divround util_lemmas
-        ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+Add LoadPath "../.." as rt.
+Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
+Require Import rt.analysis.jitter.bertogna_edf_theory.
+Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
 
-  Import Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime
-         Priority SporadicTaskArrival WorkloadBound EDFSpecificBound ResponseTimeAnalysisFP
-         ResponseTimeAnalysisEDF.
+  Import ResponseTimeAnalysisEDFJitter.
 
   (* In this section, we define the algorithm of Bertogna and Cirinei's
      response-time analysis for EDF scheduling. *)
@@ -17,6 +15,7 @@ Module ResponseTimeIterationEDF.
     Variable task_cost: sporadic_task -> nat.
     Variable task_period: sporadic_task -> nat.
     Variable task_deadline: sporadic_task -> nat.
+    Variable task_jitter: sporadic_task -> nat.
 
     (* During the iterations of the algorithm, we pass around pairs
        of tasks and computed response-time bounds. *)
@@ -26,6 +25,7 @@ Module ResponseTimeIterationEDF.
     Variable job_cost: Job -> nat.
     Variable job_deadline: Job -> nat.
     Variable job_task: Job -> sporadic_task.
+    Variable job_jitter: Job -> nat.
 
     (* Consider a platform with num_cpus processors. *)  
     Variable num_cpus: nat.
@@ -33,18 +33,18 @@ Module ResponseTimeIterationEDF.
     (* First, recall the interference bound under EDF, ... *)
     Let I (rt_bounds: seq task_with_response_time)
           (tsk: sporadic_task) (delta: time) :=
-      total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
+      total_interference_bound_edf task_cost task_period task_deadline task_jitter tsk rt_bounds delta.
 
     (* ..., which yields the following response-time bound. *)
     Definition edf_response_time_bound (rt_bounds: seq task_with_response_time)
                                            (tsk: sporadic_task) (delta: time) :=
       task_cost tsk + div_floor (I rt_bounds tsk delta) num_cpus.
 
-    (* Also note that a response-time is only valid if it is no larger
+    (* Also note that a response-time R is only valid if R + jitter is no larger
        than the deadline. *)
-    Definition R_le_deadline (pair: task_with_response_time) :=
+    Definition jitter_plus_R_le_deadline (pair: task_with_response_time) :=
       let (tsk, R) := pair in
-        R <= task_deadline tsk.
+        task_jitter tsk + R <= task_deadline tsk.
 
     (* Next we define the fixed-point iteration for computing
        Bertogna's response-time bound of a task set. *)
@@ -80,7 +80,7 @@ Module ResponseTimeIterationEDF.
        valid. *)
     Definition edf_claimed_bounds (ts: taskset_of sporadic_task) :=
       let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
-        if (all R_le_deadline R_values) then
+        if (all jitter_plus_R_le_deadline R_values) then
           Some R_values
         else None.
 
@@ -159,10 +159,10 @@ Module ResponseTimeIterationEDF.
         forall ts rt_bounds tsk R,
           edf_claimed_bounds ts = Some rt_bounds ->
           (tsk, R) \in rt_bounds ->
-          R <= task_deadline tsk.
+          task_jitter tsk + R <= task_deadline tsk.
       Proof.
         intros ts rt_bounds tsk R SOME PAIR; unfold edf_claimed_bounds in SOME.
-        destruct (all R_le_deadline (iter (max_steps ts)
+        destruct (all jitter_plus_R_le_deadline (iter (max_steps ts)
                                           edf_rta_iteration (initial_state ts))) eqn:DEADLINE;
           last by done.
         move: DEADLINE => /allP DEADLINE.
@@ -180,7 +180,7 @@ Module ResponseTimeIterationEDF.
       Proof.
         intros ts rt_bounds tsk SOME IN.
         unfold edf_claimed_bounds in SOME.
-        destruct (all R_le_deadline (iter (max_steps ts) edf_rta_iteration (initial_state ts)));
+        destruct (all jitter_plus_R_le_deadline (iter (max_steps ts) edf_rta_iteration (initial_state ts)));
           last by done.
         inversion SOME as [EQ]; clear SOME EQ.
         generalize dependent tsk.
@@ -218,22 +218,22 @@ Module ResponseTimeIterationEDF.
       Hypothesis H_cost_le_rt_bound: task_cost tsk_other <= R.
 
       Lemma interference_bound_edf_monotonic :
-        interference_bound_edf task_cost task_period task_deadline tsk delta (tsk_other, R) <=
-        interference_bound_edf task_cost task_period task_deadline tsk delta' (tsk_other, R').
+        interference_bound_edf task_cost task_period task_deadline task_jitter tsk delta (tsk_other, R) <=
+        interference_bound_edf task_cost task_period task_deadline task_jitter tsk delta' (tsk_other, R').
       Proof.
         rename H_response_time_monotonic into LEr, H_delta_monotonic into LEx,
                H_cost_le_rt_bound into LEcost, H_period_positive into GEperiod.
-        unfold interference_bound_edf, interference_bound_fp.
+        unfold interference_bound_edf, interference_bound_generic.
         rewrite leq_min; apply/andP; split.
         {
           rewrite leq_min; apply/andP; split.
-          apply leq_trans with (n :=  (minn (W task_cost task_period (fst (tsk_other, R))
+          apply leq_trans with (n :=  (minn (W_jitter task_cost task_period task_jitter (fst (tsk_other, R))
                              (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1)));
             first by apply geq_minl.
-          apply leq_trans with (n := W task_cost task_period (fst (tsk_other, R))
+          apply leq_trans with (n := W_jitter task_cost task_period task_jitter (fst (tsk_other, R))
                                                      (snd (tsk_other, R)) delta);
             [by apply geq_minl | by apply W_monotonic].
-          apply leq_trans with (n := minn (W task_cost task_period (fst (tsk_other, R)) (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1));
+          apply leq_trans with (n := minn (W_jitter task_cost task_period task_jitter (fst (tsk_other, R)) (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1));
             first by apply geq_minl.
           apply leq_trans with (n := delta - task_cost tsk + 1);
             first by apply geq_minr.
@@ -241,13 +241,13 @@ Module ResponseTimeIterationEDF.
         }
         {
           apply leq_trans with (n := edf_specific_interference_bound task_cost task_period
-                                                            task_deadline tsk tsk_other R);
+                                                            task_deadline task_jitter tsk tsk_other R);
             first by apply geq_minr.
           unfold edf_specific_interference_bound; simpl.
           rewrite leq_add2l leq_min; apply/andP; split; first by apply geq_minl.
           apply leq_trans with (n := task_deadline tsk %% task_period tsk_other -
-                                     (task_deadline tsk_other - R));
-            [by apply geq_minr | by rewrite 2?leq_sub2l].
+                                     (task_deadline tsk_other - R - task_jitter tsk_other));
+            [by apply geq_minr | by rewrite 2?leq_sub2l 2?leq_sub2r // leq_sub2l].
         }
       Qed.
 
@@ -442,12 +442,12 @@ Module ResponseTimeIterationEDF.
 
           assert (SUBST: forall l delta,
                     \sum_(j <- l | let '(tsk_other, _) := j in
-                      is_interfering_task_jlfp tsk_i tsk_other)
+                      jldp_can_interfere_with tsk_i tsk_other)
                         (let '(tsk_other, R_other) := j in
-                          interference_bound_edf task_cost task_period task_deadline tsk_i delta
+                          interference_bound_edf task_cost task_period task_deadline task_jitter tsk_i delta
                             (tsk_other, R_other)) =
-                    \sum_(j <- l | is_interfering_task_jlfp tsk_i (fst j))
-                      interference_bound_edf task_cost task_period task_deadline tsk_i delta j).
+                    \sum_(j <- l | jldp_can_interfere_with tsk_i (fst j))
+                      interference_bound_edf task_cost task_period task_deadline task_jitter tsk_i delta j).
           {
             intros l x; clear -l.
             induction l; first by rewrite 2!big_nil.
@@ -491,13 +491,13 @@ Module ResponseTimeIterationEDF.
           }
           move: GE_COST => /allP GE_COST.
 
-          assert (LESUM: \sum_(j <- x1' | is_interfering_task_jlfp tsk_i (fst j))
-                        interference_bound_edf task_cost task_period task_deadline tsk_i delta j <=                                  \sum_(j <- x2' | is_interfering_task_jlfp tsk_i (fst j))
-                        interference_bound_edf task_cost task_period task_deadline tsk_i delta' j).
+          assert (LESUM: \sum_(j <- x1' | jldp_can_interfere_with tsk_i (fst j))
+                        interference_bound_edf task_cost task_period task_deadline task_jitter tsk_i delta j <=                                  \sum_(j <- x2' | jldp_can_interfere_with tsk_i (fst j))
+                        interference_bound_edf task_cost task_period task_deadline task_jitter tsk_i delta' j).
           {
             set elem := (tsk0, R0); rewrite 2!(big_nth elem).
             rewrite -SIZE.
-            rewrite big_mkcond [\sum_(_ <- _ | is_interfering_task_jlfp _ _)_]big_mkcond.
+            rewrite big_mkcond [\sum_(_ <- _ | jldp_can_interfere_with _ _)_]big_mkcond.
             rewrite big_seq_cond [\sum_(_ <- _ | true) _]big_seq_cond.
             apply leq_sum; intros j; rewrite andbT; intros INj.
             rewrite mem_iota add0n subn0 in INj; move: INj => /andP [_ INj].
@@ -506,7 +506,7 @@ Module ResponseTimeIterationEDF.
               have MAP := @nth_map _ elem _ tsk0 (fun x => fst x).
               by rewrite -2?MAP -?SIZE //; f_equal.
             } rewrite -FSTeq.
-            destruct (is_interfering_task_jlfp tsk_i (fst (nth elem x1' j))) eqn:INTERF;
+            destruct (jldp_can_interfere_with tsk_i (fst (nth elem x1' j))) eqn:INTERF;
               last by done.
             {
               exploit (LE elem); [by rewrite /= SIZE | | intro LEj].
@@ -530,7 +530,7 @@ Module ResponseTimeIterationEDF.
               by apply interference_bound_edf_monotonic.
             }
           }
-          destruct (is_interfering_task_jlfp tsk_i tsk0) eqn:INTERFtsk0; last by done.
+          destruct (jldp_can_interfere_with tsk_i tsk0) eqn:INTERFtsk0; last by done.
           apply leq_add; last by done.
           {             
             exploit (LE (tsk0, R0)); [by rewrite /= SIZE | | intro LEj];
@@ -831,8 +831,9 @@ Module ResponseTimeIterationEDF.
           rewrite UNZIP in MAP; rewrite MAP.
           rewrite big_seq_cond [\sum_(_ <- _|true)_]big_seq_cond.
           apply leq_sum; intro i; rewrite andbT; intro IN.
-          move: LE => /allP LE; unfold R_le_deadline in LE.
-          by specialize (LE i IN); destruct i.
+          move: LE => /allP LE; unfold jitter_plus_R_le_deadline in LE.
+          specialize (LE i IN); destruct i; simpl.
+          by apply leq_trans with (n := task_jitter s + s0); first by apply leq_addl.
         }
 
         have TOOMUCH :=
@@ -906,7 +907,8 @@ Module ResponseTimeIterationEDF.
       (* ...they have valid parameters,...*)
       Hypothesis H_valid_job_parameters:
         forall (j: JobIn arr_seq),
-          valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+          valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost
+                                         job_deadline job_task job_jitter j.
       
       (* ... and satisfy the sporadic task model.*)
       Hypothesis H_sporadic_tasks:
@@ -917,10 +919,9 @@ Module ResponseTimeIterationEDF.
       Hypothesis H_at_least_one_cpu :
         num_cpus > 0.
 
-      (* ...jobs only execute after they arrived and no longer
-         than their execution costs,... *)
-      Hypothesis H_jobs_must_arrive_to_execute:
-        jobs_must_arrive_to_execute sched.
+      (* ...jobs only execute after jitter and no longer than their execution costs,... *)
+      Hypothesis H_jobs_execute_after_jitter:
+        jobs_execute_after_jitter job_jitter sched.
       Hypothesis H_completed_jobs_dont_execute:
         completed_jobs_dont_execute job_cost sched.
 
@@ -928,29 +929,16 @@ Module ResponseTimeIterationEDF.
       Hypothesis H_no_parallelism:
         jobs_dont_execute_in_parallel sched.
 
-      (* In order not to overcount job interference, we assume that
-       jobs of the same task do not execute in parallel.
-       Our proof requires a definition of interference based on
-       the sum of the individual contributions of each job:
-         I_total = I_j1 + I_j2 + ...
-       Note that under EDF, this is equivalent to task precedence
-       constraints. *)
-      Hypothesis H_no_intra_task_parallelism:
-        jobs_of_same_task_dont_execute_in_parallel job_task sched.
-
-      (* Assume that the schedule satisfies the global scheduling
-         invariant with EDF priority, i.e., if any job of tsk is
-         backlogged, every processor must be busy with jobs with
-         no greater absolute deadline. *)
-      Let higher_eq_priority :=
-        @EDF Job arr_seq job_deadline. (* TODO: implicit params seems broken *)    
-      Hypothesis H_global_scheduling_invariant:
-        JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus sched higher_eq_priority.
-
-      Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
+      (* Assume that we have a work-conserving EDF scheduler. *)
+      Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
+      Hypothesis H_edf_policy: enforces_JLDP_policy job_cost job_jitter sched (EDF job_deadline).
+
+      Let no_deadline_missed_by_task (tsk: sporadic_task) :=
         task_misses_no_deadline job_cost job_deadline job_task sched tsk.
-      Definition no_deadline_missed_by_job :=
+      Let no_deadline_missed_by_job :=
         job_misses_no_deadline job_cost job_deadline sched.
+      Let response_time_bounded_by (tsk: sporadic_task) :=
+        is_response_time_bound_of_task job_cost job_task tsk sched.
 
       (* In the following theorem, we prove that any response-time bound contained
          in edf_claimed_bounds is safe. The proof follows by direct application of
@@ -958,17 +946,20 @@ Module ResponseTimeIterationEDF.
       Theorem edf_analysis_yields_response_time_bounds :
         forall tsk R,
           (tsk, R) \In edf_claimed_bounds ts ->
-          forall j : JobIn arr_seq,
-            job_task j = tsk ->
-            completed job_cost sched j (job_arrival j + R).
+          response_time_bounded_by tsk (task_jitter tsk + R).
       Proof.
-        intros tsk R IN j JOBj.
-        destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by done.
+        intros tsk R MATCH.
+        assert (SOME: exists rt_bounds, edf_claimed_bounds ts = Some rt_bounds /\ (tsk, R) \in rt_bounds).
+        {
+          destruct (edf_claimed_bounds ts); last by done.
+          by exists l; split.
+        } clear MATCH; des.
         unfold edf_rta_iteration in *.
         have BOUND := bertogna_cirinei_response_time_bound_edf.
-        unfold is_response_time_bound_of_task in *.
+        unfold response_time_bounded_by, is_response_time_bound_of_task in *.
+        intros j JOBtsk.
         apply BOUND with (task_cost := task_cost) (task_period := task_period)
-           (task_deadline := task_deadline) (job_deadline := job_deadline)
+           (task_deadline := task_deadline) (job_deadline := job_deadline) (job_jitter := job_jitter)
            (job_task := job_task) (ts := ts) (tsk := tsk) (rt_bounds := rt_bounds); try (by ins).
           by unfold edf_claimed_bounds in SOME; desf; rewrite edf_claimed_bounds_unzip1_iteration.
           by ins; apply edf_claimed_bounds_converges with (ts := ts).
@@ -985,13 +976,12 @@ Module ResponseTimeIterationEDF.
         unfold no_deadline_missed_by_task, task_misses_no_deadline,
                job_misses_no_deadline, completed,
                edf_schedulable,
-               valid_sporadic_job in *.
+               valid_sporadic_job_with_jitter, valid_sporadic_job in *.
         rename H_valid_job_parameters into JOBPARAMS,
                H_valid_task_parameters into TASKPARAMS,
                H_restricted_deadlines into RESTR,
                H_completed_jobs_dont_execute into COMP,
-               H_jobs_must_arrive_to_execute into MUSTARRIVE,
-               H_global_scheduling_invariant into INVARIANT,
+               H_jobs_execute_after_jitter into AFTER,
                H_all_jobs_from_taskset into ALLJOBS,
                H_test_succeeds into TEST.
         
@@ -1007,15 +997,15 @@ Module ResponseTimeIterationEDF.
           [by ins | by ins | clear DL; intro DL].
    
         rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
-        apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
+        apply leq_trans with (n := service sched j (job_arrival j + task_jitter tsk + R)); last first.
         {
           unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
-          apply extend_sum; rewrite // leq_add2l.
-          specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
+          rewrite extend_sum // -addnA leq_add2l.
+          specialize (JOBPARAMS j); des; rewrite JOBPARAMS2.
           by rewrite JOBtsk.
         }
         rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
-        by apply COMPLETED.
+        by rewrite -addnA; apply COMPLETED.
       Qed.
 
       (* For completeness, since all jobs of the arrival sequence

create_makefile.sh

+coq_makefile -R . rt $(find -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile

doc/tactics.md

@@ -21,6 +21,10 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 
 - `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_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.
 
 *To be continued… please help out.*

arrival_sequence.v → model/basic/arrival_sequence.v

-Require Import Vbase job task util_lemmas
-               ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase rt.util.lemmas rt.model.basic.job rt.model.basic.task.
+Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definitions and properties of job arrival sequences. *)
 Module ArrivalSequence.

interference.v → model/basic/interference.v

-Require Import Vbase task job schedule priority workload util_divround
-               util_lemmas ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
+Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
+               rt.model.basic.priority rt.model.basic.workload.
+Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
 
-  Import ScheduleOfSporadicTask Priority Workload.
+  Import Schedule ScheduleOfSporadicTask Priority Workload.
 
-  Section InterferingTasks.
+  Section PossibleInterferingTasks.
 
     Context {sporadic_task: eqType}.
     Variable task_cost: sporadic_task -> nat.
@@ -15,25 +18,25 @@ Module Interference.
     Section FP.
 
       (* Assume an FP policy. *)
-      Variable higher_eq_priority: fp_policy sporadic_task.
+      Variable higher_eq_priority: FP_policy sporadic_task.
 
-      (* Then, tsk_other is said to interfere with tsk if it's a different
-         task with higher or equal priority. *)
-      Definition is_interfering_task_fp (tsk tsk_other: sporadic_task) :=
+      (* Under constrained dealdines, tsk_other can only interfere with tsk
+         if it's a different task with higher or equal priority. *)
+      Definition fp_can_interfere_with (tsk tsk_other: sporadic_task) :=
         higher_eq_priority tsk_other tsk && (tsk_other != tsk).
 
     End FP.
 
     Section JLFP.
 
-      (* Under JLFP policies, any two different tasks can interfere with
+      (* Under JLFP/JLDP policies, any two different tasks can interfere with
          each other. *)
-      Definition is_interfering_task_jlfp (tsk tsk_other: sporadic_task) :=
+      Definition jldp_can_interfere_with (tsk tsk_other: sporadic_task) :=
         tsk_other != tsk.
 
     End JLFP.
     
-  End InterferingTasks.
+  End PossibleInterferingTasks.
   
   Section InterferenceDefs.
 

model/basic/interference_bound.v

+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase rt.util.lemmas.
+Require Import rt.model.basic.schedule rt.model.basic.workload_bound.
+Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module InterferenceBoundGeneric.
+
+  Section Definitions.
+
+    Import Schedule WorkloadBound.
+    
+    Context {sporadic_task: eqType}.
+    Variable task_cost: sporadic_task -> nat.
+    Variable task_period: sporadic_task -> nat.
+    Variable task_deadline: sporadic_task -> nat.
+    
+    (* Let tsk be the task to be analyzed. *)
+    Variable tsk: sporadic_task.
+
+    Let task_with_response_time := (sporadic_task * time)%type.
+    
+    (* Assume a known response-time bound for each interfering task ... *)
+    Variable R_prev: seq task_with_response_time.
+
+    (* ... and an interval length delta. *)
+    Variable delta: time.
+
+    Section PerTask.
+
+      Variable tsk_R: task_with_response_time.
+      Let tsk_other := fst tsk_R.
+      Let R_other := snd tsk_R.
+    
+      (* Based on the workload bound, Bertogna and Cirinei define the
+         following interference bound for a task. *)
+      Definition interference_bound_generic :=
+        minn (W task_cost task_period tsk_other R_other delta) (delta - (task_cost tsk) + 1).
+
+    End PerTask.
+
+  End Definitions.
+
+End InterferenceBoundGeneric.
\ No newline at end of file

interference_bound_edf.v → model/basic/interference_bound_edf.v

-Require Import Vbase task job task_arrival schedule platform interference
-        workload workload_bound schedulability priority response_time
-        bertogna_fp_theory util_divround interference_edf util_lemmas
-        ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
-
-  (* In the following section, we define Bertogna and Cirinei's
-     EDF-specific per-task interference bound. *)
-Module EDFSpecificBound.
-
-  Import Job SporadicTaskset ScheduleOfSporadicTask Schedulability ResponseTime
-         Priority SporadicTaskArrival Interference InterferenceEDF.
-
-  Section EDFBoundDef.
+Add LoadPath "../.." as rt.
+Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
+Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
+               rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
+               rt.model.basic.workload rt.model.basic.workload_bound rt.model.basic.priority
+               rt.model.basic.schedulability rt.model.basic.interference
+               rt.model.basic.interference_edf rt.model.basic.interference_bound.
+Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+
+Module InterferenceBoundEDF.
+
+  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask Schedulability
+         WorkloadBound ResponseTime Priority
+         SporadicTaskArrival Interference InterferenceEDF.
+  Export InterferenceBoundGeneric.
+
+  (* In this section, we define Bertogna and Cirinei's EDF-specific
+     interference bound. *)
+  Section SpecificBoundDef.
     
     Context {sporadic_task: eqType}.
     Variable task_cost: sporadic_task -> nat.
@@ -37,9 +43,64 @@ Module EDFSpecificBound.
         (div_floor d_tsk p_other) * e_other +
         minn e_other ((d_tsk %% p_other) - (d_other - R_other)).
 
-  End EDFBoundDef.
+  End SpecificBoundDef.
+  
+  (* Next, we define the total interference bound for EDF, which combines the generic
+     and the EDF-specific bounds. *)
+  Section TotalInterferenceBoundEDF.
+
+    Context {sporadic_task: eqType}.
+    Variable task_cost: sporadic_task -> nat.
+    Variable task_period: sporadic_task -> nat.
+    Variable task_deadline: sporadic_task -> nat.
+    
+    (* Let tsk be the task to be analyzed. *)
+    Variable tsk: sporadic_task.
+
+    Let task_with_response_time := (sporadic_task * time)%type.
+    
+    (* Assume a known response-time bound for each interfering task ... *)
+    Variable R_prev: seq task_with_response_time.
+
+    (* ... and an interval length delta. *)
+    Variable delta: time.
+
+    Section PerTask.
 
-  Section ProofInterferenceBound.
+      Variable tsk_R: task_with_response_time.
+      Let tsk_other := fst tsk_R.
+      Let R_other := snd tsk_R.
+
+      (* By combining Bertogna's interference bound for a work-conserving
+         scheduler ... *)
+      Let basic_interference_bound := interference_bound_generic task_cost task_period tsk delta tsk_R.
+
+      (* ... with and EDF-specific interference bound, ... *)
+      Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
+
+      (* Bertogna and Cirinei define the following interference bound
+         under EDF scheduling. *)
+      Definition interference_bound_edf :=
+        minn basic_interference_bound edf_specific_bound.
+
+    End PerTask.
+
+    Section AllTasks.
+
+      Let interferes_with_tsk := jldp_can_interfere_with tsk.
+      
+      (* The total interference incurred by tsk is bounded by the sum
+         of individual task interferences. *)
+      Definition total_interference_bound_edf :=
+        \sum_((tsk_other, R_other) <- R_prev | interferes_with_tsk tsk_other)
+           interference_bound_edf (tsk_other, R_other).
+
+    End AllTasks.
+
+  End TotalInterferenceBoundEDF.
+  
+  (* In this section, we show that the EDF-specific interference bound is safe. *)
+  Section ProofSpecificBound.
 
     Import Schedule Interference Platform SporadicTaskset.
     
@@ -96,12 +157,10 @@ Module EDFSpecificBound.
     Let response_time_bounded_by (tsk: sporadic_task) :=
       is_response_time_bound_of_task job_cost job_task tsk sched.
 
-    (* Assume that the schedule satisfies the global scheduling invariant
-       for EDF, i.e., if any job of tsk is backlogged, every processor
-       must be busy with jobs with no larger absolute deadline. *)
-    Let higher_eq_priority := @EDF Job arr_seq job_deadline. (* TODO: implicit params broken *)    
-    Hypothesis H_global_scheduling_invariant:
-      JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus sched higher_eq_priority.
+    (* Assume that the scheduler is a work-conserving EDF scheduler. *)
+    Hypothesis H_work_conserving: work_conserving job_cost sched.
+    Hypothesis H_edf_scheduler:
+      enforces_JLDP_policy job_cost sched (EDF job_deadline).
 
     (* Let tsk_i be the task to be analyzed, ...*)
     Variable tsk_i: sporadic_task.
@@ -1055,6 +1114,60 @@ Module EDFSpecificBound.
       
     End MainProof.
     
-  End ProofInterferenceBound.
+  End ProofSpecificBound.
+
+  (* As required by the proof of convergence of EDF RTA, we show that the
+     EDF-specific bound is monotonically increasing with both the size
+     of the interval and the value of the previous response-time bounds. *)
+  Section MonotonicitySpecificBound.
 
-End EDFSpecificBound.
\ No newline at end of file
+    Context {sporadic_task: eqType}.
+    Variable task_cost: sporadic_task -> nat.
+    Variable task_period: sporadic_task -> nat.
+    Variable task_deadline: sporadic_task -> nat.
+    
+    Variable tsk tsk_other: sporadic_task.
+    Hypothesis H_period_positive: task_period tsk_other > 0.
+
+    Variable delta delta' R R': time.
+    Hypothesis H_delta_monotonic: delta <= delta'.
+    Hypothesis H_response_time_monotonic: R <= R'.
+    Hypothesis H_cost_le_rt_bound: task_cost tsk_other <= R.
+
+    Lemma interference_bound_edf_monotonic :
+      interference_bound_edf task_cost task_period task_deadline tsk delta (tsk_other, R) <=
+      interference_bound_edf task_cost task_period task_deadline tsk delta' (tsk_other, R').
+    Proof.
+      rename H_response_time_monotonic into LEr, H_delta_monotonic into LEx,
+             H_cost_le_rt_bound into LEcost, H_period_positive into GEperiod.
+      unfold interference_bound_edf, interference_bound_generic.
+      rewrite leq_min; apply/andP; split.
+      {
+        rewrite leq_min; apply/andP; split.
+        apply leq_trans with (n :=  (minn (W task_cost task_period (fst (tsk_other, R))
+                           (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1)));
+          first by apply geq_minl.
+        apply leq_trans with (n := W task_cost task_period (fst (tsk_other, R))
+                                                   (snd (tsk_other, R)) delta);
+          [by apply geq_minl | by apply W_monotonic].
+        apply leq_trans with (n := minn (W task_cost task_period (fst (tsk_other, R)) (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1));
+          first by apply geq_minl.
+        apply leq_trans with (n := delta - task_cost tsk + 1);
+          first by apply geq_minr.
+        by rewrite leq_add2r leq_sub2r.
+      }
+      {
+        apply leq_trans with (n := edf_specific_interference_bound task_cost task_period
+                                                          task_deadline tsk tsk_other R);
+          first by apply geq_minr.
+        unfold edf_specific_interference_bound; simpl.
+        rewrite leq_add2l leq_min; apply/andP; split; first by apply geq_minl.
+        apply leq_trans with (n := task_deadline tsk %% task_period tsk_other -
+                                   (task_deadline tsk_other - R));
+          [by apply geq_minr | by rewrite 2?leq_sub2l 2?leq_sub2r // leq_sub2l].
+      }
+    Qed.
+
+  End MonotonicitySpecificBound.
+
+End InterferenceBoundEDF.
\ No newline at end of file

model/basic/interference_bound_fp.v

+Add LoadPath "../.." as rt.
+Require Import rt.util.Vbase rt.util.lemmas.
+Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
+               rt.model.basic.workload_bound rt.model.basic.interference
+               rt.model.basic.interference_bound.
+Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module InterferenceBoundFP.
+
+  Import Schedule WorkloadBound Priority Interference.
+  Export InterferenceBoundGeneric.
+
+    Section Definitions.
+    
+    Context {sporadic_task: eqType}.
+    Variable task_cost: sporadic_task -> nat.
+    Variable task_period: sporadic_task -> nat.
+    Variable task_deadline: sporadic_task -> nat.
+    
+    (* Let tsk be the task to be analyzed. *)
+    Variable tsk: sporadic_task.
+
+    Let task_with_response_time := (sporadic_task * time)%type.
+    
+    (* Assume a known response-time bound for each interfering task ... *)
+    Variable R_prev: seq task_with_response_time.
+
+    (* ... and an interval length delta. *)
+    Variable delta: time.
+      
+    (* Assume an FP policy. *)
+    Variable higher_eq_priority: FP_policy sporadic_task.
+
+    Let can_interfere_with_tsk := fp_can_interfere_with higher_eq_priority tsk.  
+    Let total_interference_bound := interference_bound_generic task_cost task_period tsk delta.
+    
+    (* The total interference incurred by tsk is bounded by the sum
+       of individual task interferences. *)
+    Definition total_interference_bound_fp :=
+      \sum_((tsk_other, R_other) <- R_prev | can_interfere_with_tsk tsk_other)
+         total_interference_bound (tsk_other, R_other).
+      
+  End Definitions.
+
+End InterferenceBoundFP.
\ No newline at end of file

interference_edf.v → model/basic/interference_edf.v

-Require Import Vbase task schedule job priority interference task_arrival
-               arrival_sequence platform util_lemmas
-               ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+Add LoadPath "../.." as rt.
+Require Import rt.util.Vbase rt.util.lemmas.
+Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
+               rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference
+               rt.model.basic.arrival_sequence rt.model.basic.platform.
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
 
-  Import Schedule Priority Platform Interference.
+  Import Schedule Priority Platform Interference Priority.
   
   Section Lemmas. 
 
@@ -22,9 +25,8 @@ Module InterferenceEDF.
     (* Assume that the schedule satisfies the global scheduling invariant
        for EDF, i.e., if any job of tsk is backlogged, every processor
        must be busy with jobs with no larger absolute deadline. *)
-    Let higher_eq_priority := @EDF Job arr_seq job_deadline. (* TODO: implicit params broken *)    
-    Hypothesis H_global_scheduling_invariant:
-      JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus sched higher_eq_priority.
+    Hypothesis H_scheduler_uses_EDF:
+      enforces_JLDP_policy job_cost sched (EDF job_deadline). 
 
     (* Under EDF scheduling, a job only causes interference if its deadline
        is not larger than the deadline of the analyzed job. *)
@@ -33,17 +35,14 @@ Module InterferenceEDF.
         job_interference job_cost sched j' j t1 t2 != 0 ->
         job_arrival j + job_deadline j <= job_arrival j' + job_deadline j'.
     Proof.
-      rename H_global_scheduling_invariant into INV.
-      clear - INV. 
+      rename H_scheduler_uses_EDF into PRIO.
       intros j j' t1 t2 INTERF.
       unfold job_interference in INTERF.
       destruct ([exists t': 'I_t2, (t' >= t1) && backlogged job_cost sched j' t' &&
                                               scheduled sched j t']) eqn:EX.
       {
         move: EX => /existsP EX; destruct EX as [t' EX];move: EX => /andP [/andP [LE BACK] SCHED].
-        eapply interfering_job_has_higher_eq_prio in BACK;
-          [ | by apply INV | by apply SCHED].
-        by apply BACK.
+        by eapply PRIO in SCHED; last by apply BACK.
       }
       {
         apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL. 

job.v → model/basic/job.v

-Require Import task util_lemmas ssrnat ssrbool eqtype.  
+Add LoadPath "../../" as rt.
+Require Import rt.model.basic.task rt.util.lemmas.
+Require Import ssrnat ssrbool eqtype.  
 
 (* Properties of different types of job: *)
 Module Job.
@@ -65,32 +67,4 @@ Module Job.
 
   End ValidSporadicTaskJob.
 
-  (* 4) Job of sporadic task with jitter *)
-  Section ValidSporadicTaskJobWithJitter.
-
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> nat.
-    Variable task_deadline: sporadic_task -> nat.
-    Variable task_jitter: sporadic_task -> nat.
-    
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-    Variable job_deadline: Job -> nat.
-    Variable job_task: Job -> sporadic_task.
-    Variable job_jitter: Job -> nat.
-    
-    Variable j: Job.
-
-    (* The job jitter cannot be larger than the task (maximum) jitter.*)
-    Definition job_jitter_leq_task_jitter :=
-      job_jitter j <= task_jitter (job_task j).
-
-    Let j_is_valid_job :=
-      valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
-
-    Definition valid_sporadic_job_with_jitter :=
-      j_is_valid_job /\ job_jitter_leq_task_jitter.
-
-  End ValidSporadicTaskJobWithJitter.
-
 End Job.
\ No newline at end of file