From: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Date: Mon, 8 Oct 2012 21:48:58 +0000 (-0400)
Subject: ticketlock model: state-space simplication
X-Git-Url: https://git.lttng.org/?p=urcu.git;a=commitdiff_plain;h=d149fa02aaafa08c2d02712afd3cbbbc5f8d5f67

ticketlock model: state-space simplication

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

diff --git a/ticketlock/mem-progress.spin b/ticketlock/mem-progress.spin
index dad43a4..b739541 100644
--- a/ticketlock/mem-progress.spin
+++ b/ticketlock/mem-progress.spin
@@ -45,15 +45,8 @@ inline spin_lock(lock, ticket)
 		lock = lock + HIGH_HALF_INC;	/* overflow expected */
 	}
 
-	do
-	:: 1 ->
-		if
-		:: (LOW_HALF(lock) == ticket) ->
-			break;
-		:: else ->
-			skip;
-		fi;
-	od;
+	/* busy-wait */
+	LOW_HALF(lock) == ticket -> 1;
 }
 
 inline spin_unlock(lock)
@@ -66,9 +59,9 @@ proctype proc_A()
 	byte ticket;
 
 	do
-	:: 1 ->
-progress_A:
+	:: 
 		spin_lock(lock, ticket);
+progress_A:
 		refcount = refcount + 1;
 		refcount = refcount - 1;
 		spin_unlock(lock);
@@ -80,8 +73,7 @@ proctype proc_B()
 	byte ticket;
 
 	do
-	:: 1 ->
-		spin_lock(lock, ticket);
+	:: 	spin_lock(lock, ticket);
 		refcount = refcount + 1;
 		refcount = refcount - 1;
 		spin_unlock(lock);
diff --git a/ticketlock/mem.spin b/ticketlock/mem.spin
index 445ee9a..59acfcf 100644
--- a/ticketlock/mem.spin
+++ b/ticketlock/mem.spin
@@ -44,15 +44,8 @@ inline spin_lock(lock, ticket)
 		lock = lock + HIGH_HALF_INC;	/* overflow expected */
 	}
 
-	do
-	:: 1 ->
-		if
-		:: (LOW_HALF(lock) == ticket) ->
-			break;
-		:: else ->
-			skip;
-		fi;
-	od;
+	/* busy-wait */
+	LOW_HALF(lock) == ticket -> 1;
 }
 
 inline spin_unlock(lock)
@@ -65,8 +58,7 @@ proctype proc_X()
 	byte ticket;
 
 	do
-	:: 1->
-		spin_lock(lock, ticket);
+	::	spin_lock(lock, ticket);
 		refcount = refcount + 1;
 		refcount = refcount - 1;
 		spin_unlock(lock);