From: Mathieu Desnoyers Date: Sat, 26 Sep 2009 06:51:04 +0000 (-0400) Subject: Add futex wakeup spin model X-Git-Tag: v0.1~30 X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=commitdiff_plain;h=d4de486929b21b452a6fd94f2ca6c906c0f6b6b2 Add futex wakeup spin model Signed-off-by: Mathieu Desnoyers --- diff --git a/formal-model/futex-wakeup/.futex.spin.swp b/formal-model/futex-wakeup/.futex.spin.swp new file mode 100644 index 0000000..4e5aa44 Binary files /dev/null and b/formal-model/futex-wakeup/.futex.spin.swp differ diff --git a/formal-model/futex-wakeup/DEFINES b/formal-model/futex-wakeup/DEFINES new file mode 100644 index 0000000..7c9a54f --- /dev/null +++ b/formal-model/futex-wakeup/DEFINES @@ -0,0 +1 @@ +#define queue_has_entry (queue == 1) diff --git a/formal-model/futex-wakeup/Makefile b/formal-model/futex-wakeup/Makefile new file mode 100644 index 0000000..11d98e8 --- /dev/null +++ b/formal-model/futex-wakeup/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/formal-model/futex-wakeup/futex.ltl b/formal-model/futex-wakeup/futex.ltl new file mode 100644 index 0000000..8718641 --- /dev/null +++ b/formal-model/futex-wakeup/futex.ltl @@ -0,0 +1 @@ +([] <> !np_) diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin new file mode 100644 index 0000000..9f6ddd4 --- /dev/null +++ b/formal-model/futex-wakeup/futex.spin @@ -0,0 +1,120 @@ +/* + * futex.spin: Promela code to validate futex wakeup algorithm. + * + * Algorithm verified : + * + * queue = 0; + * fut = 0; + * runvar = 0; + * + * Waker + * queue = 1; + * if (fut == -1) { + * fut = 0; + * } + * + * Waiter + * while (1) { + * progress: + * fut = fut - 1; + * if (queue == 1) { + * fut = 0; + * } else { + * if (fut == -1) { + * while (fut == -1) { } + * } + * } + * queue = 0; + * } + * + * if queue = 1, then !_np + * + * 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 + */ + +int queue = 0; +int fut = 0; + +active proctype waker() +{ + queue = 1; + + if + :: (fut == -1) -> + fut = 0; + :: else -> + skip; + fi; + + queue = 1; + + if + :: (fut == -1) -> + fut = 0; + :: else -> + skip; + fi; + +#ifdef INJ_QUEUE_NO_WAKE + queue = 1; +#endif +} + + +active proctype waiter() +{ + do + :: 1 -> +#ifndef INJ_LATE_DEC + fut = fut - 1; +#endif + if + :: (queue == 1) -> +#ifndef INJ_LATE_DEC + fut = 0; +#endif + skip; + :: else -> +#ifdef INJ_LATE_DEC + fut = fut - 1; +#endif + if + :: (fut == -1) -> + do + :: 1 -> + if + :: (fut == -1) -> + if + :: (queue == 0) -> +progress_A: + skip; + :: else + skip; + fi; + skip; + :: else -> + break; + fi; + od; + :: else -> + skip; + fi; + fi; +progress_B: + queue = 0; + od; +} diff --git a/formal-model/futex-wakeup/futex_progress_late_dec.define b/formal-model/futex-wakeup/futex_progress_late_dec.define new file mode 100644 index 0000000..01361fb --- /dev/null +++ b/formal-model/futex-wakeup/futex_progress_late_dec.define @@ -0,0 +1 @@ +#define INJ_LATE_DEC diff --git a/formal-model/futex-wakeup/futex_progress_no_wake.define b/formal-model/futex-wakeup/futex_progress_no_wake.define new file mode 100644 index 0000000..527bb77 --- /dev/null +++ b/formal-model/futex-wakeup/futex_progress_no_wake.define @@ -0,0 +1 @@ +#define INJ_QUEUE_NO_WAKE