Add multiple reader queues to futex model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

diff --git a/formal-model/futex-wakeup/DEFINES b/formal-model/futex-wakeup/DEFINES
index 7c9a54f1d866ed54596a2147254193caebaf729b..e328b5577fc6d914170a7104c9059598a46d1a8a 100644 (file)
--- a/formal-model/futex-wakeup/DEFINES
+++ b/formal-model/futex-wakeup/DEFINES
@@ -1 +1 @@
-#define queue_has_entry        (queue == 1)
+#define queue_has_entry        (queue[0] == 1 || queue[1] == 1)

diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin
index 1cb6442ace3a1d5f0df16d82ab2135d6e0b0317d..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
@@ -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;
 }