From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Wed, 20 May 2009 04:25:17 +0000 (-0400)
Subject: Fix urcu controldataflow model remote barriers
X-Git-Tag: v0.1~214
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=19d8de31dc92430df89d90e8ba76212b764afd44;p=urcu.git

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 5c377f7..484205a 100644
--- 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 */