X-Git-Url: https://git.liburcu.org/?a=blobdiff_plain;f=spinlock%2Fmem.spin;h=9e87809ea64998947cb27f6b6c88745019f0e2e8;hb=refs%2Fheads%2Fformal-model;hp=db8a8b3b66247edcd1e1bd9656fa2597b5c990ae;hpb=03126291913d3c2df1d92137cf82767d9b490ade;p=urcu.git

diff --git a/spinlock/mem.spin b/spinlock/mem.spin
index db8a8b3..9e87809 100644
--- 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);