From: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Date: Wed, 17 Aug 2011 10:05:42 +0000 (-0400)
Subject: futex model: Add futex_progress_inverted_waiting_vs_gp_futex error injection
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=37acf64d444bf756e8f61e4eaa2ea96fadf84635;p=userspace-rcu.git

futex model: Add futex_progress_inverted_waiting_vs_gp_futex error injection

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

diff --git a/futex-wakeup/Makefile b/futex-wakeup/Makefile
index 11d98e8..2b6e243 100644
--- a/futex-wakeup/Makefile
+++ b/futex-wakeup/Makefile
@@ -29,6 +29,7 @@ default:
 	make futex_progress | tee futex_progress.log
 	make futex_progress_no_wake | tee futex_progress_no_wake.log
 	make futex_progress_late_dec | tee futex_progress_late_dec.log
+	make futex_progress_inverted_waiting_vs_gp_futex | tee futex_progress_inverted_waiting_vs_gp_futex.define.log
 	make asserts | tee asserts.log
 	make summary
 
@@ -68,6 +69,13 @@ futex_progress_late_dec: clean futex_ltl futex_progress_late_dec_define run_weak
 futex_progress_late_dec_define:
 	cp futex_progress_late_dec.define .input.define
 
+futex_progress_inverted_waiting_vs_gp_futex: clean futex_ltl futex_progress_inverted_waiting_vs_gp_futex_define run_weak_fair
+	cp .input.spin $@.spin.input
+	-cp .input.spin.trail $@.spin.input.trail
+
+futex_progress_inverted_waiting_vs_gp_futex_define:
+	cp futex_progress_inverted_waiting_vs_gp_futex.define .input.define
+
 futex_ltl:
 	touch .input.define
 	cat DEFINES > pan.ltl
diff --git a/futex-wakeup/futex.spin b/futex-wakeup/futex.spin
index 788fc44..c68a77b 100644
--- a/futex-wakeup/futex.spin
+++ b/futex-wakeup/futex.spin
@@ -100,7 +100,7 @@ restart:
 	in_registry[1] = 1;
 	do
 	:: 1 ->
-#ifndef INJ_LATE_DEC
+#if (!defined(INJ_LATE_DEC) && !defined(INJ_INVERT_WAITING_VS_GP_FUTEX))
 		gp_futex = -1;
 #endif
 		if
@@ -128,6 +128,9 @@ restart:
 		:: else ->
 			skip;
 		fi;
+#ifdef INJ_INVERT_WAITING_VS_GP_FUTEX
+		gp_futex = -1;
+#endif
 
 		if
 		:: (in_registry[0] == 0 && in_registry[1] == 0) ->
diff --git a/futex-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define b/futex-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define
new file mode 100644
index 0000000..eca05f6
--- /dev/null
+++ b/futex-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define
@@ -0,0 +1 @@
+#define INJ_INVERT_WAITING_VS_GP_FUTEX