Latest changes

BertognaResponseTimeDefs.v

@@ -781,22 +781,27 @@ Module ResponseTimeAnalysis.
     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
        bound of task 'idx' using a fixed-point iteration as follows. *)
-    Definition rt_rec (tsk_i: task_in_ts)
-                      (R_prev: tsk_i.-tuple nat) (step: nat) :=
-      iter step (fun t => task_cost tsk_i +
+    Definition rt_rec (idx: task_in_ts)
+                      (R_prev: idx.-tuple nat) (step: nat) :=
+      iter step (fun t => task_cost idx +
                        div_floor
-                         (total_interference_bound_fp ts tsk_i
-                           (fun tsk: task_in_ts => task_deadline tsk) (* CHANGE TO R_prev!*)
-                           t higher_eq_priority)
+                         (total_interference_bound_fp ts idx
+                         (ext_tuple_to_fun_index R_prev)
+                         t higher_eq_priority)
                          num_cpus)
-             (task_cost tsk_i).
+           (task_cost idx).
 
     (* We return a vector of size 'idx' containing the response-time
-       bound of the higher-priority tasks 0...idx-1 using the
-       recursion rt_rec that we just defined. *)
+       bound of the higher-priority tasks 0...idx-1 using rt_rec *)
     Definition R_hp (idx: task_in_ts) : idx.-tuple nat :=
       match idx with
       | Ordinal k Hk =>
@@ -807,14 +812,14 @@ Module ResponseTimeAnalysis.
             | S k => fun Hk =>
                         [tuple of rcons
                          (f k (ltSnm k _ Hk))
-                         (rt_rec (Ordinal Hk)
-                                 (f (S k) Hk )
+                         (rt_rec (Ordinal _)
+                                 (f k (ltSnm k _ Hk))
                                  (max_steps (Ordinal Hk)) )]
           end) k Hk
       end.
 
-    (* Then, the response-time bound R of a task idx is
-       obtained by calling rt_rec with the vector of R of the
+    (* The response-time bound R of a task idx is computed
+       by calling rt_rec with the vector R_hp of the
        higher-priority tasks. *)
     Definition R (idx: task_in_ts) :=
       rt_rec idx (R_hp idx) (max_steps idx).
@@ -868,41 +873,42 @@ Module ResponseTimeAnalysis.
     Definition no_deadline_missed_by (tsk: sporadic_task) :=
       task_misses_no_deadline job_cost job_deadline job_task
                               rate sched tsk.
-      
+
     Theorem R_converges:
       forall (tsk: task_in_ts),
         R tsk <= task_deadline tsk ->
         R tsk = task_cost tsk +
                 div_floor
                   (total_interference_bound_fp ts tsk
-                    (fun tsk: task_in_ts => task_deadline tsk) (* FIX! *)
+                    R
                     (R tsk) higher_eq_priority)
                   num_cpus.
     Proof.
+      unfold valid_sporadic_taskset, valid_sporadic_task in *.
+      rename H_valid_task_parameters into TASKPARAMS.
       rename H_sorted_ts into SORT; move: SORT => SORT.
       intros tsk LE.
 
-      unfold R, max_steps, rt_rec in *.
+      unfold R in *; unfold max_steps, rt_rec in *.
       set RHS :=  (fun t : time =>
                    task_cost tsk +
                    div_floor
                      (total_interference_bound_fp ts tsk
-                     (fun tsk0 : task_in_ts => task_deadline tsk0) t
+                     (ext_tuple_to_fun_index (R_hp tsk)) t
                      higher_eq_priority)
                    num_cpus).
       fold RHS in LE; rewrite -> addn1 in *.
-      set R := fun t => iter t RHS (task_cost tsk).
-      fold (R (task_deadline tsk).+1).
-      fold (R (task_deadline tsk).+1) in LE.
-
-      assert (NEXT: task_cost tsk +
+      set R' := fun t => iter t RHS (task_cost tsk).
+      fold (R' (task_deadline tsk).+1).
+      fold (R' (task_deadline tsk).+1) in LE.
+      Admitted.
+      (*assert (NEXT: task_cost tsk +
                   div_floor
-                    (total_interference_bound_fp ts tsk
-                      (fun tsk0: task_in_ts => task_deadline tsk0)
-                      (R (task_deadline tsk).+1) higher_eq_priority)
+                    (total_interference_bound_fp ts tsk R
+                      (R' (task_deadline tsk).+1) higher_eq_priority)
                   num_cpus =
-                    R (task_deadline tsk).+2);
-        first by unfold R; rewrite [iter _.+2 _ _]iterS.
+                    R' (task_deadline tsk).+2).
+        unfold R'. first by unfold R'; rewrite [iter _.+2 _ _]iterS.
       rewrite NEXT; clear NEXT.
 
       assert (MON: forall x1 x2, x1 <= x2 -> RHS x1 <= RHS x2).
@@ -915,7 +921,10 @@ Module ResponseTimeAnalysis.
         rewrite leq_min; apply/andP; split.
         {
           apply leq_trans with (n := W i (task_deadline i) x1);
-            [by apply geq_minl | by apply W_monotonic, LEx].
+            first by apply geq_minl.
+          exploit (TASKPARAMS (nth_task i));
+            [by rewrite mem_nth | intro PARAMS; des].
+          by apply W_monotonic.
         }
         {
           apply leq_trans with (n := x1 - task_cost tsk + 1);
@@ -950,37 +959,79 @@ Module ResponseTimeAnalysis.
         apply IHn; intros k.
         by apply (GROWS (widen_ord (leqnSn n) k)).
       }
-      apply leq_ltn_trans with (m := R (task_deadline tsk).+1) in BY1; last by ins.
-      by rewrite ltnn in BY1.
-    Qed.
-
-    (*Lemma taskP :
-      forall (ts: sporadic_taskset) (P: sporadic_task -> Prop),
-        (forall (tsk: task_in_ts), P (nth_task tsk)) <->
-                (forall (tsk: sporadic_task), (tsk \in ts) -> P tsk).*)
-    
-      Theorem taskset_schedulable_by_fp_rta :
-        forall (tsk: task_in_ts), no_deadline_missed_by tsk.
-      Proof.
-        unfold no_deadline_missed_by, task_misses_no_deadline,
-               job_misses_no_deadline, completed,
-               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_valid_policy into VALIDhp,
-               H_taskset_not_empty into NONEMPTY,
-               H_sorted_ts into SORT,
-               H_unique_priorities into UNIQ,
-               H_all_jobs_from_taskset into ALLJOBS.
-
-        rewrite -(size_sort higher_eq_priority) in NONEMPTY. 
-        unfold task_in_ts.
-
-        destruct tsk.
+      apply leq_ltn_trans with (m := R (task_deadline tsk).+1) in BY1;
+        [by rewrite ltnn in BY1 | by ins].
+    Qed.*)
+
+    Theorem taskset_schedulable_by_fp_rta :
+      forall (tsk: task_in_ts), no_deadline_missed_by tsk.
+    Proof.
+      unfold no_deadline_missed_by, task_misses_no_deadline,
+             job_misses_no_deadline, completed,
+             fp_schedulability_test,
+             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_valid_policy into VALIDhp,
+             H_taskset_not_empty into NONEMPTY,
+             H_sorted_ts into SORT,
+             H_unique_priorities into UNIQ,
+             H_all_jobs_from_taskset into ALLJOBS,
+             H_test_passes into TEST.
+      
+      rewrite -(size_sort higher_eq_priority) in NONEMPTY. 
+      move: SORT TEST => SORT /allP TEST.
+      move => tsk j /eqP JOBtsk.
+      
+      rewrite eqn_leq; apply/andP; split;
+        first by apply service_interval_le_cost.
+      apply leq_trans with (n := service rate sched j (job_arrival j + R tsk)); last first.
+      {
+        apply service_monotonic; rewrite leq_add2l.
+        specialize (JOBPARAMS j); des; rewrite JOBPARAMS1 JOBtsk.
+        apply TEST, mem_ord_enum.
+      }
+      rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
+      generalize dependent j.
+      destruct tsk as [tsk_i LTi].
+
+      induction tsk_i using strong_ind.
+      {
+        (* Base case: no higher-priority tasks *)
+        unfold sorted in SORT.
+        intros j JOBtsk.
+
+        set tsk0 := Ordinal (n:=size ts) (m:=0) LTi.
+        have BOUND := bertogna_cirinei_response_time_bound_fp.
+        unfold is_response_time_bound_of_task,
+          job_has_completed_by, completed in BOUND.
+        apply BOUND with (job_deadline := job_deadline) (ts := ts)
+                         (job_task := job_task) (tsk := tsk0)
+                         (R_other := R) (higher_eq_priority := higher_eq_priority); try ins; clear BOUND.
+          admit. (* can be proven using the definition of interference. *)
+          admit. (* tsk_other cannot exist *)
+          by apply INVARIANT with (j := j0); by ins.
+          by apply R_converges, TEST, mem_ord_enum.
+      }
+      {
+      }
+
+
+
+
+
+
+      
+      induction (size ts). unfold task_in_ts in *.
+      intro tsk. induction (size ts).
+
+      unfold task_in_ts.
+
+      destruct tsk.
         (*
         (* Apply induction from the back. *)
         elim/last_ind.

WorkloadDefs.v

@@ -168,7 +168,7 @@ Module Workload.
            rewrite DIV leq_add2r leq_min; apply/andP; split;
              first by rewrite geq_minl.
            by apply leq_trans with (n := (t1 + delta + R - e) %% p);
-             [by rewrite geq_minr | by apply ltnW, DIV0].
+             [by rewrite geq_minr | by rewrite -DIV0 addn1 leqnSn].
          }
          {
            rewrite -[minn e _]add0n -addnA; apply leq_add; first by ins.

helper.v

-Require Import Vbase ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssromega.
+Require Import Vbase ssreflect ssrbool eqtype ssrnat seq fintype bigop tuple path div ssromega.
 
 Section Pair.
 
@@ -33,6 +33,21 @@ Reserved Notation "\cat_ ( i < n ) F"
 Notation "\cat_ ( i < n ) F" :=
   (\big[cat/[::]]_(i < n) F%N) : nat_scope.
 
+Ltac des_eqrefl2 :=
+  match goal with
+    | H: context[match ?X as id return (?X = id -> _) with _ => _ end Logic.eq_refl] |- _ =>
+    let EQ := fresh "EQ" in
+    let id' := fresh "x" in
+    revert H;
+    generalize (Logic.eq_refl X); generalize X at 2 3;
+    intros id' EQ; destruct id'; intros H
+    | |- context[match ?X as id return (?X = id -> _) with _ => _ end Logic.eq_refl] =>
+    let EQ := fresh "EQ" in
+    let id' := fresh "x" in
+    generalize (Logic.eq_refl X); generalize X at 2 3;
+    intros id' EQ; destruct id'
+  end.
+
 Lemma mem_bigcat_nat:
   forall (T: eqType) x m n j (f: _ -> list T)
          (LE: m <= j < n) (IN: x \in (f j)),
@@ -52,25 +67,14 @@ Definition fun_ord_to_nat {n} {T} (x0: T) (f: 'I_n -> T) : nat -> T.
     [by apply (f (Ordinal LT)) | by apply x0].
 Defined.
 
-(* For all x: 'I_n (i.e., x < n), the conversion preserves equality. *)
-Program Definition eq_fun_ord_to_nat :
+Lemma eq_fun_ord_to_nat :
   forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
-    (fun_ord_to_nat x0 f) x = f x :=
-  fun n T x0 f x =>
-    match ltn_ord x in eq _ b return
-          ( 
-            (if b as b' return b = b' -> T then
-               fun (H : b = true) => f (@Ordinal n x ( H))
-             else fun _ => x0) Logic.eq_refl = f x
-          )
-          -> fun_ord_to_nat x0 f x = f x
-    with
-      | Logic.eq_refl => _
-    end (Logic.eq_refl (f x)).
-Next Obligation.
-  destruct x; simpl.
-  f_equal; f_equal.
-  exact: bool_irrelevance.
+    (fun_ord_to_nat x0 f) x = f x.
+Proof.
+  ins; unfold fun_ord_to_nat.
+  des_eqrefl2.
+    by f_equal; apply ord_inj.
+    by destruct x; ins; rewrite i in EQ.
 Qed.
 
 Lemma eq_bigr_ord T n op idx r (P : pred 'I_n)
@@ -102,6 +106,20 @@ Proof.
     [by apply/andP; split | by rewrite eq_fun_ord_to_nat].
 Qed.
 
+Lemma strong_ind :
+  forall (P: nat -> Prop),
+    P 0 -> (forall n, (forall k, k <= n -> P k) -> P n.+1) ->
+    forall n, P n.
+Proof.
+  intros P P0 ALL; destruct n; first by apply P0.
+  apply ALL;  generalize dependent n; induction n.
+    by intros k LE0; move: LE0; rewrite leqn0; move => /eqP LE0; subst k.
+    intros k LESn; destruct (ltngtP k n.+1) as [LT | GT | EQ].
+      by rewrite ltnS in LT; apply IHn.
+      by rewrite leqNgt GT in LESn.
+      by rewrite EQ; apply ALL, IHn.
+Qed.
+  
 Lemma exists_inP_nat t (P: nat -> bool):
   reflect (exists x, x < t /\ P x) [exists (x | x \in 'I_t), P x].
 Proof.
@@ -329,25 +347,93 @@ Proof.
     by rewrite -divn_eq addn1.
   }
   {
-    (* Case 2: y < d - 1 *)
-    rewrite -(ltn_add2r 1) in LTN.
-    rewrite subh1 in LTN; last by apply GT0.
-    rewrite -addnBA // subnn addn0 in LTN.
-    generalize LTN; apply modn_small in LTN; intro LTN'.
-    generalize LTN'; apply divn_small in LTN'; intro LTN''.
-    split.
+    assert (EQDIV: n %/ d = n.+1 %/ d).
     {
-      unfold x; apply/eqP.
-      cut ((d == 0) || (n %/ d * d == n.+1 %/ d * d)).
-      intros OR; des; first by move: OR => /eqP OR; rewrite OR ltn0 in GT1.
-      rewrite eqn_mul2r in OR; des; last by apply OR.
-      by move: OR => /eqP OR; rewrite OR ltn0 in GT1.
-      apply/orP; right.
-      rewrite -(eqn_add2l n.+1).
-      admit.
+      apply/eqP; rewrite eqn_leq; apply/andP; split;
+        first by apply leq_div2r, leqnSn.
+      rewrite leq_divRL; last by apply GT0.
+      rewrite -ltnS {2}(divn_eq n.+1 d).
+      rewrite -{1}[_ %/ d * d]addn0 ltn_add2l.
+      unfold y in *.
+      rewrite ltnNge; apply/negP; unfold not; intro BUG.
+      rewrite leqn0 in BUG; move: BUG => /eqP BUG.
+      rewrite -(modnn d) -addn1 in BUG.
+      destruct d; first by rewrite sub0n in LTN.
+      move: BUG; move/eqP; rewrite -[d.+1]addn1 eqn_modDr [d+1]addn1; move => /eqP BUG.
+      rewrite BUG -[d.+1]addn1 -addnBA // subnn addn0 in LTN.
+      by rewrite modn_small in LTN;
+        [by rewrite ltnn in LTN | by rewrite addn1 ltnSn].
     }
+    (* Case 2: y < d - 1 *)
+    split; first by rewrite -EQDIV.
     {
-      admit.
+      unfold x, y in *.
+      rewrite -2!subndiv_eq_mod.
+      rewrite subh1 ?addn1; last by apply leq_trunc_div.
+      rewrite EQDIV; apply/eqP.
+      rewrite -(eqn_add2r (n%/d*d)).
+      by rewrite subh1; last by apply leq_trunc_div.
     }
   }
-Qed.
+Qed.
\ No newline at end of file
+
+Definition antisymmetric_over_seq {T: eqType} (leT: rel T) (s: seq T) :=
+  forall x y (INx: x \in s) (INy: y \in s)
+             (LEx: leT x y) (LEy: leT y x),
+    x = y.
+
+Lemma sorted_by_index :
+  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).
+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.
+
+
+(*Program Definition fun_ord_to_nat2 {n} {T} (x0: T) (f: 'I_n -> T)
+        (x : nat) : T :=
+  match (x < n) with
+      true => (f _)
+    | false => x0
+  end.
+Next Obligation.
+  eby eapply Ordinal, Logic.eq_sym.
+Defined.
+
+Lemma eq_fun_ord_to_nat2 :
+  forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
+    (fun_ord_to_nat2 x0 f) x = f x.
+Proof.
+  ins. unfold fun_ord_to_nat2.
+  des_eqrefl.
+    by f_equal; apply ord_inj.
+    by destruct x; ins; rewrite i in EQ.
+Qed.
+
+(* For all x: 'I_n (i.e., x < n), the conversion preserves equality. *)
+Program Definition eq_fun_ord_to_nat :
+  forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
+    (fun_ord_to_nat x0 f) x = f x :=
+  fun n T x0 f x =>
+    match ltn_ord x in eq _ b return
+          ( 
+            (if b as b' return b = b' -> T then
+               fun (H : b = true) => f (@Ordinal n x ( H))
+             else fun _ => x0) Logic.eq_refl = f x
+          )
+          -> fun_ord_to_nat x0 f x = f x
+    with
+      | Logic.eq_refl => _
+    end (Logic.eq_refl (f x)).
+Next Obligation.
+  destruct x; simpl.
+  f_equal; f_equal.
+  exact: bool_irrelevance.
+Qed.*)