Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
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 | 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
make asserts | tee asserts.log
make summary
futex_progress_late_dec_define:
cp futex_progress_late_dec.define .input.define
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
futex_ltl:
touch .input.define
cat DEFINES > pan.ltl
do
:: 1 ->
#ifndef INJ_LATE_DEC
do
:: 1 ->
#ifndef INJ_LATE_DEC
futex = -1;
waiting[0] = 1;
futex = -1;
waiting[0] = 1;
+#else
+ waiting[0] = 1;
+ futex = -1;
+#endif