futex-wakeup/nto1-selective/futex.spin

   1 /*
   2  * futex.spin: Promela code to validate n wakers to 1 waiter selective
   3  * futex wakeup algorithm.
   4  *
   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.
   8
   9  * Algorithm verified :
  10  *
  11  * queue[n] = 0;
  12  * futex = 0;
  13  * futex_wake = 0;
  14  *
  15  *                          n wakers (2 loops)
  16  *
  17  *                          queue[pid] = 1;
  18  *                          if (futex == -1) {
  19  *                            if (waker[pid].waiting == 1) {
  20  *                              waker[pid].waiting = 0;
  21  *                              futex = 0;
  22  *                              futex_wake = 1;
  23  *                            }
  24  *                          }
  25  *
  26  * 1 waiter
  27  *
  28  * while (1) {
  29  *   futex = -1;
  30  *   waker[0].waiting = 1;
  31  *   waker[1].waiting = 1;
  32  *   while (!(queue[0] == 1 && queue[1] == 1)) {
  33  *       if (futex == -1) {
  34  *         futex_wake = (futex == -1 ? 0 : 1);  (atomic)
  35  *         while (futex_wake == 0) { };
  36  *       }
  37  *     }
  38  *   }
  39  *   futex = 0;
  40  *   waker[0].waiting = 0;
  41  *   waker[1].waiting = 0;
  42  * progress:
  43  *   queue[0] = 0;
  44  *   queue[1] = 0;
  45  * }
  46  *
  47  * if queue = 1, then !_np
  48  *
  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
  51  * any of the queues.
  52  *
  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
  55  * enqueuing.
  56  *
  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.
  61  *
  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.
  66  *
  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.
  70  *
  71  * Copyright (c) 2009-2011 Mathieu Desnoyers
  72  */
  73
  74 #define get_pid()       (_pid)
  75
  76 int queue[2] = 0;
  77 int waiting[2] = 0;
  78 int futex = 0;
  79 int futex_wake = 0;
  80
  81 active [2] proctype waker()
  82 {
  83         assert(get_pid() < 2);
  84
  85         /* loop 1 */
  86         queue[get_pid()] = 1;
  87
  88         if
  89         :: (futex == -1) ->
  90                 if
  91                 :: (waiting[get_pid() == 1]) ->
  92                         waiting[get_pid()] = 0;
  93                         futex = 0;
  94                         futex_wake = 1;
  95                 :: else -> skip;
  96                 fi;
  97         :: else ->
  98                 skip;
  99         fi;
 100
 101         /* loop 2 */
 102         queue[get_pid()] = 1;
 103
 104         if
 105         :: (futex == -1) ->
 106                 if
 107                 :: (waiting[get_pid() == 1]) ->
 108                         waiting[get_pid()] = 0;
 109                         futex = 0;
 110                         futex_wake = 1;
 111                 :: else -> skip;
 112                 fi;
 113         :: else ->
 114                 skip;
 115         fi;
 116
 117 #ifdef INJ_QUEUE_NO_WAKE
 118         /* loop 3 */
 119         queue[get_pid()] = 1;
 120 #endif
 121 }
 122
 123
 124 active proctype waiter()
 125 {
 126         do
 127         :: 1 ->
 128 #ifndef INJ_LATE_DEC
 129                 futex = -1;
 130                 waiting[0] = 1;
 131                 waiting[1] = 1;
 132 #endif
 133
 134                 do
 135                 :: 1 ->
 136                         if
 137                         :: (queue[0] == 1 || queue[1] == 1) ->
 138                                 break;
 139                         :: else ->
 140                                 skip;
 141                         fi;
 142 #ifdef INJ_LATE_DEC
 143                         futex = -1;
 144                         waiting[0] = 1;
 145                         waiting[1] = 1;
 146 #endif
 147                         if
 148                         :: (futex == -1) ->
 149                                 atomic {
 150                                         if
 151                                         :: (futex == -1) ->
 152                                                 futex_wake = 0;
 153                                         :: else ->
 154                                                 futex_wake = 1;
 155                                         fi;
 156                                 }
 157                                 /* block */
 158                                 do
 159                                 :: 1 ->
 160                                         if
 161                                         :: (futex_wake == 0) ->
 162                                                 skip;
 163                                         :: else ->
 164                                                 break;
 165                                         fi;
 166                                 od;
 167                         :: else ->
 168                                 skip;
 169                         fi;
 170                 od;
 171
 172                 futex = 0;
 173                 waiting[0] = 0;
 174                 waiting[1] = 0;
 175 progress:       /* progress on dequeue */
 176                 queue[0] = 0;
 177                 queue[1] = 0;
 178         od;
 179
 180 }