| 1 | #define NO_WMB |
| 2 | |
| 3 | // Poison value for freed memory |
| 4 | #define POISON 1 |
| 5 | // Memory with correct data |
| 6 | #define WINE 0 |
| 7 | #define SLAB_SIZE 2 |
| 8 | |
| 9 | #define read_poison (data_read_first[0] == POISON) |
| 10 | |
| 11 | #define RCU_GP_CTR_BIT (1 << 7) |
| 12 | #define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1) |
| 13 | |
| 14 | //disabled |
| 15 | #define REMOTE_BARRIERS |
| 16 | |
| 17 | #define ARCH_ALPHA |
| 18 | //#define ARCH_INTEL |
| 19 | //#define ARCH_POWERPC |
| 20 | /* |
| 21 | * mem.spin: Promela code to validate memory barriers with OOO memory |
| 22 | * and out-of-order instruction scheduling. |
| 23 | * |
| 24 | * This program is free software; you can redistribute it and/or modify |
| 25 | * it under the terms of the GNU General Public License as published by |
| 26 | * the Free Software Foundation; either version 2 of the License, or |
| 27 | * (at your option) any later version. |
| 28 | * |
| 29 | * This program is distributed in the hope that it will be useful, |
| 30 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 31 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
| 32 | * GNU General Public License for more details. |
| 33 | * |
| 34 | * You should have received a copy of the GNU General Public License |
| 35 | * along with this program; if not, write to the Free Software |
| 36 | * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. |
| 37 | * |
| 38 | * Copyright (c) 2009 Mathieu Desnoyers |
| 39 | */ |
| 40 | |
| 41 | /* Promela validation variables. */ |
| 42 | |
| 43 | /* specific defines "included" here */ |
| 44 | /* DEFINES file "included" here */ |
| 45 | |
| 46 | #define NR_READERS 1 |
| 47 | #define NR_WRITERS 1 |
| 48 | |
| 49 | #define NR_PROCS 2 |
| 50 | |
| 51 | #define get_pid() (_pid) |
| 52 | |
| 53 | #define get_readerid() (get_pid()) |
| 54 | |
| 55 | /* |
| 56 | * Produced process control and data flow. Updated after each instruction to |
| 57 | * show which variables are ready. Using one-hot bit encoding per variable to |
| 58 | * save state space. Used as triggers to execute the instructions having those |
| 59 | * variables as input. Leaving bits active to inhibit instruction execution. |
| 60 | * Scheme used to make instruction disabling and automatic dependency fall-back |
| 61 | * automatic. |
| 62 | */ |
| 63 | |
| 64 | #define CONSUME_TOKENS(state, bits, notbits) \ |
| 65 | ((!(state & (notbits))) && (state & (bits)) == (bits)) |
| 66 | |
| 67 | #define PRODUCE_TOKENS(state, bits) \ |
| 68 | state = state | (bits); |
| 69 | |
| 70 | #define CLEAR_TOKENS(state, bits) \ |
| 71 | state = state & ~(bits) |
| 72 | |
| 73 | /* |
| 74 | * Types of dependency : |
| 75 | * |
| 76 | * Data dependency |
| 77 | * |
| 78 | * - True dependency, Read-after-Write (RAW) |
| 79 | * |
| 80 | * This type of dependency happens when a statement depends on the result of a |
| 81 | * previous statement. This applies to any statement which needs to read a |
| 82 | * variable written by a preceding statement. |
| 83 | * |
| 84 | * - False dependency, Write-after-Read (WAR) |
| 85 | * |
| 86 | * Typically, variable renaming can ensure that this dependency goes away. |
| 87 | * However, if the statements must read and then write from/to the same variable |
| 88 | * in the OOO memory model, renaming may be impossible, and therefore this |
| 89 | * causes a WAR dependency. |
| 90 | * |
| 91 | * - Output dependency, Write-after-Write (WAW) |
| 92 | * |
| 93 | * Two writes to the same variable in subsequent statements. Variable renaming |
| 94 | * can ensure this is not needed, but can be required when writing multiple |
| 95 | * times to the same OOO mem model variable. |
| 96 | * |
| 97 | * Control dependency |
| 98 | * |
| 99 | * Execution of a given instruction depends on a previous instruction evaluating |
| 100 | * in a way that allows its execution. E.g. : branches. |
| 101 | * |
| 102 | * Useful considerations for joining dependencies after branch |
| 103 | * |
| 104 | * - Pre-dominance |
| 105 | * |
| 106 | * "We say box i dominates box j if every path (leading from input to output |
| 107 | * through the diagram) which passes through box j must also pass through box |
| 108 | * i. Thus box i dominates box j if box j is subordinate to box i in the |
| 109 | * program." |
| 110 | * |
| 111 | * http://www.hipersoft.rice.edu/grads/publications/dom14.pdf |
| 112 | * Other classic algorithm to calculate dominance : Lengauer-Tarjan (in gcc) |
| 113 | * |
| 114 | * - Post-dominance |
| 115 | * |
| 116 | * Just as pre-dominance, but with arcs of the data flow inverted, and input vs |
| 117 | * output exchanged. Therefore, i post-dominating j ensures that every path |
| 118 | * passing by j will pass by i before reaching the output. |
| 119 | * |
| 120 | * Prefetch and speculative execution |
| 121 | * |
| 122 | * If an instruction depends on the result of a previous branch, but it does not |
| 123 | * have side-effects, it can be executed before the branch result is known. |
| 124 | * however, it must be restarted if a core-synchronizing instruction is issued. |
| 125 | * Note that instructions which depend on the speculative instruction result |
| 126 | * but that have side-effects must depend on the branch completion in addition |
| 127 | * to the speculatively executed instruction. |
| 128 | * |
| 129 | * Other considerations |
| 130 | * |
| 131 | * Note about "volatile" keyword dependency : The compiler will order volatile |
| 132 | * accesses so they appear in the right order on a given CPU. They can be |
| 133 | * reordered by the CPU instruction scheduling. This therefore cannot be |
| 134 | * considered as a depencency. |
| 135 | * |
| 136 | * References : |
| 137 | * |
| 138 | * Cooper, Keith D.; & Torczon, Linda. (2005). Engineering a Compiler. Morgan |
| 139 | * Kaufmann. ISBN 1-55860-698-X. |
| 140 | * Kennedy, Ken; & Allen, Randy. (2001). Optimizing Compilers for Modern |
| 141 | * Architectures: A Dependence-based Approach. Morgan Kaufmann. ISBN |
| 142 | * 1-55860-286-0. |
| 143 | * Muchnick, Steven S. (1997). Advanced Compiler Design and Implementation. |
| 144 | * Morgan Kaufmann. ISBN 1-55860-320-4. |
| 145 | */ |
| 146 | |
| 147 | /* |
| 148 | * Note about loops and nested calls |
| 149 | * |
| 150 | * To keep this model simple, loops expressed in the framework will behave as if |
| 151 | * there was a core synchronizing instruction between loops. To see the effect |
| 152 | * of loop unrolling, manually unrolling loops is required. Note that if loops |
| 153 | * end or start with a core synchronizing instruction, the model is appropriate. |
| 154 | * Nested calls are not supported. |
| 155 | */ |
| 156 | |
| 157 | /* |
| 158 | * Only Alpha has out-of-order cache bank loads. Other architectures (intel, |
| 159 | * powerpc, arm) ensure that dependent reads won't be reordered. c.f. |
| 160 | * http://www.linuxjournal.com/article/8212) |
| 161 | */ |
| 162 | #ifdef ARCH_ALPHA |
| 163 | #define HAVE_OOO_CACHE_READ |
| 164 | #endif |
| 165 | |
| 166 | /* |
| 167 | * Each process have its own data in cache. Caches are randomly updated. |
| 168 | * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces |
| 169 | * both. |
| 170 | */ |
| 171 | |
| 172 | typedef per_proc_byte { |
| 173 | byte val[NR_PROCS]; |
| 174 | }; |
| 175 | |
| 176 | typedef per_proc_bit { |
| 177 | bit val[NR_PROCS]; |
| 178 | }; |
| 179 | |
| 180 | /* Bitfield has a maximum of 8 procs */ |
| 181 | typedef per_proc_bitfield { |
| 182 | byte bitfield; |
| 183 | }; |
| 184 | |
| 185 | #define DECLARE_CACHED_VAR(type, x) \ |
| 186 | type mem_##x; |
| 187 | |
| 188 | #define DECLARE_PROC_CACHED_VAR(type, x)\ |
| 189 | type cached_##x; \ |
| 190 | bit cache_dirty_##x; |
| 191 | |
| 192 | #define INIT_CACHED_VAR(x, v) \ |
| 193 | mem_##x = v; |
| 194 | |
| 195 | #define INIT_PROC_CACHED_VAR(x, v) \ |
| 196 | cache_dirty_##x = 0; \ |
| 197 | cached_##x = v; |
| 198 | |
| 199 | #define IS_CACHE_DIRTY(x, id) (cache_dirty_##x) |
| 200 | |
| 201 | #define READ_CACHED_VAR(x) (cached_##x) |
| 202 | |
| 203 | #define WRITE_CACHED_VAR(x, v) \ |
| 204 | atomic { \ |
| 205 | cached_##x = v; \ |
| 206 | cache_dirty_##x = 1; \ |
| 207 | } |
| 208 | |
| 209 | #define CACHE_WRITE_TO_MEM(x, id) \ |
| 210 | if \ |
| 211 | :: IS_CACHE_DIRTY(x, id) -> \ |
| 212 | mem_##x = cached_##x; \ |
| 213 | cache_dirty_##x = 0; \ |
| 214 | :: else -> \ |
| 215 | skip \ |
| 216 | fi; |
| 217 | |
| 218 | #define CACHE_READ_FROM_MEM(x, id) \ |
| 219 | if \ |
| 220 | :: !IS_CACHE_DIRTY(x, id) -> \ |
| 221 | cached_##x = mem_##x; \ |
| 222 | :: else -> \ |
| 223 | skip \ |
| 224 | fi; |
| 225 | |
| 226 | /* |
| 227 | * May update other caches if cache is dirty, or not. |
| 228 | */ |
| 229 | #define RANDOM_CACHE_WRITE_TO_MEM(x, id)\ |
| 230 | if \ |
| 231 | :: 1 -> CACHE_WRITE_TO_MEM(x, id); \ |
| 232 | :: 1 -> skip \ |
| 233 | fi; |
| 234 | |
| 235 | #define RANDOM_CACHE_READ_FROM_MEM(x, id)\ |
| 236 | if \ |
| 237 | :: 1 -> CACHE_READ_FROM_MEM(x, id); \ |
| 238 | :: 1 -> skip \ |
| 239 | fi; |
| 240 | |
| 241 | /* Must consume all prior read tokens. All subsequent reads depend on it. */ |
| 242 | inline smp_rmb(i) |
| 243 | { |
| 244 | atomic { |
| 245 | CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid()); |
| 246 | i = 0; |
| 247 | do |
| 248 | :: i < NR_READERS -> |
| 249 | CACHE_READ_FROM_MEM(urcu_active_readers[i], get_pid()); |
| 250 | i++ |
| 251 | :: i >= NR_READERS -> break |
| 252 | od; |
| 253 | CACHE_READ_FROM_MEM(rcu_ptr, get_pid()); |
| 254 | i = 0; |
| 255 | do |
| 256 | :: i < SLAB_SIZE -> |
| 257 | CACHE_READ_FROM_MEM(rcu_data[i], get_pid()); |
| 258 | i++ |
| 259 | :: i >= SLAB_SIZE -> break |
| 260 | od; |
| 261 | } |
| 262 | } |
| 263 | |
| 264 | /* Must consume all prior write tokens. All subsequent writes depend on it. */ |
| 265 | inline smp_wmb(i) |
| 266 | { |
| 267 | atomic { |
| 268 | CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid()); |
| 269 | i = 0; |
| 270 | do |
| 271 | :: i < NR_READERS -> |
| 272 | CACHE_WRITE_TO_MEM(urcu_active_readers[i], get_pid()); |
| 273 | i++ |
| 274 | :: i >= NR_READERS -> break |
| 275 | od; |
| 276 | CACHE_WRITE_TO_MEM(rcu_ptr, get_pid()); |
| 277 | i = 0; |
| 278 | do |
| 279 | :: i < SLAB_SIZE -> |
| 280 | CACHE_WRITE_TO_MEM(rcu_data[i], get_pid()); |
| 281 | i++ |
| 282 | :: i >= SLAB_SIZE -> break |
| 283 | od; |
| 284 | } |
| 285 | } |
| 286 | |
| 287 | /* Synchronization point. Must consume all prior read and write tokens. All |
| 288 | * subsequent reads and writes depend on it. */ |
| 289 | inline smp_mb(i) |
| 290 | { |
| 291 | atomic { |
| 292 | smp_wmb(i); |
| 293 | smp_rmb(i); |
| 294 | } |
| 295 | } |
| 296 | |
| 297 | #ifdef REMOTE_BARRIERS |
| 298 | |
| 299 | bit reader_barrier[NR_READERS]; |
| 300 | |
| 301 | /* |
| 302 | * We cannot leave the barriers dependencies in place in REMOTE_BARRIERS mode |
| 303 | * because they would add unexisting core synchronization and would therefore |
| 304 | * create an incomplete model. |
| 305 | * Therefore, we model the read-side memory barriers by completely disabling the |
| 306 | * memory barriers and their dependencies from the read-side. One at a time |
| 307 | * (different verification runs), we make a different instruction listen for |
| 308 | * signals. |
| 309 | */ |
| 310 | |
| 311 | #define smp_mb_reader(i, j) |
| 312 | |
| 313 | /* |
| 314 | * Service 0, 1 or many barrier requests. |
| 315 | */ |
| 316 | inline smp_mb_recv(i, j) |
| 317 | { |
| 318 | do |
| 319 | :: (reader_barrier[get_readerid()] == 1) -> |
| 320 | /* |
| 321 | * We choose to ignore cycles caused by writer busy-looping, |
| 322 | * waiting for the reader, sending barrier requests, and the |
| 323 | * reader always services them without continuing execution. |
| 324 | */ |
| 325 | progress_ignoring_mb1: |
| 326 | smp_mb(i); |
| 327 | reader_barrier[get_readerid()] = 0; |
| 328 | :: 1 -> |
| 329 | /* |
| 330 | * We choose to ignore writer's non-progress caused by the |
| 331 | * reader ignoring the writer's mb() requests. |
| 332 | */ |
| 333 | progress_ignoring_mb2: |
| 334 | break; |
| 335 | od; |
| 336 | } |
| 337 | |
| 338 | #define PROGRESS_LABEL(progressid) progress_writer_progid_##progressid: |
| 339 | |
| 340 | #define smp_mb_send(i, j, progressid) \ |
| 341 | { \ |
| 342 | smp_mb(i); \ |
| 343 | i = 0; \ |
| 344 | do \ |
| 345 | :: i < NR_READERS -> \ |
| 346 | reader_barrier[i] = 1; \ |
| 347 | /* \ |
| 348 | * Busy-looping waiting for reader barrier handling is of little\ |
| 349 | * interest, given the reader has the ability to totally ignore \ |
| 350 | * barrier requests. \ |
| 351 | */ \ |
| 352 | do \ |
| 353 | :: (reader_barrier[i] == 1) -> \ |
| 354 | PROGRESS_LABEL(progressid) \ |
| 355 | skip; \ |
| 356 | :: (reader_barrier[i] == 0) -> break; \ |
| 357 | od; \ |
| 358 | i++; \ |
| 359 | :: i >= NR_READERS -> \ |
| 360 | break \ |
| 361 | od; \ |
| 362 | smp_mb(i); \ |
| 363 | } |
| 364 | |
| 365 | #else |
| 366 | |
| 367 | #define smp_mb_send(i, j, progressid) smp_mb(i) |
| 368 | #define smp_mb_reader(i, j) smp_mb(i) |
| 369 | #define smp_mb_recv(i, j) |
| 370 | |
| 371 | #endif |
| 372 | |
| 373 | /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */ |
| 374 | DECLARE_CACHED_VAR(byte, urcu_gp_ctr); |
| 375 | /* Note ! currently only one reader */ |
| 376 | DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]); |
| 377 | /* RCU data */ |
| 378 | DECLARE_CACHED_VAR(bit, rcu_data[SLAB_SIZE]); |
| 379 | |
| 380 | /* RCU pointer */ |
| 381 | #if (SLAB_SIZE == 2) |
| 382 | DECLARE_CACHED_VAR(bit, rcu_ptr); |
| 383 | bit ptr_read_first[NR_READERS]; |
| 384 | #else |
| 385 | DECLARE_CACHED_VAR(byte, rcu_ptr); |
| 386 | byte ptr_read_first[NR_READERS]; |
| 387 | #endif |
| 388 | |
| 389 | bit data_read_first[NR_READERS]; |
| 390 | |
| 391 | bit init_done = 0; |
| 392 | |
| 393 | inline wait_init_done() |
| 394 | { |
| 395 | do |
| 396 | :: init_done == 0 -> skip; |
| 397 | :: else -> break; |
| 398 | od; |
| 399 | } |
| 400 | |
| 401 | inline ooo_mem(i) |
| 402 | { |
| 403 | atomic { |
| 404 | RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid()); |
| 405 | i = 0; |
| 406 | do |
| 407 | :: i < NR_READERS -> |
| 408 | RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i], |
| 409 | get_pid()); |
| 410 | i++ |
| 411 | :: i >= NR_READERS -> break |
| 412 | od; |
| 413 | RANDOM_CACHE_WRITE_TO_MEM(rcu_ptr, get_pid()); |
| 414 | i = 0; |
| 415 | do |
| 416 | :: i < SLAB_SIZE -> |
| 417 | RANDOM_CACHE_WRITE_TO_MEM(rcu_data[i], get_pid()); |
| 418 | i++ |
| 419 | :: i >= SLAB_SIZE -> break |
| 420 | od; |
| 421 | #ifdef HAVE_OOO_CACHE_READ |
| 422 | RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid()); |
| 423 | i = 0; |
| 424 | do |
| 425 | :: i < NR_READERS -> |
| 426 | RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i], |
| 427 | get_pid()); |
| 428 | i++ |
| 429 | :: i >= NR_READERS -> break |
| 430 | od; |
| 431 | RANDOM_CACHE_READ_FROM_MEM(rcu_ptr, get_pid()); |
| 432 | i = 0; |
| 433 | do |
| 434 | :: i < SLAB_SIZE -> |
| 435 | RANDOM_CACHE_READ_FROM_MEM(rcu_data[i], get_pid()); |
| 436 | i++ |
| 437 | :: i >= SLAB_SIZE -> break |
| 438 | od; |
| 439 | #else |
| 440 | smp_rmb(i); |
| 441 | #endif /* HAVE_OOO_CACHE_READ */ |
| 442 | } |
| 443 | } |
| 444 | |
| 445 | /* |
| 446 | * Bit encoding, urcu_reader : |
| 447 | */ |
| 448 | |
| 449 | int _proc_urcu_reader; |
| 450 | #define proc_urcu_reader _proc_urcu_reader |
| 451 | |
| 452 | /* Body of PROCEDURE_READ_LOCK */ |
| 453 | #define READ_PROD_A_READ (1 << 0) |
| 454 | #define READ_PROD_B_IF_TRUE (1 << 1) |
| 455 | #define READ_PROD_B_IF_FALSE (1 << 2) |
| 456 | #define READ_PROD_C_IF_TRUE_READ (1 << 3) |
| 457 | |
| 458 | #define PROCEDURE_READ_LOCK(base, consumetoken, consumetoken2, producetoken) \ |
| 459 | :: CONSUME_TOKENS(proc_urcu_reader, (consumetoken | consumetoken2), READ_PROD_A_READ << base) -> \ |
| 460 | ooo_mem(i); \ |
| 461 | tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \ |
| 462 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_A_READ << base); \ |
| 463 | :: CONSUME_TOKENS(proc_urcu_reader, \ |
| 464 | READ_PROD_A_READ << base, /* RAW, pre-dominant */ \ |
| 465 | (READ_PROD_B_IF_TRUE | READ_PROD_B_IF_FALSE) << base) -> \ |
| 466 | if \ |
| 467 | :: (!(tmp & RCU_GP_CTR_NEST_MASK)) -> \ |
| 468 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_TRUE << base); \ |
| 469 | :: else -> \ |
| 470 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_FALSE << base); \ |
| 471 | fi; \ |
| 472 | /* IF TRUE */ \ |
| 473 | :: CONSUME_TOKENS(proc_urcu_reader, consumetoken, /* prefetch */ \ |
| 474 | READ_PROD_C_IF_TRUE_READ << base) -> \ |
| 475 | ooo_mem(i); \ |
| 476 | tmp2 = READ_CACHED_VAR(urcu_gp_ctr); \ |
| 477 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_C_IF_TRUE_READ << base); \ |
| 478 | :: CONSUME_TOKENS(proc_urcu_reader, \ |
| 479 | (READ_PROD_B_IF_TRUE \ |
| 480 | | READ_PROD_C_IF_TRUE_READ /* pre-dominant */ \ |
| 481 | | READ_PROD_A_READ) << base, /* WAR */ \ |
| 482 | producetoken) -> \ |
| 483 | ooo_mem(i); \ |
| 484 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2); \ |
| 485 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ |
| 486 | /* IF_MERGE implies \ |
| 487 | * post-dominance */ \ |
| 488 | /* ELSE */ \ |
| 489 | :: CONSUME_TOKENS(proc_urcu_reader, \ |
| 490 | (READ_PROD_B_IF_FALSE /* pre-dominant */ \ |
| 491 | | READ_PROD_A_READ) << base, /* WAR */ \ |
| 492 | producetoken) -> \ |
| 493 | ooo_mem(i); \ |
| 494 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], \ |
| 495 | tmp + 1); \ |
| 496 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ |
| 497 | /* IF_MERGE implies \ |
| 498 | * post-dominance */ \ |
| 499 | /* ENDIF */ \ |
| 500 | skip |
| 501 | |
| 502 | /* Body of PROCEDURE_READ_LOCK */ |
| 503 | #define READ_PROC_READ_UNLOCK (1 << 0) |
| 504 | |
| 505 | #define PROCEDURE_READ_UNLOCK(base, consumetoken, producetoken) \ |
| 506 | :: CONSUME_TOKENS(proc_urcu_reader, \ |
| 507 | consumetoken, \ |
| 508 | READ_PROC_READ_UNLOCK << base) -> \ |
| 509 | ooo_mem(i); \ |
| 510 | tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \ |
| 511 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_UNLOCK << base); \ |
| 512 | :: CONSUME_TOKENS(proc_urcu_reader, \ |
| 513 | consumetoken \ |
| 514 | | (READ_PROC_READ_UNLOCK << base), /* WAR */ \ |
| 515 | producetoken) -> \ |
| 516 | ooo_mem(i); \ |
| 517 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp - 1); \ |
| 518 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ |
| 519 | skip |
| 520 | |
| 521 | |
| 522 | #define READ_PROD_NONE (1 << 0) |
| 523 | |
| 524 | /* PROCEDURE_READ_LOCK base = << 1 : 1 to 5 */ |
| 525 | #define READ_LOCK_BASE 1 |
| 526 | #define READ_LOCK_OUT (1 << 5) |
| 527 | |
| 528 | #define READ_PROC_FIRST_MB (1 << 6) |
| 529 | |
| 530 | #define READ_PROC_READ_GEN (1 << 12) |
| 531 | #define READ_PROC_ACCESS_GEN (1 << 13) |
| 532 | |
| 533 | #define READ_PROC_SECOND_MB (1 << 16) |
| 534 | |
| 535 | /* PROCEDURE_READ_UNLOCK base = << 17 : 17 to 18 */ |
| 536 | #define READ_UNLOCK_BASE 17 |
| 537 | #define READ_UNLOCK_OUT (1 << 18) |
| 538 | |
| 539 | /* Should not include branches */ |
| 540 | #define READ_PROC_ALL_TOKENS (READ_PROD_NONE \ |
| 541 | | READ_LOCK_OUT \ |
| 542 | | READ_PROC_FIRST_MB \ |
| 543 | | READ_PROC_READ_GEN \ |
| 544 | | READ_PROC_ACCESS_GEN \ |
| 545 | | READ_PROC_SECOND_MB \ |
| 546 | | READ_UNLOCK_OUT) |
| 547 | |
| 548 | /* Must clear all tokens, including branches */ |
| 549 | #define READ_PROC_ALL_TOKENS_CLEAR ((1 << 30) - 1) |
| 550 | |
| 551 | inline urcu_one_read(i, j, nest_i, tmp, tmp2) |
| 552 | { |
| 553 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_NONE); |
| 554 | |
| 555 | #ifdef NO_MB |
| 556 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); |
| 557 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); |
| 558 | #endif |
| 559 | |
| 560 | #ifdef REMOTE_BARRIERS |
| 561 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); |
| 562 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); |
| 563 | #endif |
| 564 | |
| 565 | do |
| 566 | :: 1 -> |
| 567 | |
| 568 | #ifdef REMOTE_BARRIERS |
| 569 | /* |
| 570 | * Signal-based memory barrier will only execute when the |
| 571 | * execution order appears in program order. |
| 572 | */ |
| 573 | if |
| 574 | :: 1 -> |
| 575 | atomic { |
| 576 | if |
| 577 | :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE, |
| 578 | READ_LOCK_OUT |
| 579 | | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN |
| 580 | | READ_UNLOCK_OUT) |
| 581 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE |
| 582 | | READ_LOCK_OUT, |
| 583 | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN |
| 584 | | READ_UNLOCK_OUT) |
| 585 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE |
| 586 | | READ_LOCK_OUT |
| 587 | | READ_PROC_READ_GEN, READ_PROC_ACCESS_GEN |
| 588 | | READ_UNLOCK_OUT) |
| 589 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE |
| 590 | | READ_LOCK_OUT |
| 591 | | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN, |
| 592 | READ_UNLOCK_OUT) |
| 593 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE |
| 594 | | READ_LOCK_OUT |
| 595 | | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN |
| 596 | | READ_UNLOCK_OUT, 0) -> |
| 597 | goto non_atomic3; |
| 598 | non_atomic3_end: |
| 599 | skip; |
| 600 | fi; |
| 601 | } |
| 602 | fi; |
| 603 | |
| 604 | goto non_atomic3_skip; |
| 605 | non_atomic3: |
| 606 | smp_mb_recv(i, j); |
| 607 | goto non_atomic3_end; |
| 608 | non_atomic3_skip: |
| 609 | |
| 610 | #endif /* REMOTE_BARRIERS */ |
| 611 | |
| 612 | atomic { |
| 613 | if |
| 614 | PROCEDURE_READ_LOCK(READ_LOCK_BASE, READ_PROD_NONE, 0, READ_LOCK_OUT); |
| 615 | |
| 616 | :: CONSUME_TOKENS(proc_urcu_reader, |
| 617 | READ_LOCK_OUT, /* post-dominant */ |
| 618 | READ_PROC_FIRST_MB) -> |
| 619 | smp_mb_reader(i, j); |
| 620 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); |
| 621 | |
| 622 | :: CONSUME_TOKENS(proc_urcu_reader, |
| 623 | READ_PROC_FIRST_MB, /* mb() orders reads */ |
| 624 | READ_PROC_READ_GEN) -> |
| 625 | ooo_mem(i); |
| 626 | ptr_read_first[get_readerid()] = READ_CACHED_VAR(rcu_ptr); |
| 627 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN); |
| 628 | |
| 629 | :: CONSUME_TOKENS(proc_urcu_reader, |
| 630 | READ_PROC_FIRST_MB /* mb() orders reads */ |
| 631 | | READ_PROC_READ_GEN, |
| 632 | READ_PROC_ACCESS_GEN) -> |
| 633 | /* smp_read_barrier_depends */ |
| 634 | goto rmb1; |
| 635 | rmb1_end: |
| 636 | data_read_first[get_readerid()] = |
| 637 | READ_CACHED_VAR(rcu_data[ptr_read_first[get_readerid()]]); |
| 638 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN); |
| 639 | |
| 640 | |
| 641 | :: CONSUME_TOKENS(proc_urcu_reader, |
| 642 | READ_PROC_ACCESS_GEN /* mb() orders reads */ |
| 643 | | READ_PROC_READ_GEN /* mb() orders reads */ |
| 644 | | READ_PROC_FIRST_MB /* mb() ordered */ |
| 645 | | READ_LOCK_OUT, /* post-dominant */ |
| 646 | READ_PROC_SECOND_MB) -> |
| 647 | smp_mb_reader(i, j); |
| 648 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); |
| 649 | |
| 650 | PROCEDURE_READ_UNLOCK(READ_UNLOCK_BASE, |
| 651 | READ_PROC_SECOND_MB /* mb() orders reads */ |
| 652 | | READ_PROC_FIRST_MB /* mb() orders reads */ |
| 653 | | READ_LOCK_OUT, /* RAW */ |
| 654 | READ_UNLOCK_OUT); |
| 655 | |
| 656 | :: CONSUME_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS, 0) -> |
| 657 | CLEAR_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS_CLEAR); |
| 658 | break; |
| 659 | fi; |
| 660 | } |
| 661 | od; |
| 662 | /* |
| 663 | * Dependency between consecutive loops : |
| 664 | * RAW dependency on |
| 665 | * WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1) |
| 666 | * tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); |
| 667 | * between loops. |
| 668 | * _WHEN THE MB()s are in place_, they add full ordering of the |
| 669 | * generation pointer read wrt active reader count read, which ensures |
| 670 | * execution will not spill across loop execution. |
| 671 | * However, in the event mb()s are removed (execution using signal |
| 672 | * handler to promote barrier()() -> smp_mb()), nothing prevents one loop |
| 673 | * to spill its execution on other loop's execution. |
| 674 | */ |
| 675 | goto end; |
| 676 | rmb1: |
| 677 | #ifndef NO_RMB |
| 678 | smp_rmb(i); |
| 679 | #else |
| 680 | ooo_mem(i); |
| 681 | #endif |
| 682 | goto rmb1_end; |
| 683 | end: |
| 684 | skip; |
| 685 | } |
| 686 | |
| 687 | |
| 688 | |
| 689 | active proctype urcu_reader() |
| 690 | { |
| 691 | byte i, j, nest_i; |
| 692 | byte tmp, tmp2; |
| 693 | |
| 694 | /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */ |
| 695 | DECLARE_PROC_CACHED_VAR(byte, urcu_gp_ctr); |
| 696 | /* Note ! currently only one reader */ |
| 697 | DECLARE_PROC_CACHED_VAR(byte, urcu_active_readers[NR_READERS]); |
| 698 | /* RCU data */ |
| 699 | DECLARE_PROC_CACHED_VAR(bit, rcu_data[SLAB_SIZE]); |
| 700 | |
| 701 | /* RCU pointer */ |
| 702 | #if (SLAB_SIZE == 2) |
| 703 | DECLARE_PROC_CACHED_VAR(bit, rcu_ptr); |
| 704 | #else |
| 705 | DECLARE_PROC_CACHED_VAR(byte, rcu_ptr); |
| 706 | #endif |
| 707 | |
| 708 | atomic { |
| 709 | INIT_PROC_CACHED_VAR(urcu_gp_ctr, 1); |
| 710 | INIT_PROC_CACHED_VAR(rcu_ptr, 0); |
| 711 | |
| 712 | i = 0; |
| 713 | do |
| 714 | :: i < NR_READERS -> |
| 715 | INIT_PROC_CACHED_VAR(urcu_active_readers[i], 0); |
| 716 | i++; |
| 717 | :: i >= NR_READERS -> break |
| 718 | od; |
| 719 | INIT_PROC_CACHED_VAR(rcu_data[0], WINE); |
| 720 | i = 1; |
| 721 | do |
| 722 | :: i < SLAB_SIZE -> |
| 723 | INIT_PROC_CACHED_VAR(rcu_data[i], POISON); |
| 724 | i++ |
| 725 | :: i >= SLAB_SIZE -> break |
| 726 | od; |
| 727 | } |
| 728 | |
| 729 | wait_init_done(); |
| 730 | |
| 731 | assert(get_pid() < NR_PROCS); |
| 732 | |
| 733 | end_reader: |
| 734 | do |
| 735 | :: 1 -> |
| 736 | /* |
| 737 | * We do not test reader's progress here, because we are mainly |
| 738 | * interested in writer's progress. The reader never blocks |
| 739 | * anyway. We have to test for reader/writer's progress |
| 740 | * separately, otherwise we could think the writer is doing |
| 741 | * progress when it's blocked by an always progressing reader. |
| 742 | */ |
| 743 | #ifdef READER_PROGRESS |
| 744 | progress_reader: |
| 745 | #endif |
| 746 | urcu_one_read(i, j, nest_i, tmp, tmp2); |
| 747 | od; |
| 748 | } |
| 749 | |
| 750 | /* no name clash please */ |
| 751 | #undef proc_urcu_reader |
| 752 | |
| 753 | |
| 754 | /* Model the RCU update process. */ |
| 755 | |
| 756 | /* |
| 757 | * Bit encoding, urcu_writer : |
| 758 | * Currently only supports one reader. |
| 759 | */ |
| 760 | |
| 761 | int _proc_urcu_writer; |
| 762 | #define proc_urcu_writer _proc_urcu_writer |
| 763 | |
| 764 | #define WRITE_PROD_NONE (1 << 0) |
| 765 | |
| 766 | #define WRITE_DATA (1 << 1) |
| 767 | #define WRITE_PROC_WMB (1 << 2) |
| 768 | #define WRITE_XCHG_PTR (1 << 3) |
| 769 | |
| 770 | #define WRITE_PROC_FIRST_MB (1 << 4) |
| 771 | |
| 772 | /* first flip */ |
| 773 | #define WRITE_PROC_FIRST_READ_GP (1 << 5) |
| 774 | #define WRITE_PROC_FIRST_WRITE_GP (1 << 6) |
| 775 | #define WRITE_PROC_FIRST_WAIT (1 << 7) |
| 776 | #define WRITE_PROC_FIRST_WAIT_LOOP (1 << 8) |
| 777 | |
| 778 | /* second flip */ |
| 779 | #define WRITE_PROC_SECOND_READ_GP (1 << 9) |
| 780 | #define WRITE_PROC_SECOND_WRITE_GP (1 << 10) |
| 781 | #define WRITE_PROC_SECOND_WAIT (1 << 11) |
| 782 | #define WRITE_PROC_SECOND_WAIT_LOOP (1 << 12) |
| 783 | |
| 784 | #define WRITE_PROC_SECOND_MB (1 << 13) |
| 785 | |
| 786 | #define WRITE_FREE (1 << 14) |
| 787 | |
| 788 | #define WRITE_PROC_ALL_TOKENS (WRITE_PROD_NONE \ |
| 789 | | WRITE_DATA \ |
| 790 | | WRITE_PROC_WMB \ |
| 791 | | WRITE_XCHG_PTR \ |
| 792 | | WRITE_PROC_FIRST_MB \ |
| 793 | | WRITE_PROC_FIRST_READ_GP \ |
| 794 | | WRITE_PROC_FIRST_WRITE_GP \ |
| 795 | | WRITE_PROC_FIRST_WAIT \ |
| 796 | | WRITE_PROC_SECOND_READ_GP \ |
| 797 | | WRITE_PROC_SECOND_WRITE_GP \ |
| 798 | | WRITE_PROC_SECOND_WAIT \ |
| 799 | | WRITE_PROC_SECOND_MB \ |
| 800 | | WRITE_FREE) |
| 801 | |
| 802 | #define WRITE_PROC_ALL_TOKENS_CLEAR ((1 << 15) - 1) |
| 803 | |
| 804 | /* |
| 805 | * Mutexes are implied around writer execution. A single writer at a time. |
| 806 | */ |
| 807 | active proctype urcu_writer() |
| 808 | { |
| 809 | byte i, j; |
| 810 | byte tmp, tmp2, tmpa; |
| 811 | byte cur_data = 0, old_data, loop_nr = 0; |
| 812 | byte cur_gp_val = 0; /* |
| 813 | * Keep a local trace of the current parity so |
| 814 | * we don't add non-existing dependencies on the global |
| 815 | * GP update. Needed to test single flip case. |
| 816 | */ |
| 817 | |
| 818 | /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */ |
| 819 | DECLARE_PROC_CACHED_VAR(byte, urcu_gp_ctr); |
| 820 | /* Note ! currently only one reader */ |
| 821 | DECLARE_PROC_CACHED_VAR(byte, urcu_active_readers[NR_READERS]); |
| 822 | /* RCU data */ |
| 823 | DECLARE_PROC_CACHED_VAR(bit, rcu_data[SLAB_SIZE]); |
| 824 | |
| 825 | /* RCU pointer */ |
| 826 | #if (SLAB_SIZE == 2) |
| 827 | DECLARE_PROC_CACHED_VAR(bit, rcu_ptr); |
| 828 | #else |
| 829 | DECLARE_PROC_CACHED_VAR(byte, rcu_ptr); |
| 830 | #endif |
| 831 | |
| 832 | atomic { |
| 833 | INIT_PROC_CACHED_VAR(urcu_gp_ctr, 1); |
| 834 | INIT_PROC_CACHED_VAR(rcu_ptr, 0); |
| 835 | |
| 836 | i = 0; |
| 837 | do |
| 838 | :: i < NR_READERS -> |
| 839 | INIT_PROC_CACHED_VAR(urcu_active_readers[i], 0); |
| 840 | i++; |
| 841 | :: i >= NR_READERS -> break |
| 842 | od; |
| 843 | INIT_PROC_CACHED_VAR(rcu_data[0], WINE); |
| 844 | i = 1; |
| 845 | do |
| 846 | :: i < SLAB_SIZE -> |
| 847 | INIT_PROC_CACHED_VAR(rcu_data[i], POISON); |
| 848 | i++ |
| 849 | :: i >= SLAB_SIZE -> break |
| 850 | od; |
| 851 | } |
| 852 | |
| 853 | |
| 854 | wait_init_done(); |
| 855 | |
| 856 | assert(get_pid() < NR_PROCS); |
| 857 | |
| 858 | do |
| 859 | :: (loop_nr < 3) -> |
| 860 | #ifdef WRITER_PROGRESS |
| 861 | progress_writer1: |
| 862 | #endif |
| 863 | loop_nr = loop_nr + 1; |
| 864 | |
| 865 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROD_NONE); |
| 866 | |
| 867 | #ifdef NO_WMB |
| 868 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB); |
| 869 | #endif |
| 870 | |
| 871 | #ifdef NO_MB |
| 872 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB); |
| 873 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB); |
| 874 | #endif |
| 875 | |
| 876 | #ifdef SINGLE_FLIP |
| 877 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); |
| 878 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP); |
| 879 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT); |
| 880 | /* For single flip, we need to know the current parity */ |
| 881 | cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT; |
| 882 | #endif |
| 883 | |
| 884 | do :: 1 -> |
| 885 | atomic { |
| 886 | if |
| 887 | |
| 888 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 889 | WRITE_PROD_NONE, |
| 890 | WRITE_DATA) -> |
| 891 | ooo_mem(i); |
| 892 | cur_data = (cur_data + 1) % SLAB_SIZE; |
| 893 | WRITE_CACHED_VAR(rcu_data[cur_data], WINE); |
| 894 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_DATA); |
| 895 | |
| 896 | |
| 897 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 898 | WRITE_DATA, |
| 899 | WRITE_PROC_WMB) -> |
| 900 | smp_wmb(i); |
| 901 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB); |
| 902 | |
| 903 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 904 | WRITE_PROC_WMB, |
| 905 | WRITE_XCHG_PTR) -> |
| 906 | /* rcu_xchg_pointer() */ |
| 907 | atomic { |
| 908 | old_data = READ_CACHED_VAR(rcu_ptr); |
| 909 | WRITE_CACHED_VAR(rcu_ptr, cur_data); |
| 910 | } |
| 911 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_XCHG_PTR); |
| 912 | |
| 913 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 914 | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR, |
| 915 | WRITE_PROC_FIRST_MB) -> |
| 916 | goto smp_mb_send1; |
| 917 | smp_mb_send1_end: |
| 918 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB); |
| 919 | |
| 920 | /* first flip */ |
| 921 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 922 | WRITE_PROC_FIRST_MB, |
| 923 | WRITE_PROC_FIRST_READ_GP) -> |
| 924 | tmpa = READ_CACHED_VAR(urcu_gp_ctr); |
| 925 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_READ_GP); |
| 926 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 927 | WRITE_PROC_FIRST_MB | WRITE_PROC_WMB |
| 928 | | WRITE_PROC_FIRST_READ_GP, |
| 929 | WRITE_PROC_FIRST_WRITE_GP) -> |
| 930 | ooo_mem(i); |
| 931 | WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT); |
| 932 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WRITE_GP); |
| 933 | |
| 934 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 935 | //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */ |
| 936 | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ |
| 937 | WRITE_PROC_FIRST_WAIT | WRITE_PROC_FIRST_WAIT_LOOP) -> |
| 938 | ooo_mem(i); |
| 939 | //smp_mb(i); /* TEST */ |
| 940 | /* ONLY WAITING FOR READER 0 */ |
| 941 | tmp2 = READ_CACHED_VAR(urcu_active_readers[0]); |
| 942 | #ifndef SINGLE_FLIP |
| 943 | /* In normal execution, we are always starting by |
| 944 | * waiting for the even parity. |
| 945 | */ |
| 946 | cur_gp_val = RCU_GP_CTR_BIT; |
| 947 | #endif |
| 948 | if |
| 949 | :: (tmp2 & RCU_GP_CTR_NEST_MASK) |
| 950 | && ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) -> |
| 951 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP); |
| 952 | :: else -> |
| 953 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT); |
| 954 | fi; |
| 955 | |
| 956 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 957 | //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */ |
| 958 | WRITE_PROC_FIRST_WRITE_GP |
| 959 | | WRITE_PROC_FIRST_READ_GP |
| 960 | | WRITE_PROC_FIRST_WAIT_LOOP |
| 961 | | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR |
| 962 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ |
| 963 | 0) -> |
| 964 | #ifndef GEN_ERROR_WRITER_PROGRESS |
| 965 | goto smp_mb_send2; |
| 966 | smp_mb_send2_end: |
| 967 | /* The memory barrier will invalidate the |
| 968 | * second read done as prefetching. Note that all |
| 969 | * instructions with side-effects depending on |
| 970 | * WRITE_PROC_SECOND_READ_GP should also depend on |
| 971 | * completion of this busy-waiting loop. */ |
| 972 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); |
| 973 | #else |
| 974 | ooo_mem(i); |
| 975 | #endif |
| 976 | /* This instruction loops to WRITE_PROC_FIRST_WAIT */ |
| 977 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP | WRITE_PROC_FIRST_WAIT); |
| 978 | |
| 979 | /* second flip */ |
| 980 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 981 | //WRITE_PROC_FIRST_WAIT | //test /* no dependency. Could pre-fetch, no side-effect. */ |
| 982 | WRITE_PROC_FIRST_WRITE_GP |
| 983 | | WRITE_PROC_FIRST_READ_GP |
| 984 | | WRITE_PROC_FIRST_MB, |
| 985 | WRITE_PROC_SECOND_READ_GP) -> |
| 986 | ooo_mem(i); |
| 987 | //smp_mb(i); /* TEST */ |
| 988 | tmpa = READ_CACHED_VAR(urcu_gp_ctr); |
| 989 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); |
| 990 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 991 | WRITE_PROC_FIRST_WAIT /* dependency on first wait, because this |
| 992 | * instruction has globally observable |
| 993 | * side-effects. |
| 994 | */ |
| 995 | | WRITE_PROC_FIRST_MB |
| 996 | | WRITE_PROC_WMB |
| 997 | | WRITE_PROC_FIRST_READ_GP |
| 998 | | WRITE_PROC_FIRST_WRITE_GP |
| 999 | | WRITE_PROC_SECOND_READ_GP, |
| 1000 | WRITE_PROC_SECOND_WRITE_GP) -> |
| 1001 | ooo_mem(i); |
| 1002 | WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT); |
| 1003 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP); |
| 1004 | |
| 1005 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 1006 | //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */ |
| 1007 | WRITE_PROC_FIRST_WAIT |
| 1008 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ |
| 1009 | WRITE_PROC_SECOND_WAIT | WRITE_PROC_SECOND_WAIT_LOOP) -> |
| 1010 | ooo_mem(i); |
| 1011 | //smp_mb(i); /* TEST */ |
| 1012 | /* ONLY WAITING FOR READER 0 */ |
| 1013 | tmp2 = READ_CACHED_VAR(urcu_active_readers[0]); |
| 1014 | if |
| 1015 | :: (tmp2 & RCU_GP_CTR_NEST_MASK) |
| 1016 | && ((tmp2 ^ 0) & RCU_GP_CTR_BIT) -> |
| 1017 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP); |
| 1018 | :: else -> |
| 1019 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT); |
| 1020 | fi; |
| 1021 | |
| 1022 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 1023 | //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */ |
| 1024 | WRITE_PROC_SECOND_WRITE_GP |
| 1025 | | WRITE_PROC_FIRST_WRITE_GP |
| 1026 | | WRITE_PROC_SECOND_READ_GP |
| 1027 | | WRITE_PROC_FIRST_READ_GP |
| 1028 | | WRITE_PROC_SECOND_WAIT_LOOP |
| 1029 | | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR |
| 1030 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ |
| 1031 | 0) -> |
| 1032 | #ifndef GEN_ERROR_WRITER_PROGRESS |
| 1033 | goto smp_mb_send3; |
| 1034 | smp_mb_send3_end: |
| 1035 | #else |
| 1036 | ooo_mem(i); |
| 1037 | #endif |
| 1038 | /* This instruction loops to WRITE_PROC_SECOND_WAIT */ |
| 1039 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP | WRITE_PROC_SECOND_WAIT); |
| 1040 | |
| 1041 | |
| 1042 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 1043 | WRITE_PROC_FIRST_WAIT |
| 1044 | | WRITE_PROC_SECOND_WAIT |
| 1045 | | WRITE_PROC_FIRST_READ_GP |
| 1046 | | WRITE_PROC_SECOND_READ_GP |
| 1047 | | WRITE_PROC_FIRST_WRITE_GP |
| 1048 | | WRITE_PROC_SECOND_WRITE_GP |
| 1049 | | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR |
| 1050 | | WRITE_PROC_FIRST_MB, |
| 1051 | WRITE_PROC_SECOND_MB) -> |
| 1052 | goto smp_mb_send4; |
| 1053 | smp_mb_send4_end: |
| 1054 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB); |
| 1055 | |
| 1056 | :: CONSUME_TOKENS(proc_urcu_writer, |
| 1057 | WRITE_XCHG_PTR |
| 1058 | | WRITE_PROC_FIRST_WAIT |
| 1059 | | WRITE_PROC_SECOND_WAIT |
| 1060 | | WRITE_PROC_WMB /* No dependency on |
| 1061 | * WRITE_DATA because we |
| 1062 | * write to a |
| 1063 | * different location. */ |
| 1064 | | WRITE_PROC_SECOND_MB |
| 1065 | | WRITE_PROC_FIRST_MB, |
| 1066 | WRITE_FREE) -> |
| 1067 | WRITE_CACHED_VAR(rcu_data[old_data], POISON); |
| 1068 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_FREE); |
| 1069 | |
| 1070 | :: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) -> |
| 1071 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR); |
| 1072 | break; |
| 1073 | fi; |
| 1074 | } |
| 1075 | od; |
| 1076 | /* |
| 1077 | * Note : Promela model adds implicit serialization of the |
| 1078 | * WRITE_FREE instruction. Normally, it would be permitted to |
| 1079 | * spill on the next loop execution. Given the validation we do |
| 1080 | * checks for the data entry read to be poisoned, it's ok if |
| 1081 | * we do not check "late arriving" memory poisoning. |
| 1082 | */ |
| 1083 | :: else -> break; |
| 1084 | od; |
| 1085 | /* |
| 1086 | * Given the reader loops infinitely, let the writer also busy-loop |
| 1087 | * with progress here so, with weak fairness, we can test the |
| 1088 | * writer's progress. |
| 1089 | */ |
| 1090 | end_writer: |
| 1091 | do |
| 1092 | :: 1 -> |
| 1093 | #ifdef WRITER_PROGRESS |
| 1094 | progress_writer2: |
| 1095 | #endif |
| 1096 | #ifdef READER_PROGRESS |
| 1097 | /* |
| 1098 | * Make sure we don't block the reader's progress. |
| 1099 | */ |
| 1100 | smp_mb_send(i, j, 5); |
| 1101 | #endif |
| 1102 | skip; |
| 1103 | od; |
| 1104 | |
| 1105 | /* Non-atomic parts of the loop */ |
| 1106 | goto end; |
| 1107 | smp_mb_send1: |
| 1108 | smp_mb_send(i, j, 1); |
| 1109 | goto smp_mb_send1_end; |
| 1110 | #ifndef GEN_ERROR_WRITER_PROGRESS |
| 1111 | smp_mb_send2: |
| 1112 | smp_mb_send(i, j, 2); |
| 1113 | goto smp_mb_send2_end; |
| 1114 | smp_mb_send3: |
| 1115 | smp_mb_send(i, j, 3); |
| 1116 | goto smp_mb_send3_end; |
| 1117 | #endif |
| 1118 | smp_mb_send4: |
| 1119 | smp_mb_send(i, j, 4); |
| 1120 | goto smp_mb_send4_end; |
| 1121 | end: |
| 1122 | skip; |
| 1123 | } |
| 1124 | |
| 1125 | /* no name clash please */ |
| 1126 | #undef proc_urcu_writer |
| 1127 | |
| 1128 | |
| 1129 | /* Leave after the readers and writers so the pid count is ok. */ |
| 1130 | init { |
| 1131 | byte i, j; |
| 1132 | |
| 1133 | atomic { |
| 1134 | INIT_CACHED_VAR(urcu_gp_ctr, 1); |
| 1135 | INIT_CACHED_VAR(rcu_ptr, 0); |
| 1136 | |
| 1137 | i = 0; |
| 1138 | do |
| 1139 | :: i < NR_READERS -> |
| 1140 | INIT_CACHED_VAR(urcu_active_readers[i], 0); |
| 1141 | ptr_read_first[i] = 1; |
| 1142 | data_read_first[i] = WINE; |
| 1143 | i++; |
| 1144 | :: i >= NR_READERS -> break |
| 1145 | od; |
| 1146 | INIT_CACHED_VAR(rcu_data[0], WINE); |
| 1147 | i = 1; |
| 1148 | do |
| 1149 | :: i < SLAB_SIZE -> |
| 1150 | INIT_CACHED_VAR(rcu_data[i], POISON); |
| 1151 | i++ |
| 1152 | :: i >= SLAB_SIZE -> break |
| 1153 | od; |
| 1154 | |
| 1155 | init_done = 1; |
| 1156 | } |
| 1157 | } |