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