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 11d98e814dc70c19c6aba5384271e7f116d8ab74..2b6e243c89e8c5ccb129923254ee4addb619585f 100644 (file)
--- 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 788fc44351e154b1fd87fdb43b8208e58204dedd..c68a77b75fbf30217bc07dd26004491a90b460a8 100644 (file)
--- 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 (file)
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