From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Fri, 8 May 2009 19:54:54 +0000 (-0400)
Subject: formal verif : move bits produced declarations closer to processes
X-Git-Tag: v0.1~247
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=3db2d75b432e617014976239f694b91de2bc0d7d;p=userspace-rcu.git

formal verif : move bits produced declarations closer to processes

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
---

diff --git a/formal-model/ooomem-double-update-minimal/mem.spin b/formal-model/ooomem-double-update-minimal/mem.spin
index 9fc540a..bae92d6 100644
--- a/formal-model/ooomem-double-update-minimal/mem.spin
+++ b/formal-model/ooomem-double-update-minimal/mem.spin
@@ -40,26 +40,6 @@
 #define CLEAR_TOKENS(state, bits)	\
 	state = (state) & ~(bits)
 
-/*
- * Bit encoding, proc_one_produced :
- */
-
-#define P1_PROD_NONE	(1 << 0)
-
-#define P1_READ_ONE	(1 << 1)
-#define P1_RMB		(1 << 2)
-#define P1_READ_TWO	(1 << 3)
-
-int proc_one_produced;
-
-#define P2_PROD_NONE	(1 << 0)
-
-#define P2_WRITE_ONE	(1 << 1)
-#define P2_WMB		(1 << 2)
-#define P2_WRITE_TWO	(1 << 3)
-
-int proc_two_produced;
-
 #define NR_PROCS 2
 
 #define get_pid()	(_pid)
@@ -168,6 +148,18 @@ DECLARE_CACHED_VAR(byte, beta, 0);
 byte read_one = 2;
 byte read_two = 2;
 
+/*
+ * Bit encoding, proc_one_produced :
+ */
+
+#define P1_PROD_NONE	(1 << 0)
+
+#define P1_READ_ONE	(1 << 1)
+#define P1_RMB		(1 << 2)
+#define P1_READ_TWO	(1 << 3)
+
+int proc_one_produced;
+
 active proctype test_proc_one()
 {
 	assert(get_pid() < NR_PROCS);
@@ -203,6 +195,19 @@ active proctype test_proc_one()
 	assert(read_one != 1 || read_two == 1);
 }
 
+
+/*
+ * Bit encoding, proc_two_produced :
+ */
+
+#define P2_PROD_NONE	(1 << 0)
+
+#define P2_WRITE_ONE	(1 << 1)
+#define P2_WMB		(1 << 2)
+#define P2_WRITE_TWO	(1 << 3)
+
+int proc_two_produced;
+
 active proctype test_proc_two()
 {
 	assert(get_pid() < NR_PROCS);
diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin
index 828ff4a..cb206d2 100644
--- a/formal-model/ooomem-two-writes/mem.spin
+++ b/formal-model/ooomem-two-writes/mem.spin
@@ -40,30 +40,6 @@
 #define CLEAR_TOKENS(state, bits)	\
 	state = (state) & ~(bits)
 
-/*
- * Bit encoding, proc_one_produced :
- */
-
-#define P1_PROD_NONE	(1 << 0)
-
-#define P1_WRITE	(1 << 1)
-#define P1_WMB		(1 << 2)
-#define P1_SYNC_CORE	(1 << 3)
-#define P1_RMB		(1 << 4)
-#define P1_READ		(1 << 5)
-
-int proc_one_produced;
-
-#define P2_PROD_NONE	(1 << 0)
-
-#define P2_WRITE	(1 << 1)
-#define P2_WMB		(1 << 2)
-#define P2_SYNC_CORE	(1 << 3)
-#define P2_RMB		(1 << 4)
-#define P2_READ		(1 << 5)
-
-int proc_two_produced;
-
 #define NR_PROCS 2
 
 #define get_pid()	(_pid)
@@ -172,6 +148,20 @@ DECLARE_CACHED_VAR(byte, beta, 0);
 byte read_one = 2;
 byte read_two = 2;
 
+/*
+ * Bit encoding, proc_one_produced :
+ */
+
+#define P1_PROD_NONE	(1 << 0)
+
+#define P1_WRITE	(1 << 1)
+#define P1_WMB		(1 << 2)
+#define P1_SYNC_CORE	(1 << 3)
+#define P1_RMB		(1 << 4)
+#define P1_READ		(1 << 5)
+
+int proc_one_produced;
+
 active proctype test_proc_one()
 {
 	assert(get_pid() < NR_PROCS);
@@ -222,6 +212,21 @@ active proctype test_proc_one()
 	assert(!(read_one == 0 && read_two == 0));
 }
 
+
+/*
+ * Bit encoding, proc_two_produced :
+ */
+
+#define P2_PROD_NONE	(1 << 0)
+
+#define P2_WRITE	(1 << 1)
+#define P2_WMB		(1 << 2)
+#define P2_SYNC_CORE	(1 << 3)
+#define P2_RMB		(1 << 4)
+#define P2_READ		(1 << 5)
+
+int proc_two_produced;
+
 active proctype test_proc_two()
 {
 	assert(get_pid() < NR_PROCS);