From 37acf64d444bf756e8f61e4eaa2ea96fadf84635 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Wed, 17 Aug 2011 06:05:42 -0400 Subject: [PATCH] futex model: Add futex_progress_inverted_waiting_vs_gp_futex error injection Signed-off-by: Mathieu Desnoyers --- futex-wakeup/Makefile | 8 ++++++++ futex-wakeup/futex.spin | 5 ++++- .../futex_progress_inverted_waiting_vs_gp_futex.define | 1 + 3 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 futex-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define 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 -- 2.34.1