futex-wakeup/futex.spin

   1 /*
   2  * futex.spin: Promela code to validate futex wakeup algorithm.
   3  *
   4  * Algorithm verified :
   5  *
   6  * queue = 0;
   7  * waiting = 0;
   8  * gp_futex = 0;
   9  * gp = 1;
  10  *
  11  *                          Waker
  12  *                          while (1) {
  13  *                            this.queue = gp;
  14  *                            if (gp_futex == -1) {
  15  *                              gp_futex = 0;
  16  *                              futex_wake = 1;
  17  *                            }
  18  *                          }
  19  *
  20  * Waiter
  21  * in_registry = 1;
  22  * while (1) {
  23  *   gp_futex = -1;
  24  *   in_registry &= (queue != gp);
  25  *   if (all in_registry == 0) {
  26  * progress:
  27  *     gp_futex = 0;
  28  *     gp = !gp;
  29  *     restart;
  30  *   } else {
  31  *     futex_wake = (gp_futex == -1 ? 0 : 1);
  32  *     while (futex_wake == 0) { }
  33  *   }
  34  *   queue = 0;
  35  * }
  36  *
  37  * By testing progress, i.e. [] <> !np_, we check that an infinite sequence
  38  * of update_counter_and_wait (and consequently of synchronize_rcu) will
  39  * not block.
  40  *
  41  * This program is free software; you can redistribute it and/or modify
  42  * it under the terms of the GNU General Public License as published by
  43  * the Free Software Foundation; either version 2 of the License, or
  44  * (at your option) any later version.
  45  *
  46  * This program is distributed in the hope that it will be useful,
  47  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  48  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  49  * GNU General Public License for more details.
  50  *
  51  * You should have received a copy of the GNU General Public License
  52  * along with this program; if not, write to the Free Software
  53  * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
  54  *
  55  * Copyright (c) 2009 Mathieu Desnoyers
  56  */
  57
  58 #define get_pid()       (_pid)
  59
  60 int queue[2] = 0;
  61 int futex_wake = 0;
  62 int gp_futex = 0;
  63 int gp = 1;
  64 int in_registry[2] = 0;
  65
  66 active [2] proctype waker()
  67 {
  68         assert(get_pid() < 2);
  69
  70         do
  71         :: 1 ->
  72                 queue[get_pid()] = gp;
  73
  74                 if
  75                 :: (gp_futex == -1) ->
  76                         gp_futex = 0;
  77 #ifndef INJ_QUEUE_NO_WAKE
  78                         futex_wake = 1;
  79 #endif
  80                 :: else ->
  81                         skip;
  82                 fi;
  83         od;
  84 }
  85
  86
  87 active proctype waiter()
  88 {
  89 restart:
  90         in_registry[0] = 1;
  91         in_registry[1] = 1;
  92         do
  93         :: 1 ->
  94 #ifndef INJ_LATE_DEC
  95                 gp_futex = -1;
  96 #endif
  97
  98                 if
  99                 :: (in_registry[0] == 1 && queue[0] == gp) ->
 100                         in_registry[0] = 0;
 101                 :: else ->
 102                         skip;
 103                 fi;
 104                 if
 105                 :: (in_registry[1] == 1 && queue[1] == gp) ->
 106                         in_registry[1] = 0;
 107                 :: else ->
 108                         skip;
 109                 fi;
 110                 if
 111                 :: (in_registry[0] == 0 && in_registry[1] == 0) ->
 112 progress:
 113 #ifndef INJ_LATE_DEC
 114                         gp_futex = 0;
 115 #endif
 116                         gp = !gp;
 117                         goto restart;
 118                 :: else ->
 119 #ifdef INJ_LATE_DEC
 120                         gp_futex = -1;
 121 #endif
 122                         futex_wake = gp_futex + 1;
 123                         do
 124                         :: 1 ->
 125                                 if
 126                                 :: (futex_wake == 0) ->
 127                                         skip;
 128                                 :: else ->
 129                                         break;
 130                                 fi;
 131                         od;
 132                 fi;
 133         od;
 134 }