From: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Date: Mon, 8 Oct 2012 21:30:57 +0000 (-0400)
Subject: spinlock model: Simplify state-space
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=a9227ee907160443d0e4b1639b274ab9278d92fa;p=userspace-rcu.git

spinlock model: Simplify state-space

Remove useless busy-looping, useless in Promela. Same semantic as the
new code:

Quoting Michel Dagenais <michel.dagenais@polymtl.ca>:

> http://spinroot.com/spin/Man/condition.html
> In Promela , a standalone expression is a valid statement. Execution
> of a condition statement is blocked until the expression evaluates to
> a non-zero value (or, equivalently, to the boolean value true ).
>
> http://spinroot.com/spin/Man/separators.html
> The semicolon and the arrow are equivalent statement separators in
> Promela. The convention is to reserve the use of the arrow separator
> to follow condition statements. The arrow symbol can thus be used to
> visually identify those points in the code where execution could
> block.

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

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