Update formal model from local copy

[urcu.git] / formal-model / futex-wakeup / futex.spin

diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin
index 9f6ddd46cdcb11d838d31144f732452a08736d2e..5459a537b8f4b14f76bdde80eb8dddeb77548e2a 100644 (file)
--- 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;
 }