X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Ffutex-wakeup%2Ffutex.spin;h=5459a537b8f4b14f76bdde80eb8dddeb77548e2a;hb=ba59a0c7b244a0939a2298fc76a9002436ef9674;hp=9f6ddd46cdcb11d838d31144f732452a08736d2e;hpb=d4de486929b21b452a6fd94f2ca6c906c0f6b6b2;p=urcu.git

diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin
index 9f6ddd4..5459a53 100644
--- a/formal-model/futex-wakeup/futex.spin
+++ b/formal-model/futex-wakeup/futex.spin
@@ -46,12 +46,16 @@
  * Copyright (c) 2009 Mathieu Desnoyers
  */
 
-int queue = 0;
+#define get_pid()       (_pid)
+
+int queue[2] = 0;
 int fut = 0;
 
-active proctype waker()
+active [2] proctype waker()
 {
-	queue = 1;
+	assert(get_pid() < 2);
+
+	queue[get_pid()] = 1;
 
 	if
 	:: (fut == -1) ->
@@ -60,7 +64,7 @@ active proctype waker()
 		skip;
 	fi;
 
-	queue = 1;
+	queue[get_pid()] = 1;
 
 	if
 	:: (fut == -1) ->
@@ -70,7 +74,7 @@ active proctype waker()
 	fi;
 
 #ifdef INJ_QUEUE_NO_WAKE
-	queue = 1;
+	queue[get_pid()] = 1;
 #endif
 }
 
@@ -83,7 +87,7 @@ active proctype waiter()
 		fut = fut - 1;
 #endif
 		if
-		:: (queue == 1) ->
+		:: (queue[0] == 1 || queue[1] == 1) ->
 #ifndef INJ_LATE_DEC
 			fut = 0;
 #endif
@@ -98,13 +102,6 @@ active proctype waiter()
 				:: 1 ->
 					if
 					:: (fut == -1) ->
-						if
-						:: (queue == 0) ->
-progress_A:
-							skip;
-						:: else
-							skip;
-						fi;
 						skip;
 					:: else ->
 						break;
@@ -114,7 +111,14 @@ progress_A:
 				skip;
 			fi;
 		fi;
-progress_B:
-		queue = 0;
+progress:
+		if
+		:: queue[0] == 1 ->
+			queue[0] = 0;
+		fi;
+		if
+		:: queue[1] == 1 ->
+			queue[1] = 0;
+		fi;
 	od;
 }