From: Mathieu Desnoyers Date: Sat, 27 Aug 2011 15:09:19 +0000 (-0400) Subject: Update nto1-selective model comments X-Git-Url: http://git.liburcu.org/?p=userspace-rcu.git;a=commitdiff_plain;h=575c1e87f3e48e96a2ceab427057a37041e9d611 Update nto1-selective model comments Signed-off-by: Mathieu Desnoyers --- diff --git a/futex-wakeup/nto1-selective/futex.spin b/futex-wakeup/nto1-selective/futex.spin index c68a77b..556f96f 100644 --- a/futex-wakeup/nto1-selective/futex.spin +++ b/futex-wakeup/nto1-selective/futex.spin @@ -1,5 +1,9 @@ /* - * futex.spin: Promela code to validate futex wakeup algorithm. + * 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 : * @@ -56,7 +60,7 @@ * 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 + * Copyright (c) 2009-2011 Mathieu Desnoyers */ #define get_pid() (_pid)