projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Update nto1-selective model comments
[urcu.git]
/
futex-wakeup
/
nto1-selective
/
futex.spin
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 :
*
*
* 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.
*
* 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)
*/
#define get_pid() (_pid)
This page took
0.024724 seconds
and
4
git commands to generate.