X-Git-Url: https://git.lttng.org/?a=blobdiff_plain;f=formal-model%2Furcu-controldataflow%2Furcu.spin;h=44bbe523e153abfe52c39ee3eac957a4b7f22f46;hb=794a737edb08278087a6628a37235d19ff68fce1;hp=484205a1dd999a9fd6c97f214e964b9aa2a884ff;hpb=19d8de31dc92430df89d90e8ba76212b764afd44;p=urcu.git

diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin
index 484205a..44bbe52 100644
--- a/formal-model/urcu-controldataflow/urcu.spin
+++ b/formal-model/urcu-controldataflow/urcu.spin
@@ -243,7 +243,6 @@ inline smp_mb(i, j)
 	}
 }
 
-
 #ifdef REMOTE_BARRIERS
 
 bit reader_barrier[NR_READERS];
@@ -269,32 +268,53 @@ inline smp_mb_recv(i, j)
 	:: (reader_barrier[get_readerid()] == 1) ->
 		smp_mb(i, j);
 		reader_barrier[get_readerid()] = 0;
-	:: 1 -> skip;
+	:: 1 ->
+	/*
+	 * Busy-looping waiting for other barrier requests are not considered as
+	 * non-progress.
+	 */
+#ifdef READER_PROGRESS
+progress_reader2:
+#endif
+		skip;
 	:: 1 -> break;
 	od;
 }
 
-inline smp_mb_send(i, j)
-{
-	smp_mb(i, j);
-	i = 0;
-	do
-	:: i < NR_READERS ->
-		reader_barrier[i] = 1;
-		do
-		:: (reader_barrier[i] == 1) -> skip;
-		:: (reader_barrier[i] == 0) -> break;
-		od;
-		i++;
-	:: i >= NR_READERS ->
-		break
-	od;
-	smp_mb(i, j);
+#ifdef WRITER_PROGRESS
+#define PROGRESS_LABEL(progressid)	progress_writer_progid_##progressid:
+#else
+#define PROGRESS_LABEL(progressid)
+#endif
+
+#define smp_mb_send(i, j, progressid)						\
+{										\
+	smp_mb(i, j);								\
+	i = 0;									\
+	do									\
+	:: i < NR_READERS ->							\
+		reader_barrier[i] = 1;						\
+		do								\
+		:: (reader_barrier[i] == 1) ->					\
+		/*								\
+		 * Busy-looping waiting for reader barrier handling is of little\
+		 * interest, given the reader has the ability to totally ignore	\
+		 * barrier requests.						\
+		 */								\
+PROGRESS_LABEL(progressid)							\
+			skip;							\
+		:: (reader_barrier[i] == 0) -> break;				\
+		od;								\
+		i++;								\
+	:: i >= NR_READERS ->							\
+		break								\
+	od;									\
+	smp_mb(i, j);								\
 }
 
 #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)
 
@@ -592,7 +612,7 @@ non_atomic3_end:
 
 		goto non_atomic3_skip;
 non_atomic3:
-		smp_mb_recv(i, j);	
+		smp_mb_recv(i, j);
 		goto non_atomic3_end;
 non_atomic3_skip:
 
@@ -841,6 +861,11 @@ active proctype urcu_writer()
 	byte i, j;
 	byte tmp, tmp2, tmpa;
 	byte old_gen;
+	byte cur_gp_val = 0;	/*
+				 * Keep a local trace of the current parity so
+				 * we don't add non-existing dependencies on the global
+				 * GP update. Needed to test single flip case.
+				 */
 
 	wait_init_done();
 
@@ -882,13 +907,18 @@ 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
+		do :: 1 ->
+		atomic {
+		if
 		:: CONSUME_TOKENS(proc_urcu_writer,
 				  WRITE_PROD_NONE,
 				  WRITE_PROC_FIRST_MB) ->
-			smp_mb_send(i, j);
+			goto smp_mb_send1;
+smp_mb_send1_end:
 			PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB);
 
 		/* first flip */
@@ -911,9 +941,15 @@ progress_writer1:
 			ooo_mem(i);
 			/* ONLY WAITING FOR READER 0 */
 			tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
+#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 ^ RCU_GP_CTR_BIT) & RCU_GP_CTR_BIT) ->
+					&& ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) ->
 				PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP);
 			:: else	->
 				PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT);
@@ -927,7 +963,8 @@ progress_writer1:
 				  | WRITE_PROC_FIRST_MB,	/* can be reordered before/after flips */
 				  0) ->
 #ifndef GEN_ERROR_WRITER_PROGRESS
-			smp_mb_send(i, j);
+			goto smp_mb_send2;
+smp_mb_send2_end:
 #else
 			ooo_mem(i);
 #endif
@@ -942,7 +979,6 @@ progress_writer1:
 				  | WRITE_PROC_FIRST_READ_GP
 				  | WRITE_PROC_FIRST_MB,
 				  WRITE_PROC_SECOND_READ_GP) ->
-			//smp_mb_send(i, j);		//TEST
 			ooo_mem(i);
 			tmpa = READ_CACHED_VAR(urcu_gp_ctr);
 			PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
@@ -982,7 +1018,8 @@ progress_writer1:
 				  | WRITE_PROC_FIRST_MB,	/* can be reordered before/after flips */
 				  0) ->
 #ifndef GEN_ERROR_WRITER_PROGRESS
-			smp_mb_send(i, j);
+			goto smp_mb_send3;
+smp_mb_send3_end:
 #else
 			ooo_mem(i);
 #endif
@@ -999,12 +1036,15 @@ progress_writer1:
 				  | WRITE_PROC_SECOND_WRITE_GP
 				  | WRITE_PROC_FIRST_MB,
 				  WRITE_PROC_SECOND_MB) ->
-			smp_mb_send(i, j);
+			goto smp_mb_send4;
+smp_mb_send4_end:
 			PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB);
 
 		:: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) ->
 			CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR);
 			break;
+		fi;
+		}
 		od;
 
 		write_lock = 0;
@@ -1028,6 +1068,25 @@ progress_writer2:
 #endif
 		skip;
 	od;
+
+	/* Non-atomic parts of the loop */
+	goto end;
+smp_mb_send1:
+	smp_mb_send(i, j, 1);
+	goto smp_mb_send1_end;
+#ifndef GEN_ERROR_WRITER_PROGRESS
+smp_mb_send2:
+	smp_mb_send(i, j, 2);
+	goto smp_mb_send2_end;
+smp_mb_send3:
+	smp_mb_send(i, j, 3);
+	goto smp_mb_send3_end;
+#endif
+smp_mb_send4:
+	smp_mb_send(i, j, 4);
+	goto smp_mb_send4_end;
+end:
+	skip;
 }
 
 /* no name clash please */