From ef781656a07c5a52fd09508336994f29c8bb8cb3 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Sat, 27 Aug 2011 13:53:02 -0400 Subject: [PATCH] Add 1ton readonly waiter model Signed-off-by: Mathieu Desnoyers --- futex-wakeup/1ton-readonly-waiter/DEFINES | 1 + futex-wakeup/1ton-readonly-waiter/Makefile | 116 +++++++++++++ futex-wakeup/1ton-readonly-waiter/futex.ltl | 1 + futex-wakeup/1ton-readonly-waiter/futex.spin | 153 ++++++++++++++++++ .../futex_progress_misorder.define | 1 + .../futex_progress_misorder_wake.define | 1 + .../futex_progress_no_wake.define | 1 + 7 files changed, 274 insertions(+) create mode 100644 futex-wakeup/1ton-readonly-waiter/DEFINES create mode 100644 futex-wakeup/1ton-readonly-waiter/Makefile create mode 100644 futex-wakeup/1ton-readonly-waiter/futex.ltl create mode 100644 futex-wakeup/1ton-readonly-waiter/futex.spin create mode 100644 futex-wakeup/1ton-readonly-waiter/futex_progress_misorder.define create mode 100644 futex-wakeup/1ton-readonly-waiter/futex_progress_misorder_wake.define create mode 100644 futex-wakeup/1ton-readonly-waiter/futex_progress_no_wake.define diff --git a/futex-wakeup/1ton-readonly-waiter/DEFINES b/futex-wakeup/1ton-readonly-waiter/DEFINES new file mode 100644 index 0000000..23e90f2 --- /dev/null +++ b/futex-wakeup/1ton-readonly-waiter/DEFINES @@ -0,0 +1 @@ +#define isactive (_active == 1) diff --git a/futex-wakeup/1ton-readonly-waiter/Makefile b/futex-wakeup/1ton-readonly-waiter/Makefile new file mode 100644 index 0000000..2fe2c96 --- /dev/null +++ b/futex-wakeup/1ton-readonly-waiter/Makefile @@ -0,0 +1,116 @@ +# This program is free software; you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program; if not, write to the Free Software +# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. +# +# Copyright (C) Mathieu Desnoyers, 2009 +# +# Authors: Mathieu Desnoyers + +#CFLAGS=-DSAFETY +#CFLAGS=-DHASH64 -DREACH +CFLAGS=-DHASH64 + +#try pan -i to get the smallest trace. + +SPINFILE=futex.spin +SPINFILE_FAIR=futex.spin + +default: + make futex_progress | tee futex_progress.log + make futex_progress_misorder | tee futex_progress_misorder.log + make futex_progress_no_wake | tee futex_progress_no_wake.log + make futex_progress_misorder_wake | tee futex_progress_misorder_wake.log + make asserts | tee asserts.log + make summary + +#show trail : spin -v -t -N pan.ltl input.spin +# after each individual make. + +summary: + @echo + @echo "Verification summary" + @grep error *.log + +asserts: clean + cat DEFINES > .input.spin + cat ${SPINFILE} >> .input.spin + rm -f .input.spin.trail + spin -a -X .input.spin + gcc -w ${CFLAGS} -DSAFETY -o pan pan.c + ./pan -v -c1 -X -m10000000 -w19 + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +futex_progress: clean futex_ltl run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +futex_progress_no_wake: clean futex_ltl futex_progress_no_wake_define run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +futex_progress_no_wake_define: + cp futex_progress_no_wake.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_progress_misorder_wake: clean futex_ltl futex_progress_misorder_wake_define run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +futex_progress_misorder_wake_define: + cp futex_progress_misorder_wake.define .input.define + +futex_ltl: + touch .input.define + cat DEFINES > pan.ltl + cat .input.define >> pan.ltl + spin -f "!(`cat futex.ltl | grep -v ^//`)" >> pan.ltl + +run: pan + ./pan -a -v -c1 -X -m10000000 -w19 + +pan: pan.c + gcc -w ${CFLAGS} -o pan pan.c + +pan.c: pan.ltl ${SPINFILE} + cat DEFINES > .input.spin + cat .input.define >> .input.spin + cat ${SPINFILE} >> .input.spin + rm -f .input.spin.trail + spin -a -X -N pan.ltl .input.spin + +run_weak_fair: pan_fair + ./pan_fair -a -f -v -c1 -X -m10000000 -w20 + +pan_fair: pan_fair.c + gcc -w ${CFLAGS} -o pan_fair pan_fair.c + +pan_fair.c: pan.ltl ${SPINFILE_FAIR} + cat DEFINES > .input.spin + cat .input.define >> .input.spin + cat ${SPINFILE_FAIR} >> .input.spin + rm -f .input.spin.trail + spin -a -X -N pan.ltl .input.spin + mv pan.c pan_fair.c + +.PHONY: clean default distclean summary +clean: + rm -f pan* trail.out .input.spin* *.spin.trail .input.define +distclean: + rm -f *.trail *.input *.log diff --git a/futex-wakeup/1ton-readonly-waiter/futex.ltl b/futex-wakeup/1ton-readonly-waiter/futex.ltl new file mode 100644 index 0000000..b3c5981 --- /dev/null +++ b/futex-wakeup/1ton-readonly-waiter/futex.ltl @@ -0,0 +1 @@ +([] <> ((!np_) || (!isactive))) diff --git a/futex-wakeup/1ton-readonly-waiter/futex.spin b/futex-wakeup/1ton-readonly-waiter/futex.spin new file mode 100644 index 0000000..2038308 --- /dev/null +++ b/futex-wakeup/1ton-readonly-waiter/futex.spin @@ -0,0 +1,153 @@ +/* + * futex.spin: Promela code to validate 1 waker to n waiters futex + * wakeup algorithm, where waiters have read-only access to the futex. + * + * In this model, the waker thread unconditionally wakes all waiters if + * they need to be awakened. We guarantee that all waiters will never + * wait forever if they need to be awakened, even if the waker is + * inactive after requiring the wakeup. When "active" is set (e.g. a + * daemon is available to service waiter requests), the waiter should + * progress. + * + * Algorithm verified : + * + * active = 0; (waker daemon is active) + * futex = 0; + * futex_wake = 0; + * + * 1 waker (2 loops) + * + * futex = 0; + * active = 1; (e.g. listen()) + * futex_wake = 1; + * active = 0; (e.g. close()) + * futex = -1; + * + * n waiters (read-only) + * + * while (1) { + * if (active == 0) { + * if (futex == -1) { + * futex_wake = (futex == -1 ? 0 : 1); (atomic) + * while (futex_wake == 0) { }; + * } + * } + * progress: + * } + * + * if active = 1, then !_np + * + * By testing progress, i.e. [] <> ((!np_) || (!isactive)), we + * check that waiters we can never block forever if the waker is active. + * + * The waker performs only 2 loops (and NOT an infinite number of loops) + * because we really want to see what happens when the waker stops + * running. + * + * This program is free software; you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation; either version 2 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + * + * Copyright (c) 2009 Mathieu Desnoyers + */ + +#define get_pid() (_pid) + +int _active = 0; +int futex = 0; +int futex_wake = 0; + +active proctype waker() +{ + /* loop 1 */ + futex = 0; + _active = 1; + futex_wake = 1; + _active = 0; + futex = -1; + + /* loop 2 */ +#ifndef INJ_MISORDER_WAKE + futex = 0; + _active = 1; + futex_wake = 1; +#else + futex_wake = 1; + futex = 0; + _active = 1; +#endif + +#ifdef INJ_QUEUE_NO_WAKE + _active = 0; + futex = -1; + + /* loop 3 */ + futex = 0; + _active = 1; +#endif +} + +/* + * The INJ_MISORDER error-injection test case succeeds, which means + * order of active vs futex value read does not matter. It is + * understandable because every time the active value is enabled by the + * waker, a wake is performed. + * + * However, the order in which wakeup sets the futex value vs sending + * the wakeup DOES matter, as shows the INJ_MISORDER_WAKE + * error-injection. + */ +active [2] proctype waiter() +{ + do + :: 1 -> + if +#ifndef INJ_MISORDER + :: (_active == 0) -> +#else + :: (futex == -1) -> +#endif + if +#ifndef INJ_MISORDER + :: (futex == -1) -> +#else + :: (_active == 0) -> +#endif + atomic { + if + :: (futex == -1) -> + futex_wake = 0; + :: else -> + futex_wake = 1; + fi; + } + /* block */ + do + :: 1 -> + if + :: (futex_wake == 0) -> + skip; + :: else -> + break; + fi; + od; + :: else -> + skip; + fi; + :: else -> + skip; + fi; +progress: + skip; + od; +} diff --git a/futex-wakeup/1ton-readonly-waiter/futex_progress_misorder.define b/futex-wakeup/1ton-readonly-waiter/futex_progress_misorder.define new file mode 100644 index 0000000..0d42b57 --- /dev/null +++ b/futex-wakeup/1ton-readonly-waiter/futex_progress_misorder.define @@ -0,0 +1 @@ +#define INJ_MISORDER diff --git a/futex-wakeup/1ton-readonly-waiter/futex_progress_misorder_wake.define b/futex-wakeup/1ton-readonly-waiter/futex_progress_misorder_wake.define new file mode 100644 index 0000000..8de7df6 --- /dev/null +++ b/futex-wakeup/1ton-readonly-waiter/futex_progress_misorder_wake.define @@ -0,0 +1 @@ +#define INJ_MISORDER_WAKE diff --git a/futex-wakeup/1ton-readonly-waiter/futex_progress_no_wake.define b/futex-wakeup/1ton-readonly-waiter/futex_progress_no_wake.define new file mode 100644 index 0000000..527bb77 --- /dev/null +++ b/futex-wakeup/1ton-readonly-waiter/futex_progress_no_wake.define @@ -0,0 +1 @@ +#define INJ_QUEUE_NO_WAKE -- 2.34.1