From: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Date: Tue, 9 Oct 2012 04:12:03 +0000 (-0400)
Subject: Revert "ticketlock model: state-space simplication"
X-Git-Url: https://git.lttng.org/?p=urcu.git;a=commitdiff_plain;h=7ecea09ec7dfbfd9ad1db25f217b85abd89664d0

Revert "ticketlock model: state-space simplication"

This reverts commit d149fa02aaafa08c2d02712afd3cbbbc5f8d5f67.

Need to study impact on progress.

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

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