From d4de486929b21b452a6fd94f2ca6c906c0f6b6b2 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Sat, 26 Sep 2009 02:51:04 -0400 Subject: [PATCH] Add futex wakeup spin model Signed-off-by: Mathieu Desnoyers --- formal-model/futex-wakeup/.futex.spin.swp | Bin 0 -> 12288 bytes formal-model/futex-wakeup/DEFINES | 1 + formal-model/futex-wakeup/Makefile | 108 ++++++++++++++++ formal-model/futex-wakeup/futex.ltl | 1 + formal-model/futex-wakeup/futex.spin | 120 ++++++++++++++++++ .../futex_progress_late_dec.define | 1 + .../futex_progress_no_wake.define | 1 + 7 files changed, 232 insertions(+) create mode 100644 formal-model/futex-wakeup/.futex.spin.swp create mode 100644 formal-model/futex-wakeup/DEFINES create mode 100644 formal-model/futex-wakeup/Makefile create mode 100644 formal-model/futex-wakeup/futex.ltl create mode 100644 formal-model/futex-wakeup/futex.spin create mode 100644 formal-model/futex-wakeup/futex_progress_late_dec.define create mode 100644 formal-model/futex-wakeup/futex_progress_no_wake.define diff --git a/formal-model/futex-wakeup/.futex.spin.swp b/formal-model/futex-wakeup/.futex.spin.swp new file mode 100644 index 0000000000000000000000000000000000000000..4e5aa44ca9b6363250f0ac39aace1f9ded312f34 GIT binary patch literal 12288 zcmeI2U1%It6vuB1(ym%9_DK*qZJ{J(H@lnA)@G?VNjJ^be60Inj3{At=g#h!*}3a{ zBuztGL3~ml^vx$}K_3)~=z}N*wN;9h>PtZo1knfSlhOxE3sV1gcJ?FfHhuBMatD6d z%$#%2J?DSV+=b*;QqSh5>A+B$;o8pF-cQ$#+MD;Yk6&c0DjLnecu86|yh6W*s8}}N z(C=gvFlmTtGVr+THT5b_xYZzO3b&!#iH0z^oiqcVA4@Fji#%wyZic+37uXE0Z)5B#_znC5 zegV>#O*os3DYSK zm8~+p>RU^kAYs*CX>wZDEuXssgXrQDo$A_+u)eNm%Gq*uVP1Z#VxjKvm8HMs<5}^O}j$m$Y^g8(70%>xK^$1(?E5QhEu77 zG_Ct}iwAU=dyZJac~kgF*9j3ghVEO!iBrz04#jETK`QY^)8>@7aV8Z#Q4Am~jf|w? zG$uS>x=w498cwIviS$V7K%B}&ZAeDbZQ;~t+4Adz={&hMHCJzB$TGzF8Oj$h zbDD5Dr=l?ZW!>d+_`C?ntBb%ksIFsaU0&r_VuN(5q9hV#IPSQgx@CJ|+SA#>_@p*d(#CRAxzaqrXChac$rg(=F-#k8!u031%&=S@hkHUIy6ThboGQ_cb-2pV*mOauq4tZq8NCK?`M;Q$> zG`zOs2J-9Z3Atik9d%V!`c-bquJEF+$jEZ2sypa~t|W49-7%8kT4EEEal(|$&fAcV z%e)-gx!^P->j~*X9S^)O;eGU&sPhY)mg_jdy>6df?b^}Iy*uz~6sNU6Mt9VGNyAy> zn9jD24KQ-MW!no~+usSJGH#Sed&FG0$HCB=6PfnEdTZ(L(b?F-Is5zIY5!X9=-%Fp zuo-R~cMeC|WgAI1H*l78xAkp}+uqFD@xsNDzM5SV*hA_K+0d3L-z2G%G+`V+79Niu lrMxQ|+?Lyh5pFk2x@}>b<1Ht=eDXj&wyP-E5KHc5{{m<5p6mbs literal 0 HcmV?d00001 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 -- 2.34.1