From: Mathieu Desnoyers Date: Sat, 27 Aug 2011 14:16:52 +0000 (-0400) Subject: Move futex wakeup model to nto1-selective X-Git-Url: https://git.lttng.org/?p=urcu.git;a=commitdiff_plain;h=c14f083d1667973769d0cdcf2041476b90a29fdd Move futex wakeup model to nto1-selective Signed-off-by: Mathieu Desnoyers --- diff --git a/futex-wakeup/DEFINES b/futex-wakeup/DEFINES deleted file mode 100644 index 3e0a545..0000000 --- a/futex-wakeup/DEFINES +++ /dev/null @@ -1 +0,0 @@ -/* no defines needed yet */ diff --git a/futex-wakeup/Makefile b/futex-wakeup/Makefile deleted file mode 100644 index 2b6e243..0000000 --- a/futex-wakeup/Makefile +++ /dev/null @@ -1,116 +0,0 @@ -# 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 futex_progress_inverted_waiting_vs_gp_futex | tee futex_progress_inverted_waiting_vs_gp_futex.define.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_progress_inverted_waiting_vs_gp_futex: clean futex_ltl futex_progress_inverted_waiting_vs_gp_futex_define run_weak_fair - cp .input.spin $@.spin.input - -cp .input.spin.trail $@.spin.input.trail - -futex_progress_inverted_waiting_vs_gp_futex_define: - cp futex_progress_inverted_waiting_vs_gp_futex.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/futex.ltl b/futex-wakeup/futex.ltl deleted file mode 100644 index 8718641..0000000 --- a/futex-wakeup/futex.ltl +++ /dev/null @@ -1 +0,0 @@ -([] <> !np_) diff --git a/futex-wakeup/futex.spin b/futex-wakeup/futex.spin deleted file mode 100644 index c68a77b..0000000 --- a/futex-wakeup/futex.spin +++ /dev/null @@ -1,159 +0,0 @@ -/* - * futex.spin: Promela code to validate futex wakeup algorithm. - * - * Algorithm verified : - * - * queue = 0; - * waiting = 0; - * gp_futex = 0; - * gp = 1; - * - * Waker - * while (1) { - * this.queue = gp; - * if (this.waiting == 1) { - * this.waiting = 0; - * if (gp_futex == -1) { - * gp_futex = 0; - * futex_wake = 1; - * } - * } - * } - * - * Waiter - * in_registry = 1; - * while (1) { - * gp_futex = -1; - * waiting |= (queue != gp); - * in_registry &= (queue != gp); - * if (all in_registry == 0) { - * progress: - * gp_futex = 0; - * gp = !gp; - * restart; - * } else { - * futex_wake = (gp_futex == -1 ? 0 : 1); - * while (futex_wake == 0) { } - * } - * queue = 0; - * } - * - * By testing progress, i.e. [] <> !np_, we check that an infinite sequence - * of update_counter_and_wait (and consequently of synchronize_rcu) will - * not block. - * - * 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 waiting[2] = 0; -int futex_wake = 0; -int gp_futex = 0; -int gp = 1; -int in_registry[2] = 0; - -active [2] proctype waker() -{ - assert(get_pid() < 2); - - do - :: 1 -> - queue[get_pid()] = gp; - - if - :: (waiting[get_pid()] == 1) -> - waiting[get_pid()] = 0; - if - :: (gp_futex == -1) -> - gp_futex = 0; -#ifndef INJ_QUEUE_NO_WAKE - futex_wake = 1; -#endif - :: else -> - skip; - fi; - fi; - od; -} - - -active proctype waiter() -{ -restart: - in_registry[0] = 1; - in_registry[1] = 1; - do - :: 1 -> -#if (!defined(INJ_LATE_DEC) && !defined(INJ_INVERT_WAITING_VS_GP_FUTEX)) - gp_futex = -1; -#endif - if - :: (in_registry[0] == 1 && queue[0] != gp) -> - waiting[0] = 1; - :: else -> - skip; - fi; - if - :: (in_registry[1] == 1 && queue[1] != gp) -> - waiting[1] = 1; - :: else -> - skip; - fi; - - if - :: (in_registry[0] == 1 && queue[0] == gp) -> - in_registry[0] = 0; - :: else -> - skip; - fi; - if - :: (in_registry[1] == 1 && queue[1] == gp) -> - in_registry[1] = 0; - :: else -> - skip; - fi; -#ifdef INJ_INVERT_WAITING_VS_GP_FUTEX - gp_futex = -1; -#endif - - if - :: (in_registry[0] == 0 && in_registry[1] == 0) -> -progress: -#ifndef INJ_LATE_DEC - gp_futex = 0; -#endif - gp = !gp; - goto restart; - :: else -> -#ifdef INJ_LATE_DEC - gp_futex = -1; -#endif - futex_wake = gp_futex + 1; - do - :: 1 -> - if - :: (futex_wake == 0) -> - skip; - :: else -> - break; - fi; - od; - fi; - od; -} diff --git a/futex-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define b/futex-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define deleted file mode 100644 index eca05f6..0000000 --- a/futex-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define +++ /dev/null @@ -1 +0,0 @@ -#define INJ_INVERT_WAITING_VS_GP_FUTEX diff --git a/futex-wakeup/futex_progress_late_dec.define b/futex-wakeup/futex_progress_late_dec.define deleted file mode 100644 index 01361fb..0000000 --- a/futex-wakeup/futex_progress_late_dec.define +++ /dev/null @@ -1 +0,0 @@ -#define INJ_LATE_DEC diff --git a/futex-wakeup/futex_progress_no_wake.define b/futex-wakeup/futex_progress_no_wake.define deleted file mode 100644 index 527bb77..0000000 --- a/futex-wakeup/futex_progress_no_wake.define +++ /dev/null @@ -1 +0,0 @@ -#define INJ_QUEUE_NO_WAKE diff --git a/futex-wakeup/nto1-selective/DEFINES b/futex-wakeup/nto1-selective/DEFINES new file mode 100644 index 0000000..3e0a545 --- /dev/null +++ b/futex-wakeup/nto1-selective/DEFINES @@ -0,0 +1 @@ +/* no defines needed yet */ diff --git a/futex-wakeup/nto1-selective/Makefile b/futex-wakeup/nto1-selective/Makefile new file mode 100644 index 0000000..2b6e243 --- /dev/null +++ b/futex-wakeup/nto1-selective/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_no_wake | tee futex_progress_no_wake.log + make futex_progress_late_dec | tee futex_progress_late_dec.log + make futex_progress_inverted_waiting_vs_gp_futex | tee futex_progress_inverted_waiting_vs_gp_futex.define.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_progress_inverted_waiting_vs_gp_futex: clean futex_ltl futex_progress_inverted_waiting_vs_gp_futex_define run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +futex_progress_inverted_waiting_vs_gp_futex_define: + cp futex_progress_inverted_waiting_vs_gp_futex.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-selective/futex.ltl b/futex-wakeup/nto1-selective/futex.ltl new file mode 100644 index 0000000..8718641 --- /dev/null +++ b/futex-wakeup/nto1-selective/futex.ltl @@ -0,0 +1 @@ +([] <> !np_) diff --git a/futex-wakeup/nto1-selective/futex.spin b/futex-wakeup/nto1-selective/futex.spin new file mode 100644 index 0000000..c68a77b --- /dev/null +++ b/futex-wakeup/nto1-selective/futex.spin @@ -0,0 +1,159 @@ +/* + * futex.spin: Promela code to validate futex wakeup algorithm. + * + * Algorithm verified : + * + * queue = 0; + * waiting = 0; + * gp_futex = 0; + * gp = 1; + * + * Waker + * while (1) { + * this.queue = gp; + * if (this.waiting == 1) { + * this.waiting = 0; + * if (gp_futex == -1) { + * gp_futex = 0; + * futex_wake = 1; + * } + * } + * } + * + * Waiter + * in_registry = 1; + * while (1) { + * gp_futex = -1; + * waiting |= (queue != gp); + * in_registry &= (queue != gp); + * if (all in_registry == 0) { + * progress: + * gp_futex = 0; + * gp = !gp; + * restart; + * } else { + * futex_wake = (gp_futex == -1 ? 0 : 1); + * while (futex_wake == 0) { } + * } + * queue = 0; + * } + * + * By testing progress, i.e. [] <> !np_, we check that an infinite sequence + * of update_counter_and_wait (and consequently of synchronize_rcu) will + * not block. + * + * 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 waiting[2] = 0; +int futex_wake = 0; +int gp_futex = 0; +int gp = 1; +int in_registry[2] = 0; + +active [2] proctype waker() +{ + assert(get_pid() < 2); + + do + :: 1 -> + queue[get_pid()] = gp; + + if + :: (waiting[get_pid()] == 1) -> + waiting[get_pid()] = 0; + if + :: (gp_futex == -1) -> + gp_futex = 0; +#ifndef INJ_QUEUE_NO_WAKE + futex_wake = 1; +#endif + :: else -> + skip; + fi; + fi; + od; +} + + +active proctype waiter() +{ +restart: + in_registry[0] = 1; + in_registry[1] = 1; + do + :: 1 -> +#if (!defined(INJ_LATE_DEC) && !defined(INJ_INVERT_WAITING_VS_GP_FUTEX)) + gp_futex = -1; +#endif + if + :: (in_registry[0] == 1 && queue[0] != gp) -> + waiting[0] = 1; + :: else -> + skip; + fi; + if + :: (in_registry[1] == 1 && queue[1] != gp) -> + waiting[1] = 1; + :: else -> + skip; + fi; + + if + :: (in_registry[0] == 1 && queue[0] == gp) -> + in_registry[0] = 0; + :: else -> + skip; + fi; + if + :: (in_registry[1] == 1 && queue[1] == gp) -> + in_registry[1] = 0; + :: else -> + skip; + fi; +#ifdef INJ_INVERT_WAITING_VS_GP_FUTEX + gp_futex = -1; +#endif + + if + :: (in_registry[0] == 0 && in_registry[1] == 0) -> +progress: +#ifndef INJ_LATE_DEC + gp_futex = 0; +#endif + gp = !gp; + goto restart; + :: else -> +#ifdef INJ_LATE_DEC + gp_futex = -1; +#endif + futex_wake = gp_futex + 1; + do + :: 1 -> + if + :: (futex_wake == 0) -> + skip; + :: else -> + break; + fi; + od; + fi; + od; +} diff --git a/futex-wakeup/nto1-selective/futex_progress_inverted_waiting_vs_gp_futex.define b/futex-wakeup/nto1-selective/futex_progress_inverted_waiting_vs_gp_futex.define new file mode 100644 index 0000000..eca05f6 --- /dev/null +++ b/futex-wakeup/nto1-selective/futex_progress_inverted_waiting_vs_gp_futex.define @@ -0,0 +1 @@ +#define INJ_INVERT_WAITING_VS_GP_FUTEX diff --git a/futex-wakeup/nto1-selective/futex_progress_late_dec.define b/futex-wakeup/nto1-selective/futex_progress_late_dec.define new file mode 100644 index 0000000..01361fb --- /dev/null +++ b/futex-wakeup/nto1-selective/futex_progress_late_dec.define @@ -0,0 +1 @@ +#define INJ_LATE_DEC diff --git a/futex-wakeup/nto1-selective/futex_progress_no_wake.define b/futex-wakeup/nto1-selective/futex_progress_no_wake.define new file mode 100644 index 0000000..527bb77 --- /dev/null +++ b/futex-wakeup/nto1-selective/futex_progress_no_wake.define @@ -0,0 +1 @@ +#define INJ_QUEUE_NO_WAKE