Fiinished correctness of FP RTA

BertognaResponseTimeDefs.v

@@ -286,10 +286,9 @@ Module ResponseTimeAnalysis.
     Let is_response_time_bound (tsk: task_in_ts) :=
       is_response_time_bound_of_task job_cost job_task tsk rate sched.
 
-    (* Assume that we know a response-time bound for the
-       tasks that interfere with tsk. *)
+    (* Assume a known response-time bound for any interfering task *)
     Variable R_other: task_in_ts -> time.
-
+    
     (* We derive the response-time bounds for FP and EDF scheduling
        separately. *)
     Section UnderFPScheduling.
@@ -306,11 +305,16 @@ Module ResponseTimeAnalysis.
       (* Assume that for any interfering task, a response-time
          bound R_other is known. *)
       Hypothesis H_response_time_of_interfering_tasks_is_known:
-        forall tsk_other job_cost,
+        forall tsk_other,
           is_interfering_task tsk_other ->
           is_response_time_bound_of_task job_cost job_task tsk_other
                                          rate sched (R_other tsk_other).
 
+      (* Assume that the response-time bounds are larger than task costs. *)
+      Hypothesis R_other_ge_cost:
+        forall (tsk_other: task_in_ts),
+          R_other tsk_other >= task_cost tsk_other.
+      
       (* Assume that no deadline is missed by any interfering task, i.e.,
          response-time bound R_other <= deadline. *)
       Hypothesis H_interfering_tasks_miss_no_deadlines:
@@ -426,9 +430,9 @@ Module ResponseTimeAnalysis.
                (job_cost := job_cost) (job_deadline := job_deadline); ins;
               [ by rewrite RATE
               | by apply TASK_PARAMS, mem_tnth
-              | by apply RESTR, mem_tnth
-              | by red; ins; red; apply RESP |].
-            red; red; move => j' /eqP JOBtsk' _.
+              | by apply RESTR, mem_tnth 
+              | by red; red; ins; apply RESP |].
+            red; red; move => j' /eqP JOBtsk' _;
             unfold job_misses_no_deadline.
             specialize (PARAMS j'); des.
             rewrite PARAMS1 JOBtsk'.
@@ -750,10 +754,7 @@ Module ResponseTimeAnalysis.
       Hypothesis response_time_no_larger_than_deadline:
         R <= task_deadline tsk.
 
-      Theorem bertogna_cirinei_response_time_bound_jlfp :
-        is_response_time_bound tsk R.
-      Proof.
-      Admitted.
+      (* to be completed... *)
       
     End UnderJLFPScheduling.
     
@@ -777,24 +778,19 @@ Module ResponseTimeAnalysis.
 
     Hypothesis H_taskset_not_empty: size ts > 0.
 
+    (* Assume the task set has no duplicates. *)
+    Hypothesis H_ts_is_a_set: uniq ts.
+
+    (* Assume that higher_eq_priority is a total order. *)
+    Hypothesis H_reflexive: reflexive higher_eq_priority.
+    Hypothesis H_transitive: transitive higher_eq_priority.
     Hypothesis H_unique_priorities:
-      forall tsk1 tsk2,
-        tsk1 \in ts ->
-        tsk2 \in ts ->
-        higher_eq_priority tsk1 tsk2 ->
-        higher_eq_priority tsk2 tsk1 ->         
-        tsk1 = tsk2.
+      antisymmetric_over_seq higher_eq_priority ts.
 
     Hypothesis H_sorted_ts: sorted higher_eq_priority ts.
     
     Definition max_steps (tsk: task_in_ts) :=
       task_deadline tsk + 1.
-
-    Definition ext_tuple_to_fun_index {idx: task_in_ts} (hp: idx.-tuple nat) : task_in_ts -> nat.
-      intros tsk; destruct (tsk < idx) eqn:LT.
-        by apply (tnth hp (Ordinal LT)).
-        by apply 0.
-    Defined.
     
     (* Given a vector of size 'idx' containing known response-time bounds
        for the higher-priority tasks, we compute the response-time
@@ -841,8 +837,6 @@ Module ResponseTimeAnalysis.
     
     Section Proof.
 
-      Hypothesis H_test_passes: fp_schedulability_test.
-
       Context {arr_seq: arrival_sequence Job}.
       Hypothesis H_all_jobs_from_taskset:
         forall (j: JobIn arr_seq), job_task j \in ts.
@@ -883,6 +877,19 @@ Module ResponseTimeAnalysis.
         task_misses_no_deadline job_cost job_deadline job_task
                                 rate sched tsk.
 
+      (* First, we prove that R is no less than the cost of the task.
+         This is required by the workload bound. *)
+      Lemma R_ge_cost:
+        forall (tsk: task_in_ts), R tsk >= task_cost tsk.
+      Proof.
+        intros tsk.
+        unfold R, rt_rec.
+        destruct (max_steps tsk); first by apply leqnn.
+        by rewrite iterS; apply leq_addr.
+      Qed.
+
+      (* Then, we show that either the fixed-point iteration of R converges
+         or it becomes greater than the deadline. *)
       Theorem R_converges:
         forall (tsk: task_in_ts),
           R tsk <= task_deadline tsk ->
@@ -971,6 +978,10 @@ Module ResponseTimeAnalysis.
           [by rewrite ltnn in BY1 | by ins].
       Qed.*)
 
+      (* Finally, we show that if the schedulability test suceeds, ...*)
+      Hypothesis H_test_passes: fp_schedulability_test.
+
+      (*..., then no task misses its deadline. *)
       Theorem taskset_schedulable_by_fp_rta :
         forall (tsk: task_in_ts), no_deadline_missed_by tsk.
       Proof.
@@ -1026,13 +1037,17 @@ Module ResponseTimeAnalysis.
           by apply R_converges, TEST, mem_ord_enum.
           by ins; apply INVARIANT with (j := j0); ins.
           by ins; apply TEST, mem_ord_enum.
+          by ins; apply R_ge_cost. 
           {
-            intros tsk_other job_cost'' INTERF.
+            intros tsk_other INTERF.
             unfold is_interfering_task in INTERF.
             move: INTERF => /andP INTERF; des.
-            (* This part is simple. Since tsk0 is the first task,
-               there cannot be a higher-priority task tsk_other. *)
-            admit.
+            assert (LE: tsk_other < tsk0).
+            {
+              rewrite ltn_neqAle; apply/andP; split; first by ins.
+              by apply leq_ij_implies_before_ij with (leT := higher_eq_priority); try red; ins.
+            }
+            by rewrite ltn0 in LE. 
           }
         }
         {
@@ -1049,30 +1064,28 @@ Module ResponseTimeAnalysis.
           by apply R_converges, TEST, mem_ord_enum.
           by ins; apply INVARIANT with (j := j0); ins.  
           by ins; apply TEST, mem_ord_enum.
+          by ins; apply R_ge_cost.
           {
-            (* Here we need to prove that *for any job cost function*,
-               R is a response-time bound for the higher-priority tasks. *)
-            intros tsk_other job_cost'' INTERF j' JOBtsk'.
+            intros tsk_other INTERF j' JOBtsk'.
             move: INTERF => /andP INTERF; des.
             assert (HP: tsk_other < tsk_i').
             {
-              (*  just need to show that the index of tsk_other is less
-                  than the index of the lower priority task tsk_i'. *)
-              admit.
+              rewrite ltn_neqAle; apply/andP; split; first by ins.
+              by apply leq_ij_implies_before_ij with (leT := higher_eq_priority); try red; ins.
             }
             assert (LT: tsk_other < size ts).
-              by apply ltn_trans with (n := tsk_i');
-                [by apply HP | by apply LTi].
+              by apply ltn_trans with (n := tsk_i'); [by apply HP | by apply LTi].
             specialize (IH tsk_other HP LT j').
             exploit IH; last (clear IH; intro IH).
               by rewrite JOBtsk'; unfold nth_task; f_equal; apply ord_inj.
               by instantiate (1 := job_cost'); apply JOBPARAMS.
               by apply COMP.
               by apply INVARIANT.
-              by admit.
-              (* STUCK HERE!!! We cannot prove that R upper-bounds the response
-                 time of tsk_other *for any job cost function* *)
-          } 
+              {
+                move: IH => /eqP IH; rewrite -IH; apply/eqP.
+                by repeat f_equal; apply ord_inj; ins.
+              }
+          }
         }
       Qed.
 

PlatformDefs.v

@@ -66,6 +66,6 @@ End Uniprocessor.
 Proof.
   unfold valid_platform, identical_multiprocessor, mp_cpus_nonzero,
   mp_scheduling_invariant; ins.
-Admitted.*)
+Qed.*)
 
 End IdenticalMultiprocessor. *)
\ No newline at end of file

WorkloadDefs.v

@@ -229,7 +229,7 @@ Module Workload.
 
     (* Before starting the proof, let's give simpler names to the definitions. *)
     Definition response_time_bound_of (tsk: sporadic_task) (R: time) :=
-      forall job_cost,
+      (*forall job_cost,*)
         is_response_time_bound_of_task job_cost job_task tsk rate sched R.
     Definition no_deadline_misses_by (tsk: sporadic_task) (t: time) :=
       task_misses_no_deadline_before job_cost job_deadline job_task
@@ -257,9 +257,11 @@ Module Workload.
     Hypothesis restricted_deadline: task_deadline tsk <= task_period tsk.
 
     (* Assume that a response-time bound R_tsk for that task in any
-       schedule of this processor platform is also given. *)
+       schedule of this processor platform is also given,
+       such that R_tsk >= task_cost tsk. *)
     Variable R_tsk: time.
     Hypothesis response_time_bound: response_time_bound_of tsk R_tsk.
+    Hypothesis response_time_ge_cost: R_tsk >= task_cost tsk.
     
     (* Consider an interval [t1, t1 + delta), with no deadline misses. *)
     Variable t1 delta: time.
@@ -370,12 +372,12 @@ Module Workload.
       rename FST0 into FSTin, FST into FSTtask, FST1 into FSTserv.
 
       (* Since there is at least one job of the task, we show that R_tsk >= cost tsk. *)
-      assert (GEcost: R_tsk >= task_cost tsk).
+      (*assert (GEcost: R_tsk >= task_cost tsk).
       {
 
         apply (response_time_ub_ge_task_cost job_task) with (sched0 := sched) (rate0 := rate); ins.
         by exists (nth elem sorted_jobs 0); rewrite FSTtask.
-      }
+      }*)
                                 
       (* Now we show that the bound holds for a singleton set of interfering jobs. *)
       destruct n.

helper.v

@@ -382,20 +382,67 @@ Definition antisymmetric_over_seq {T: eqType} (leT: rel T) (s: seq T) :=
              (LEx: leT x y) (LEy: leT y x),
     x = y.
 
-Lemma sorted_by_index :
+Lemma before_ij_implies_leq_ij :
   forall {T: eqType} (s: seq T) (leT: rel T)
-         (SORT: sorted leT s) (ANTI: antisymmetric_over_seq leT s)
-         (i1 i2: 'I_(size s)) (LE: i1 < i2),
-    leT (tnth (in_tuple s) i1) (tnth (in_tuple s) i2).
+         (SORT: sorted leT s) (REFL: reflexive leT)
+         (TRANS: transitive leT)
+         (i j: 'I_(size s)) (LE: i <= j),
+         leT (tnth (in_tuple s) i) (tnth (in_tuple s) j).
 Proof.
-  intros.
-  destruct s.
-  destruct i1 as [i1 LT1].
-    by remember i1 as i1'; have BUG := LT1; rewrite Heqi1' ltn0 in BUG.
-  destruct i1.
-  induction m.  simpl.
-Admitted.
+  destruct i as [i Hi], j as [j Hj]; ins.
+  destruct s; first by exfalso; rewrite ltn0 in Hi.
+  rewrite 2!(tnth_nth s) /=.
+  move: SORT => /pathP SORT.
+  assert (EQ: j = i + (j - i)); first by rewrite subnKC.
+  remember (j - i) as delta; rewrite EQ; rewrite EQ in LE Hj.
+  clear EQ Heqdelta LE.
+  induction delta; first by rewrite addn0; apply REFL.
+  {
+    unfold transitive in *.
+    apply TRANS with (y := (nth s (s :: s0) (i + delta))).
+    {
+      apply IHdelta.
+      apply ltn_trans with (n := i + delta.+1); last by apply Hj.
+      by rewrite ltn_add2l ltnSn.
+    }
+    {
+      rewrite -addn1 addnA addn1.
+      rewrite -nth_behead /=.
+      by apply SORT, leq_trans with (n := i + delta.+1);
+        [ rewrite ltn_add2l ltnSn | by ins].
+    }
+  }
+Qed.
+
+Lemma leq_ij_implies_before_ij :
+  forall {T: eqType} (s: seq T) (leT: rel T)
+         (SORT: sorted leT s)
+         (REFL: reflexive leT)
+         (TRANS: transitive leT)
+         (ANTI: antisymmetric_over_seq leT s)
+         (i j: 'I_(size s)) (UNIQ: uniq s)
+         (REL: leT (tnth (in_tuple s) i) (tnth (in_tuple s) j)),
+           i <= j.
+Proof.
+  ins; destruct i as [i Hi], j as [j Hj]; simpl.
+  destruct s; [by clear REL; rewrite ltn0 in Hi | simpl in SORT].
+  destruct (leqP i j) as [| LT]; first by ins.
+  assert (EQ: i = j + (i - j)).
+    by rewrite subnKC; [by ins | apply ltnW].
+  unfold antisymmetric_over_seq in *.
+  assert (REL': leT (tnth (in_tuple (s :: s0)) (Ordinal Hj)) (tnth (in_tuple (s :: s0)) (Ordinal Hi))).
+    by apply before_ij_implies_leq_ij; try by ins; apply ltnW.
+  apply ANTI in REL'; try (by ins); try apply mem_tnth.
+  move: REL'; rewrite 2!(tnth_nth s) /=; move/eqP.
+  rewrite nth_uniq //; move => /eqP REL'.
+  by subst; rewrite ltnn in LT.
+Qed.
 
+Definition ext_tuple_to_fun_index {T} {ts: seq T} {idx: 'I_(size ts)} (hp: idx.-tuple nat) : 'I_(size ts) -> nat.
+  intros tsk; destruct (tsk < idx) eqn:LT.
+    by apply (tnth hp (Ordinal LT)).
+    by apply 0.
+Defined.
 
 (*Program Definition fun_ord_to_nat2 {n} {T} (x0: T) (f: 'I_n -> T)
         (x : nat) : T :=