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