X-Git-Url: https://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu-controldataflow%2Furcu.spin;h=44bbe523e153abfe52c39ee3eac957a4b7f22f46;hp=7c7953f58784509a6441878b6bd93796ad5d2cce;hb=794a737edb08278087a6628a37235d19ff68fce1;hpb=3019378271548c1d591c762b2e33d7153916f55d

diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin
index 7c7953f..44bbe52 100644
--- a/formal-model/urcu-controldataflow/urcu.spin
+++ b/formal-model/urcu-controldataflow/urcu.spin
@@ -314,7 +314,7 @@ PROGRESS_LABEL(progressid)							\
 
 #else
 
-#define smp_mb_send	smp_mb
+#define smp_mb_send(i, j, progressid)	smp_mb(i, j)
 #define smp_mb_reader	smp_mb
 #define smp_mb_recv(i, j)
 
@@ -907,6 +907,8 @@ progress_writer1:
 		PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
 		PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP);
 		PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT);
+		/* For single flip, we need to know the current parity */
+		cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT;
 #endif
 
 		do :: 1 ->
@@ -939,7 +941,12 @@ smp_mb_send1_end:
 			ooo_mem(i);
 			/* ONLY WAITING FOR READER 0 */
 			tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
-			cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT;
+#ifndef SINGLE_FLIP
+			/* In normal execution, we are always starting by
+			 * waiting for the even parity.
+			 */
+			cur_gp_val = RCU_GP_CTR_BIT;
+#endif
 			if
 			:: (tmp2 & RCU_GP_CTR_NEST_MASK)
 					&& ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) ->
@@ -993,10 +1000,9 @@ smp_mb_send2_end:
 			ooo_mem(i);
 			/* ONLY WAITING FOR READER 0 */
 			tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
-			cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT;
 			if
 			:: (tmp2 & RCU_GP_CTR_NEST_MASK)
-					&& ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) ->
+					&& ((tmp2 ^ 0) & RCU_GP_CTR_BIT) ->
 				PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP);
 			:: else	->
 				PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT);