Update nto1-selective model comments

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

diff --git a/futex-wakeup/nto1-selective/futex.spin b/futex-wakeup/nto1-selective/futex.spin
index c68a77b75fbf30217bc07dd26004491a90b460a8..556f96fad7b175aa5bc78879aa25e99917ab3680 100644 (file)
--- 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)