From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Thu, 26 Feb 2009 23:01:12 +0000 (-0500)
Subject: Add reader nesting test
X-Git-Tag: v0.1~274
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=06d6106d9482f3a2805a2512ef0cda203088f2f5;p=urcu.git

Add reader nesting test

Add readers with configurable nesting level.

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

diff --git a/formal-model/urcu/DEFINES b/formal-model/urcu/DEFINES
index 855dbd5..4224b32 100644
--- a/formal-model/urcu/DEFINES
+++ b/formal-model/urcu/DEFINES
@@ -3,3 +3,7 @@
 
 #define read_free_race	(read_generation == last_free_gen)
 #define read_free	(free_done && data_access)
+
+#ifndef READER_NEST_LEVEL
+#define READER_NEST_LEVEL 1
+#endif
diff --git a/formal-model/urcu/Makefile b/formal-model/urcu/Makefile
index c52c4ba..498241b 100644
--- a/formal-model/urcu/Makefile
+++ b/formal-model/urcu/Makefile
@@ -23,6 +23,7 @@ SPINFILE=urcu.spin
 
 default:
 	make urcu_free | tee urcu_free.log
+	make urcu_free_nested | tee urcu_free_nested.log
 	make urcu_free_no_rmb | tee urcu_free_no_rmb.log
 	make urcu_free_no_wmb | tee urcu_free_no_wmb.log
 	make urcu_free_no_mb | tee urcu_free_no_mb.log
@@ -55,6 +56,13 @@ urcu_free: clean urcu_free_ltl run
 	cp .input.spin $@.spin.input
 	-cp .input.spin.trail $@.spin.input.trail
 
+urcu_free_nested: clean urcu_free_ltl urcu_free_nested_define run
+	cp .input.spin $@.spin.input
+	-cp .input.spin.trail $@.spin.input.trail
+
+urcu_free_nested_define:
+	cp urcu_free_nested.define .input.define
+
 urcu_free_no_rmb: clean urcu_free_ltl urcu_free_no_rmb_define run
 	cp .input.spin $@.spin.input
 	-cp .input.spin.trail $@.spin.input.trail
@@ -129,8 +137,8 @@ urcu_progress_writer_error_define:
 
 urcu_progress_writer_error_ltl:
 	touch .input.define
-	cat DEFINES > pan.ltl
 	cat .input.define >> pan.ltl
+	cat DEFINES > pan.ltl
 	spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
 
 
@@ -144,8 +152,8 @@ pan: pan.c
 	gcc -w ${CFLAGS} -o pan pan.c
 
 pan.c: pan.ltl ${SPINFILE}
-	cat DEFINES > .input.spin
 	cat .input.define >> .input.spin
+	cat DEFINES > .input.spin
 	cat ${SPINFILE} >> .input.spin
 	rm -f .input.spin.trail
 	spin -a -X -N pan.ltl .input.spin
diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin
index e9271f8..17c6612 100644
--- a/formal-model/urcu/urcu.spin
+++ b/formal-model/urcu/urcu.spin
@@ -178,7 +178,7 @@ inline wait_for_quiescent_state(tmp, i, j)
 
 active [NR_READERS] proctype urcu_reader()
 {
-	byte i;
+	byte i, nest_i;
 	byte tmp, tmp2;
 
 	assert(get_pid() < NR_PROCS);
@@ -196,33 +196,47 @@ end_reader:
 #ifdef READER_PROGRESS
 progress_reader:
 #endif
-		ooo_mem(i);
-		tmp = READ_CACHED_VAR(urcu_active_readers_one);
-		ooo_mem(i);
-		if
-		:: (!(tmp & RCU_GP_CTR_NEST_MASK))
-			->
-			tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
+		nest_i = 0;
+		do
+		:: nest_i < READER_NEST_LEVEL ->
 			ooo_mem(i);
-			WRITE_CACHED_VAR(urcu_active_readers_one, tmp2);
-		:: else	->
-			WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1);
-		fi;
+			tmp = READ_CACHED_VAR(urcu_active_readers_one);
+			ooo_mem(i);
+			if
+			:: (!(tmp & RCU_GP_CTR_NEST_MASK))
+				->
+				tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
+				ooo_mem(i);
+				WRITE_CACHED_VAR(urcu_active_readers_one, tmp2);
+			:: else	->
+				WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1);
+			fi;
+			ooo_mem(i);
+			smp_mb(i);
+			nest_i++;
+		:: nest_i >= READER_NEST_LEVEL -> break;
+		od;
+
 		ooo_mem(i);
-		smp_mb(i);
 		read_generation = READ_CACHED_VAR(generation_ptr);
 		ooo_mem(i);
 		data_access = 1;
 		ooo_mem(i);
 		data_access = 0;
+
+		nest_i = 0;
+		do
+		:: nest_i < READER_NEST_LEVEL ->
+			ooo_mem(i);
+			smp_mb(i);
+			ooo_mem(i);
+			tmp2 = READ_CACHED_VAR(urcu_active_readers_one);
+			ooo_mem(i);
+			WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1);
+			nest_i++;
+		:: nest_i >= READER_NEST_LEVEL -> break;
+		od;
 		ooo_mem(i);
-		smp_mb(i);
-		ooo_mem(i);
-		tmp2 = READ_CACHED_VAR(urcu_active_readers_one);
-		ooo_mem(i);
-		WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1);
-		ooo_mem(i);
-		//wakeup_all(i);
 		//smp_mc(i);	/* added */
 	od;
 }