From: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Date: Tue, 9 Oct 2012 04:12:47 +0000 (-0400)
Subject: Revert "spinlock model: Simplify state-space"
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=refs%2Fheads%2Fformal-model;p=userspace-rcu.git

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 072d4d2..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);