Fix urcu controldataflow model remote barriers

Need to split the pointer read from the data access to allow the writer to issue
a memory barrier (actually more than one) to let the single flip race occur.

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

diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin
index 5c377f78879d87bb85505acc7bdb045571b4067a..484205a1dd999a9fd6c97f214e964b9aa2a884ff 100644 (file)
--- a/formal-model/urcu-controldataflow/urcu.spin
+++ b/formal-model/urcu-controldataflow/urcu.spin
@@ -441,30 +441,32 @@ int _proc_urcu_reader;
 #define READ_LOCK_NESTED_OUT           (1 << 11)
 
 #define READ_PROC_READ_GEN             (1 << 12)
+#define READ_PROC_ACCESS_GEN           (1 << 13)
 
-/* PROCEDURE_READ_UNLOCK (NESTED) base = << 13 : 13 to 14 */
-#define READ_UNLOCK_NESTED_BASE                13
-#define READ_UNLOCK_NESTED_OUT         (1 << 14)
+/* PROCEDURE_READ_UNLOCK (NESTED) base = << 14 : 14 to 15 */
+#define READ_UNLOCK_NESTED_BASE                14
+#define READ_UNLOCK_NESTED_OUT         (1 << 15)
 
-#define READ_PROC_SECOND_MB            (1 << 15)
+#define READ_PROC_SECOND_MB            (1 << 16)
 
-/* PROCEDURE_READ_UNLOCK base = << 16 : 16 to 17 */
-#define READ_UNLOCK_BASE               16
-#define READ_UNLOCK_OUT                        (1 << 17)
+/* PROCEDURE_READ_UNLOCK base = << 17 : 17 to 18 */
+#define READ_UNLOCK_BASE               17
+#define READ_UNLOCK_OUT                        (1 << 18)
 
-/* PROCEDURE_READ_LOCK_UNROLL base = << 18 : 18 to 22 */
-#define READ_LOCK_UNROLL_BASE          18
-#define READ_LOCK_OUT_UNROLL           (1 << 22)
+/* PROCEDURE_READ_LOCK_UNROLL base = << 19 : 19 to 23 */
+#define READ_LOCK_UNROLL_BASE          19
+#define READ_LOCK_OUT_UNROLL           (1 << 23)
 
-#define READ_PROC_THIRD_MB             (1 << 23)
+#define READ_PROC_THIRD_MB             (1 << 24)
 
-#define READ_PROC_READ_GEN_UNROLL      (1 << 24)
+#define READ_PROC_READ_GEN_UNROLL      (1 << 25)
+#define READ_PROC_ACCESS_GEN_UNROLL    (1 << 26)
 
-#define READ_PROC_FOURTH_MB            (1 << 25)
+#define READ_PROC_FOURTH_MB            (1 << 27)
 
-/* PROCEDURE_READ_UNLOCK_UNROLL base = << 26 : 26 to 27 */
-#define READ_UNLOCK_UNROLL_BASE                26
-#define READ_UNLOCK_OUT_UNROLL         (1 << 27)
+/* PROCEDURE_READ_UNLOCK_UNROLL base = << 28 : 28 to 29 */
+#define READ_UNLOCK_UNROLL_BASE                28
+#define READ_UNLOCK_OUT_UNROLL         (1 << 29)
 
 
 /* Should not include branches */
@@ -473,17 +475,19 @@ int _proc_urcu_reader;
                                        | READ_PROC_FIRST_MB            \
                                        | READ_LOCK_NESTED_OUT          \
                                        | READ_PROC_READ_GEN            \
+                                       | READ_PROC_ACCESS_GEN          \
                                        | READ_UNLOCK_NESTED_OUT        \
                                        | READ_PROC_SECOND_MB           \
                                        | READ_UNLOCK_OUT               \
                                        | READ_LOCK_OUT_UNROLL          \
                                        | READ_PROC_THIRD_MB            \
                                        | READ_PROC_READ_GEN_UNROLL     \
+                                       | READ_PROC_ACCESS_GEN_UNROLL   \
                                        | READ_PROC_FOURTH_MB           \
                                        | READ_UNLOCK_OUT_UNROLL)
 
 /* Must clear all tokens, including branches */
-#define READ_PROC_ALL_TOKENS_CLEAR     ((1 << 28) - 1)
+#define READ_PROC_ALL_TOKENS_CLEAR     ((1 << 30) - 1)
 
 inline urcu_one_read(i, j, nest_i, tmp, tmp2)
 {
@@ -517,50 +521,66 @@ inline urcu_one_read(i, j, nest_i, tmp, tmp2)
                                if
                                :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE,
                                                READ_LOCK_OUT | READ_LOCK_NESTED_OUT
-                                               | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT
+                                               | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
                                                | READ_UNLOCK_OUT
                                                | READ_LOCK_OUT_UNROLL
-                                               | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
                                        || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT,
                                                READ_LOCK_NESTED_OUT
-                                               | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT
+                                               | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
                                                | READ_UNLOCK_OUT
                                                | READ_LOCK_OUT_UNROLL
-                                               | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
                                        || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | READ_LOCK_NESTED_OUT,
-                                               READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT
+                                               READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
                                                | READ_UNLOCK_OUT
                                                | READ_LOCK_OUT_UNROLL
-                                               | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
                                        || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
                                                | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN,
+                                               READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
+                                               | READ_UNLOCK_OUT
+                                               | READ_LOCK_OUT_UNROLL
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                       || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
+                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN,
                                                READ_UNLOCK_NESTED_OUT
                                                | READ_UNLOCK_OUT
                                                | READ_LOCK_OUT_UNROLL
-                                               | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
                                        || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
-                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT,
+                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
+                                               | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT,
                                                READ_UNLOCK_OUT
                                                | READ_LOCK_OUT_UNROLL
-                                               | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
                                        || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
-                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT
+                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
+                                               | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
                                                | READ_UNLOCK_OUT,
                                                READ_LOCK_OUT_UNROLL
-                                               | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
                                        || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
-                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT
+                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
+                                               | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
                                                | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL,
-                                               READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                               READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
                                        || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
-                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT
+                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
+                                               | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
                                                | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL
                                                | READ_PROC_READ_GEN_UNROLL,
+                                               READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
+                                       || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
+                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
+                                               | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
+                                               | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL,
                                                READ_UNLOCK_OUT_UNROLL)
                                        || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
-                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT
+                                               | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
                                                | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL
-                                               | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL,
+                                               | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL,
                                                0) ->
                                        goto non_atomic3;
 non_atomic3_end:
@@ -597,9 +617,17 @@ non_atomic3_skip:
                                ooo_mem(i);
                                read_generation[get_readerid()] =
                                        READ_CACHED_VAR(generation_ptr);
+                               PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN);
+
+                       :: CONSUME_TOKENS(proc_urcu_reader,
+                                         READ_PROC_FIRST_MB            /* mb() orders reads */
+                                         | READ_PROC_READ_GEN,
+                                         READ_PROC_ACCESS_GEN) ->
+                               ooo_mem(i);
                                goto non_atomic;
 non_atomic_end:
-                               PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN);
+                               PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN);
+
 
                        /* Note : we remove the nested memory barrier from the read unlock
                         * model, given it is not usually needed. The implementation has the barrier
@@ -615,7 +643,8 @@ non_atomic_end:
 
 
                        :: CONSUME_TOKENS(proc_urcu_reader,
-                                         READ_PROC_READ_GEN            /* mb() orders reads */
+                                         READ_PROC_ACCESS_GEN          /* mb() orders reads */
+                                         | READ_PROC_READ_GEN          /* mb() orders reads */
                                          | READ_PROC_FIRST_MB          /* mb() ordered */
                                          | READ_LOCK_OUT               /* post-dominant */
                                          | READ_LOCK_NESTED_OUT        /* post-dominant */
@@ -665,12 +694,22 @@ non_atomic_end:
                                ooo_mem(i);
                                read_generation[get_readerid()] =
                                        READ_CACHED_VAR(generation_ptr);
+                               PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN_UNROLL);
+
+                       :: CONSUME_TOKENS(proc_urcu_reader,
+                                         READ_PROC_READ_GEN_UNROLL
+                                         | READ_PROC_FIRST_MB          /* mb() orders reads */
+                                         | READ_PROC_SECOND_MB         /* mb() orders reads */
+                                         | READ_PROC_THIRD_MB,         /* mb() orders reads */
+                                         READ_PROC_ACCESS_GEN_UNROLL) ->
+                               ooo_mem(i);
                                goto non_atomic2;
 non_atomic2_end:
-                               PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN_UNROLL);
+                               PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN_UNROLL);
 
                        :: CONSUME_TOKENS(proc_urcu_reader,
                                          READ_PROC_READ_GEN_UNROLL     /* mb() orders reads */
+                                         | READ_PROC_ACCESS_GEN_UNROLL /* mb() orders reads */
                                          | READ_PROC_FIRST_MB          /* mb() ordered */
                                          | READ_PROC_SECOND_MB         /* mb() ordered */
                                          | READ_PROC_THIRD_MB          /* mb() ordered */