From cabf78e4575bedadcf850c29bad7e09fd32d57d9 Mon Sep 17 00:00:00 2001
From: Felipe Lisboa <lisboafelipe5@gmail.com>
Date: Wed, 5 May 2021 19:10:43 +0200
Subject: [PATCH] Added constraint on having one ACT between PREs
---
coq/Arbiter.v | 4 +-
coq/Commands.v | 3 ++
coq/FIFO.v | 61 ++++++++++++++++++++++++---
coq/Trace.v | 26 ++++++++++++
coq/trace2.v | 112 +++++++++++++++++++++++++++++++++++++++++++++++++
5 files changed, 199 insertions(+), 7 deletions(-)
create mode 100644 coq/trace2.v
diff --git a/coq/Arbiter.v b/coq/Arbiter.v
index 60a9e9d..45d5864 100644
--- a/coq/Arbiter.v
+++ b/coq/Arbiter.v
@@ -25,7 +25,7 @@ Section Arbiter.
Arbitrate : Trace_t;
(* All Requests must handled *)
- Req_handled : forall req, req \in Requests -> exists cmd : Command_t, cmd \in Arbitrate.(Commands) ->
- Match req cmd
+ Req_handled : forall req, req \in Requests ->
+ exists cmd : Command_t, (cmd \in Arbitrate.(Commands)) && ((Match req cmd))
}.
End Arbiter.
diff --git a/coq/Commands.v b/coq/Commands.v
index f017937..2b8c59c 100644
--- a/coq/Commands.v
+++ b/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.
diff --git a/coq/FIFO.v b/coq/FIFO.v
index fda5cee..f53d7b8 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -218,21 +218,72 @@ Section FIFO.
- by apply (IHReqs' a b) in Ia.
Qed.
+ Lemma Between_cons req Reqs a b:
+ a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+ Between ((FIFO_trace Reqs).(Cmds)) a b =
+ Between (FIFO_trace (req :: Reqs)).(Cmds) a b.
+ Proof.
+ Admitted.
+
+ Lemma FIFO_trace_Cmds_PRE_ok Reqs :
+ forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+ PRE_to_PRE a b -> Same_Bank a b -> Before a b ->
+ exists c : Command_t, isACT c /\ Same_Bank a c /\ c \in Between (FIFO_trace Reqs).(Cmds) a b.
+ Proof.
+ intros a b a_cmds b_cmds ab_PRE ab_BANK a_not_b.
+ evar (req_date : nat).
+ evar (t : nat).
+ evar (req_kind : Request_kind_t).
+ set (req := mkReq req_date req_kind a.(Request).(Bank)).
+ exists (ACT_of_req req t).
+ split.
+ - auto.
+ - split.
+ - by unfold ACT_of_req, Same_Bank.
+ - induction Reqs.
+ - auto.
+ - simpl in a_cmds.
+ move : a_cmds => /orP [ /eqP a_eq | /orP [ /eqP a_eq | /orP [ /eqP a_eq | Ia]] ];
+ move : b_cmds => /orP [ /eqP b_eq | /orP [ /eqP b_eq | /orP [ /eqP b_eq | Ib]] ].
+ - admit.
+ - admit.
+ - admit.
+ - admit.
+ - admit.
+ - admit.
+ - admit.
+ - admit.
+ - admit.
+ - admit.
+ - (*they are the same*) admit.
+ - (*easy due to order*) admit.
+ - admit.
+ - admit.
+ - (* interesting - induction on Reqs until find request of A until I find my ACT cmd (?)*) admit.
+ - rewrite <- Between_cons. apply IHReqs in Ia. apply Ia. all : auto.
+ Admitted.
+
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).
+ Admit Obligations.
+
+ (*
Next Obligation.
induction Requests.
- auto.
- - by apply (FIFO_trace_uniq a) in IHl.
- Qed.
+ - by apply (FIFO_trace_uniq a) in IHl.*)
+
Lemma FIFO_arbiter_handled req:
- req \in Requests -> exists cmd : Command_t, cmd \in FIFO_arbitrate.(Commands) ->
- Match req cmd.
+ req \in Requests -> exists cmd : Command_t, (cmd \in FIFO_arbitrate.(Commands)) /\
+ ((cmd \in FIFO_arbitrate.(Commands)) -> Match req cmd).
Proof.
intros.
exists (Cmd_of_req req 5).
+ split.
+ - admit.
+ -
unfold FIFO_arbitrate in *. simpl in *.
induction Requests.
- by rewrite in_nil in H.
diff --git a/coq/Trace.v b/coq/Trace.v
index 8164b3b..2f74616 100644
--- a/coq/Trace.v
+++ b/coq/Trace.v
@@ -8,14 +8,35 @@ Section Trace.
Definition Same_Bank (a b : Command_t) :=
a.(Request).(Bank) == b.(Request).(Bank).
+ Definition Same_Bank_3 (a b c : Command_t) :=
+ Same_Bank a b && Same_Bank a c.
+
Definition ACT_to_ACT (a b : Command_t) :=
isACT a && isACT b.
+ Definition PRE_to_PRE (a b : Command_t) :=
+ isPRE a && isPRE b.
+
Definition Before (a b : Command_t) :=
a.(CDate) < b.(CDate).
Definition Apart (a b : Command_t) t :=
a.(CDate) + t < b.(CDate).
+
+(*
+ Fixpoint Between (l : Commands_t) (a b : Command_t) : Commands_t :=
+ match l with
+ | [::] => [::]
+ | hd :: seq => if ((hd.(CDate) >= a.(CDate)) && (hd.(CDate) <= b.(CDate)))
+ then [:: hd] ++ (Between seq a b)
+ else [::]
+ end.
+*)
+
+ Definition Between (l : Commands_t) (a b : Command_t) : Commands_t :=
+ [seq cmds <- l | (cmds.(CDate) > a.(CDate)) && (cmds.(CDate) < b.(CDate))].
+
+ Check Between.
Record Trace_t := mkTrace
{
@@ -28,6 +49,11 @@ Section Trace.
(* All commands have to occur before the current time instant *)
Cmds_time_ok : forall cmd, cmd \in Commands -> cmd.(CDate) <= Time;
+ (* Between any two PREs to the same bank, there has to be an ACT to the same bank in between *)
+ Cmds_PRE_ok : forall a b, a \in Commands -> b \in Commands ->
+ PRE_to_PRE a b -> Same_Bank a b -> a != b ->
+ exists c : Command_t, isACT c /\ Same_Bank a c /\ c \in Between Commands a b;
+
(* Ensure that the time between two ACT commands respects T_RC *)
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 ->
diff --git a/coq/trace2.v b/coq/trace2.v
new file mode 100644
index 0000000..e410ca8
--- /dev/null
+++ b/coq/trace2.v
@@ -0,0 +1,112 @@
+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Export ssreflect ssrnat ssrbool ssrfun seq eqtype.
+From sdram Require Export Commands Bank.
+
+Section Trace.
+
+ Context {BANK_CFG : Bank_configuration}.
+
+ (*
+ Program Instance BANK_CFG : Bank_configuration :=
+ {
+ BANKS := 2;
+ T_RC := 3
+ }.
+*)
+
+ Definition Same_Bank (a b : Command_t) :=
+ a.(Request).(Bank) == b.(Request).(Bank).
+
+ Definition Same_Bank_3 (a b c : Command_t) :=
+ Same_Bank a b && Same_Bank a c.
+
+ Lemma Same_Bank_eq :
+ forall a b c : Command_t, Same_Bank a b -> Same_Bank a c -> Same_Bank b c.
+ Proof.
+ intros a b c S_ab S_ac.
+ unfold Same_Bank in *.
+ move : S_ab => /eqP /esym S_ab.
+ move : S_ac => /eqP /esym S_ac.
+ apply /eqP.
+ by rewrite S_ab.
+ Qed.
+
+ Lemma Same_Bank_3_eq :
+ forall a b c : Command_t, Same_Bank_3 a b c -> Same_Bank a b && Same_Bank a c && Same_Bank b c.
+ Proof.
+ intros a b c S_3.
+ unfold Same_Bank_3 in *.
+ move : S_3 => /andP S_3.
+ apply /andP. split.
+ - by apply /andP. destruct S_3 as [s3_1 s3_2]. move : s3_1 s3_2. apply Same_Bank_eq.
+ Qed.
+
+ Definition ACT_to_ACT (a b : Command_t) :=
+ isACT a && isACT b.
+
+ Definition PRE_to_PRE (a b : Command_t) :=
+ isPRE a && isPRE b.
+
+ Definition Before (a b : Command_t) :=
+ a.(CDate) < b.(CDate).
+
+ Definition Apart (a b : Command_t) t :=
+ a.(CDate) + t < b.(CDate).
+
+ (* Filters a sequence of commands to include just the ones with date between a and b *)
+ Fixpoint Between (l : Commands_t) (a b : Command_t) : Commands_t :=
+ match l with
+ | [::] => [::]
+ | hd :: seq => if ((hd.(CDate) >= a.(CDate)) && (hd.(CDate) <= b.(CDate)))
+ then [:: hd] ++ (Between seq a b)
+ else [::]
+ end.
+
+ (* Create a boolean function *)
+
+ (*
+ Program Definition req1 := mkReq 0 RD 0.
+ Program Definition req2 := mkReq 1 RD 1.
+ Program Definition req3 := mkReq 2 RD 0.
+ Definition PRE_req1 := PRE_of_req req1 0.
+ Definition ACT_req1 := ACT_of_req req1 1.
+ Definition CMD_req1 := Cmd_of_req req1 2.
+ Definition PRE_req2 := PRE_of_req req2 4.
+ Definition ACT_req2 := ACT_of_req req2 5.
+ Definition CMD_req2 := Cmd_of_req req2 6.
+ Definition PRE_req3 := PRE_of_req req2 7.
+ Definition ACT_req3 := ACT_of_req req2 8.
+ Definition CMD_req3 := Cmd_of_req req2 9.
+
+ Definition test_CMDS : Commands_t := [::PRE_req1;ACT_req1;CMD_req1;PRE_req2;ACT_req2;CMD_req2;PRE_req3;ACT_req3;CMD_req3].
+ Print test_CMDS.
+ Check test_CMDS.
+
+ Definition test_between := Between test_CMDS PRE_req1 PRE_req3.
+ Compute test_between.
+ *)
+
+ Record Trace_t := mkTrace
+ {
+ Commands : Commands_t;
+ Time : nat;
+
+ (* All commands must be uniq *)
+ Cmds_uniq : uniq Commands;
+
+ (* All commands have to occur before the current time instant *)
+ Cmds_time_ok : forall cmd, cmd \in Commands -> cmd.(CDate) <= Time;
+
+ (* Between any two PREs to the same bank, there has to be an ACT to the same bank in between *)
+ Cmds_PRE_ok : forall a b c, a \in Commands -> b \in Commands -> c \in Commands ->
+ PRE_to_PRE a b -> isACT c -> Same_Bank_3 a b c ->
+ c \in Between Commands a b;
+
+ (* Ensure that the time between two ACT commands respects T_RC *)
+ 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;
+ }.
+
+ Program Definition Trace_empty := mkTrace [::] 0 _ _ _.
+End Trace.
\ No newline at end of file
--
GitLab