[ltt-dev] [PATCH v2 2/3] model optimization of the waker (selective wake)

[Paolo Bonzini]

This patch adds to the model an optimization, whereby threads are
told whether they are still being waited on, and skip the futex wakeup
if not.
---
 futex-wakeup/futex.spin |   40 +++++++++++++++++++++++++++++++---------
 1 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/futex-wakeup/futex.spin b/futex-wakeup/futex.spin
index ab41a0a..44acd7e 100644
--- a/futex-wakeup/futex.spin
+++ b/futex-wakeup/futex.spin
@@ -9,9 +9,12 @@
  *                          Waker
  *                          while (1) {
  *                            this.queue = gp;
- *                            if (gp_futex == -1) {
- *                              gp_futex = 0;
- *                              futex_wake = 1;
+ *                            if (this.waiting == 1) {
+ *                              this.waiting = 0;
+ *                              if (gp_futex == -1) {
+ *                                gp_futex = 0;
+ *                                futex_wake = 1;
+ *                              }
  *                            }
  *                          }
  *
@@ -19,6 +22,7 @@
  * in_registry = 1;
  * while (1) {
  *   gp_futex = -1;
+ *   waiting |= (queue != gp);
  *   in_registry &= (queue != gp);
  *   if (all in_registry == 0) {
  * progress:
@@ -56,6 +60,7 @@
 #define get_pid()       (_pid)
 
 int queue[2] = 0;
+int waiting[2] = 0;
 int futex_wake = 0;
 int gp_futex = 0;
 int gp = 1;
@@ -69,14 +74,18 @@ active [2] proctype waker()
 	:: 1 ->
 		queue[get_pid()] = gp;
 	
-		if
-		:: (gp_futex == -1) ->
-			gp_futex = 0;
+		if
+		:: (waiting[get_pid()] == 1) ->
+			waiting[get_pid()] = 0;
+			if
+			:: (gp_futex == -1) ->
+				gp_futex = 0;
 #ifndef INJ_QUEUE_NO_WAKE
-			futex_wake = 1;
+				futex_wake = 1;
 #endif
-		:: else ->
-			skip;
+			:: else ->
+				skip;
+			fi;
 		fi;
 	od;
 }
@@ -92,6 +101,18 @@ restart:
 #ifndef INJ_LATE_DEC
 		gp_futex = -1;
 #endif
+		if
+		:: (in_registry[0] == 1 && queue[0] != gp) ->
+			waiting[0] = 1;
+                :: else ->
+		        skip;
+		fi;
+		if
+		:: (in_registry[1] == 1 && queue[1] != gp) ->
+			waiting[1] = 1;
+                :: else ->
+		        skip;
+		fi;
 
 		if
 		:: (in_registry[0] == 1 && queue[0] == gp) ->
@@ -105,6 +126,7 @@ restart:
 		:: else ->
 			skip;
 		fi;
+
 		if
 		:: (in_registry[0] == 0 && in_registry[1] == 0) ->
 progress:
-- 
1.7.6