implement T_RP constraint

coq/Bank.v

@@ -7,9 +7,11 @@ Class Bank_configuration :=
   BANKS  : nat;
 
   T_RC   : nat;    (* ACT to ACT delay intra-bank *)
+  T_RP   : nat;    (* PRE to ACT delay intra-bank *)
 
   BANKS_pos : BANKS != 0;
-  T_RC_pos  : T_RC != 0
+  T_RC_pos  : T_RC != 0;
+  T_RP_pos  : T_RP != 0
 }.
 
 Section Banks.

coq/Commands.v

@@ -74,6 +74,9 @@ Section Commands.
   Definition isACT (cmd : Command_t) :=
     cmd.(CKind) == ACT.
 
+  Definition isPRE (cmd : Command_t) :=
+    cmd.(CKind) == PRE.
+
   Definition PRE_of_req req t :=
     mkCmd t PRE req.
 

coq/FIFO.v

@@ -5,6 +5,10 @@ Section FIFO.
   Context {BANK_CFG : Bank_configuration}.
   Context {Input    : Requests_t}.
 
+  Definition FIFO_PRE_date := 1.
+  Definition FIFO_ACT_date := FIFO_PRE_date + T_RP + 1.
+  Definition FIFO_CMD_date := FIFO_ACT_date + 1.
+
   Class FIFO_configuration :=
   {
     FIFO_wait : nat;
@@ -13,6 +17,10 @@ Section FIFO.
     FIFO_cmds : 3 < FIFO_wait;
     (* have to respect T_RC *)
     FIFO_T_RC : T_RC < FIFO_wait;
+
+    FIFO_T_PRE : FIFO_PRE_date <= FIFO_wait;
+    FIFO_T_ACT : FIFO_ACT_date <= FIFO_wait;
+    FIFO_T_CMD : FIFO_CMD_date <= FIFO_wait;
   }.
 
   Context {FIFO_CFG : FIFO_configuration }.
@@ -25,9 +33,9 @@ Section FIFO.
 
   Local Definition FIFO_req req State : FIFO_state_t :=
     let time := maxn State.(Time) req.(Date) in
-    let PRE_date := time + 1 in
-    let ACT_date := time + 2 in
-    let CMD_date := time + 3 in
+    let PRE_date := time + FIFO_PRE_date in
+    let ACT_date := time + FIFO_ACT_date in
+    let CMD_date := time + FIFO_CMD_date in
       let PRE := PRE_of_req req PRE_date in
       let ACT := ACT_of_req req ACT_date in
       let CMD := Cmd_of_req req CMD_date in
@@ -51,6 +59,17 @@ Section FIFO.
     by apply ltn_trans with (m := n) in H.
   Qed.
 
+  Lemma FIFO_T_RP : T_RP < FIFO_wait.
+  Proof.
+    specialize FIFO_T_ACT as H.
+    unfold FIFO_ACT_date in H.
+    rewrite addn1 in H.
+    apply ltn_trans with (n := FIFO_PRE_date + T_RP).
+    - rewrite addnC. apply nat_ltnn_add.
+      by unfold FIFO_PRE_date.
+    - done.
+  Qed.
+
   Lemma FIFO_trace_time_monotone req Reqs:
     (FIFO_trace Reqs).(Time) < (FIFO_trace (req::Reqs)).(Time).
   Proof.
@@ -77,8 +96,11 @@ Section FIFO.
     induction Reqs; auto.
     simpl in *.
     rewrite -> 3 in_cons in H.
-    decompose_FIFO_cmds H H; subst;
-      try (rewrite leq_add2l; by apply lt_FIFO_wait).
+    specialize FIFO_T_PRE as Hpre.
+    specialize FIFO_T_ACT as Hact.
+    specialize FIFO_T_CMD as Hcmd.
+    decompose_FIFO_cmds H H; subst; simpl; 
+      try by rewrite leq_add2l.
     apply IHReqs in H.
     by apply nat_le_lemaxn_add with (x := FIFO_wait) (o := a.(Date)) in H.
   Qed.
@@ -134,24 +156,24 @@ Section FIFO.
         - set T := maxn (FIFO_trace Reqs').(Time) r.(Date).
           unfold maxn. simpl.
           destruct (T + FIFO_wait < req.(Date)) eqn:Hlt.
-          1  : rewrite <- (ltn_add2r 2) in Hlt.
-          1  : apply ltn_trans with (n := T + FIFO_wait + 2); auto.
-          1,2: rewrite addnCAC [T + FIFO_wait + 2]addnCAC.
-          1,2: rewrite [2 + _]addnC.
+          1  : rewrite <- (ltn_add2r FIFO_ACT_date) in Hlt.
+          1  : apply ltn_trans with (n := T + FIFO_wait + FIFO_ACT_date); auto.
+          1,2: rewrite addnCAC [T + FIFO_wait + FIFO_ACT_date]addnCAC.
+          1,2: rewrite [FIFO_ACT_date + _]addnC.
           1,2: rewrite ltn_add2r ltn_add2r.
           1,2: by specialize FIFO_T_RC.
          - set T := maxn (FIFO_trace (r :: Reqs')).(Time) req.(Date).
           set Tf := (FIFO_trace Reqs').(Time) + FIFO_wait.
           specialize (FIFO_trace_dist r Reqs') as Hdist.
           apply leq_trans with (p := T) in Hdist.
-          - rewrite <- (leq_add2r 2) in Hdist.
-            rewrite addnS in Hdist.
+          - rewrite <- (leq_add2r FIFO_ACT_date) in Hdist. 
+            rewrite addnS in Hdist. 
             apply FIFO_trace_time_ok in Ia as H.
             rewrite <- (leq_add2r T_RC) in H.
             apply leq_ltn_trans with (p := Tf) in H.
-            - apply ltn_trans with (p := Tf + 1) in H.
-              - by apply ltn_trans with (p := T + 2) in H.
-              - rewrite <- addn1. by rewrite leqnn.
+            - apply ltn_trans with (p := Tf + (T_RP + 1)) in H.
+              - by apply ltn_trans with (p := T + FIFO_ACT_date) in H.
+              - apply nat_ltnn_add. rewrite addn_gt0. apply /orP. by right.
             - rewrite ltn_add2l. by specialize FIFO_T_RC.
           - unfold T. by apply leq_maxl.
     - contradict aBb. subst a.
@@ -161,9 +183,70 @@ Section FIFO.
     - by apply (IHReqs' a b) in Ia.
   Qed.
 
+  Lemma nat_add_lt_add m1 m2 n1 n2: is_true ((m1 < m2) && (n1 < n2)) -> is_true (m1 + n1 < m2 + n2).
+  Proof.
+    intros.
+    rewrite <- addn1. rewrite addnACl addnC.
+    apply leq_add.
+    - rewrite addnC addn1. by move : H => /andP /proj1 H. 
+    - apply ltnW. by move : H => /andP /proj2 H. 
+  Qed.
+
+  Lemma FIFO_trace_T_RP_ok Reqs: 
+    forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+                    PRE_to_ACT a b -> Same_Bank a b -> Before a b ->
+                    Apart a b T_RP.
+  Proof.
+    induction Reqs as [| req Reqs']; auto.
+    intros a b Ia Ib PtA SB aBb.
+    decompose_FIFO_cmds Ib Cmdb; decompose_FIFO_cmds Ia Cmda;
+      try (contradict_PtoA PtA req).
+    - unfold Apart. subst. simpl.
+      unfold FIFO_ACT_date.
+      rewrite addnCAC addnC ltn_add2l addnC. by apply nat_ltnn_add.
+    - destruct Reqs'.
+      - by contradict Ia.
+      - decompose_FIFO_cmds Ia Cmda;
+          try contradict_PtoA PtA req; try contradict_PtoA PtA r;
+          subst; unfold Apart, ACT_of_req, PRE_of_req; simpl.
+        - set T := maxn (FIFO_trace Reqs').(Time) r.(Date).
+          unfold maxn. simpl.
+          destruct (T + FIFO_wait < req.(Date)) eqn:Hlt.
+          1  : rewrite <- (ltn_add2r FIFO_ACT_date) in Hlt.
+          1  : apply ltn_trans with (n := T + FIFO_wait + FIFO_ACT_date); auto.
+          1,2: rewrite addnCAC [T + FIFO_wait + FIFO_ACT_date]addnCAC.
+          1,2: rewrite [FIFO_ACT_date + _]addnC.
+          1,2: rewrite ltn_add2r.
+          1,2: apply nat_add_lt_add.
+          1,2: apply /andP; split.
+          1,3: by specialize FIFO_T_RP.
+          1,2: unfold FIFO_ACT_date.
+          1,2: rewrite addnCAC addnC; apply nat_ltnn_add.
+          1,2: rewrite addn_gt0; apply /orP; by left.
+         - set T := maxn (FIFO_trace (r :: Reqs')).(Time) req.(Date).
+          set Tf := (FIFO_trace Reqs').(Time) + FIFO_wait.
+          specialize (FIFO_trace_dist r Reqs') as Hdist.
+          apply leq_trans with (p := T) in Hdist.
+          - rewrite <- (leq_add2r FIFO_ACT_date) in Hdist. 
+            rewrite addnS in Hdist. 
+            apply FIFO_trace_time_ok in Ia as H.
+            rewrite <- (leq_add2r T_RP) in H.
+            apply leq_ltn_trans with (p := Tf) in H.
+            - apply ltn_trans with (p := Tf + (T_RP + 1)) in H.
+              - by apply ltn_trans with (p := T + FIFO_ACT_date) in H.
+              - apply nat_ltnn_add. rewrite addn_gt0. apply /orP. by right.
+            - rewrite ltn_add2l. by specialize FIFO_T_RP.
+          - unfold T. by apply leq_maxl.
+    - contradict aBb. subst a.
+      apply /negP.
+      unfold Before, ACT_of_req. rewrite <- leqNgt. apply nat_le_lemaxn_add.
+      by apply (FIFO_trace_time_ok Reqs') in Ib.
+    - by apply (IHReqs' a b) in Ia.
+  Qed.
+
   Program Definition FIFO_arbitrate :=
     let State := FIFO_trace Requests in
-      mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) (FIFO_trace_T_RC_ok Requests).
+      mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) (FIFO_trace_T_RC_ok Requests) (FIFO_trace_T_RP_ok Requests).
   Next Obligation.
     induction Requests; auto.
     by apply (FIFO_trace_uniq a) in IHl.
@@ -172,7 +255,7 @@ Section FIFO.
   Lemma FIFO_arbiter_handled req:
     req \in Requests -> exists cmd : Command_t, cmd \in FIFO_arbitrate.(Commands) ->
                     Match req cmd.
-  Proof.
+  Proof. 
     intros.
     exists (Cmd_of_req req 5).
     unfold FIFO_arbitrate in *. simpl in *.
@@ -198,12 +281,13 @@ Section Test.
   Program Instance BANK_CFG : Bank_configuration :=
   {
     BANKS := 1;
-    T_RC  := 3
+    T_RC  := 3;
+    T_RP  := 7
   }.
 
   Program Instance FIFO_CFG : FIFO_configuration :=
   { 
-    FIFO_wait := 4
+    FIFO_wait := 10
   }.
 
   Program Definition Req1 := mkReq 3 RD 0.

coq/Trace.v

@@ -11,6 +11,9 @@ Section Trace.
   Definition ACT_to_ACT (a b : Command_t) :=
     isACT a && isACT b.
 
+  Definition PRE_to_ACT (a b : Command_t) :=
+    isPRE a && isACT b.
+
   Definition Before (a b : Command_t) :=
     a.(CDate) < b.(CDate).
 
@@ -32,11 +35,20 @@ Section Trace.
     Cmds_T_RC_ok : forall a b, a \in Commands -> b \in Commands ->
                     ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
                     Apart a b T_RC;
+
+    (* Ensure that the time between a PRE and an ACT commands respects T_RC *)
+    Cmds_T_RP_ok : forall a b, a \in Commands -> b \in Commands ->
+                    PRE_to_ACT a b -> Same_Bank a b -> Before a b ->
+                    Apart a b T_RP;
   }.
 
   Program Definition Trace_empty := mkTrace [::] 0 _ _ _.
 End Trace.
 
 Ltac contradict_AtoA H req :=
-  (contradict H; subst;unfold ACT_to_ACT, isACT, PRE_of_req, Cmd_of_req, Kind_of_req; simpl; destruct (Kind req));
+  (contradict H; subst; unfold ACT_to_ACT, isACT, PRE_of_req, Cmd_of_req, Kind_of_req; simpl; destruct (Kind req));
   (done + apply /negP; rewrite negb_and; apply /orP; by right).
+
+Ltac contradict_PtoA H req :=
+  (contradict H; subst; unfold PRE_to_ACT, isACT, isPRE, PRE_of_req, Cmd_of_req, Kind_of_req; simpl; destruct (Kind req);
+   (done + apply /negP; rewrite negb_and; apply /orP; by right)).