formal-model/urcu-nosched-model/result-standard-execution-nest/urcu_progress_writer_error.spin.input

   1 #define WRITER_PROGRESS
   2 #define GEN_ERROR_WRITER_PROGRESS
   3
   4 #define read_free_race  (read_generation[0] == last_free_gen)
   5 #define read_free       (free_done && data_access[0])
   6
   7 //#define TEST_SIGNAL
   8 //#define TEST_SIGNAL_ON_READ
   9 //#define TEST_SIGNAL_ON_WRITE
  10
  11 #define RCU_GP_CTR_BIT (1 << 7)
  12 #define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1)
  13
  14 #ifndef READER_NEST_LEVEL
  15 //#define READER_NEST_LEVEL 1
  16 #define READER_NEST_LEVEL 2
  17 #endif
  18
  19 #define REMOTE_BARRIERS
  20 /*
  21  * mem.spin: Promela code to validate memory barriers with OOO memory.
  22  *
  23  * This program is free software; you can redistribute it and/or modify
  24  * it under the terms of the GNU General Public License as published by
  25  * the Free Software Foundation; either version 2 of the License, or
  26  * (at your option) any later version.
  27  *
  28  * This program is distributed in the hope that it will be useful,
  29  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  30  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  31  * GNU General Public License for more details.
  32  *
  33  * You should have received a copy of the GNU General Public License
  34  * along with this program; if not, write to the Free Software
  35  * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
  36  *
  37  * Copyright (c) 2009 Mathieu Desnoyers
  38  */
  39
  40 /* Promela validation variables. */
  41
  42 /* specific defines "included" here */
  43 /* DEFINES file "included" here */
  44
  45 /* All signal readers have same PID and uses same reader variable */
  46 #ifdef TEST_SIGNAL_ON_WRITE
  47
  48 #define NR_READERS 1    /* the writer is also a signal reader */
  49 #define NR_WRITERS 1
  50
  51 #define NR_PROCS 1
  52
  53 #define get_pid()       (0)
  54
  55 #elif defined(TEST_SIGNAL_ON_READ)
  56
  57 #define get_pid()       ((_pid < 2) -> 0 : 1)
  58
  59 #define NR_READERS 1
  60 #define NR_WRITERS 1
  61
  62 #define NR_PROCS 2
  63
  64 #else
  65
  66 #define get_pid()       (_pid)
  67
  68 #define NR_READERS 1
  69 #define NR_WRITERS 1
  70
  71 #define NR_PROCS 2
  72
  73 #endif
  74
  75 #define get_readerid()  (get_pid())
  76
  77 /*
  78  * Each process have its own data in cache. Caches are randomly updated.
  79  * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces
  80  * both.
  81  */
  82
  83 typedef per_proc_byte {
  84         byte val[NR_PROCS];
  85 };
  86
  87 /* Bitfield has a maximum of 8 procs */
  88 typedef per_proc_bit {
  89         byte bitfield;
  90 };
  91
  92 #define DECLARE_CACHED_VAR(type, x)     \
  93         type mem_##x;                   \
  94         per_proc_##type cached_##x;     \
  95         per_proc_bit cache_dirty_##x;
  96
  97 #define INIT_CACHED_VAR(x, v, j)        \
  98         mem_##x = v;                    \
  99         cache_dirty_##x.bitfield = 0;   \
 100         j = 0;                          \
 101         do                              \
 102         :: j < NR_PROCS ->              \
 103                 cached_##x.val[j] = v;  \
 104                 j++                     \
 105         :: j >= NR_PROCS -> break       \
 106         od;
 107
 108 #define IS_CACHE_DIRTY(x, id)   (cache_dirty_##x.bitfield & (1 << id))
 109
 110 #define READ_CACHED_VAR(x)      (cached_##x.val[get_pid()])
 111
 112 #define WRITE_CACHED_VAR(x, v)                          \
 113         atomic {                                        \
 114                 cached_##x.val[get_pid()] = v;          \
 115                 cache_dirty_##x.bitfield =              \
 116                         cache_dirty_##x.bitfield | (1 << get_pid());    \
 117         }
 118
 119 #define CACHE_WRITE_TO_MEM(x, id)                       \
 120         if                                              \
 121         :: IS_CACHE_DIRTY(x, id) ->                     \
 122                 mem_##x = cached_##x.val[id];           \
 123                 cache_dirty_##x.bitfield =              \
 124                         cache_dirty_##x.bitfield & (~(1 << id));        \
 125         :: else ->                                      \
 126                 skip                                    \
 127         fi;
 128
 129 #define CACHE_READ_FROM_MEM(x, id)      \
 130         if                              \
 131         :: !IS_CACHE_DIRTY(x, id) ->    \
 132                 cached_##x.val[id] = mem_##x;\
 133         :: else ->                      \
 134                 skip                    \
 135         fi;
 136
 137 /*
 138  * May update other caches if cache is dirty, or not.
 139  */
 140 #define RANDOM_CACHE_WRITE_TO_MEM(x, id)\
 141         if                              \
 142         :: 1 -> CACHE_WRITE_TO_MEM(x, id);      \
 143         :: 1 -> skip                    \
 144         fi;
 145
 146 #define RANDOM_CACHE_READ_FROM_MEM(x, id)\
 147         if                              \
 148         :: 1 -> CACHE_READ_FROM_MEM(x, id);     \
 149         :: 1 -> skip                    \
 150         fi;
 151
 152 /*
 153  * Remote barriers tests the scheme where a signal (or IPI) is sent to all
 154  * reader threads to promote their compiler barrier to a smp_mb().
 155  */
 156 #ifdef REMOTE_BARRIERS
 157
 158 inline smp_rmb_pid(i, j)
 159 {
 160         atomic {
 161                 CACHE_READ_FROM_MEM(urcu_gp_ctr, i);
 162                 j = 0;
 163                 do
 164                 :: j < NR_READERS ->
 165                         CACHE_READ_FROM_MEM(urcu_active_readers[j], i);
 166                         j++
 167                 :: j >= NR_READERS -> break
 168                 od;
 169                 CACHE_READ_FROM_MEM(generation_ptr, i);
 170         }
 171 }
 172
 173 inline smp_wmb_pid(i, j)
 174 {
 175         atomic {
 176                 CACHE_WRITE_TO_MEM(urcu_gp_ctr, i);
 177                 j = 0;
 178                 do
 179                 :: j < NR_READERS ->
 180                         CACHE_WRITE_TO_MEM(urcu_active_readers[j], i);
 181                         j++
 182                 :: j >= NR_READERS -> break
 183                 od;
 184                 CACHE_WRITE_TO_MEM(generation_ptr, i);
 185         }
 186 }
 187
 188 inline smp_mb_pid(i, j)
 189 {
 190         atomic {
 191 #ifndef NO_WMB
 192                 smp_wmb_pid(i, j);
 193 #endif
 194 #ifndef NO_RMB
 195                 smp_rmb_pid(i, j);
 196 #endif
 197 #ifdef NO_WMB
 198 #ifdef NO_RMB
 199                 ooo_mem(j);
 200 #endif
 201 #endif
 202         }
 203 }
 204
 205 /*
 206  * Readers do a simple barrier(), writers are doing a smp_mb() _and_ sending a
 207  * signal or IPI to have all readers execute a smp_mb.
 208  * We are not modeling the whole rendez-vous between readers and writers here,
 209  * we just let the writer update each reader's caches remotely.
 210  */
 211 inline smp_mb_writer(i, j)
 212 {
 213         smp_mb_pid(get_pid(), j);
 214         i = 0;
 215         do
 216         :: i < NR_READERS ->
 217                 smp_mb_pid(i, j);
 218                 i++;
 219         :: i >= NR_READERS -> break
 220         od;
 221         smp_mb_pid(get_pid(), j);
 222 }
 223
 224 inline smp_mb_reader(i, j)
 225 {
 226         skip;
 227 }
 228
 229 #else
 230
 231 inline smp_rmb(i, j)
 232 {
 233         atomic {
 234                 CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
 235                 i = 0;
 236                 do
 237                 :: i < NR_READERS ->
 238                         CACHE_READ_FROM_MEM(urcu_active_readers[i], get_pid());
 239                         i++
 240                 :: i >= NR_READERS -> break
 241                 od;
 242                 CACHE_READ_FROM_MEM(generation_ptr, get_pid());
 243         }
 244 }
 245
 246 inline smp_wmb(i, j)
 247 {
 248         atomic {
 249                 CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
 250                 i = 0;
 251                 do
 252                 :: i < NR_READERS ->
 253                         CACHE_WRITE_TO_MEM(urcu_active_readers[i], get_pid());
 254                         i++
 255                 :: i >= NR_READERS -> break
 256                 od;
 257                 CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
 258         }
 259 }
 260
 261 inline smp_mb(i, j)
 262 {
 263         atomic {
 264 #ifndef NO_WMB
 265                 smp_wmb(i, j);
 266 #endif
 267 #ifndef NO_RMB
 268                 smp_rmb(i, j);
 269 #endif
 270 #ifdef NO_WMB
 271 #ifdef NO_RMB
 272                 ooo_mem(i);
 273 #endif
 274 #endif
 275         }
 276 }
 277
 278 inline smp_mb_writer(i, j)
 279 {
 280         smp_mb(i, j);
 281 }
 282
 283 inline smp_mb_reader(i, j)
 284 {
 285         smp_mb(i, j);
 286 }
 287
 288 #endif
 289
 290 /* Keep in sync manually with smp_rmb, wmp_wmb, ooo_mem and init() */
 291 DECLARE_CACHED_VAR(byte, urcu_gp_ctr);
 292 /* Note ! currently only two readers */
 293 DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
 294 /* pointer generation */
 295 DECLARE_CACHED_VAR(byte, generation_ptr);
 296
 297 byte last_free_gen = 0;
 298 bit free_done = 0;
 299 byte read_generation[NR_READERS];
 300 bit data_access[NR_READERS];
 301
 302 bit write_lock = 0;
 303
 304 bit init_done = 0;
 305
 306 bit sighand_exec = 0;
 307
 308 inline wait_init_done()
 309 {
 310         do
 311         :: init_done == 0 -> skip;
 312         :: else -> break;
 313         od;
 314 }
 315
 316 #ifdef TEST_SIGNAL
 317
 318 inline wait_for_sighand_exec()
 319 {
 320         sighand_exec = 0;
 321         do
 322         :: sighand_exec == 0 -> skip;
 323         :: else -> break;
 324         od;
 325 }
 326
 327 #ifdef TOO_BIG_STATE_SPACE
 328 inline wait_for_sighand_exec()
 329 {
 330         sighand_exec = 0;
 331         do
 332         :: sighand_exec == 0 -> skip;
 333         :: else ->
 334                 if
 335                 :: 1 -> break;
 336                 :: 1 -> sighand_exec = 0;
 337                         skip;
 338                 fi;
 339         od;
 340 }
 341 #endif
 342
 343 #else
 344
 345 inline wait_for_sighand_exec()
 346 {
 347         skip;
 348 }
 349
 350 #endif
 351
 352 #ifdef TEST_SIGNAL_ON_WRITE
 353 /* Block on signal handler execution */
 354 inline dispatch_sighand_write_exec()
 355 {
 356         sighand_exec = 1;
 357         do
 358         :: sighand_exec == 1 ->
 359                 skip;
 360         :: else ->
 361                 break;
 362         od;
 363 }
 364
 365 #else
 366
 367 inline dispatch_sighand_write_exec()
 368 {
 369         skip;
 370 }
 371
 372 #endif
 373
 374 #ifdef TEST_SIGNAL_ON_READ
 375 /* Block on signal handler execution */
 376 inline dispatch_sighand_read_exec()
 377 {
 378         sighand_exec = 1;
 379         do
 380         :: sighand_exec == 1 ->
 381                 skip;
 382         :: else ->
 383                 break;
 384         od;
 385 }
 386
 387 #else
 388
 389 inline dispatch_sighand_read_exec()
 390 {
 391         skip;
 392 }
 393
 394 #endif
 395
 396
 397 inline ooo_mem(i)
 398 {
 399         atomic {
 400                 RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
 401                 i = 0;
 402                 do
 403                 :: i < NR_READERS ->
 404                         RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i],
 405                                 get_pid());
 406                         i++
 407                 :: i >= NR_READERS -> break
 408                 od;
 409                 RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
 410                 RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
 411                 i = 0;
 412                 do
 413                 :: i < NR_READERS ->
 414                         RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i],
 415                                 get_pid());
 416                         i++
 417                 :: i >= NR_READERS -> break
 418                 od;
 419                 RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid());
 420         }
 421 }
 422
 423 inline wait_for_reader(tmp, tmp2, i, j)
 424 {
 425         do
 426         :: 1 ->
 427                 tmp2 = READ_CACHED_VAR(urcu_active_readers[tmp]);
 428                 ooo_mem(i);
 429                 dispatch_sighand_write_exec();
 430                 if
 431                 :: (tmp2 & RCU_GP_CTR_NEST_MASK)
 432                         && ((tmp2 ^ READ_CACHED_VAR(urcu_gp_ctr))
 433                                 & RCU_GP_CTR_BIT) ->
 434 #ifndef GEN_ERROR_WRITER_PROGRESS
 435                         smp_mb_writer(i, j);
 436 #else
 437                         ooo_mem(i);
 438 #endif
 439                         dispatch_sighand_write_exec();
 440                 :: else ->
 441                         break;
 442                 fi;
 443         od;
 444 }
 445
 446 inline wait_for_quiescent_state(tmp, tmp2, i, j)
 447 {
 448         tmp = 0;
 449         do
 450         :: tmp < NR_READERS ->
 451                 wait_for_reader(tmp, tmp2, i, j);
 452                 if
 453                 :: (NR_READERS > 1) && (tmp < NR_READERS - 1)
 454                         -> ooo_mem(i);
 455                            dispatch_sighand_write_exec();
 456                 :: else
 457                         -> skip;
 458                 fi;
 459                 tmp++
 460         :: tmp >= NR_READERS -> break
 461         od;
 462 }
 463
 464 /* Model the RCU read-side critical section. */
 465
 466 #ifndef TEST_SIGNAL_ON_WRITE
 467
 468 inline urcu_one_read(i, j, nest_i, tmp, tmp2)
 469 {
 470         nest_i = 0;
 471         do
 472         :: nest_i < READER_NEST_LEVEL ->
 473                 ooo_mem(i);
 474                 dispatch_sighand_read_exec();
 475                 tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
 476                 ooo_mem(i);
 477                 dispatch_sighand_read_exec();
 478                 if
 479                 :: (!(tmp & RCU_GP_CTR_NEST_MASK))
 480                         ->
 481                         tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
 482                         ooo_mem(i);
 483                         dispatch_sighand_read_exec();
 484                         WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
 485                                          tmp2);
 486                 :: else ->
 487                         WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
 488                                          tmp + 1);
 489                 fi;
 490                 smp_mb_reader(i, j);
 491                 dispatch_sighand_read_exec();
 492                 nest_i++;
 493         :: nest_i >= READER_NEST_LEVEL -> break;
 494         od;
 495
 496         read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
 497         data_access[get_readerid()] = 1;
 498         data_access[get_readerid()] = 0;
 499
 500         nest_i = 0;
 501         do
 502         :: nest_i < READER_NEST_LEVEL ->
 503                 smp_mb_reader(i, j);
 504                 dispatch_sighand_read_exec();
 505                 tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
 506                 ooo_mem(i);
 507                 dispatch_sighand_read_exec();
 508                 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
 509                 nest_i++;
 510         :: nest_i >= READER_NEST_LEVEL -> break;
 511         od;
 512         //ooo_mem(i);
 513         //dispatch_sighand_read_exec();
 514         //smp_mc(i);    /* added */
 515 }
 516
 517 active proctype urcu_reader()
 518 {
 519         byte i, j, nest_i;
 520         byte tmp, tmp2;
 521
 522         wait_init_done();
 523
 524         assert(get_pid() < NR_PROCS);
 525
 526 end_reader:
 527         do
 528         :: 1 ->
 529                 /*
 530                  * We do not test reader's progress here, because we are mainly
 531                  * interested in writer's progress. The reader never blocks
 532                  * anyway. We have to test for reader/writer's progress
 533                  * separately, otherwise we could think the writer is doing
 534                  * progress when it's blocked by an always progressing reader.
 535                  */
 536 #ifdef READER_PROGRESS
 537 progress_reader:
 538 #endif
 539                 urcu_one_read(i, j, nest_i, tmp, tmp2);
 540         od;
 541 }
 542
 543 #endif //!TEST_SIGNAL_ON_WRITE
 544
 545 #ifdef TEST_SIGNAL
 546 /* signal handler reader */
 547
 548 inline urcu_one_read_sig(i, j, nest_i, tmp, tmp2)
 549 {
 550         nest_i = 0;
 551         do
 552         :: nest_i < READER_NEST_LEVEL ->
 553                 ooo_mem(i);
 554                 tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
 555                 ooo_mem(i);
 556                 if
 557                 :: (!(tmp & RCU_GP_CTR_NEST_MASK))
 558                         ->
 559                         tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
 560                         ooo_mem(i);
 561                         WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
 562                                          tmp2);
 563                 :: else ->
 564                         WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
 565                                          tmp + 1);
 566                 fi;
 567                 smp_mb_reader(i, j);
 568                 nest_i++;
 569         :: nest_i >= READER_NEST_LEVEL -> break;
 570         od;
 571
 572         read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
 573         data_access[get_readerid()] = 1;
 574         data_access[get_readerid()] = 0;
 575
 576         nest_i = 0;
 577         do
 578         :: nest_i < READER_NEST_LEVEL ->
 579                 smp_mb_reader(i, j);
 580                 tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
 581                 ooo_mem(i);
 582                 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
 583                 nest_i++;
 584         :: nest_i >= READER_NEST_LEVEL -> break;
 585         od;
 586         //ooo_mem(i);
 587         //smp_mc(i);    /* added */
 588 }
 589
 590 active proctype urcu_reader_sig()
 591 {
 592         byte i, j, nest_i;
 593         byte tmp, tmp2;
 594
 595         wait_init_done();
 596
 597         assert(get_pid() < NR_PROCS);
 598
 599 end_reader:
 600         do
 601         :: 1 ->
 602                 wait_for_sighand_exec();
 603                 /*
 604                  * We do not test reader's progress here, because we are mainly
 605                  * interested in writer's progress. The reader never blocks
 606                  * anyway. We have to test for reader/writer's progress
 607                  * separately, otherwise we could think the writer is doing
 608                  * progress when it's blocked by an always progressing reader.
 609                  */
 610 #ifdef READER_PROGRESS
 611 progress_reader:
 612 #endif
 613                 urcu_one_read_sig(i, j, nest_i, tmp, tmp2);
 614         od;
 615 }
 616
 617 #endif
 618
 619 /* Model the RCU update process. */
 620
 621 active proctype urcu_writer()
 622 {
 623         byte i, j;
 624         byte tmp, tmp2;
 625         byte old_gen;
 626
 627         wait_init_done();
 628
 629         assert(get_pid() < NR_PROCS);
 630
 631         do
 632         :: (READ_CACHED_VAR(generation_ptr) < 5) ->
 633 #ifdef WRITER_PROGRESS
 634 progress_writer1:
 635 #endif
 636                 ooo_mem(i);
 637                 dispatch_sighand_write_exec();
 638                 atomic {
 639                         old_gen = READ_CACHED_VAR(generation_ptr);
 640                         WRITE_CACHED_VAR(generation_ptr, old_gen + 1);
 641                 }
 642                 ooo_mem(i);
 643                 dispatch_sighand_write_exec();
 644
 645                 do
 646                 :: 1 ->
 647                         atomic {
 648                                 if
 649                                 :: write_lock == 0 ->
 650                                         write_lock = 1;
 651                                         break;
 652                                 :: else ->
 653                                         skip;
 654                                 fi;
 655                         }
 656                 od;
 657                 smp_mb_writer(i, j);
 658                 dispatch_sighand_write_exec();
 659                 tmp = READ_CACHED_VAR(urcu_gp_ctr);
 660                 ooo_mem(i);
 661                 dispatch_sighand_write_exec();
 662                 WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
 663                 ooo_mem(i);
 664                 dispatch_sighand_write_exec();
 665                 //smp_mc(i);
 666                 wait_for_quiescent_state(tmp, tmp2, i, j);
 667                 //smp_mc(i);
 668 #ifndef SINGLE_FLIP
 669                 ooo_mem(i);
 670                 dispatch_sighand_write_exec();
 671                 tmp = READ_CACHED_VAR(urcu_gp_ctr);
 672                 ooo_mem(i);
 673                 dispatch_sighand_write_exec();
 674                 WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
 675                 //smp_mc(i);
 676                 ooo_mem(i);
 677                 dispatch_sighand_write_exec();
 678                 wait_for_quiescent_state(tmp, tmp2, i, j);
 679 #endif
 680                 smp_mb_writer(i, j);
 681                 dispatch_sighand_write_exec();
 682                 write_lock = 0;
 683                 /* free-up step, e.g., kfree(). */
 684                 atomic {
 685                         last_free_gen = old_gen;
 686                         free_done = 1;
 687                 }
 688         :: else -> break;
 689         od;
 690         /*
 691          * Given the reader loops infinitely, let the writer also busy-loop
 692          * with progress here so, with weak fairness, we can test the
 693          * writer's progress.
 694          */
 695 end_writer:
 696         do
 697         :: 1 ->
 698 #ifdef WRITER_PROGRESS
 699 progress_writer2:
 700 #endif
 701                 dispatch_sighand_write_exec();
 702         od;
 703 }
 704
 705 /* Leave after the readers and writers so the pid count is ok. */
 706 init {
 707         byte i, j;
 708
 709         atomic {
 710                 INIT_CACHED_VAR(urcu_gp_ctr, 1, j);
 711                 INIT_CACHED_VAR(generation_ptr, 0, j);
 712
 713                 i = 0;
 714                 do
 715                 :: i < NR_READERS ->
 716                         INIT_CACHED_VAR(urcu_active_readers[i], 0, j);
 717                         read_generation[i] = 1;
 718                         data_access[i] = 0;
 719                         i++;
 720                 :: i >= NR_READERS -> break
 721                 od;
 722                 init_done = 1;
 723         }
 724 }