X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Ffutex-wakeup%2Ffutex.spin;fp=formal-model%2Ffutex-wakeup%2Ffutex.spin;h=5459a537b8f4b14f76bdde80eb8dddeb77548e2a;hp=1cb6442ace3a1d5f0df16d82ab2135d6e0b0317d;hb=29f38067765e2d60bbf9bebcf6b7d3084b8bdec0;hpb=9b35d5dcf52a88861328f442ee0ef6812ec9b35b

diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin
index 1cb6442..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
@@ -108,6 +112,13 @@ active proctype waiter()
 			fi;
 		fi;
 progress:
-		queue = 0;
+		if
+		:: queue[0] == 1 ->
+			queue[0] = 0;
+		fi;
+		if
+		:: queue[1] == 1 ->
+			queue[1] = 0;
+		fi;
 	od;
 }