Fix makefile, set default nesting to 2

[urcu.git] / formal-model / urcu / urcu.spin

diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin
index 17c6612c8c23880961be2fa63d99b08cfb09e030..903782b352ee6a5f8a1d58af29b78fbfea46f355 100644 (file)
--- 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);