[ltt-dev] [PATCH v2 1/3] new futex model

[Paolo Bonzini]

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.
---
 futex-wakeup/DEFINES    |    2 +-
 futex-wakeup/futex.ltl  |    2 +-
 futex-wakeup/futex.spin |  134 +++++++++++++++++++++++++----------------------
 3 files changed, 73 insertions(+), 65 deletions(-)

diff --git a/futex-wakeup/DEFINES b/futex-wakeup/DEFINES
index e328b55..3e0a545 100644
--- 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 3d6842e..8718641 100644
--- 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 5459a53..ab41a0a 100644
--- 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 +56,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;
 }
-- 
1.7.6