X-Git-Url: https://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu-controldataflow%2Furcu.spin;h=dd5d17d32b33cbad437caae1ab2da8c9dffdc842;hb=f24274b95c646682a448694eb0c759311cb7a5af;hp=12f841ce46ed7225be2c8fe83b63d938483a00e6;hpb=caeea74ce58faba3ef2bb7d2bd925d9009803086;p=urcu.git

diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin
index 12f841c..dd5d17d 100644
--- a/formal-model/urcu-controldataflow/urcu.spin
+++ b/formal-model/urcu-controldataflow/urcu.spin
@@ -126,6 +126,14 @@
  * Nested calls are not supported.
  */
 
+/*
+ * Only Alpha has out-of-order cache bank loads. Other architectures (intel,
+ * powerpc, arm) ensure that dependent reads won't be reordered. c.f.
+ * http://www.linuxjournal.com/article/8212)
+#ifdef ARCH_ALPHA
+#define HAVE_OOO_CACHE_READ
+#endif
+
 /*
  * Each process have its own data in cache. Caches are randomly updated.
  * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces
@@ -206,7 +214,7 @@ typedef per_proc_bitfield {
 	fi;
 
 /* Must consume all prior read tokens. All subsequent reads depend on it. */
-inline smp_rmb(i, j)
+inline smp_rmb(i)
 {
 	atomic {
 		CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
@@ -229,7 +237,7 @@ inline smp_rmb(i, j)
 }
 
 /* Must consume all prior write tokens. All subsequent writes depend on it. */
-inline smp_wmb(i, j)
+inline smp_wmb(i)
 {
 	atomic {
 		CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
@@ -253,11 +261,11 @@ inline smp_wmb(i, j)
 
 /* Synchronization point. Must consume all prior read and write tokens. All
  * subsequent reads and writes depend on it. */
-inline smp_mb(i, j)
+inline smp_mb(i)
 {
 	atomic {
-		smp_wmb(i, j);
-		smp_rmb(i, j);
+		smp_wmb(i);
+		smp_rmb(i);
 	}
 }
 
@@ -284,28 +292,29 @@ inline smp_mb_recv(i, j)
 {
 	do
 	:: (reader_barrier[get_readerid()] == 1) ->
-		smp_mb(i, j);
+		/*
+		 * We choose to ignore cycles caused by writer busy-looping,
+		 * waiting for the reader, sending barrier requests, and the
+		 * reader always services them without continuing execution.
+		 */
+progress_ignoring_mb1:
+		smp_mb(i);
 		reader_barrier[get_readerid()] = 0;
 	:: 1 ->
-		/* We choose to ignore writer's non-progress caused from the
-		 * reader ignoring the writer's mb() requests */
-#ifdef WRITER_PROGRESS
-progress_writer_from_reader:
-#endif
+		/*
+		 * We choose to ignore writer's non-progress caused by the
+		 * reader ignoring the writer's mb() requests.
+		 */
+progress_ignoring_mb2:
 		break;
 	od;
 }
 
-#ifdef WRITER_PROGRESS
-//#define PROGRESS_LABEL(progressid)	progress_writer_progid_##progressid:
-#define PROGRESS_LABEL(progressid)
-#else
-#define PROGRESS_LABEL(progressid)
-#endif
+#define PROGRESS_LABEL(progressid)	progress_writer_progid_##progressid:
 
 #define smp_mb_send(i, j, progressid)						\
 {										\
-	smp_mb(i, j);								\
+	smp_mb(i);								\
 	i = 0;									\
 	do									\
 	:: i < NR_READERS ->							\
@@ -315,22 +324,23 @@ progress_writer_from_reader:
 		 * interest, given the reader has the ability to totally ignore	\
 		 * barrier requests.						\
 		 */								\
-PROGRESS_LABEL(progressid)							\
 		do								\
-		:: (reader_barrier[i] == 1) -> skip;				\
+		:: (reader_barrier[i] == 1) ->					\
+PROGRESS_LABEL(progressid)							\
+			skip;							\
 		:: (reader_barrier[i] == 0) -> break;				\
 		od;								\
 		i++;								\
 	:: i >= NR_READERS ->							\
 		break								\
 	od;									\
-	smp_mb(i, j);								\
+	smp_mb(i);								\
 }
 
 #else
 
-#define smp_mb_send(i, j, progressid)	smp_mb(i, j)
-#define smp_mb_reader	smp_mb
+#define smp_mb_send(i, j, progressid)	smp_mb(i)
+#define smp_mb_reader	smp_mb(i)
 #define smp_mb_recv(i, j)
 
 #endif
@@ -386,6 +396,7 @@ inline ooo_mem(i)
 			i++
 		:: i >= SLAB_SIZE -> break
 		od;
+#ifdef HAVE_OOO_CACHE_READ
 		RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
 		i = 0;
 		do
@@ -403,6 +414,9 @@ inline ooo_mem(i)
 			i++
 		:: i >= SLAB_SIZE -> break
 		od;
+#else
+		smp_rmb(i);
+#endif /* HAVE_OOO_CACHE_READ */
 	}
 }
 
@@ -641,7 +655,6 @@ non_atomic3_end:
 					skip;
 				fi;
 			}
-		:: 1 -> skip;
 		fi;
 
 		goto non_atomic3_skip;
@@ -810,14 +823,14 @@ rmb2_end:
 	goto end;
 rmb1:
 #ifndef NO_RMB
-	smp_rmb(i, j);
+	smp_rmb(i);
 #else
 	ooo_mem(i);
 #endif
 	goto rmb1_end;
 rmb2:
 #ifndef NO_RMB
-	smp_rmb(i, j);
+	smp_rmb(i);
 #else
 	ooo_mem(i);
 #endif
@@ -927,7 +940,7 @@ active proctype urcu_writer()
 	assert(get_pid() < NR_PROCS);
 
 	do
-	:: (loop_nr < 4) ->
+	:: (loop_nr < 3) ->
 #ifdef WRITER_PROGRESS
 progress_writer1:
 #endif
@@ -968,7 +981,7 @@ progress_writer1:
 		:: CONSUME_TOKENS(proc_urcu_writer,
 				  WRITE_DATA,
 				  WRITE_PROC_WMB) ->
-			smp_wmb(i, j);
+			smp_wmb(i);
 			PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB);
 
 		:: CONSUME_TOKENS(proc_urcu_writer,
@@ -1151,6 +1164,12 @@ end_writer:
 	:: 1 ->
 #ifdef WRITER_PROGRESS
 progress_writer2:
+#endif
+#ifdef READER_PROGRESS
+		/*
+		 * Make sure we don't block the reader's progress.
+		 */
+		smp_mb_send(i, j, 5);
 #endif
 		skip;
 	od;