Revert "spinlock model: Simplify state-space"

This reverts commit a9227ee907160443d0e4b1639b274ab9278d92fa.

Need to study impact on progress.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

diff --git a/spinlock/mem.spin b/spinlock/mem.spin
index 072d4d22c9610b52e91e98085f7794c4d3f2883b..9e87809ea64998947cb27f6b6c88745019f0e2e8 100644 (file)
--- a/spinlock/mem.spin
+++ b/spinlock/mem.spin
@@ -21,7 +21,17 @@ byte refcount = 0;
 
 inline spin_lock(lock)
 {
-       atomic{ !lock -> lock = 1}
+       do
+       :: 1 -> atomic {
+                       if
+                       :: (lock) ->
+                               skip;
+                       :: else ->
+                               lock = 1;
+                               break;
+                       fi;
+               }
+       od;
 }
 
 inline spin_unlock(lock)
@@ -32,7 +42,8 @@ inline spin_unlock(lock)
 proctype proc_X()
 {
        do
-       ::      spin_lock(lock);
+       :: 1 ->
+               spin_lock(lock);
                refcount = refcount + 1;
                refcount = refcount - 1;
                spin_unlock(lock);