From 3646de2f5d9217207c3b5340baae0a2c988f165e Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Sat, 27 Aug 2011 12:32:36 -0400 Subject: [PATCH] 1to1 selective wakeup: add misorder injection test Signed-off-by: Mathieu Desnoyers --- futex-wakeup/nto1-selective/Makefile | 8 ++++++++ futex-wakeup/nto1-selective/futex.spin | 5 +++++ .../nto1-selective/futex_progress_misorder.define | 1 + 3 files changed, 14 insertions(+) create mode 100644 futex-wakeup/nto1-selective/futex_progress_misorder.define diff --git a/futex-wakeup/nto1-selective/Makefile b/futex-wakeup/nto1-selective/Makefile index 11d98e8..2c7f84e 100644 --- a/futex-wakeup/nto1-selective/Makefile +++ b/futex-wakeup/nto1-selective/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_misorder | tee futex_progress_misorder.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_misorder: clean futex_ltl futex_progress_misorder_define run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +futex_progress_misorder_define: + cp futex_progress_misorder.define .input.define + futex_ltl: touch .input.define cat DEFINES > pan.ltl diff --git a/futex-wakeup/nto1-selective/futex.spin b/futex-wakeup/nto1-selective/futex.spin index 6f854fc..558ace1 100644 --- a/futex-wakeup/nto1-selective/futex.spin +++ b/futex-wakeup/nto1-selective/futex.spin @@ -126,8 +126,13 @@ active proctype waiter() do :: 1 -> #ifndef INJ_LATE_DEC +#ifndef INJ_MISORDER futex = -1; waiting[0] = 1; +#else + waiting[0] = 1; + futex = -1; +#endif waiting[1] = 1; #endif diff --git a/futex-wakeup/nto1-selective/futex_progress_misorder.define b/futex-wakeup/nto1-selective/futex_progress_misorder.define new file mode 100644 index 0000000..0d42b57 --- /dev/null +++ b/futex-wakeup/nto1-selective/futex_progress_misorder.define @@ -0,0 +1 @@ +#define INJ_MISORDER -- 2.34.1