spinlock model: Simplify state-space

[userspace-rcu.git] / spinlock / mem.spin

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