Fix formal model nesting

Also, the original model I sent out has a minor bug that prevents it
from fully modeling the nested-read-side case.  The patch below fixes this.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
index e5bfff32464c0e4d6d0985df50cb8fa6db2555b0..611464b3eb660b61d6269b5c64210afe6754d950 100644 (file)
--- a/formal-model/urcu.spin
+++ b/formal-model/urcu.spin
@@ -124,9 +124,13 @@ proctype urcu_reader()
                                break;
                        :: tmp < 4 && reader_progress[tmp] != 0 ->
                                tmp = tmp + 1;
-                       :: tmp >= 4 ->
+                       :: tmp >= 4 &&
+                          reader_progress[0] == reader_progress[3] ->
                                done = 1;
                                break;
+                       :: tmp >= 4 &&
+                          reader_progress[0] != reader_progress[3] ->
+                               break;
                        od;
                        do
                        :: tmp < 4 && reader_progress[tmp] == 0 ->