new futex model

Rewrite the model to include the futex primitives and the list
move algorithm used by urcu.  The model implements a full-blown
parity-flipping RCU where grace period waits are driven exclusively
by futexes.  It runs the waker and waiter infinitely, asserting
that progress states (parity flips) are reached infinite times.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

diff --git a/futex-wakeup/DEFINES b/futex-wakeup/DEFINES
index e328b5577fc6d914170a7104c9059598a46d1a8a..3e0a5456786b7ae54e5d39e24b09e19c1e5278bb 100644 (file)
--- a/futex-wakeup/DEFINES
+++ b/futex-wakeup/DEFINES
@@ -1 +1 @@
-#define queue_has_entry        (queue[0] == 1 || queue[1] == 1)
+/* no defines needed yet */

diff --git a/futex-wakeup/futex.ltl b/futex-wakeup/futex.ltl
index 3d6842e5d9971e1212a77a2fab94f764d6aa0cf6..87186413c9ba4e59e8b4c3814696692c1f974418 100644 (file)
--- a/futex-wakeup/futex.ltl
+++ b/futex-wakeup/futex.ltl
@@ -1 +1 @@
-([] <> ((!np_) || (!queue_has_entry)))
+([] <> !np_)

diff --git a/futex-wakeup/futex.spin b/futex-wakeup/futex.spin
index 5459a537b8f4b14f76bdde80eb8dddeb77548e2a..381174b1236950f03c3395e8aba27d53012079a9 100644 (file)
--- a/futex-wakeup/futex.spin
+++ b/futex-wakeup/futex.spin
@@ -4,30 +4,39 @@
  * Algorithm verified :
  *
  * queue = 0;
- * fut = 0;
- * runvar = 0;
+ * waiting = 0;
+ * gp_futex = 0;
+ * gp = 1;
  *
- *                            Waker
- *                            queue = 1;
- *                            if (fut == -1) {
- *                              fut = 0;
+ *                          Waker
+ *                          while (1) {
+ *                            this.queue = gp;
+ *                            if (gp_futex == -1) {
+ *                              gp_futex = 0;
+ *                              futex_wake = 1;
  *                            }
+ *                          }
  *
  * Waiter
+ * in_registry = 1;
  * while (1) {
- *   progress:
- *   fut = fut - 1;
- *   if (queue == 1) {
- *     fut = 0;
+ *   gp_futex = -1;
+ *   in_registry &= (queue != gp);
+ *   if (all in_registry == 0) {
+ * progress:
+ *     gp_futex = 0;
+ *     gp = !gp;
+ *     restart;
  *   } else {
- *     if (fut == -1) {
- *        while (fut == -1) { }
- *     }
+ *     futex_wake = (gp_futex == -1 ? 0 : 1);
+ *     while (futex_wake == 0) { }
  *   }
  *   queue = 0;
  * }
  *
- * if queue = 1, then !_np
+ * By testing progress, i.e. [] <> !np_, we check that an infinite sequence
+ * of update_counter_and_wait (and consequently of synchronize_rcu) will
+ * not block.
  *
  * This program is free software; you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
@@ -49,76 +58,77 @@
 #define get_pid()       (_pid)
 
 int queue[2] = 0;
-int fut = 0;
+int futex_wake = 0;
+int gp_futex = 0;
+int gp = 1;
+int in_registry[2] = 0;
 
 active [2] proctype waker()
 {
        assert(get_pid() < 2);
 
-       queue[get_pid()] = 1;
-
-       if
-       :: (fut == -1) ->
-               fut = 0;
-       :: else ->
-               skip;
-       fi;
-
-       queue[get_pid()] = 1;
-
-       if
-       :: (fut == -1) ->
-               fut = 0;
-       :: else ->
-               skip;
-       fi;
-
-#ifdef INJ_QUEUE_NO_WAKE
-       queue[get_pid()] = 1;
+       do
+       :: 1 ->
+               queue[get_pid()] = gp;
+       
+               if
+               :: (gp_futex == -1) ->
+                       gp_futex = 0;
+#ifndef INJ_QUEUE_NO_WAKE
+                       futex_wake = 1;
 #endif
+               :: else ->
+                       skip;
+               fi;
+       od;
 }
 
 
 active proctype waiter()
 {
+restart:
+       in_registry[0] = 1;
+       in_registry[1] = 1;
        do
        :: 1 ->
 #ifndef INJ_LATE_DEC
-               fut = fut - 1;
+               gp_futex = -1;
 #endif
+
                if
-               :: (queue[0] == 1 || queue[1] == 1) ->
-#ifndef INJ_LATE_DEC
-                       fut = 0;
-#endif
-                       skip;
+               :: (in_registry[0] == 1 && queue[0] == gp) ->
+                       in_registry[0] = 0;
                :: else ->
-#ifdef INJ_LATE_DEC
-                       fut = fut - 1;
-#endif
-                       if
-                       :: (fut == -1) ->
-                               do
-                               :: 1 ->
-                                       if
-                                       :: (fut == -1) ->
-                                               skip;
-                                       :: else ->
-                                               break;
-                                       fi;
-                               od;
-                       :: else ->
-                               skip;
-                       fi;
+                       skip;
                fi;
-progress:
                if
-               :: queue[0] == 1 ->
-                       queue[0] = 0;
+               :: (in_registry[1] == 1 && queue[1] == gp) ->
+                       in_registry[1] = 0;
+               :: else ->
+                       skip;
                fi;
                if
-               :: queue[1] == 1 ->
-                       queue[1] = 0;
+               :: (in_registry[0] == 0 && in_registry[1] == 0) ->
+progress:
+#ifndef INJ_LATE_DEC
+                       gp_futex = 0;
+#endif
+                       gp = !gp;
+                       goto restart;
+               :: else ->
+#ifdef INJ_LATE_DEC
+                       gp_futex = -1;
+#endif
+                       futex_wake = gp_futex + 1;
+                       do
+                       :: 1 ->
+                               if
+                               :: (futex_wake == 0) ->
+                                       skip;
+                               :: else ->
+                                       break;
+                               fi;
+                       od;
                fi;
        od;
 }