formal-model/urcu/urcu.spin

   1 /*
   2  * mem.spin: Promela code to validate memory barriers with OOO memory.
   3  *
   4  * This program is free software; you can redistribute it and/or modify
   5  * it under the terms of the GNU General Public License as published by
   6  * the Free Software Foundation; either version 2 of the License, or
   7  * (at your option) any later version.
   8  *
   9  * This program is distributed in the hope that it will be useful,
  10  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  11  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  12  * GNU General Public License for more details.
  13  *
  14  * You should have received a copy of the GNU General Public License
  15  * along with this program; if not, write to the Free Software
  16  * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
  17  *
  18  * Copyright (c) 2009 Mathieu Desnoyers
  19  */
  20
  21 /* Promela validation variables. */
  22
  23 #define NR_READERS 1
  24 #define NR_WRITERS 1
  25
  26 #define NR_PROCS 2
  27
  28 #define get_pid()       (_pid)
  29
  30 /*
  31  * Each process have its own data in cache. Caches are randomly updated.
  32  * smp_wmb and smp_rmb forces cache updates (write and read), wmb_mb forces
  33  * both.
  34  */
  35
  36 #define DECLARE_CACHED_VAR(type, x, v)  \
  37         type mem_##x = v;               \
  38         type cached_##x[NR_PROCS] = v;  \
  39         bit cache_dirty_##x[NR_PROCS] = 0
  40
  41 #define IS_CACHE_DIRTY(x, id)   (cache_dirty_##x[id])
  42
  43 #define READ_CACHED_VAR(x)      (cached_##x[get_pid()])
  44
  45 #define WRITE_CACHED_VAR(x, v)          \
  46         atomic {                        \
  47                 cached_##x[get_pid()] = v;      \
  48                 cache_dirty_##x[get_pid()] = 1; \
  49         }
  50
  51 #define CACHE_WRITE_TO_MEM(x, id)               \
  52         if                                      \
  53         :: IS_CACHE_DIRTY(x, id) ->             \
  54                 mem_##x = cached_##x[id];       \
  55                 cache_dirty_##x[id] = 0;        \
  56         :: else ->                              \
  57                 skip                            \
  58         fi;
  59
  60 #define CACHE_READ_FROM_MEM(x, id)      \
  61         if                              \
  62         :: !IS_CACHE_DIRTY(x, id) ->    \
  63                 cached_##x[id] = mem_##x;\
  64         :: else ->                      \
  65                 skip                    \
  66         fi;
  67
  68 /*
  69  * May update other caches if cache is dirty, or not.
  70  */
  71 #define RANDOM_CACHE_WRITE_TO_MEM(x, id)\
  72         if                              \
  73         :: 1 -> CACHE_WRITE_TO_MEM(x, id);      \
  74         :: 1 -> skip                    \
  75         fi;
  76
  77 #define RANDOM_CACHE_READ_FROM_MEM(x, id)\
  78         if                              \
  79         :: 1 -> CACHE_READ_FROM_MEM(x, id);     \
  80         :: 1 -> skip                    \
  81         fi;
  82
  83 inline smp_rmb(i)
  84 {
  85         atomic {
  86                 CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
  87                 CACHE_READ_FROM_MEM(urcu_active_readers_one, get_pid());
  88                 CACHE_READ_FROM_MEM(generation_ptr, get_pid());
  89         }
  90 }
  91
  92 inline smp_wmb(i)
  93 {
  94         atomic {
  95                 CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
  96                 CACHE_WRITE_TO_MEM(urcu_active_readers_one, get_pid());
  97                 CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
  98         }
  99 }
 100
 101 inline smp_mb(i)
 102 {
 103         atomic {
 104 #ifndef NO_WMB
 105                 smp_wmb(i);
 106 #endif
 107 #ifndef NO_RMB
 108                 smp_rmb(i);
 109 #endif
 110                 skip;
 111         }
 112 }
 113
 114 /* Keep in sync manually with smp_rmb, wmp_wmb and ooo_mem */
 115 DECLARE_CACHED_VAR(byte, urcu_gp_ctr, 1);
 116 /* Note ! currently only one reader */
 117 DECLARE_CACHED_VAR(byte, urcu_active_readers_one, 0);
 118 /* pointer generation */
 119 DECLARE_CACHED_VAR(byte, generation_ptr, 0);
 120
 121 byte last_free_gen = 0;
 122 bit free_done = 0;
 123 byte read_generation = 1;
 124 bit data_access = 0;
 125
 126 bit write_lock = 0;
 127
 128 inline ooo_mem(i)
 129 {
 130         atomic {
 131                 RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
 132                 RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers_one,
 133                                                 get_pid());
 134                 RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
 135                 RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
 136                 RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers_one,
 137                                                 get_pid());
 138                 RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid());
 139         }
 140 }
 141
 142 #define get_readerid()  (get_pid())
 143 #define get_writerid()  (get_readerid() + NR_READERS)
 144
 145 inline wait_for_reader(tmp, id, i)
 146 {
 147         do
 148         :: 1 ->
 149                 ooo_mem(i);
 150                 tmp = READ_CACHED_VAR(urcu_active_readers_one);
 151                 if
 152                 :: (tmp & RCU_GP_CTR_NEST_MASK)
 153                         && ((tmp ^ READ_CACHED_VAR(urcu_gp_ctr))
 154                                 & RCU_GP_CTR_BIT) ->
 155 #ifndef GEN_ERROR_WRITER_PROGRESS
 156                         smp_mb(i);
 157 #else
 158                         skip;
 159 #endif
 160                 :: else ->
 161                         break;
 162                 fi;
 163         od;
 164 }
 165
 166 inline wait_for_quiescent_state(tmp, i, j)
 167 {
 168         i = 0;
 169         do
 170         :: i < NR_READERS ->
 171                 wait_for_reader(tmp, i, j);
 172                 i++
 173         :: i >= NR_READERS -> break
 174         od;
 175 }
 176
 177 /* Model the RCU read-side critical section. */
 178
 179 active [NR_READERS] proctype urcu_reader()
 180 {
 181         byte i, nest_i;
 182         byte tmp, tmp2;
 183
 184         assert(get_pid() < NR_PROCS);
 185
 186 end_reader:
 187         do
 188         :: 1 ->
 189                 /*
 190                  * We do not test reader's progress here, because we are mainly
 191                  * interested in writer's progress. The reader never blocks
 192                  * anyway. We have to test for reader/writer's progress
 193                  * separately, otherwise we could think the writer is doing
 194                  * progress when it's blocked by an always progressing reader.
 195                  */
 196 #ifdef READER_PROGRESS
 197 progress_reader:
 198 #endif
 199                 nest_i = 0;
 200                 do
 201                 :: nest_i < READER_NEST_LEVEL ->
 202                         ooo_mem(i);
 203                         tmp = READ_CACHED_VAR(urcu_active_readers_one);
 204                         ooo_mem(i);
 205                         if
 206                         :: (!(tmp & RCU_GP_CTR_NEST_MASK))
 207                                 ->
 208                                 tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
 209                                 ooo_mem(i);
 210                                 WRITE_CACHED_VAR(urcu_active_readers_one, tmp2);
 211                         :: else ->
 212                                 WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1);
 213                         fi;
 214                         ooo_mem(i);
 215                         smp_mb(i);
 216                         nest_i++;
 217                 :: nest_i >= READER_NEST_LEVEL -> break;
 218                 od;
 219
 220                 ooo_mem(i);
 221                 read_generation = READ_CACHED_VAR(generation_ptr);
 222                 ooo_mem(i);
 223                 data_access = 1;
 224                 ooo_mem(i);
 225                 data_access = 0;
 226
 227                 nest_i = 0;
 228                 do
 229                 :: nest_i < READER_NEST_LEVEL ->
 230                         ooo_mem(i);
 231                         smp_mb(i);
 232                         ooo_mem(i);
 233                         tmp2 = READ_CACHED_VAR(urcu_active_readers_one);
 234                         ooo_mem(i);
 235                         WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1);
 236                         nest_i++;
 237                 :: nest_i >= READER_NEST_LEVEL -> break;
 238                 od;
 239                 ooo_mem(i);
 240                 //smp_mc(i);    /* added */
 241         od;
 242 }
 243
 244
 245 /* Model the RCU update process. */
 246
 247 active [NR_WRITERS] proctype urcu_writer()
 248 {
 249         byte i, j;
 250         byte tmp;
 251         byte old_gen;
 252
 253         assert(get_pid() < NR_PROCS);
 254
 255         do
 256         :: (READ_CACHED_VAR(generation_ptr) < 5) ->
 257 #ifdef WRITER_PROGRESS
 258 progress_writer1:
 259 #endif
 260                 ooo_mem(i);
 261                 atomic {
 262                         old_gen = READ_CACHED_VAR(generation_ptr);
 263                         WRITE_CACHED_VAR(generation_ptr, old_gen + 1);
 264                 }
 265                 ooo_mem(i);
 266
 267                 do
 268                 :: 1 ->
 269                         atomic {
 270                                 if
 271                                 :: write_lock == 0 ->
 272                                         write_lock = 1;
 273                                         break;
 274                                 :: else ->
 275                                         skip;
 276                                 fi;
 277                         }
 278                 od;
 279                 smp_mb(i);
 280                 ooo_mem(i);
 281                 tmp = READ_CACHED_VAR(urcu_gp_ctr);
 282                 ooo_mem(i);
 283                 WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
 284                 ooo_mem(i);
 285                 //smp_mc(i);
 286                 wait_for_quiescent_state(tmp, i, j);
 287                 //smp_mc(i);
 288         #ifndef SINGLE_FLIP
 289                 ooo_mem(i);
 290                 tmp = READ_CACHED_VAR(urcu_gp_ctr);
 291                 ooo_mem(i);
 292                 WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
 293                 //smp_mc(i);
 294                 ooo_mem(i);
 295                 wait_for_quiescent_state(tmp, i, j);
 296         #endif
 297                 ooo_mem(i);
 298                 smp_mb(i);
 299                 ooo_mem(i);
 300                 write_lock = 0;
 301                 /* free-up step, e.g., kfree(). */
 302                 atomic {
 303                         last_free_gen = old_gen;
 304                         free_done = 1;
 305                 }
 306         :: else -> break;
 307         od;
 308         /*
 309          * Given the reader loops infinitely, let the writer also busy-loop
 310          * with progress here so, with weak fairness, we can test the
 311          * writer's progress.
 312          */
 313 end_writer:
 314         do
 315         :: 1 ->
 316 #ifdef WRITER_PROGRESS
 317 progress_writer2:
 318 #endif
 319                 skip;
 320         od;
 321 }