From: Mathieu Desnoyers Date: Sat, 27 Aug 2011 15:08:39 +0000 (-0400) Subject: Add nto1 futex wakeup scheme model X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=e922fbe49f26c6bee783582aadbecf794aae1d64;p=userspace-rcu.git Add nto1 futex wakeup scheme model Signed-off-by: Mathieu Desnoyers --- diff --git a/futex-wakeup/nto1/DEFINES b/futex-wakeup/nto1/DEFINES new file mode 100644 index 0000000..c6d28b2 --- /dev/null +++ b/futex-wakeup/nto1/DEFINES @@ -0,0 +1 @@ +#define queue_has_entry (queue[0] == 1 || queue[1] == 1) diff --git a/futex-wakeup/nto1/Makefile b/futex-wakeup/nto1/Makefile new file mode 100644 index 0000000..11d98e8 --- /dev/null +++ b/futex-wakeup/nto1/Makefile @@ -0,0 +1,108 @@ +# 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_no_wake | tee futex_progress_no_wake.log + make futex_progress_late_dec | tee futex_progress_late_dec.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_late_dec: clean futex_ltl futex_progress_late_dec_define run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +futex_progress_late_dec_define: + cp futex_progress_late_dec.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/nto1/futex.ltl b/futex-wakeup/nto1/futex.ltl new file mode 100644 index 0000000..3d6842e --- /dev/null +++ b/futex-wakeup/nto1/futex.ltl @@ -0,0 +1 @@ +([] <> ((!np_) || (!queue_has_entry))) diff --git a/futex-wakeup/nto1/futex.spin b/futex-wakeup/nto1/futex.spin new file mode 100644 index 0000000..f599a00 --- /dev/null +++ b/futex-wakeup/nto1/futex.spin @@ -0,0 +1,152 @@ +/* + * futex.spin: Promela code to validate n wakers to 1 waiter futex + * wakeup algorithm. + * + * In this model, waker threads unconditionally wake the waiter if it + * needs to be awakened. We guarantee that the waiter will never wait + * forever if it needs to be awakened, even if the waker is inactive + * after requiring the wakeup. + * + * Algorithm verified : + * + * queue = 0; + * futex = 0; + * futex_wake = 0; + * + * n wakers (2 loops) + * + * queue = 1; + * if (futex == -1) { + * futex = 0; + * futex_wake = 1; + * } + * + * 1 waiter + * + * while (1) { + * progress: + * futex = -1; + * if (queue == 1) { + * futex = 0; + * } else { + * if (futex == -1) { + * futex_wake = (futex == -1 ? 0 : 1); (atomic) + * while (futex_wake == 0) { }; + * } + * queue = 0; + * } + * + * if queue = 1, then !_np + * + * By testing progress, i.e. [] <> ((!np_) || (!queue_has_entry)), we + * check that we can never block forever if there is an entry in the + * queue. + * + * 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 + * enqueuing. + * + * 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 queue[2] = 0; +int futex = 0; +int futex_wake = 0; + +active [2] proctype waker() +{ + assert(get_pid() < 2); + + /* loop 1 */ + queue[get_pid()] = 1; + + if + :: (futex == -1) -> + futex = 0; + futex_wake = 1; + :: else -> + skip; + fi; + + /* loop 2 */ + queue[get_pid()] = 1; + + if + :: (futex == -1) -> + futex = 0; + futex_wake = 1; + :: else -> + skip; + fi; + +#ifdef INJ_QUEUE_NO_WAKE + /* loop 3 */ + queue[get_pid()] = 1; +#endif +} + + +active proctype waiter() +{ + do + :: 1 -> +#ifndef INJ_LATE_DEC + futex = -1; +#endif + + if + :: (queue[0] == 1 || queue[1] == 1) -> +#ifndef INJ_LATE_DEC + futex = 0; +#endif + skip; + :: else -> +#ifdef INJ_LATE_DEC + futex = -1; +#endif + if + :: (futex == -1) -> + 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; + fi; +progress: /* Progress on dequeue */ + queue[0] = 0; + queue[1] = 0; + od; + +} diff --git a/futex-wakeup/nto1/futex_progress_late_dec.define b/futex-wakeup/nto1/futex_progress_late_dec.define new file mode 100644 index 0000000..01361fb --- /dev/null +++ b/futex-wakeup/nto1/futex_progress_late_dec.define @@ -0,0 +1 @@ +#define INJ_LATE_DEC diff --git a/futex-wakeup/nto1/futex_progress_no_wake.define b/futex-wakeup/nto1/futex_progress_no_wake.define new file mode 100644 index 0000000..527bb77 --- /dev/null +++ b/futex-wakeup/nto1/futex_progress_no_wake.define @@ -0,0 +1 @@ +#define INJ_QUEUE_NO_WAKE