formal verif : move bits produced declarations closer to processes

[urcu.git] / formal-model / ooomem-two-writes / mem.spin

diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin
index 4892c5ec333249b74d3b8beab5ff5bee40a268b1..cb206d2596ef0a24b5b1d29aafba953e0dd1b356 100644 (file)
--- 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);
@@ -184,6 +174,9 @@ active proctype test_proc_one()
 #ifdef NO_RMB
        PRODUCE_TOKENS(proc_one_produced, P1_RMB);
 #endif
+#ifdef NO_SYNC
+       PRODUCE_TOKENS(proc_one_produced, P1_SYNC_CORE);
+#endif
 
        do
        :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE, P1_WRITE) ->
@@ -219,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);
@@ -231,6 +239,9 @@ active proctype test_proc_two()
 #ifdef NO_RMB
        PRODUCE_TOKENS(proc_two_produced, P2_RMB);
 #endif
+#ifdef NO_SYNC
+       PRODUCE_TOKENS(proc_two_produced, P2_SYNC_CORE);
+#endif
 
        do
        :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE, P2_WRITE) ->