X-Git-Url: http://git.lttng.org/?a=blobdiff_plain;f=formal-model%2Ffutex-wakeup%2Ffutex.spin;h=1cb6442ace3a1d5f0df16d82ab2135d6e0b0317d;hb=9b35d5dcf52a88861328f442ee0ef6812ec9b35b;hp=9f6ddd46cdcb11d838d31144f732452a08736d2e;hpb=4ccf3e7c5f7b23c99278d56e95b82b4e337a172b;p=urcu.git

diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin
index 9f6ddd4..1cb6442 100644
--- a/formal-model/futex-wakeup/futex.spin
+++ b/formal-model/futex-wakeup/futex.spin
@@ -98,13 +98,6 @@ active proctype waiter()
 				:: 1 ->
 					if
 					:: (fut == -1) ->
-						if
-						:: (queue == 0) ->
-progress_A:
-							skip;
-						:: else
-							skip;
-						fi;
 						skip;
 					:: else ->
 						break;
@@ -114,7 +107,7 @@ progress_A:
 				skip;
 			fi;
 		fi;
-progress_B:
+progress:
 		queue = 0;
 	od;
 }