From: Mathieu Desnoyers Date: Mon, 29 Aug 2011 14:28:03 +0000 (-0400) Subject: Add back urcu QSBR selective wakeup model X-Git-Url: http://git.liburcu.org/?p=userspace-rcu.git;a=commitdiff_plain;h=2e33016fc8b527cb35e466c1e093f0d0bd7ed296 Add back urcu QSBR selective wakeup model Signed-off-by: Mathieu Desnoyers --- diff --git a/urcu-qsbr-selective-wakeup/DEFINES b/urcu-qsbr-selective-wakeup/DEFINES new file mode 100644 index 0000000..3e0a545 --- /dev/null +++ b/urcu-qsbr-selective-wakeup/DEFINES @@ -0,0 +1 @@ +/* no defines needed yet */ diff --git a/urcu-qsbr-selective-wakeup/Makefile b/urcu-qsbr-selective-wakeup/Makefile new file mode 100644 index 0000000..2b6e243 --- /dev/null +++ b/urcu-qsbr-selective-wakeup/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/urcu-qsbr-selective-wakeup/futex.ltl b/urcu-qsbr-selective-wakeup/futex.ltl new file mode 100644 index 0000000..8718641 --- /dev/null +++ b/urcu-qsbr-selective-wakeup/futex.ltl @@ -0,0 +1 @@ +([] <> !np_) diff --git a/urcu-qsbr-selective-wakeup/futex.spin b/urcu-qsbr-selective-wakeup/futex.spin new file mode 100644 index 0000000..556f96f --- /dev/null +++ b/urcu-qsbr-selective-wakeup/futex.spin @@ -0,0 +1,163 @@ +/* + * futex.spin: Promela code to validate n wakers to 1 waiter selective + * futex wakeup algorithm. + * + * In this model, waker threads are told whether they are still being + * waited on, and skip the futex wakeup if not. + * + * 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-2011 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/urcu-qsbr-selective-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define b/urcu-qsbr-selective-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define new file mode 100644 index 0000000..eca05f6 --- /dev/null +++ b/urcu-qsbr-selective-wakeup/futex_progress_inverted_waiting_vs_gp_futex.define @@ -0,0 +1 @@ +#define INJ_INVERT_WAITING_VS_GP_FUTEX diff --git a/urcu-qsbr-selective-wakeup/futex_progress_late_dec.define b/urcu-qsbr-selective-wakeup/futex_progress_late_dec.define new file mode 100644 index 0000000..01361fb --- /dev/null +++ b/urcu-qsbr-selective-wakeup/futex_progress_late_dec.define @@ -0,0 +1 @@ +#define INJ_LATE_DEC diff --git a/urcu-qsbr-selective-wakeup/futex_progress_no_wake.define b/urcu-qsbr-selective-wakeup/futex_progress_no_wake.define new file mode 100644 index 0000000..527bb77 --- /dev/null +++ b/urcu-qsbr-selective-wakeup/futex_progress_no_wake.define @@ -0,0 +1 @@ +#define INJ_QUEUE_NO_WAKE