[ltt-dev] [PATCH v2 3/3] more interesting late_dec variant

[Paolo Bonzini]

This patch changes the futex_progress_late_dec model to trigger a different
failure, a reordering of the waiting[] assignments vs. the gp_futex
assignment.
---
 futex-wakeup/futex.spin |    8 +++-----
 1 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/futex-wakeup/futex.spin b/futex-wakeup/futex.spin
index 44acd7e..2294b2b 100644
--- a/futex-wakeup/futex.spin
+++ b/futex-wakeup/futex.spin
@@ -113,6 +113,9 @@ restart:
                 :: else ->
 		        skip;
 		fi;
+#ifdef INJ_LATE_DEC
+		gp_futex = -1;
+#endif
 
 		if
 		:: (in_registry[0] == 1 && queue[0] == gp) ->
@@ -130,15 +133,10 @@ restart:
 		if
 		:: (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 ->
-- 
1.7.6