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 /*
  84  * Remote barriers tests the scheme where a signal (or IPI) is sent to all
  85  * reader threads to promote their compiler barrier to a smp_mb().
  86  */
  87 #ifdef REMOTE_BARRIERS
  88
  89 inline smp_rmb_pid(i)
  90 {
  91         atomic {
  92                 CACHE_READ_FROM_MEM(urcu_gp_ctr, i);
  93                 CACHE_READ_FROM_MEM(urcu_active_readers_one, i);
  94                 CACHE_READ_FROM_MEM(generation_ptr, i);
  95         }
  96 }
  97
  98 inline smp_wmb_pid(i)
  99 {
 100         atomic {
 101                 CACHE_WRITE_TO_MEM(urcu_gp_ctr, i);
 102                 CACHE_WRITE_TO_MEM(urcu_active_readers_one, i);
 103                 CACHE_WRITE_TO_MEM(generation_ptr, i);
 104         }
 105 }
 106
 107 inline smp_mb_pid(i)
 108 {
 109         atomic {
 110 #ifndef NO_WMB
 111                 smp_wmb_pid(i);
 112 #endif
 113 #ifndef NO_RMB
 114                 smp_rmb_pid(i);
 115 #endif
 116                 skip;
 117         }
 118 }
 119
 120 /*
 121  * Readers do a simple barrier(), writers are doing a smp_mb() _and_ sending a
 122  * signal or IPI to have all readers execute a smp_mb.
 123  * We are not modeling the whole rendez-vous between readers and writers here,
 124  * we just let the writer update each reader's caches remotely.
 125  */
 126 inline smp_mb(i)
 127 {
 128         if
 129         :: get_pid() >= NR_READERS ->
 130                 smp_mb_pid(get_pid());
 131                 i = 0;
 132                 do
 133                 :: i < NR_READERS ->
 134                         smp_mb_pid(i);
 135                         i++;
 136                 :: i >= NR_READERS -> break
 137                 od;
 138                 smp_mb_pid(get_pid());
 139         :: else -> skip;
 140         fi;
 141 }
 142
 143 #else
 144
 145 inline smp_rmb(i)
 146 {
 147         atomic {
 148                 CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
 149                 CACHE_READ_FROM_MEM(urcu_active_readers_one, get_pid());
 150                 CACHE_READ_FROM_MEM(generation_ptr, get_pid());
 151         }
 152 }
 153
 154 inline smp_wmb(i)
 155 {
 156         atomic {
 157                 CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
 158                 CACHE_WRITE_TO_MEM(urcu_active_readers_one, get_pid());
 159                 CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
 160         }
 161 }
 162
 163 inline smp_mb(i)
 164 {
 165         atomic {
 166 #ifndef NO_WMB
 167                 smp_wmb(i);
 168 #endif
 169 #ifndef NO_RMB
 170                 smp_rmb(i);
 171 #endif
 172                 skip;
 173         }
 174 }
 175
 176 #endif
 177
 178 /* Keep in sync manually with smp_rmb, wmp_wmb and ooo_mem */
 179 DECLARE_CACHED_VAR(byte, urcu_gp_ctr, 1);
 180 /* Note ! currently only one reader */
 181 DECLARE_CACHED_VAR(byte, urcu_active_readers_one, 0);
 182 /* pointer generation */
 183 DECLARE_CACHED_VAR(byte, generation_ptr, 0);
 184
 185 byte last_free_gen = 0;
 186 bit free_done = 0;
 187 byte read_generation = 1;
 188 bit data_access = 0;
 189
 190 bit write_lock = 0;
 191
 192 inline ooo_mem(i)
 193 {
 194         atomic {
 195                 RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
 196                 RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers_one,
 197                                                 get_pid());
 198                 RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
 199                 RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
 200                 RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers_one,
 201                                                 get_pid());
 202                 RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid());
 203         }
 204 }
 205
 206 #define get_readerid()  (get_pid())
 207 #define get_writerid()  (get_readerid() + NR_READERS)
 208
 209 inline wait_for_reader(tmp, id, i)
 210 {
 211         do
 212         :: 1 ->
 213                 ooo_mem(i);
 214                 tmp = READ_CACHED_VAR(urcu_active_readers_one);
 215                 if
 216                 :: (tmp & RCU_GP_CTR_NEST_MASK)
 217                         && ((tmp ^ READ_CACHED_VAR(urcu_gp_ctr))
 218                                 & RCU_GP_CTR_BIT) ->
 219 #ifndef GEN_ERROR_WRITER_PROGRESS
 220                         smp_mb(i);
 221 #else
 222                         skip;
 223 #endif
 224                 :: else ->
 225                         break;
 226                 fi;
 227         od;
 228 }
 229
 230 inline wait_for_quiescent_state(tmp, i, j)
 231 {
 232         i = 0;
 233         do
 234         :: i < NR_READERS ->
 235                 wait_for_reader(tmp, i, j);
 236                 i++
 237         :: i >= NR_READERS -> break
 238         od;
 239 }
 240
 241 /* Model the RCU read-side critical section. */
 242
 243 active [NR_READERS] proctype urcu_reader()
 244 {
 245         byte i, nest_i;
 246         byte tmp, tmp2;
 247
 248         assert(get_pid() < NR_PROCS);
 249
 250 end_reader:
 251         do
 252         :: 1 ->
 253                 /*
 254                  * We do not test reader's progress here, because we are mainly
 255                  * interested in writer's progress. The reader never blocks
 256                  * anyway. We have to test for reader/writer's progress
 257                  * separately, otherwise we could think the writer is doing
 258                  * progress when it's blocked by an always progressing reader.
 259                  */
 260 #ifdef READER_PROGRESS
 261 progress_reader:
 262 #endif
 263                 nest_i = 0;
 264                 do
 265                 :: nest_i < READER_NEST_LEVEL ->
 266                         ooo_mem(i);
 267                         tmp = READ_CACHED_VAR(urcu_active_readers_one);
 268                         ooo_mem(i);
 269                         if
 270                         :: (!(tmp & RCU_GP_CTR_NEST_MASK))
 271                                 ->
 272                                 tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
 273                                 ooo_mem(i);
 274                                 WRITE_CACHED_VAR(urcu_active_readers_one, tmp2);
 275                         :: else ->
 276                                 WRITE_CACHED_VAR(urcu_active_readers_one,
 277                                                  tmp + 1);
 278                         fi;
 279                         ooo_mem(i);
 280                         smp_mb(i);
 281                         nest_i++;
 282                 :: nest_i >= READER_NEST_LEVEL -> break;
 283                 od;
 284
 285                 ooo_mem(i);
 286                 read_generation = READ_CACHED_VAR(generation_ptr);
 287                 ooo_mem(i);
 288                 data_access = 1;
 289                 ooo_mem(i);
 290                 data_access = 0;
 291
 292                 nest_i = 0;
 293                 do
 294                 :: nest_i < READER_NEST_LEVEL ->
 295                         ooo_mem(i);
 296                         smp_mb(i);
 297                         ooo_mem(i);
 298                         tmp2 = READ_CACHED_VAR(urcu_active_readers_one);
 299                         ooo_mem(i);
 300                         WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1);
 301                         nest_i++;
 302                 :: nest_i >= READER_NEST_LEVEL -> break;
 303                 od;
 304                 ooo_mem(i);
 305                 //smp_mc(i);    /* added */
 306         od;
 307 }
 308
 309
 310 /* Model the RCU update process. */
 311
 312 active [NR_WRITERS] proctype urcu_writer()
 313 {
 314         byte i, j;
 315         byte tmp;
 316         byte old_gen;
 317
 318         assert(get_pid() < NR_PROCS);
 319
 320         do
 321         :: (READ_CACHED_VAR(generation_ptr) < 5) ->
 322 #ifdef WRITER_PROGRESS
 323 progress_writer1:
 324 #endif
 325                 ooo_mem(i);
 326                 atomic {
 327                         old_gen = READ_CACHED_VAR(generation_ptr);
 328                         WRITE_CACHED_VAR(generation_ptr, old_gen + 1);
 329                 }
 330                 ooo_mem(i);
 331
 332                 do
 333                 :: 1 ->
 334                         atomic {
 335                                 if
 336                                 :: write_lock == 0 ->
 337                                         write_lock = 1;
 338                                         break;
 339                                 :: else ->
 340                                         skip;
 341                                 fi;
 342                         }
 343                 od;
 344                 smp_mb(i);
 345                 ooo_mem(i);
 346                 tmp = READ_CACHED_VAR(urcu_gp_ctr);
 347                 ooo_mem(i);
 348                 WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
 349                 ooo_mem(i);
 350                 //smp_mc(i);
 351                 wait_for_quiescent_state(tmp, i, j);
 352                 //smp_mc(i);
 353 #ifndef SINGLE_FLIP
 354                 ooo_mem(i);
 355                 tmp = READ_CACHED_VAR(urcu_gp_ctr);
 356                 ooo_mem(i);
 357                 WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
 358                 //smp_mc(i);
 359                 ooo_mem(i);
 360                 wait_for_quiescent_state(tmp, i, j);
 361 #endif
 362                 ooo_mem(i);
 363                 smp_mb(i);
 364                 ooo_mem(i);
 365                 write_lock = 0;
 366                 /* free-up step, e.g., kfree(). */
 367                 atomic {
 368                         last_free_gen = old_gen;
 369                         free_done = 1;
 370                 }
 371         :: else -> break;
 372         od;
 373         /*
 374          * Given the reader loops infinitely, let the writer also busy-loop
 375          * with progress here so, with weak fairness, we can test the
 376          * writer's progress.
 377          */
 378 end_writer:
 379         do
 380         :: 1 ->
 381 #ifdef WRITER_PROGRESS
 382 progress_writer2:
 383 #endif
 384                 skip;
 385         od;
 386 }