2 * futex.spin: Promela code to validate n wakers to 1 waiter selective
3 * futex wakeup algorithm.
5 * In this model, waker threads are told whether they are still being
6 * waited on, and skip the futex wakeup if not. The waiter progresses
7 * each time it sees data in both queues.
19 * if (waker[pid].waiting == 1) {
20 * waker[pid].waiting = 0;
30 * waker[0].waiting = 1;
31 * waker[1].waiting = 1;
32 * while (!(queue[0] == 1 && queue[1] == 1)) {
34 * futex_wake = (futex == -1 ? 0 : 1); (atomic)
35 * while (futex_wake == 0) { };
40 * waker[0].waiting = 0;
41 * waker[1].waiting = 0;
47 * if queue = 1, then !_np
49 * By testing progress, i.e. [] <> ((!np_) || (!queue_has_entry)), we
50 * check that we can never block forever if there is an entry in the
53 * The waker performs only 2 loops (and NOT an infinite number of loops)
54 * because we really want to see what happens when the waker stops
57 * This program is free software; you can redistribute it and/or modify
58 * it under the terms of the GNU General Public License as published by
59 * the Free Software Foundation; either version 2 of the License, or
60 * (at your option) any later version.
62 * This program is distributed in the hope that it will be useful,
63 * but WITHOUT ANY WARRANTY; without even the implied warranty of
64 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
65 * GNU General Public License for more details.
67 * You should have received a copy of the GNU General Public License
68 * along with this program; if not, write to the Free Software
69 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
71 * Copyright (c) 2009-2011 Mathieu Desnoyers
74 #define get_pid() (_pid)
81 active [2] proctype waker()
83 assert(get_pid() < 2);
91 :: (waiting[get_pid() == 1]) ->
92 waiting[get_pid()] = 0;
102 queue[get_pid()] = 1;
107 :: (waiting[get_pid() == 1]) ->
108 waiting[get_pid()] = 0;
117 #ifdef INJ_QUEUE_NO_WAKE
119 queue[get_pid()] = 1;
124 active proctype waiter()
142 :: (queue[0] == 1 || queue[1] == 1) ->
166 :: (futex_wake == 0) ->
180 progress: /* progress on dequeue */