Revert "ticketlock model: state-space simplication"

[urcu.git] / ticketlock / mem.spin

diff --git a/ticketlock/mem.spin b/ticketlock/mem.spin
index 59acfcf054dbb5ac1ae7ad556a315c9b31da88ce..445ee9a6d4193da200ebbf810d2aeb91088b871a 100644 (file)
--- a/ticketlock/mem.spin
+++ b/ticketlock/mem.spin
@@ -44,8 +44,15 @@ inline spin_lock(lock, ticket)
                lock = lock + HIGH_HALF_INC;    /* overflow expected */
        }
 
-       /* busy-wait */
-       LOW_HALF(lock) == ticket -> 1;
+       do
+       :: 1 ->
+               if
+               :: (LOW_HALF(lock) == ticket) ->
+                       break;
+               :: else ->
+                       skip;
+               fi;
+       od;
 }
 
 inline spin_unlock(lock)
@@ -58,7 +65,8 @@ proctype proc_X()
        byte ticket;
 
        do
-       ::      spin_lock(lock, ticket);
+       :: 1->
+               spin_lock(lock, ticket);
                refcount = refcount + 1;
                refcount = refcount - 1;
                spin_unlock(lock);