From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Thu, 26 Feb 2009 23:13:46 +0000 (-0500)
Subject: Fix makefile, set default nesting to 2
X-Git-Tag: v0.1~272
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=d4e437ba8e99a9cd38c4ccb1c243427935c8f293;p=userspace-rcu.git

Fix makefile, set default nesting to 2

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

diff --git a/formal-model/urcu/Makefile b/formal-model/urcu/Makefile
index 498241b..4488219 100644
--- a/formal-model/urcu/Makefile
+++ b/formal-model/urcu/Makefile
@@ -93,8 +93,8 @@ urcu_free_single_flip_define:
 
 urcu_free_ltl:
 	touch .input.define
-	cat DEFINES > pan.ltl
 	cat .input.define >> pan.ltl
+	cat DEFINES >> pan.ltl
 	spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl
 
 # Progress checks
@@ -109,8 +109,8 @@ urcu_progress_writer_define:
 
 urcu_progress_writer_ltl:
 	touch .input.define
-	cat DEFINES > pan.ltl
-	cat .input.define >> pan.ltl
+	cat .input.define > pan.ltl
+	cat DEFINES >> pan.ltl
 	spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
 
 urcu_progress_reader: clean urcu_progress_reader_ltl \
@@ -123,8 +123,8 @@ urcu_progress_reader_define:
 
 urcu_progress_reader_ltl:
 	touch .input.define
-	cat DEFINES > pan.ltl
-	cat .input.define >> pan.ltl
+	cat .input.define > pan.ltl
+	cat DEFINES >> pan.ltl
 	spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
 
 urcu_progress_writer_error: clean urcu_progress_writer_error_ltl \
@@ -137,8 +137,8 @@ urcu_progress_writer_error_define:
 
 urcu_progress_writer_error_ltl:
 	touch .input.define
-	cat .input.define >> pan.ltl
-	cat DEFINES > pan.ltl
+	cat .input.define > pan.ltl
+	cat DEFINES >> pan.ltl
 	spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
 
 
@@ -152,8 +152,8 @@ pan: pan.c
 	gcc -w ${CFLAGS} -o pan pan.c
 
 pan.c: pan.ltl ${SPINFILE}
-	cat .input.define >> .input.spin
-	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 17c6612..903782b 100644
--- a/formal-model/urcu/urcu.spin
+++ b/formal-model/urcu/urcu.spin
@@ -209,7 +209,8 @@ progress_reader:
 				ooo_mem(i);
 				WRITE_CACHED_VAR(urcu_active_readers_one, tmp2);
 			:: else	->
-				WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1);
+				WRITE_CACHED_VAR(urcu_active_readers_one,
+						 tmp + 1);
 			fi;
 			ooo_mem(i);
 			smp_mb(i);
@@ -285,7 +286,7 @@ progress_writer1:
 		//smp_mc(i);
 		wait_for_quiescent_state(tmp, i, j);
 		//smp_mc(i);
-	#ifndef SINGLE_FLIP
+#ifndef SINGLE_FLIP
 		ooo_mem(i);
 		tmp = READ_CACHED_VAR(urcu_gp_ctr);
 		ooo_mem(i);
@@ -293,7 +294,7 @@ progress_writer1:
 		//smp_mc(i);
 		ooo_mem(i);
 		wait_for_quiescent_state(tmp, i, j);
-	#endif
+#endif
 		ooo_mem(i);
 		smp_mb(i);
 		ooo_mem(i);