Remove motonicity lemmas

BertognaResponseTimeDefsEDF.v

@@ -103,16 +103,26 @@ Module ResponseTimeAnalysisEDF.
        unit speed, and that there exists at least one processor. *)
     Hypothesis H_no_parallelism:
       jobs_dont_execute_in_parallel sched.
-    Hypothesis H_no_intra_task_parallelism:
-      jobs_of_same_task_dont_execute_in_parallel job_task sched.
     Hypothesis H_rate_equals_one :
       forall j cpu, rate j cpu = 1.
     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.
+       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 we have a task set where all tasks have valid
        parameters and restricted deadlines. *)
     Variable ts: taskset_of sporadic_task.
+    Hypothesis all_jobs_from_taskset:
+      forall (j: JobIn arr_seq), job_task j \in ts.
     Hypothesis H_valid_task_parameters:
       valid_sporadic_taskset task_cost task_period task_deadline ts.
     Hypothesis H_restricted_deadlines:
@@ -904,7 +914,7 @@ Module ResponseTimeAnalysisEDF.
           rewrite (eq_bigr (fun i => if (i \in ts) && true then (if is_interfering_task_jlfp tsk' i && task_is_scheduled job_task sched i t then 1 else 0) else 0));
             last by ins; destruct (i \in ts) eqn:IN; rewrite ?andTb ?andFb.
           rewrite -big_mkcond -big_seq_cond -big_mkcond sum1_count.
-          by eapply cpus_busy_with_interfering_tasks;
+          by eapply cpus_busy_with_interfering_tasks; try (by done);
             [by apply INVARIANT | by apply JOBtsk | by apply BACK].
         }
         

BertognaResponseTimeEDFComp.v

@@ -275,6 +275,14 @@ Module ResponseTimeIterationEDF.
       (* ...and do not execute in parallel. *)
       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.
 
@@ -873,7 +881,7 @@ Module ResponseTimeIterationEDF.
         apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
         {
           unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
-          apply service_monotonic; rewrite leq_add2l.
+          apply extend_sum; rewrite // leq_add2l.
           specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
           by rewrite JOBtsk.
         }

BertognaResponseTimeFP.v

@@ -690,7 +690,7 @@ Module ResponseTimeIterationFP.
         apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
         {
           unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
-          apply service_monotonic; rewrite leq_add2l.
+          apply extend_sum; rewrite // leq_add2l.
           specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
           by rewrite JOBtsk.
         }

BertognaResponseTimeFPJitter.v

@@ -691,7 +691,7 @@ Module ResponseTimeIterationFPWithJitter.
         apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
         {
           unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
-          apply service_monotonic; rewrite leq_add2l.
+          apply extend_sum; rewrite // leq_add2l.
           specialize (JOBPARAMS j); des; rewrite JOBPARAMS2.
           by rewrite JOBtsk.
         }

GuanFP.v

@@ -726,7 +726,7 @@ Module ResponseTimeIterationFPGuan.
         apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
         {
           unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
-          apply service_monotonic; rewrite leq_add2l.
+          apply extend_sum; rewrite // leq_add2l.
           specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
           by rewrite JOBtsk.
         }

InterferenceDefs.v

@@ -125,21 +125,6 @@ Module Interference.
         by rewrite big_const_nat iter_addn mul1n addn0 leqnn.
       Qed.
 
-      Lemma job_interference_monotonic :
-        forall j_other t1 t2 t1' t2',
-          t1' <= t1 ->
-          t2 <= t2' ->
-          job_interference j_other t1 t2 <= job_interference j_other t1' t2'.
-      Proof.
-        unfold job_interference; intros tsk t1 t2 t1' t2' LE1 LE2.
-        destruct (t1 <= t2) eqn:LE12;
-          last by apply negbT in LE12; rewrite -ltnNge in LE12; rewrite big_geq // ltnW.
-        rewrite -> big_cat_nat with (m := t1') (n := t1); try (by done); simpl;
-          last by apply leq_trans with (n := t2).
-        rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
-        by rewrite addnC -addnA; apply leq_addr.
-      Qed.
-
       Lemma job_interference_le_delta :
         forall j_other t1 delta,
           job_interference j_other t1 (t1 + delta) <= delta.
@@ -184,21 +169,6 @@ Module Interference.
         by destruct (sched cpu t); [rewrite HAScpu mul1n rate_positive | by ins].
       Qed.
 
-      Lemma task_interference_monotonic :
-        forall tsk t1 t2 t1' t2',
-          t1' <= t1 ->
-          t2 <= t2' ->
-          task_interference tsk t1 t2 <= task_interference tsk t1' t2'.
-      Proof.
-        unfold task_interference; intros tsk t1 t2 t1' t2' LE1 LE2.
-        destruct (t1 <= t2) eqn:LE12;
-          last by apply negbT in LE12; rewrite -ltnNge in LE12; rewrite big_geq // ltnW.
-        rewrite -> big_cat_nat with (m := t1') (n := t1); try (by done); simpl;
-          last by apply leq_trans with (n := t2).
-        rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
-        by rewrite addnC -addnA; apply leq_addr.
-    Qed.
-      
     End BasicLemmas.
 
     Section EquivalenceTaskInterference.

PlatformDefs.v

 Require Import Vbase TaskDefs ScheduleDefs JobDefs PriorityDefs
                InterferenceDefs helper
-               ssreflect ssrbool eqtype ssrnat seq fintype.
+               ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Platform.
 
-  Import Schedule SporadicTaskset Interference Priority.
+  Import ScheduleOfSporadicTask SporadicTaskset Interference Priority.
 
   Section SchedulingInvariants.
     
@@ -104,6 +104,11 @@ Module Platform.
           by rewrite ltnn in BUG.
         Qed.
 
+        Hypothesis all_jobs_from_taskset:
+          forall (j: JobIn arr_seq), job_task j \in ts.
+        Hypothesis no_intra_task_parallelism:
+          jobs_of_same_task_dont_execute_in_parallel job_task sched.
+
         Lemma cpus_busy_with_interfering_tasks :
           forall (j: JobIn arr_seq) tsk t,
             job_task j = tsk ->
@@ -114,10 +119,27 @@ Module Platform.
                  task_is_scheduled job_task sched j t)
               ts = num_cpus.
         Proof.
+          rename all_jobs_from_taskset into FROMTS,
+                 no_intra_task_parallelism into NOINTRA,
+                 H_invariant_holds into INV.
+          unfold JLFP_JLDP_scheduling_invariant_holds in *.
           intros j tsk t JOBtsk BACK.
-          move: H_invariant_holds => bla.
-          apply/eqP; rewrite eqn_leq; apply/andP; split.
-          admit. admit.
+          apply eq_trans with (y := count (fun j_other => higher_eq_priority t j_other j) (jobs_scheduled_at sched t));
+            last by apply INV.
+          unfold jobs_scheduled_at, task_is_scheduled.
+          induction num_cpus.
+          {
+            rewrite big_ord0 /=.
+            apply eq_trans with (y := count pred0 ts); last by apply count_pred0.
+            apply eq_count; red; ins.
+            apply negbTE; rewrite negb_and; apply/orP; right.
+            apply/negP; red; intro BUG; move: BUG => /existsP BUG.
+            by destruct BUG as [x0]; destruct x0.
+          }
+          {
+            rewrite big_ord_recr /=.
+            admit.
+          }     
         Qed.
         
       End BasicLemmas.

ScheduleDefs.v

@@ -203,29 +203,6 @@ Module Schedule.
 
     Section Basic.
 
-      Lemma service_monotonic : (* TODO: REMOVE! *)
-        forall t t', t <= t' ->
-           service rate sched j t <= service rate sched j t'.
-      Proof.
-        unfold service; ins; rewrite -> big_cat_nat with (p := t') (n := t);
-          by  [apply leq_addr | by ins | by ins].
-      Qed.
-
-      Lemma sum_service_monotonic :
-        forall t1 t2 t1' t2',
-          t1' <= t1 ->
-          t2 <= t2' ->
-            service_during rate sched j t1 t2 <= service_during rate sched j t1' t2'.
-      Proof.
-        unfold service_during; intros t1 t2 t1' t2' LE1 LE2.
-        destruct (t1 <= t2) eqn:LE12;
-          last by apply negbT in LE12; rewrite -ltnNge in LE12; rewrite big_geq // ltnW.
-        rewrite -> big_cat_nat with (m := t1') (n := t1); try (by done); simpl;
-          last by apply leq_trans with (n := t2).
-        rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
-        by rewrite addnC -addnA; apply leq_addr.
-      Qed.
-
       Lemma not_scheduled_no_service :
         forall t,
           ~~ scheduled sched j t -> service_at rate sched j t = 0.
@@ -335,7 +312,7 @@ Module Schedule.
         rewrite eqn_leq; apply/andP; split;
           first by apply service_interval_le_cost.
         by apply leq_trans with (n := service rate sched j t);
-          [by rewrite COMPt | by apply service_monotonic].
+          [by rewrite COMPt | by apply extend_sum].
       Qed.
       
     End Completion.

WorkloadDefs.v

@@ -36,20 +36,12 @@ Module Workload.
         \sum_(cpu < num_cpus)
           service_of_task cpu (sched cpu t).
 
-    (* We provide an alternative definition for workload,
-       which is more suitable for our proof.
-       It requires computing the list of jobs that are scheduled
-       between t1 and t2 (without duplicates). *)
-    Definition jobs_scheduled_between (t1 t2: time) :=
-      undup (\cat_(t1 <= t < t2)
-               \cat_(cpu < num_cpus)
-                 make_sequence (sched cpu t)).
     
     (* Now, we define workload by summing up the cumulative service
        during [t1,t2) of the scheduled jobs, but only those spawned
        by the task that we care about. *)
     Definition workload_joblist (t1 t2: time) :=
-      \sum_(j <- jobs_scheduled_between t1 t2 | job_task j == tsk)
+      \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk)
         service_during rate sched j t1 t2.
 
     Lemma scheduled_between_helper :
@@ -112,7 +104,7 @@ Module Workload.
     Lemma scheduled_between_implies_service :
       forall j t1 t2,
         (forall j cpu, rate j cpu > 0) ->
-        (j \in jobs_scheduled_between t1 t2) =
+        (j \in jobs_scheduled_between sched t1 t2) =
         (service_during rate sched j t1 t2 != 0).
     Proof.
       intros j t1 t2 RATE; unfold service_during; rewrite mem_undup.
@@ -127,30 +119,15 @@ Module Workload.
       by apply scheduled_between_helper, RATE.
     Qed.
 
-    Lemma workload_monotonic :
-      forall t1 t2 t1' t2',
-        t1' <= t1 ->
-        t2 <= t2' ->
-        workload t1 t2 <= workload t1' t2'.
-    Proof.
-      unfold workload; intros t1 t2 t1' t2' LE1 LE2.
-      destruct (t1 <= t2) eqn:LE12;
-        last by apply negbT in LE12; rewrite -ltnNge in LE12; rewrite big_geq // ltnW.
-      rewrite -> big_cat_nat with (m := t1') (n := t1); try (by done); simpl;
-        last by apply leq_trans with (n := t2).
-      rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
-      by rewrite addnC -addnA; apply leq_addr.
-    Qed.
-
     (* Next, we show that the two definitions are equivalent. *)
     Lemma workload_eq_workload_joblist :
       forall t1 t2,
       workload t1 t2 = workload_joblist t1 t2.
     Proof.
       intros t1 t2; unfold workload, workload_joblist, service_during.
-      rewrite [\sum_(j <- jobs_scheduled_between _ _ | _) _]exchange_big /=.
+      rewrite [\sum_(j <- jobs_scheduled_between _ _ _ | _) _]exchange_big /=.
       apply eq_big_nat; unfold service_at; intros t LEt.
-      rewrite [\sum_(i <- jobs_scheduled_between _ _ | _) _](eq_bigr (fun i =>
+      rewrite [\sum_(i <- jobs_scheduled_between _ _ _ | _) _](eq_bigr (fun i =>
                \sum_(cpu < num_cpus) (sched cpu t == Some i) * rate i cpu));
         last by ins; rewrite big_mkcond; apply eq_bigr; ins; rewrite mulnbl.
       rewrite exchange_big /=; apply eq_bigr.