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 e9271f82bb58e3acdef1db13aa7226e011d48200..903782b352ee6a5f8a1d58af29b78fbfea46f355 100644 (file)
--- 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,48 @@ 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;
 }
@@ -271,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);
@@ -279,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);