From 575c1e87f3e48e96a2ceab427057a37041e9d611 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Sat, 27 Aug 2011 11:09:19 -0400 Subject: [PATCH] Update nto1-selective model comments Signed-off-by: Mathieu Desnoyers --- futex-wakeup/nto1-selective/futex.spin | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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) -- 2.34.1