X-Git-Url: http://git.liburcu.org/?p=userspace-rcu.git;a=blobdiff_plain;f=ticketlock%2Fmem-progress.spin;fp=ticketlock%2Fmem-progress.spin;h=dad43a45062a90e307b9b00c44d0eafe66bc49d3;hp=b7395413dea110b4006e50313168579b9eebcbea;hb=7ecea09ec7dfbfd9ad1db25f217b85abd89664d0;hpb=d149fa02aaafa08c2d02712afd3cbbbc5f8d5f67

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);