1Explanation of the Linux-Kernel Memory Consistency Model 2~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3 4:Author: Alan Stern <stern@rowland.harvard.edu> 5:Created: October 2017 6 7.. Contents 8 9 1. INTRODUCTION 10 2. BACKGROUND 11 3. A SIMPLE EXAMPLE 12 4. A SELECTION OF MEMORY MODELS 13 5. ORDERING AND CYCLES 14 6. EVENTS 15 7. THE PROGRAM ORDER RELATION: po AND po-loc 16 8. A WARNING 17 9. DEPENDENCY RELATIONS: data, addr, and ctrl 18 10. THE READS-FROM RELATION: rf, rfi, and rfe 19 11. CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe 20 12. THE FROM-READS RELATION: fr, fri, and fre 21 13. AN OPERATIONAL MODEL 22 14. PROPAGATION ORDER RELATION: cumul-fence 23 15. DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL 24 16. SEQUENTIAL CONSISTENCY PER VARIABLE 25 17. ATOMIC UPDATES: rmw 26 18. THE PRESERVED PROGRAM ORDER RELATION: ppo 27 19. AND THEN THERE WAS ALPHA 28 20. THE HAPPENS-BEFORE RELATION: hb 29 21. THE PROPAGATES-BEFORE RELATION: pb 30 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-fence, and rb 31 23. LOCKING 32 24. ODDS AND ENDS 33 34 35 36INTRODUCTION 37------------ 38 39The Linux-kernel memory consistency model (LKMM) is rather complex and 40obscure. This is particularly evident if you read through the 41linux-kernel.bell and linux-kernel.cat files that make up the formal 42version of the model; they are extremely terse and their meanings are 43far from clear. 44 45This document describes the ideas underlying the LKMM, but excluding 46the modeling of bare C (or plain) shared memory accesses. It is meant 47for people who want to understand how the model was designed. It does 48not go into the details of the code in the .bell and .cat files; 49rather, it explains in English what the code expresses symbolically. 50 51Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed 52toward beginners; they explain what memory consistency models are and 53the basic notions shared by all such models. People already familiar 54with these concepts can skim or skip over them. Sections 6 (EVENTS) 55through 12 (THE FROM_READS RELATION) describe the fundamental 56relations used in many models. Starting in Section 13 (AN OPERATIONAL 57MODEL), the workings of the LKMM itself are covered. 58 59Warning: The code examples in this document are not written in the 60proper format for litmus tests. They don't include a header line, the 61initializations are not enclosed in braces, the global variables are 62not passed by pointers, and they don't have an "exists" clause at the 63end. Converting them to the right format is left as an exercise for 64the reader. 65 66 67BACKGROUND 68---------- 69 70A memory consistency model (or just memory model, for short) is 71something which predicts, given a piece of computer code running on a 72particular kind of system, what values may be obtained by the code's 73load instructions. The LKMM makes these predictions for code running 74as part of the Linux kernel. 75 76In practice, people tend to use memory models the other way around. 77That is, given a piece of code and a collection of values specified 78for the loads, the model will predict whether it is possible for the 79code to run in such a way that the loads will indeed obtain the 80specified values. Of course, this is just another way of expressing 81the same idea. 82 83For code running on a uniprocessor system, the predictions are easy: 84Each load instruction must obtain the value written by the most recent 85store instruction accessing the same location (we ignore complicating 86factors such as DMA and mixed-size accesses.) But on multiprocessor 87systems, with multiple CPUs making concurrent accesses to shared 88memory locations, things aren't so simple. 89 90Different architectures have differing memory models, and the Linux 91kernel supports a variety of architectures. The LKMM has to be fairly 92permissive, in the sense that any behavior allowed by one of these 93architectures also has to be allowed by the LKMM. 94 95 96A SIMPLE EXAMPLE 97---------------- 98 99Here is a simple example to illustrate the basic concepts. Consider 100some code running as part of a device driver for an input device. The 101driver might contain an interrupt handler which collects data from the 102device, stores it in a buffer, and sets a flag to indicate the buffer 103is full. Running concurrently on a different CPU might be a part of 104the driver code being executed by a process in the midst of a read(2) 105system call. This code tests the flag to see whether the buffer is 106ready, and if it is, copies the data back to userspace. The buffer 107and the flag are memory locations shared between the two CPUs. 108 109We can abstract out the important pieces of the driver code as follows 110(the reason for using WRITE_ONCE() and READ_ONCE() instead of simple 111assignment statements is discussed later): 112 113 int buf = 0, flag = 0; 114 115 P0() 116 { 117 WRITE_ONCE(buf, 1); 118 WRITE_ONCE(flag, 1); 119 } 120 121 P1() 122 { 123 int r1; 124 int r2 = 0; 125 126 r1 = READ_ONCE(flag); 127 if (r1) 128 r2 = READ_ONCE(buf); 129 } 130 131Here the P0() function represents the interrupt handler running on one 132CPU and P1() represents the read() routine running on another. The 133value 1 stored in buf represents input data collected from the device. 134Thus, P0 stores the data in buf and then sets flag. Meanwhile, P1 135reads flag into the private variable r1, and if it is set, reads the 136data from buf into a second private variable r2 for copying to 137userspace. (Presumably if flag is not set then the driver will wait a 138while and try again.) 139 140This pattern of memory accesses, where one CPU stores values to two 141shared memory locations and another CPU loads from those locations in 142the opposite order, is widely known as the "Message Passing" or MP 143pattern. It is typical of memory access patterns in the kernel. 144 145Please note that this example code is a simplified abstraction. Real 146buffers are usually larger than a single integer, real device drivers 147usually use sleep and wakeup mechanisms rather than polling for I/O 148completion, and real code generally doesn't bother to copy values into 149private variables before using them. All that is beside the point; 150the idea here is simply to illustrate the overall pattern of memory 151accesses by the CPUs. 152 153A memory model will predict what values P1 might obtain for its loads 154from flag and buf, or equivalently, what values r1 and r2 might end up 155with after the code has finished running. 156 157Some predictions are trivial. For instance, no sane memory model would 158predict that r1 = 42 or r2 = -7, because neither of those values ever 159gets stored in flag or buf. 160 161Some nontrivial predictions are nonetheless quite simple. For 162instance, P1 might run entirely before P0 begins, in which case r1 and 163r2 will both be 0 at the end. Or P0 might run entirely before P1 164begins, in which case r1 and r2 will both be 1. 165 166The interesting predictions concern what might happen when the two 167routines run concurrently. One possibility is that P1 runs after P0's 168store to buf but before the store to flag. In this case, r1 and r2 169will again both be 0. (If P1 had been designed to read buf 170unconditionally then we would instead have r1 = 0 and r2 = 1.) 171 172However, the most interesting possibility is where r1 = 1 and r2 = 0. 173If this were to occur it would mean the driver contains a bug, because 174incorrect data would get sent to the user: 0 instead of 1. As it 175happens, the LKMM does predict this outcome can occur, and the example 176driver code shown above is indeed buggy. 177 178 179A SELECTION OF MEMORY MODELS 180---------------------------- 181 182The first widely cited memory model, and the simplest to understand, 183is Sequential Consistency. According to this model, systems behave as 184if each CPU executed its instructions in order but with unspecified 185timing. In other words, the instructions from the various CPUs get 186interleaved in a nondeterministic way, always according to some single 187global order that agrees with the order of the instructions in the 188program source for each CPU. The model says that the value obtained 189by each load is simply the value written by the most recently executed 190store to the same memory location, from any CPU. 191 192For the MP example code shown above, Sequential Consistency predicts 193that the undesired result r1 = 1, r2 = 0 cannot occur. The reasoning 194goes like this: 195 196 Since r1 = 1, P0 must store 1 to flag before P1 loads 1 from 197 it, as loads can obtain values only from earlier stores. 198 199 P1 loads from flag before loading from buf, since CPUs execute 200 their instructions in order. 201 202 P1 must load 0 from buf before P0 stores 1 to it; otherwise r2 203 would be 1 since a load obtains its value from the most recent 204 store to the same address. 205 206 P0 stores 1 to buf before storing 1 to flag, since it executes 207 its instructions in order. 208 209 Since an instruction (in this case, P1's store to flag) cannot 210 execute before itself, the specified outcome is impossible. 211 212However, real computer hardware almost never follows the Sequential 213Consistency memory model; doing so would rule out too many valuable 214performance optimizations. On ARM and PowerPC architectures, for 215instance, the MP example code really does sometimes yield r1 = 1 and 216r2 = 0. 217 218x86 and SPARC follow yet a different memory model: TSO (Total Store 219Ordering). This model predicts that the undesired outcome for the MP 220pattern cannot occur, but in other respects it differs from Sequential 221Consistency. One example is the Store Buffer (SB) pattern, in which 222each CPU stores to its own shared location and then loads from the 223other CPU's location: 224 225 int x = 0, y = 0; 226 227 P0() 228 { 229 int r0; 230 231 WRITE_ONCE(x, 1); 232 r0 = READ_ONCE(y); 233 } 234 235 P1() 236 { 237 int r1; 238 239 WRITE_ONCE(y, 1); 240 r1 = READ_ONCE(x); 241 } 242 243Sequential Consistency predicts that the outcome r0 = 0, r1 = 0 is 244impossible. (Exercise: Figure out the reasoning.) But TSO allows 245this outcome to occur, and in fact it does sometimes occur on x86 and 246SPARC systems. 247 248The LKMM was inspired by the memory models followed by PowerPC, ARM, 249x86, Alpha, and other architectures. However, it is different in 250detail from each of them. 251 252 253ORDERING AND CYCLES 254------------------- 255 256Memory models are all about ordering. Often this is temporal ordering 257(i.e., the order in which certain events occur) but it doesn't have to 258be; consider for example the order of instructions in a program's 259source code. We saw above that Sequential Consistency makes an 260important assumption that CPUs execute instructions in the same order 261as those instructions occur in the code, and there are many other 262instances of ordering playing central roles in memory models. 263 264The counterpart to ordering is a cycle. Ordering rules out cycles: 265It's not possible to have X ordered before Y, Y ordered before Z, and 266Z ordered before X, because this would mean that X is ordered before 267itself. The analysis of the MP example under Sequential Consistency 268involved just such an impossible cycle: 269 270 W: P0 stores 1 to flag executes before 271 X: P1 loads 1 from flag executes before 272 Y: P1 loads 0 from buf executes before 273 Z: P0 stores 1 to buf executes before 274 W: P0 stores 1 to flag. 275 276In short, if a memory model requires certain accesses to be ordered, 277and a certain outcome for the loads in a piece of code can happen only 278if those accesses would form a cycle, then the memory model predicts 279that outcome cannot occur. 280 281The LKMM is defined largely in terms of cycles, as we will see. 282 283 284EVENTS 285------ 286 287The LKMM does not work directly with the C statements that make up 288kernel source code. Instead it considers the effects of those 289statements in a more abstract form, namely, events. The model 290includes three types of events: 291 292 Read events correspond to loads from shared memory, such as 293 calls to READ_ONCE(), smp_load_acquire(), or 294 rcu_dereference(). 295 296 Write events correspond to stores to shared memory, such as 297 calls to WRITE_ONCE(), smp_store_release(), or atomic_set(). 298 299 Fence events correspond to memory barriers (also known as 300 fences), such as calls to smp_rmb() or rcu_read_lock(). 301 302These categories are not exclusive; a read or write event can also be 303a fence. This happens with functions like smp_load_acquire() or 304spin_lock(). However, no single event can be both a read and a write. 305Atomic read-modify-write accesses, such as atomic_inc() or xchg(), 306correspond to a pair of events: a read followed by a write. (The 307write event is omitted for executions where it doesn't occur, such as 308a cmpxchg() where the comparison fails.) 309 310Other parts of the code, those which do not involve interaction with 311shared memory, do not give rise to events. Thus, arithmetic and 312logical computations, control-flow instructions, or accesses to 313private memory or CPU registers are not of central interest to the 314memory model. They only affect the model's predictions indirectly. 315For example, an arithmetic computation might determine the value that 316gets stored to a shared memory location (or in the case of an array 317index, the address where the value gets stored), but the memory model 318is concerned only with the store itself -- its value and its address 319-- not the computation leading up to it. 320 321Events in the LKMM can be linked by various relations, which we will 322describe in the following sections. The memory model requires certain 323of these relations to be orderings, that is, it requires them not to 324have any cycles. 325 326 327THE PROGRAM ORDER RELATION: po AND po-loc 328----------------------------------------- 329 330The most important relation between events is program order (po). You 331can think of it as the order in which statements occur in the source 332code after branches are taken into account and loops have been 333unrolled. A better description might be the order in which 334instructions are presented to a CPU's execution unit. Thus, we say 335that X is po-before Y (written as "X ->po Y" in formulas) if X occurs 336before Y in the instruction stream. 337 338This is inherently a single-CPU relation; two instructions executing 339on different CPUs are never linked by po. Also, it is by definition 340an ordering so it cannot have any cycles. 341 342po-loc is a sub-relation of po. It links two memory accesses when the 343first comes before the second in program order and they access the 344same memory location (the "-loc" suffix). 345 346Although this may seem straightforward, there is one subtle aspect to 347program order we need to explain. The LKMM was inspired by low-level 348architectural memory models which describe the behavior of machine 349code, and it retains their outlook to a considerable extent. The 350read, write, and fence events used by the model are close in spirit to 351individual machine instructions. Nevertheless, the LKMM describes 352kernel code written in C, and the mapping from C to machine code can 353be extremely complex. 354 355Optimizing compilers have great freedom in the way they translate 356source code to object code. They are allowed to apply transformations 357that add memory accesses, eliminate accesses, combine them, split them 358into pieces, or move them around. The use of READ_ONCE(), WRITE_ONCE(), 359or one of the other atomic or synchronization primitives prevents a 360large number of compiler optimizations. In particular, it is guaranteed 361that the compiler will not remove such accesses from the generated code 362(unless it can prove the accesses will never be executed), it will not 363change the order in which they occur in the code (within limits imposed 364by the C standard), and it will not introduce extraneous accesses. 365 366The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather 367than ordinary memory accesses. Thanks to this usage, we can be certain 368that in the MP example, the compiler won't reorder P0's write event to 369buf and P0's write event to flag, and similarly for the other shared 370memory accesses in the examples. 371 372Since private variables are not shared between CPUs, they can be 373accessed normally without READ_ONCE() or WRITE_ONCE(). In fact, they 374need not even be stored in normal memory at all -- in principle a 375private variable could be stored in a CPU register (hence the convention 376that these variables have names starting with the letter 'r'). 377 378 379A WARNING 380--------- 381 382The protections provided by READ_ONCE(), WRITE_ONCE(), and others are 383not perfect; and under some circumstances it is possible for the 384compiler to undermine the memory model. Here is an example. Suppose 385both branches of an "if" statement store the same value to the same 386location: 387 388 r1 = READ_ONCE(x); 389 if (r1) { 390 WRITE_ONCE(y, 2); 391 ... /* do something */ 392 } else { 393 WRITE_ONCE(y, 2); 394 ... /* do something else */ 395 } 396 397For this code, the LKMM predicts that the load from x will always be 398executed before either of the stores to y. However, a compiler could 399lift the stores out of the conditional, transforming the code into 400something resembling: 401 402 r1 = READ_ONCE(x); 403 WRITE_ONCE(y, 2); 404 if (r1) { 405 ... /* do something */ 406 } else { 407 ... /* do something else */ 408 } 409 410Given this version of the code, the LKMM would predict that the load 411from x could be executed after the store to y. Thus, the memory 412model's original prediction could be invalidated by the compiler. 413 414Another issue arises from the fact that in C, arguments to many 415operators and function calls can be evaluated in any order. For 416example: 417 418 r1 = f(5) + g(6); 419 420The object code might call f(5) either before or after g(6); the 421memory model cannot assume there is a fixed program order relation 422between them. (In fact, if the functions are inlined then the 423compiler might even interleave their object code.) 424 425 426DEPENDENCY RELATIONS: data, addr, and ctrl 427------------------------------------------ 428 429We say that two events are linked by a dependency relation when the 430execution of the second event depends in some way on a value obtained 431from memory by the first. The first event must be a read, and the 432value it obtains must somehow affect what the second event does. 433There are three kinds of dependencies: data, address (addr), and 434control (ctrl). 435 436A read and a write event are linked by a data dependency if the value 437obtained by the read affects the value stored by the write. As a very 438simple example: 439 440 int x, y; 441 442 r1 = READ_ONCE(x); 443 WRITE_ONCE(y, r1 + 5); 444 445The value stored by the WRITE_ONCE obviously depends on the value 446loaded by the READ_ONCE. Such dependencies can wind through 447arbitrarily complicated computations, and a write can depend on the 448values of multiple reads. 449 450A read event and another memory access event are linked by an address 451dependency if the value obtained by the read affects the location 452accessed by the other event. The second event can be either a read or 453a write. Here's another simple example: 454 455 int a[20]; 456 int i; 457 458 r1 = READ_ONCE(i); 459 r2 = READ_ONCE(a[r1]); 460 461Here the location accessed by the second READ_ONCE() depends on the 462index value loaded by the first. Pointer indirection also gives rise 463to address dependencies, since the address of a location accessed 464through a pointer will depend on the value read earlier from that 465pointer. 466 467Finally, a read event and another memory access event are linked by a 468control dependency if the value obtained by the read affects whether 469the second event is executed at all. Simple example: 470 471 int x, y; 472 473 r1 = READ_ONCE(x); 474 if (r1) 475 WRITE_ONCE(y, 1984); 476 477Execution of the WRITE_ONCE() is controlled by a conditional expression 478which depends on the value obtained by the READ_ONCE(); hence there is 479a control dependency from the load to the store. 480 481It should be pretty obvious that events can only depend on reads that 482come earlier in program order. Symbolically, if we have R ->data X, 483R ->addr X, or R ->ctrl X (where R is a read event), then we must also 484have R ->po X. It wouldn't make sense for a computation to depend 485somehow on a value that doesn't get loaded from shared memory until 486later in the code! 487 488 489THE READS-FROM RELATION: rf, rfi, and rfe 490----------------------------------------- 491 492The reads-from relation (rf) links a write event to a read event when 493the value loaded by the read is the value that was stored by the 494write. In colloquial terms, the load "reads from" the store. We 495write W ->rf R to indicate that the load R reads from the store W. We 496further distinguish the cases where the load and the store occur on 497the same CPU (internal reads-from, or rfi) and where they occur on 498different CPUs (external reads-from, or rfe). 499 500For our purposes, a memory location's initial value is treated as 501though it had been written there by an imaginary initial store that 502executes on a separate CPU before the program runs. 503 504Usage of the rf relation implicitly assumes that loads will always 505read from a single store. It doesn't apply properly in the presence 506of load-tearing, where a load obtains some of its bits from one store 507and some of them from another store. Fortunately, use of READ_ONCE() 508and WRITE_ONCE() will prevent load-tearing; it's not possible to have: 509 510 int x = 0; 511 512 P0() 513 { 514 WRITE_ONCE(x, 0x1234); 515 } 516 517 P1() 518 { 519 int r1; 520 521 r1 = READ_ONCE(x); 522 } 523 524and end up with r1 = 0x1200 (partly from x's initial value and partly 525from the value stored by P0). 526 527On the other hand, load-tearing is unavoidable when mixed-size 528accesses are used. Consider this example: 529 530 union { 531 u32 w; 532 u16 h[2]; 533 } x; 534 535 P0() 536 { 537 WRITE_ONCE(x.h[0], 0x1234); 538 WRITE_ONCE(x.h[1], 0x5678); 539 } 540 541 P1() 542 { 543 int r1; 544 545 r1 = READ_ONCE(x.w); 546 } 547 548If r1 = 0x56781234 (little-endian!) at the end, then P1 must have read 549from both of P0's stores. It is possible to handle mixed-size and 550unaligned accesses in a memory model, but the LKMM currently does not 551attempt to do so. It requires all accesses to be properly aligned and 552of the location's actual size. 553 554 555CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe 556------------------------------------------------------------------ 557 558Cache coherence is a general principle requiring that in a 559multi-processor system, the CPUs must share a consistent view of the 560memory contents. Specifically, it requires that for each location in 561shared memory, the stores to that location must form a single global 562ordering which all the CPUs agree on (the coherence order), and this 563ordering must be consistent with the program order for accesses to 564that location. 565 566To put it another way, for any variable x, the coherence order (co) of 567the stores to x is simply the order in which the stores overwrite one 568another. The imaginary store which establishes x's initial value 569comes first in the coherence order; the store which directly 570overwrites the initial value comes second; the store which overwrites 571that value comes third, and so on. 572 573You can think of the coherence order as being the order in which the 574stores reach x's location in memory (or if you prefer a more 575hardware-centric view, the order in which the stores get written to 576x's cache line). We write W ->co W' if W comes before W' in the 577coherence order, that is, if the value stored by W gets overwritten, 578directly or indirectly, by the value stored by W'. 579 580Coherence order is required to be consistent with program order. This 581requirement takes the form of four coherency rules: 582 583 Write-write coherence: If W ->po-loc W' (i.e., W comes before 584 W' in program order and they access the same location), where W 585 and W' are two stores, then W ->co W'. 586 587 Write-read coherence: If W ->po-loc R, where W is a store and R 588 is a load, then R must read from W or from some other store 589 which comes after W in the coherence order. 590 591 Read-write coherence: If R ->po-loc W, where R is a load and W 592 is a store, then the store which R reads from must come before 593 W in the coherence order. 594 595 Read-read coherence: If R ->po-loc R', where R and R' are two 596 loads, then either they read from the same store or else the 597 store read by R comes before the store read by R' in the 598 coherence order. 599 600This is sometimes referred to as sequential consistency per variable, 601because it means that the accesses to any single memory location obey 602the rules of the Sequential Consistency memory model. (According to 603Wikipedia, sequential consistency per variable and cache coherence 604mean the same thing except that cache coherence includes an extra 605requirement that every store eventually becomes visible to every CPU.) 606 607Any reasonable memory model will include cache coherence. Indeed, our 608expectation of cache coherence is so deeply ingrained that violations 609of its requirements look more like hardware bugs than programming 610errors: 611 612 int x; 613 614 P0() 615 { 616 WRITE_ONCE(x, 17); 617 WRITE_ONCE(x, 23); 618 } 619 620If the final value stored in x after this code ran was 17, you would 621think your computer was broken. It would be a violation of the 622write-write coherence rule: Since the store of 23 comes later in 623program order, it must also come later in x's coherence order and 624thus must overwrite the store of 17. 625 626 int x = 0; 627 628 P0() 629 { 630 int r1; 631 632 r1 = READ_ONCE(x); 633 WRITE_ONCE(x, 666); 634 } 635 636If r1 = 666 at the end, this would violate the read-write coherence 637rule: The READ_ONCE() load comes before the WRITE_ONCE() store in 638program order, so it must not read from that store but rather from one 639coming earlier in the coherence order (in this case, x's initial 640value). 641 642 int x = 0; 643 644 P0() 645 { 646 WRITE_ONCE(x, 5); 647 } 648 649 P1() 650 { 651 int r1, r2; 652 653 r1 = READ_ONCE(x); 654 r2 = READ_ONCE(x); 655 } 656 657If r1 = 5 (reading from P0's store) and r2 = 0 (reading from the 658imaginary store which establishes x's initial value) at the end, this 659would violate the read-read coherence rule: The r1 load comes before 660the r2 load in program order, so it must not read from a store that 661comes later in the coherence order. 662 663(As a minor curiosity, if this code had used normal loads instead of 664READ_ONCE() in P1, on Itanium it sometimes could end up with r1 = 5 665and r2 = 0! This results from parallel execution of the operations 666encoded in Itanium's Very-Long-Instruction-Word format, and it is yet 667another motivation for using READ_ONCE() when accessing shared memory 668locations.) 669 670Just like the po relation, co is inherently an ordering -- it is not 671possible for a store to directly or indirectly overwrite itself! And 672just like with the rf relation, we distinguish between stores that 673occur on the same CPU (internal coherence order, or coi) and stores 674that occur on different CPUs (external coherence order, or coe). 675 676On the other hand, stores to different memory locations are never 677related by co, just as instructions on different CPUs are never 678related by po. Coherence order is strictly per-location, or if you 679prefer, each location has its own independent coherence order. 680 681 682THE FROM-READS RELATION: fr, fri, and fre 683----------------------------------------- 684 685The from-reads relation (fr) can be a little difficult for people to 686grok. It describes the situation where a load reads a value that gets 687overwritten by a store. In other words, we have R ->fr W when the 688value that R reads is overwritten (directly or indirectly) by W, or 689equivalently, when R reads from a store which comes earlier than W in 690the coherence order. 691 692For example: 693 694 int x = 0; 695 696 P0() 697 { 698 int r1; 699 700 r1 = READ_ONCE(x); 701 WRITE_ONCE(x, 2); 702 } 703 704The value loaded from x will be 0 (assuming cache coherence!), and it 705gets overwritten by the value 2. Thus there is an fr link from the 706READ_ONCE() to the WRITE_ONCE(). If the code contained any later 707stores to x, there would also be fr links from the READ_ONCE() to 708them. 709 710As with rf, rfi, and rfe, we subdivide the fr relation into fri (when 711the load and the store are on the same CPU) and fre (when they are on 712different CPUs). 713 714Note that the fr relation is determined entirely by the rf and co 715relations; it is not independent. Given a read event R and a write 716event W for the same location, we will have R ->fr W if and only if 717the write which R reads from is co-before W. In symbols, 718 719 (R ->fr W) := (there exists W' with W' ->rf R and W' ->co W). 720 721 722AN OPERATIONAL MODEL 723-------------------- 724 725The LKMM is based on various operational memory models, meaning that 726the models arise from an abstract view of how a computer system 727operates. Here are the main ideas, as incorporated into the LKMM. 728 729The system as a whole is divided into the CPUs and a memory subsystem. 730The CPUs are responsible for executing instructions (not necessarily 731in program order), and they communicate with the memory subsystem. 732For the most part, executing an instruction requires a CPU to perform 733only internal operations. However, loads, stores, and fences involve 734more. 735 736When CPU C executes a store instruction, it tells the memory subsystem 737to store a certain value at a certain location. The memory subsystem 738propagates the store to all the other CPUs as well as to RAM. (As a 739special case, we say that the store propagates to its own CPU at the 740time it is executed.) The memory subsystem also determines where the 741store falls in the location's coherence order. In particular, it must 742arrange for the store to be co-later than (i.e., to overwrite) any 743other store to the same location which has already propagated to CPU C. 744 745When a CPU executes a load instruction R, it first checks to see 746whether there are any as-yet unexecuted store instructions, for the 747same location, that come before R in program order. If there are, it 748uses the value of the po-latest such store as the value obtained by R, 749and we say that the store's value is forwarded to R. Otherwise, the 750CPU asks the memory subsystem for the value to load and we say that R 751is satisfied from memory. The memory subsystem hands back the value 752of the co-latest store to the location in question which has already 753propagated to that CPU. 754 755(In fact, the picture needs to be a little more complicated than this. 756CPUs have local caches, and propagating a store to a CPU really means 757propagating it to the CPU's local cache. A local cache can take some 758time to process the stores that it receives, and a store can't be used 759to satisfy one of the CPU's loads until it has been processed. On 760most architectures, the local caches process stores in 761First-In-First-Out order, and consequently the processing delay 762doesn't matter for the memory model. But on Alpha, the local caches 763have a partitioned design that results in non-FIFO behavior. We will 764discuss this in more detail later.) 765 766Note that load instructions may be executed speculatively and may be 767restarted under certain circumstances. The memory model ignores these 768premature executions; we simply say that the load executes at the 769final time it is forwarded or satisfied. 770 771Executing a fence (or memory barrier) instruction doesn't require a 772CPU to do anything special other than informing the memory subsystem 773about the fence. However, fences do constrain the way CPUs and the 774memory subsystem handle other instructions, in two respects. 775 776First, a fence forces the CPU to execute various instructions in 777program order. Exactly which instructions are ordered depends on the 778type of fence: 779 780 Strong fences, including smp_mb() and synchronize_rcu(), force 781 the CPU to execute all po-earlier instructions before any 782 po-later instructions; 783 784 smp_rmb() forces the CPU to execute all po-earlier loads 785 before any po-later loads; 786 787 smp_wmb() forces the CPU to execute all po-earlier stores 788 before any po-later stores; 789 790 Acquire fences, such as smp_load_acquire(), force the CPU to 791 execute the load associated with the fence (e.g., the load 792 part of an smp_load_acquire()) before any po-later 793 instructions; 794 795 Release fences, such as smp_store_release(), force the CPU to 796 execute all po-earlier instructions before the store 797 associated with the fence (e.g., the store part of an 798 smp_store_release()). 799 800Second, some types of fence affect the way the memory subsystem 801propagates stores. When a fence instruction is executed on CPU C: 802 803 For each other CPU C', smp_wmb() forces all po-earlier stores 804 on C to propagate to C' before any po-later stores do. 805 806 For each other CPU C', any store which propagates to C before 807 a release fence is executed (including all po-earlier 808 stores executed on C) is forced to propagate to C' before the 809 store associated with the release fence does. 810 811 Any store which propagates to C before a strong fence is 812 executed (including all po-earlier stores on C) is forced to 813 propagate to all other CPUs before any instructions po-after 814 the strong fence are executed on C. 815 816The propagation ordering enforced by release fences and strong fences 817affects stores from other CPUs that propagate to CPU C before the 818fence is executed, as well as stores that are executed on C before the 819fence. We describe this property by saying that release fences and 820strong fences are A-cumulative. By contrast, smp_wmb() fences are not 821A-cumulative; they only affect the propagation of stores that are 822executed on C before the fence (i.e., those which precede the fence in 823program order). 824 825rcu_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have 826other properties which we discuss later. 827 828 829PROPAGATION ORDER RELATION: cumul-fence 830--------------------------------------- 831 832The fences which affect propagation order (i.e., strong, release, and 833smp_wmb() fences) are collectively referred to as cumul-fences, even 834though smp_wmb() isn't A-cumulative. The cumul-fence relation is 835defined to link memory access events E and F whenever: 836 837 E and F are both stores on the same CPU and an smp_wmb() fence 838 event occurs between them in program order; or 839 840 F is a release fence and some X comes before F in program order, 841 where either X = E or else E ->rf X; or 842 843 A strong fence event occurs between some X and F in program 844 order, where either X = E or else E ->rf X. 845 846The operational model requires that whenever W and W' are both stores 847and W ->cumul-fence W', then W must propagate to any given CPU 848before W' does. However, for different CPUs C and C', it does not 849require W to propagate to C before W' propagates to C'. 850 851 852DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL 853------------------------------------------------- 854 855The LKMM is derived from the restrictions imposed by the design 856outlined above. These restrictions involve the necessity of 857maintaining cache coherence and the fact that a CPU can't operate on a 858value before it knows what that value is, among other things. 859 860The formal version of the LKMM is defined by five requirements, or 861axioms: 862 863 Sequential consistency per variable: This requires that the 864 system obey the four coherency rules. 865 866 Atomicity: This requires that atomic read-modify-write 867 operations really are atomic, that is, no other stores can 868 sneak into the middle of such an update. 869 870 Happens-before: This requires that certain instructions are 871 executed in a specific order. 872 873 Propagation: This requires that certain stores propagate to 874 CPUs and to RAM in a specific order. 875 876 Rcu: This requires that RCU read-side critical sections and 877 grace periods obey the rules of RCU, in particular, the 878 Grace-Period Guarantee. 879 880The first and second are quite common; they can be found in many 881memory models (such as those for C11/C++11). The "happens-before" and 882"propagation" axioms have analogs in other memory models as well. The 883"rcu" axiom is specific to the LKMM. 884 885Each of these axioms is discussed below. 886 887 888SEQUENTIAL CONSISTENCY PER VARIABLE 889----------------------------------- 890 891According to the principle of cache coherence, the stores to any fixed 892shared location in memory form a global ordering. We can imagine 893inserting the loads from that location into this ordering, by placing 894each load between the store that it reads from and the following 895store. This leaves the relative positions of loads that read from the 896same store unspecified; let's say they are inserted in program order, 897first for CPU 0, then CPU 1, etc. 898 899You can check that the four coherency rules imply that the rf, co, fr, 900and po-loc relations agree with this global ordering; in other words, 901whenever we have X ->rf Y or X ->co Y or X ->fr Y or X ->po-loc Y, the 902X event comes before the Y event in the global ordering. The LKMM's 903"coherence" axiom expresses this by requiring the union of these 904relations not to have any cycles. This means it must not be possible 905to find events 906 907 X0 -> X1 -> X2 -> ... -> Xn -> X0, 908 909where each of the links is either rf, co, fr, or po-loc. This has to 910hold if the accesses to the fixed memory location can be ordered as 911cache coherence demands. 912 913Although it is not obvious, it can be shown that the converse is also 914true: This LKMM axiom implies that the four coherency rules are 915obeyed. 916 917 918ATOMIC UPDATES: rmw 919------------------- 920 921What does it mean to say that a read-modify-write (rmw) update, such 922as atomic_inc(&x), is atomic? It means that the memory location (x in 923this case) does not get altered between the read and the write events 924making up the atomic operation. In particular, if two CPUs perform 925atomic_inc(&x) concurrently, it must be guaranteed that the final 926value of x will be the initial value plus two. We should never have 927the following sequence of events: 928 929 CPU 0 loads x obtaining 13; 930 CPU 1 loads x obtaining 13; 931 CPU 0 stores 14 to x; 932 CPU 1 stores 14 to x; 933 934where the final value of x is wrong (14 rather than 15). 935 936In this example, CPU 0's increment effectively gets lost because it 937occurs in between CPU 1's load and store. To put it another way, the 938problem is that the position of CPU 0's store in x's coherence order 939is between the store that CPU 1 reads from and the store that CPU 1 940performs. 941 942The same analysis applies to all atomic update operations. Therefore, 943to enforce atomicity the LKMM requires that atomic updates follow this 944rule: Whenever R and W are the read and write events composing an 945atomic read-modify-write and W' is the write event which R reads from, 946there must not be any stores coming between W' and W in the coherence 947order. Equivalently, 948 949 (R ->rmw W) implies (there is no X with R ->fr X and X ->co W), 950 951where the rmw relation links the read and write events making up each 952atomic update. This is what the LKMM's "atomic" axiom says. 953 954 955THE PRESERVED PROGRAM ORDER RELATION: ppo 956----------------------------------------- 957 958There are many situations where a CPU is obligated to execute two 959instructions in program order. We amalgamate them into the ppo (for 960"preserved program order") relation, which links the po-earlier 961instruction to the po-later instruction and is thus a sub-relation of 962po. 963 964The operational model already includes a description of one such 965situation: Fences are a source of ppo links. Suppose X and Y are 966memory accesses with X ->po Y; then the CPU must execute X before Y if 967any of the following hold: 968 969 A strong (smp_mb() or synchronize_rcu()) fence occurs between 970 X and Y; 971 972 X and Y are both stores and an smp_wmb() fence occurs between 973 them; 974 975 X and Y are both loads and an smp_rmb() fence occurs between 976 them; 977 978 X is also an acquire fence, such as smp_load_acquire(); 979 980 Y is also a release fence, such as smp_store_release(). 981 982Another possibility, not mentioned earlier but discussed in the next 983section, is: 984 985 X and Y are both loads, X ->addr Y (i.e., there is an address 986 dependency from X to Y), and X is a READ_ONCE() or an atomic 987 access. 988 989Dependencies can also cause instructions to be executed in program 990order. This is uncontroversial when the second instruction is a 991store; either a data, address, or control dependency from a load R to 992a store W will force the CPU to execute R before W. This is very 993simply because the CPU cannot tell the memory subsystem about W's 994store before it knows what value should be stored (in the case of a 995data dependency), what location it should be stored into (in the case 996of an address dependency), or whether the store should actually take 997place (in the case of a control dependency). 998 999Dependencies to load instructions are more problematic. To begin with, 1000there is no such thing as a data dependency to a load. Next, a CPU 1001has no reason to respect a control dependency to a load, because it 1002can always satisfy the second load speculatively before the first, and 1003then ignore the result if it turns out that the second load shouldn't 1004be executed after all. And lastly, the real difficulties begin when 1005we consider address dependencies to loads. 1006 1007To be fair about it, all Linux-supported architectures do execute 1008loads in program order if there is an address dependency between them. 1009After all, a CPU cannot ask the memory subsystem to load a value from 1010a particular location before it knows what that location is. However, 1011the split-cache design used by Alpha can cause it to behave in a way 1012that looks as if the loads were executed out of order (see the next 1013section for more details). The kernel includes a workaround for this 1014problem when the loads come from READ_ONCE(), and therefore the LKMM 1015includes address dependencies to loads in the ppo relation. 1016 1017On the other hand, dependencies can indirectly affect the ordering of 1018two loads. This happens when there is a dependency from a load to a 1019store and a second, po-later load reads from that store: 1020 1021 R ->dep W ->rfi R', 1022 1023where the dep link can be either an address or a data dependency. In 1024this situation we know it is possible for the CPU to execute R' before 1025W, because it can forward the value that W will store to R'. But it 1026cannot execute R' before R, because it cannot forward the value before 1027it knows what that value is, or that W and R' do access the same 1028location. However, if there is merely a control dependency between R 1029and W then the CPU can speculatively forward W to R' before executing 1030R; if the speculation turns out to be wrong then the CPU merely has to 1031restart or abandon R'. 1032 1033(In theory, a CPU might forward a store to a load when it runs across 1034an address dependency like this: 1035 1036 r1 = READ_ONCE(ptr); 1037 WRITE_ONCE(*r1, 17); 1038 r2 = READ_ONCE(*r1); 1039 1040because it could tell that the store and the second load access the 1041same location even before it knows what the location's address is. 1042However, none of the architectures supported by the Linux kernel do 1043this.) 1044 1045Two memory accesses of the same location must always be executed in 1046program order if the second access is a store. Thus, if we have 1047 1048 R ->po-loc W 1049 1050(the po-loc link says that R comes before W in program order and they 1051access the same location), the CPU is obliged to execute W after R. 1052If it executed W first then the memory subsystem would respond to R's 1053read request with the value stored by W (or an even later store), in 1054violation of the read-write coherence rule. Similarly, if we had 1055 1056 W ->po-loc W' 1057 1058and the CPU executed W' before W, then the memory subsystem would put 1059W' before W in the coherence order. It would effectively cause W to 1060overwrite W', in violation of the write-write coherence rule. 1061(Interestingly, an early ARMv8 memory model, now obsolete, proposed 1062allowing out-of-order writes like this to occur. The model avoided 1063violating the write-write coherence rule by requiring the CPU not to 1064send the W write to the memory subsystem at all!) 1065 1066 1067AND THEN THERE WAS ALPHA 1068------------------------ 1069 1070As mentioned above, the Alpha architecture is unique in that it does 1071not appear to respect address dependencies to loads. This means that 1072code such as the following: 1073 1074 int x = 0; 1075 int y = -1; 1076 int *ptr = &y; 1077 1078 P0() 1079 { 1080 WRITE_ONCE(x, 1); 1081 smp_wmb(); 1082 WRITE_ONCE(ptr, &x); 1083 } 1084 1085 P1() 1086 { 1087 int *r1; 1088 int r2; 1089 1090 r1 = ptr; 1091 r2 = READ_ONCE(*r1); 1092 } 1093 1094can malfunction on Alpha systems (notice that P1 uses an ordinary load 1095to read ptr instead of READ_ONCE()). It is quite possible that r1 = &x 1096and r2 = 0 at the end, in spite of the address dependency. 1097 1098At first glance this doesn't seem to make sense. We know that the 1099smp_wmb() forces P0's store to x to propagate to P1 before the store 1100to ptr does. And since P1 can't execute its second load 1101until it knows what location to load from, i.e., after executing its 1102first load, the value x = 1 must have propagated to P1 before the 1103second load executed. So why doesn't r2 end up equal to 1? 1104 1105The answer lies in the Alpha's split local caches. Although the two 1106stores do reach P1's local cache in the proper order, it can happen 1107that the first store is processed by a busy part of the cache while 1108the second store is processed by an idle part. As a result, the x = 1 1109value may not become available for P1's CPU to read until after the 1110ptr = &x value does, leading to the undesirable result above. The 1111final effect is that even though the two loads really are executed in 1112program order, it appears that they aren't. 1113 1114This could not have happened if the local cache had processed the 1115incoming stores in FIFO order. By contrast, other architectures 1116maintain at least the appearance of FIFO order. 1117 1118In practice, this difficulty is solved by inserting a special fence 1119between P1's two loads when the kernel is compiled for the Alpha 1120architecture. In fact, as of version 4.15, the kernel automatically 1121adds this fence (called smp_read_barrier_depends() and defined as 1122nothing at all on non-Alpha builds) after every READ_ONCE() and atomic 1123load. The effect of the fence is to cause the CPU not to execute any 1124po-later instructions until after the local cache has finished 1125processing all the stores it has already received. Thus, if the code 1126was changed to: 1127 1128 P1() 1129 { 1130 int *r1; 1131 int r2; 1132 1133 r1 = READ_ONCE(ptr); 1134 r2 = READ_ONCE(*r1); 1135 } 1136 1137then we would never get r1 = &x and r2 = 0. By the time P1 executed 1138its second load, the x = 1 store would already be fully processed by 1139the local cache and available for satisfying the read request. Thus 1140we have yet another reason why shared data should always be read with 1141READ_ONCE() or another synchronization primitive rather than accessed 1142directly. 1143 1144The LKMM requires that smp_rmb(), acquire fences, and strong fences 1145share this property with smp_read_barrier_depends(): They do not allow 1146the CPU to execute any po-later instructions (or po-later loads in the 1147case of smp_rmb()) until all outstanding stores have been processed by 1148the local cache. In the case of a strong fence, the CPU first has to 1149wait for all of its po-earlier stores to propagate to every other CPU 1150in the system; then it has to wait for the local cache to process all 1151the stores received as of that time -- not just the stores received 1152when the strong fence began. 1153 1154And of course, none of this matters for any architecture other than 1155Alpha. 1156 1157 1158THE HAPPENS-BEFORE RELATION: hb 1159------------------------------- 1160 1161The happens-before relation (hb) links memory accesses that have to 1162execute in a certain order. hb includes the ppo relation and two 1163others, one of which is rfe. 1164 1165W ->rfe R implies that W and R are on different CPUs. It also means 1166that W's store must have propagated to R's CPU before R executed; 1167otherwise R could not have read the value stored by W. Therefore W 1168must have executed before R, and so we have W ->hb R. 1169 1170The equivalent fact need not hold if W ->rfi R (i.e., W and R are on 1171the same CPU). As we have already seen, the operational model allows 1172W's value to be forwarded to R in such cases, meaning that R may well 1173execute before W does. 1174 1175It's important to understand that neither coe nor fre is included in 1176hb, despite their similarities to rfe. For example, suppose we have 1177W ->coe W'. This means that W and W' are stores to the same location, 1178they execute on different CPUs, and W comes before W' in the coherence 1179order (i.e., W' overwrites W). Nevertheless, it is possible for W' to 1180execute before W, because the decision as to which store overwrites 1181the other is made later by the memory subsystem. When the stores are 1182nearly simultaneous, either one can come out on top. Similarly, 1183R ->fre W means that W overwrites the value which R reads, but it 1184doesn't mean that W has to execute after R. All that's necessary is 1185for the memory subsystem not to propagate W to R's CPU until after R 1186has executed, which is possible if W executes shortly before R. 1187 1188The third relation included in hb is like ppo, in that it only links 1189events that are on the same CPU. However it is more difficult to 1190explain, because it arises only indirectly from the requirement of 1191cache coherence. The relation is called prop, and it links two events 1192on CPU C in situations where a store from some other CPU comes after 1193the first event in the coherence order and propagates to C before the 1194second event executes. 1195 1196This is best explained with some examples. The simplest case looks 1197like this: 1198 1199 int x; 1200 1201 P0() 1202 { 1203 int r1; 1204 1205 WRITE_ONCE(x, 1); 1206 r1 = READ_ONCE(x); 1207 } 1208 1209 P1() 1210 { 1211 WRITE_ONCE(x, 8); 1212 } 1213 1214If r1 = 8 at the end then P0's accesses must have executed in program 1215order. We can deduce this from the operational model; if P0's load 1216had executed before its store then the value of the store would have 1217been forwarded to the load, so r1 would have ended up equal to 1, not 12188. In this case there is a prop link from P0's write event to its read 1219event, because P1's store came after P0's store in x's coherence 1220order, and P1's store propagated to P0 before P0's load executed. 1221 1222An equally simple case involves two loads of the same location that 1223read from different stores: 1224 1225 int x = 0; 1226 1227 P0() 1228 { 1229 int r1, r2; 1230 1231 r1 = READ_ONCE(x); 1232 r2 = READ_ONCE(x); 1233 } 1234 1235 P1() 1236 { 1237 WRITE_ONCE(x, 9); 1238 } 1239 1240If r1 = 0 and r2 = 9 at the end then P0's accesses must have executed 1241in program order. If the second load had executed before the first 1242then the x = 9 store must have been propagated to P0 before the first 1243load executed, and so r1 would have been 9 rather than 0. In this 1244case there is a prop link from P0's first read event to its second, 1245because P1's store overwrote the value read by P0's first load, and 1246P1's store propagated to P0 before P0's second load executed. 1247 1248Less trivial examples of prop all involve fences. Unlike the simple 1249examples above, they can require that some instructions are executed 1250out of program order. This next one should look familiar: 1251 1252 int buf = 0, flag = 0; 1253 1254 P0() 1255 { 1256 WRITE_ONCE(buf, 1); 1257 smp_wmb(); 1258 WRITE_ONCE(flag, 1); 1259 } 1260 1261 P1() 1262 { 1263 int r1; 1264 int r2; 1265 1266 r1 = READ_ONCE(flag); 1267 r2 = READ_ONCE(buf); 1268 } 1269 1270This is the MP pattern again, with an smp_wmb() fence between the two 1271stores. If r1 = 1 and r2 = 0 at the end then there is a prop link 1272from P1's second load to its first (backwards!). The reason is 1273similar to the previous examples: The value P1 loads from buf gets 1274overwritten by P0's store to buf, the fence guarantees that the store 1275to buf will propagate to P1 before the store to flag does, and the 1276store to flag propagates to P1 before P1 reads flag. 1277 1278The prop link says that in order to obtain the r1 = 1, r2 = 0 result, 1279P1 must execute its second load before the first. Indeed, if the load 1280from flag were executed first, then the buf = 1 store would already 1281have propagated to P1 by the time P1's load from buf executed, so r2 1282would have been 1 at the end, not 0. (The reasoning holds even for 1283Alpha, although the details are more complicated and we will not go 1284into them.) 1285 1286But what if we put an smp_rmb() fence between P1's loads? The fence 1287would force the two loads to be executed in program order, and it 1288would generate a cycle in the hb relation: The fence would create a ppo 1289link (hence an hb link) from the first load to the second, and the 1290prop relation would give an hb link from the second load to the first. 1291Since an instruction can't execute before itself, we are forced to 1292conclude that if an smp_rmb() fence is added, the r1 = 1, r2 = 0 1293outcome is impossible -- as it should be. 1294 1295The formal definition of the prop relation involves a coe or fre link, 1296followed by an arbitrary number of cumul-fence links, ending with an 1297rfe link. You can concoct more exotic examples, containing more than 1298one fence, although this quickly leads to diminishing returns in terms 1299of complexity. For instance, here's an example containing a coe link 1300followed by two cumul-fences and an rfe link, utilizing the fact that 1301release fences are A-cumulative: 1302 1303 int x, y, z; 1304 1305 P0() 1306 { 1307 int r0; 1308 1309 WRITE_ONCE(x, 1); 1310 r0 = READ_ONCE(z); 1311 } 1312 1313 P1() 1314 { 1315 WRITE_ONCE(x, 2); 1316 smp_wmb(); 1317 WRITE_ONCE(y, 1); 1318 } 1319 1320 P2() 1321 { 1322 int r2; 1323 1324 r2 = READ_ONCE(y); 1325 smp_store_release(&z, 1); 1326 } 1327 1328If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop 1329link from P0's store to its load. This is because P0's store gets 1330overwritten by P1's store since x = 2 at the end (a coe link), the 1331smp_wmb() ensures that P1's store to x propagates to P2 before the 1332store to y does (the first cumul-fence), the store to y propagates to P2 1333before P2's load and store execute, P2's smp_store_release() 1334guarantees that the stores to x and y both propagate to P0 before the 1335store to z does (the second cumul-fence), and P0's load executes after the 1336store to z has propagated to P0 (an rfe link). 1337 1338In summary, the fact that the hb relation links memory access events 1339in the order they execute means that it must not have cycles. This 1340requirement is the content of the LKMM's "happens-before" axiom. 1341 1342The LKMM defines yet another relation connected to times of 1343instruction execution, but it is not included in hb. It relies on the 1344particular properties of strong fences, which we cover in the next 1345section. 1346 1347 1348THE PROPAGATES-BEFORE RELATION: pb 1349---------------------------------- 1350 1351The propagates-before (pb) relation capitalizes on the special 1352features of strong fences. It links two events E and F whenever some 1353store is coherence-later than E and propagates to every CPU and to RAM 1354before F executes. The formal definition requires that E be linked to 1355F via a coe or fre link, an arbitrary number of cumul-fences, an 1356optional rfe link, a strong fence, and an arbitrary number of hb 1357links. Let's see how this definition works out. 1358 1359Consider first the case where E is a store (implying that the sequence 1360of links begins with coe). Then there are events W, X, Y, and Z such 1361that: 1362 1363 E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F, 1364 1365where the * suffix indicates an arbitrary number of links of the 1366specified type, and the ? suffix indicates the link is optional (Y may 1367be equal to X). Because of the cumul-fence links, we know that W will 1368propagate to Y's CPU before X does, hence before Y executes and hence 1369before the strong fence executes. Because this fence is strong, we 1370know that W will propagate to every CPU and to RAM before Z executes. 1371And because of the hb links, we know that Z will execute before F. 1372Thus W, which comes later than E in the coherence order, will 1373propagate to every CPU and to RAM before F executes. 1374 1375The case where E is a load is exactly the same, except that the first 1376link in the sequence is fre instead of coe. 1377 1378The existence of a pb link from E to F implies that E must execute 1379before F. To see why, suppose that F executed first. Then W would 1380have propagated to E's CPU before E executed. If E was a store, the 1381memory subsystem would then be forced to make E come after W in the 1382coherence order, contradicting the fact that E ->coe W. If E was a 1383load, the memory subsystem would then be forced to satisfy E's read 1384request with the value stored by W or an even later store, 1385contradicting the fact that E ->fre W. 1386 1387A good example illustrating how pb works is the SB pattern with strong 1388fences: 1389 1390 int x = 0, y = 0; 1391 1392 P0() 1393 { 1394 int r0; 1395 1396 WRITE_ONCE(x, 1); 1397 smp_mb(); 1398 r0 = READ_ONCE(y); 1399 } 1400 1401 P1() 1402 { 1403 int r1; 1404 1405 WRITE_ONCE(y, 1); 1406 smp_mb(); 1407 r1 = READ_ONCE(x); 1408 } 1409 1410If r0 = 0 at the end then there is a pb link from P0's load to P1's 1411load: an fre link from P0's load to P1's store (which overwrites the 1412value read by P0), and a strong fence between P1's store and its load. 1413In this example, the sequences of cumul-fence and hb links are empty. 1414Note that this pb link is not included in hb as an instance of prop, 1415because it does not start and end on the same CPU. 1416 1417Similarly, if r1 = 0 at the end then there is a pb link from P1's load 1418to P0's. This means that if both r1 and r2 were 0 there would be a 1419cycle in pb, which is not possible since an instruction cannot execute 1420before itself. Thus, adding smp_mb() fences to the SB pattern 1421prevents the r0 = 0, r1 = 0 outcome. 1422 1423In summary, the fact that the pb relation links events in the order 1424they execute means that it cannot have cycles. This requirement is 1425the content of the LKMM's "propagation" axiom. 1426 1427 1428RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-fence, and rb 1429------------------------------------------------------------- 1430 1431RCU (Read-Copy-Update) is a powerful synchronization mechanism. It 1432rests on two concepts: grace periods and read-side critical sections. 1433 1434A grace period is the span of time occupied by a call to 1435synchronize_rcu(). A read-side critical section (or just critical 1436section, for short) is a region of code delimited by rcu_read_lock() 1437at the start and rcu_read_unlock() at the end. Critical sections can 1438be nested, although we won't make use of this fact. 1439 1440As far as memory models are concerned, RCU's main feature is its 1441Grace-Period Guarantee, which states that a critical section can never 1442span a full grace period. In more detail, the Guarantee says: 1443 1444 For any critical section C and any grace period G, at least 1445 one of the following statements must hold: 1446 1447(1) C ends before G does, and in addition, every store that 1448 propagates to C's CPU before the end of C must propagate to 1449 every CPU before G ends. 1450 1451(2) G starts before C does, and in addition, every store that 1452 propagates to G's CPU before the start of G must propagate 1453 to every CPU before C starts. 1454 1455In particular, it is not possible for a critical section to both start 1456before and end after a grace period. 1457 1458Here is a simple example of RCU in action: 1459 1460 int x, y; 1461 1462 P0() 1463 { 1464 rcu_read_lock(); 1465 WRITE_ONCE(x, 1); 1466 WRITE_ONCE(y, 1); 1467 rcu_read_unlock(); 1468 } 1469 1470 P1() 1471 { 1472 int r1, r2; 1473 1474 r1 = READ_ONCE(x); 1475 synchronize_rcu(); 1476 r2 = READ_ONCE(y); 1477 } 1478 1479The Grace Period Guarantee tells us that when this code runs, it will 1480never end with r1 = 1 and r2 = 0. The reasoning is as follows. r1 = 1 1481means that P0's store to x propagated to P1 before P1 called 1482synchronize_rcu(), so P0's critical section must have started before 1483P1's grace period, contrary to part (2) of the Guarantee. On the 1484other hand, r2 = 0 means that P0's store to y, which occurs before the 1485end of the critical section, did not propagate to P1 before the end of 1486the grace period, contrary to part (1). Together the results violate 1487the Guarantee. 1488 1489In the kernel's implementations of RCU, the requirements for stores 1490to propagate to every CPU are fulfilled by placing strong fences at 1491suitable places in the RCU-related code. Thus, if a critical section 1492starts before a grace period does then the critical section's CPU will 1493execute an smp_mb() fence after the end of the critical section and 1494some time before the grace period's synchronize_rcu() call returns. 1495And if a critical section ends after a grace period does then the 1496synchronize_rcu() routine will execute an smp_mb() fence at its start 1497and some time before the critical section's opening rcu_read_lock() 1498executes. 1499 1500What exactly do we mean by saying that a critical section "starts 1501before" or "ends after" a grace period? Some aspects of the meaning 1502are pretty obvious, as in the example above, but the details aren't 1503entirely clear. The LKMM formalizes this notion by means of the 1504rcu-link relation. rcu-link encompasses a very general notion of 1505"before": If E and F are RCU fence events (i.e., rcu_read_lock(), 1506rcu_read_unlock(), or synchronize_rcu()) then among other things, 1507E ->rcu-link F includes cases where E is po-before some memory-access 1508event X, F is po-after some memory-access event Y, and we have any of 1509X ->rfe Y, X ->co Y, or X ->fr Y. 1510 1511The formal definition of the rcu-link relation is more than a little 1512obscure, and we won't give it here. It is closely related to the pb 1513relation, and the details don't matter unless you want to comb through 1514a somewhat lengthy formal proof. Pretty much all you need to know 1515about rcu-link is the information in the preceding paragraph. 1516 1517The LKMM also defines the rcu-gp and rcu-rscsi relations. They bring 1518grace periods and read-side critical sections into the picture, in the 1519following way: 1520 1521 E ->rcu-gp F means that E and F are in fact the same event, 1522 and that event is a synchronize_rcu() fence (i.e., a grace 1523 period). 1524 1525 E ->rcu-rscsi F means that E and F are the rcu_read_unlock() 1526 and rcu_read_lock() fence events delimiting some read-side 1527 critical section. (The 'i' at the end of the name emphasizes 1528 that this relation is "inverted": It links the end of the 1529 critical section to the start.) 1530 1531If we think of the rcu-link relation as standing for an extended 1532"before", then X ->rcu-gp Y ->rcu-link Z roughly says that X is a 1533grace period which ends before Z begins. (In fact it covers more than 1534this, because it also includes cases where some store propagates to 1535Z's CPU before Z begins but doesn't propagate to some other CPU until 1536after X ends.) Similarly, X ->rcu-rscsi Y ->rcu-link Z says that X is 1537the end of a critical section which starts before Z begins. 1538 1539The LKMM goes on to define the rcu-fence relation as a sequence of 1540rcu-gp and rcu-rscsi links separated by rcu-link links, in which the 1541number of rcu-gp links is >= the number of rcu-rscsi links. For 1542example: 1543 1544 X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V 1545 1546would imply that X ->rcu-fence V, because this sequence contains two 1547rcu-gp links and one rcu-rscsi link. (It also implies that 1548X ->rcu-fence T and Z ->rcu-fence V.) On the other hand: 1549 1550 X ->rcu-rscsi Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V 1551 1552does not imply X ->rcu-fence V, because the sequence contains only 1553one rcu-gp link but two rcu-rscsi links. 1554 1555The rcu-fence relation is important because the Grace Period Guarantee 1556means that rcu-fence acts kind of like a strong fence. In particular, 1557E ->rcu-fence F implies not only that E begins before F ends, but also 1558that any write po-before E will propagate to every CPU before any 1559instruction po-after F can execute. (However, it does not imply that 1560E must execute before F; in fact, each synchronize_rcu() fence event 1561is linked to itself by rcu-fence as a degenerate case.) 1562 1563To prove this in full generality requires some intellectual effort. 1564We'll consider just a very simple case: 1565 1566 G ->rcu-gp W ->rcu-link Z ->rcu-rscsi F. 1567 1568This formula means that G and W are the same event (a grace period), 1569and there are events X, Y and a read-side critical section C such that: 1570 1571 1. G = W is po-before or equal to X; 1572 1573 2. X comes "before" Y in some sense (including rfe, co and fr); 1574 1575 2. Y is po-before Z; 1576 1577 4. Z is the rcu_read_unlock() event marking the end of C; 1578 1579 5. F is the rcu_read_lock() event marking the start of C. 1580 1581From 1 - 4 we deduce that the grace period G ends before the critical 1582section C. Then part (2) of the Grace Period Guarantee says not only 1583that G starts before C does, but also that any write which executes on 1584G's CPU before G starts must propagate to every CPU before C starts. 1585In particular, the write propagates to every CPU before F finishes 1586executing and hence before any instruction po-after F can execute. 1587This sort of reasoning can be extended to handle all the situations 1588covered by rcu-fence. 1589 1590Finally, the LKMM defines the RCU-before (rb) relation in terms of 1591rcu-fence. This is done in essentially the same way as the pb 1592relation was defined in terms of strong-fence. We will omit the 1593details; the end result is that E ->rb F implies E must execute 1594before F, just as E ->pb F does (and for much the same reasons). 1595 1596Putting this all together, the LKMM expresses the Grace Period 1597Guarantee by requiring that the rb relation does not contain a cycle. 1598Equivalently, this "rcu" axiom requires that there are no events E 1599and F with E ->rcu-link F ->rcu-fence E. Or to put it a third way, 1600the axiom requires that there are no cycles consisting of rcu-gp and 1601rcu-rscsi alternating with rcu-link, where the number of rcu-gp links 1602is >= the number of rcu-rscsi links. 1603 1604Justifying the axiom isn't easy, but it is in fact a valid 1605formalization of the Grace Period Guarantee. We won't attempt to go 1606through the detailed argument, but the following analysis gives a 1607taste of what is involved. Suppose both parts of the Guarantee are 1608violated: A critical section starts before a grace period, and some 1609store propagates to the critical section's CPU before the end of the 1610critical section but doesn't propagate to some other CPU until after 1611the end of the grace period. 1612 1613Putting symbols to these ideas, let L and U be the rcu_read_lock() and 1614rcu_read_unlock() fence events delimiting the critical section in 1615question, and let S be the synchronize_rcu() fence event for the grace 1616period. Saying that the critical section starts before S means there 1617are events Q and R where Q is po-after L (which marks the start of the 1618critical section), Q is "before" R in the sense used by the rcu-link 1619relation, and R is po-before the grace period S. Thus we have: 1620 1621 L ->rcu-link S. 1622 1623Let W be the store mentioned above, let Y come before the end of the 1624critical section and witness that W propagates to the critical 1625section's CPU by reading from W, and let Z on some arbitrary CPU be a 1626witness that W has not propagated to that CPU, where Z happens after 1627some event X which is po-after S. Symbolically, this amounts to: 1628 1629 S ->po X ->hb* Z ->fr W ->rf Y ->po U. 1630 1631The fr link from Z to W indicates that W has not propagated to Z's CPU 1632at the time that Z executes. From this, it can be shown (see the 1633discussion of the rcu-link relation earlier) that S and U are related 1634by rcu-link: 1635 1636 S ->rcu-link U. 1637 1638Since S is a grace period we have S ->rcu-gp S, and since L and U are 1639the start and end of the critical section C we have U ->rcu-rscsi L. 1640From this we obtain: 1641 1642 S ->rcu-gp S ->rcu-link U ->rcu-rscsi L ->rcu-link S, 1643 1644a forbidden cycle. Thus the "rcu" axiom rules out this violation of 1645the Grace Period Guarantee. 1646 1647For something a little more down-to-earth, let's see how the axiom 1648works out in practice. Consider the RCU code example from above, this 1649time with statement labels added: 1650 1651 int x, y; 1652 1653 P0() 1654 { 1655 L: rcu_read_lock(); 1656 X: WRITE_ONCE(x, 1); 1657 Y: WRITE_ONCE(y, 1); 1658 U: rcu_read_unlock(); 1659 } 1660 1661 P1() 1662 { 1663 int r1, r2; 1664 1665 Z: r1 = READ_ONCE(x); 1666 S: synchronize_rcu(); 1667 W: r2 = READ_ONCE(y); 1668 } 1669 1670 1671If r2 = 0 at the end then P0's store at Y overwrites the value that 1672P1's load at W reads from, so we have W ->fre Y. Since S ->po W and 1673also Y ->po U, we get S ->rcu-link U. In addition, S ->rcu-gp S 1674because S is a grace period. 1675 1676If r1 = 1 at the end then P1's load at Z reads from P0's store at X, 1677so we have X ->rfe Z. Together with L ->po X and Z ->po S, this 1678yields L ->rcu-link S. And since L and U are the start and end of a 1679critical section, we have U ->rcu-rscsi L. 1680 1681Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S ->rcu-link U is a 1682forbidden cycle, violating the "rcu" axiom. Hence the outcome is not 1683allowed by the LKMM, as we would expect. 1684 1685For contrast, let's see what can happen in a more complicated example: 1686 1687 int x, y, z; 1688 1689 P0() 1690 { 1691 int r0; 1692 1693 L0: rcu_read_lock(); 1694 r0 = READ_ONCE(x); 1695 WRITE_ONCE(y, 1); 1696 U0: rcu_read_unlock(); 1697 } 1698 1699 P1() 1700 { 1701 int r1; 1702 1703 r1 = READ_ONCE(y); 1704 S1: synchronize_rcu(); 1705 WRITE_ONCE(z, 1); 1706 } 1707 1708 P2() 1709 { 1710 int r2; 1711 1712 L2: rcu_read_lock(); 1713 r2 = READ_ONCE(z); 1714 WRITE_ONCE(x, 1); 1715 U2: rcu_read_unlock(); 1716 } 1717 1718If r0 = r1 = r2 = 1 at the end, then similar reasoning to before shows 1719that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp S1 ->rcu-link U2 ->rcu-rscsi 1720L2 ->rcu-link U0. However this cycle is not forbidden, because the 1721sequence of relations contains fewer instances of rcu-gp (one) than of 1722rcu-rscsi (two). Consequently the outcome is allowed by the LKMM. 1723The following instruction timing diagram shows how it might actually 1724occur: 1725 1726P0 P1 P2 1727-------------------- -------------------- -------------------- 1728rcu_read_lock() 1729WRITE_ONCE(y, 1) 1730 r1 = READ_ONCE(y) 1731 synchronize_rcu() starts 1732 . rcu_read_lock() 1733 . WRITE_ONCE(x, 1) 1734r0 = READ_ONCE(x) . 1735rcu_read_unlock() . 1736 synchronize_rcu() ends 1737 WRITE_ONCE(z, 1) 1738 r2 = READ_ONCE(z) 1739 rcu_read_unlock() 1740 1741This requires P0 and P2 to execute their loads and stores out of 1742program order, but of course they are allowed to do so. And as you 1743can see, the Grace Period Guarantee is not violated: The critical 1744section in P0 both starts before P1's grace period does and ends 1745before it does, and the critical section in P2 both starts after P1's 1746grace period does and ends after it does. 1747 1748Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in 1749addition to normal RCU. The ideas involved are much the same as 1750above, with new relations srcu-gp and srcu-rscsi added to represent 1751SRCU grace periods and read-side critical sections. There is a 1752restriction on the srcu-gp and srcu-rscsi links that can appear in an 1753rcu-fence sequence (the srcu-rscsi links must be paired with srcu-gp 1754links having the same SRCU domain with proper nesting); the details 1755are relatively unimportant. 1756 1757 1758LOCKING 1759------- 1760 1761The LKMM includes locking. In fact, there is special code for locking 1762in the formal model, added in order to make tools run faster. 1763However, this special code is intended to be more or less equivalent 1764to concepts we have already covered. A spinlock_t variable is treated 1765the same as an int, and spin_lock(&s) is treated almost the same as: 1766 1767 while (cmpxchg_acquire(&s, 0, 1) != 0) 1768 cpu_relax(); 1769 1770This waits until s is equal to 0 and then atomically sets it to 1, 1771and the read part of the cmpxchg operation acts as an acquire fence. 1772An alternate way to express the same thing would be: 1773 1774 r = xchg_acquire(&s, 1); 1775 1776along with a requirement that at the end, r = 0. Similarly, 1777spin_trylock(&s) is treated almost the same as: 1778 1779 return !cmpxchg_acquire(&s, 0, 1); 1780 1781which atomically sets s to 1 if it is currently equal to 0 and returns 1782true if it succeeds (the read part of the cmpxchg operation acts as an 1783acquire fence only if the operation is successful). spin_unlock(&s) 1784is treated almost the same as: 1785 1786 smp_store_release(&s, 0); 1787 1788The "almost" qualifiers above need some explanation. In the LKMM, the 1789store-release in a spin_unlock() and the load-acquire which forms the 1790first half of the atomic rmw update in a spin_lock() or a successful 1791spin_trylock() -- we can call these things lock-releases and 1792lock-acquires -- have two properties beyond those of ordinary releases 1793and acquires. 1794 1795First, when a lock-acquire reads from a lock-release, the LKMM 1796requires that every instruction po-before the lock-release must 1797execute before any instruction po-after the lock-acquire. This would 1798naturally hold if the release and acquire operations were on different 1799CPUs, but the LKMM says it holds even when they are on the same CPU. 1800For example: 1801 1802 int x, y; 1803 spinlock_t s; 1804 1805 P0() 1806 { 1807 int r1, r2; 1808 1809 spin_lock(&s); 1810 r1 = READ_ONCE(x); 1811 spin_unlock(&s); 1812 spin_lock(&s); 1813 r2 = READ_ONCE(y); 1814 spin_unlock(&s); 1815 } 1816 1817 P1() 1818 { 1819 WRITE_ONCE(y, 1); 1820 smp_wmb(); 1821 WRITE_ONCE(x, 1); 1822 } 1823 1824Here the second spin_lock() reads from the first spin_unlock(), and 1825therefore the load of x must execute before the load of y. Thus we 1826cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the 1827MP pattern). 1828 1829This requirement does not apply to ordinary release and acquire 1830fences, only to lock-related operations. For instance, suppose P0() 1831in the example had been written as: 1832 1833 P0() 1834 { 1835 int r1, r2, r3; 1836 1837 r1 = READ_ONCE(x); 1838 smp_store_release(&s, 1); 1839 r3 = smp_load_acquire(&s); 1840 r2 = READ_ONCE(y); 1841 } 1842 1843Then the CPU would be allowed to forward the s = 1 value from the 1844smp_store_release() to the smp_load_acquire(), executing the 1845instructions in the following order: 1846 1847 r3 = smp_load_acquire(&s); // Obtains r3 = 1 1848 r2 = READ_ONCE(y); 1849 r1 = READ_ONCE(x); 1850 smp_store_release(&s, 1); // Value is forwarded 1851 1852and thus it could load y before x, obtaining r2 = 0 and r1 = 1. 1853 1854Second, when a lock-acquire reads from a lock-release, and some other 1855stores W and W' occur po-before the lock-release and po-after the 1856lock-acquire respectively, the LKMM requires that W must propagate to 1857each CPU before W' does. For example, consider: 1858 1859 int x, y; 1860 spinlock_t x; 1861 1862 P0() 1863 { 1864 spin_lock(&s); 1865 WRITE_ONCE(x, 1); 1866 spin_unlock(&s); 1867 } 1868 1869 P1() 1870 { 1871 int r1; 1872 1873 spin_lock(&s); 1874 r1 = READ_ONCE(x); 1875 WRITE_ONCE(y, 1); 1876 spin_unlock(&s); 1877 } 1878 1879 P2() 1880 { 1881 int r2, r3; 1882 1883 r2 = READ_ONCE(y); 1884 smp_rmb(); 1885 r3 = READ_ONCE(x); 1886 } 1887 1888If r1 = 1 at the end then the spin_lock() in P1 must have read from 1889the spin_unlock() in P0. Hence the store to x must propagate to P2 1890before the store to y does, so we cannot have r2 = 1 and r3 = 0. 1891 1892These two special requirements for lock-release and lock-acquire do 1893not arise from the operational model. Nevertheless, kernel developers 1894have come to expect and rely on them because they do hold on all 1895architectures supported by the Linux kernel, albeit for various 1896differing reasons. 1897 1898 1899ODDS AND ENDS 1900------------- 1901 1902This section covers material that didn't quite fit anywhere in the 1903earlier sections. 1904 1905The descriptions in this document don't always match the formal 1906version of the LKMM exactly. For example, the actual formal 1907definition of the prop relation makes the initial coe or fre part 1908optional, and it doesn't require the events linked by the relation to 1909be on the same CPU. These differences are very unimportant; indeed, 1910instances where the coe/fre part of prop is missing are of no interest 1911because all the other parts (fences and rfe) are already included in 1912hb anyway, and where the formal model adds prop into hb, it includes 1913an explicit requirement that the events being linked are on the same 1914CPU. 1915 1916Another minor difference has to do with events that are both memory 1917accesses and fences, such as those corresponding to smp_load_acquire() 1918calls. In the formal model, these events aren't actually both reads 1919and fences; rather, they are read events with an annotation marking 1920them as acquires. (Or write events annotated as releases, in the case 1921smp_store_release().) The final effect is the same. 1922 1923Although we didn't mention it above, the instruction execution 1924ordering provided by the smp_rmb() fence doesn't apply to read events 1925that are part of a non-value-returning atomic update. For instance, 1926given: 1927 1928 atomic_inc(&x); 1929 smp_rmb(); 1930 r1 = READ_ONCE(y); 1931 1932it is not guaranteed that the load from y will execute after the 1933update to x. This is because the ARMv8 architecture allows 1934non-value-returning atomic operations effectively to be executed off 1935the CPU. Basically, the CPU tells the memory subsystem to increment 1936x, and then the increment is carried out by the memory hardware with 1937no further involvement from the CPU. Since the CPU doesn't ever read 1938the value of x, there is nothing for the smp_rmb() fence to act on. 1939 1940The LKMM defines a few extra synchronization operations in terms of 1941things we have already covered. In particular, rcu_dereference() is 1942treated as READ_ONCE() and rcu_assign_pointer() is treated as 1943smp_store_release() -- which is basically how the Linux kernel treats 1944them. 1945 1946There are a few oddball fences which need special treatment: 1947smp_mb__before_atomic(), smp_mb__after_atomic(), and 1948smp_mb__after_spinlock(). The LKMM uses fence events with special 1949annotations for them; they act as strong fences just like smp_mb() 1950except for the sets of events that they order. Instead of ordering 1951all po-earlier events against all po-later events, as smp_mb() does, 1952they behave as follows: 1953 1954 smp_mb__before_atomic() orders all po-earlier events against 1955 po-later atomic updates and the events following them; 1956 1957 smp_mb__after_atomic() orders po-earlier atomic updates and 1958 the events preceding them against all po-later events; 1959 1960 smp_mb_after_spinlock() orders po-earlier lock acquisition 1961 events and the events preceding them against all po-later 1962 events. 1963 1964Interestingly, RCU and locking each introduce the possibility of 1965deadlock. When faced with code sequences such as: 1966 1967 spin_lock(&s); 1968 spin_lock(&s); 1969 spin_unlock(&s); 1970 spin_unlock(&s); 1971 1972or: 1973 1974 rcu_read_lock(); 1975 synchronize_rcu(); 1976 rcu_read_unlock(); 1977 1978what does the LKMM have to say? Answer: It says there are no allowed 1979executions at all, which makes sense. But this can also lead to 1980misleading results, because if a piece of code has multiple possible 1981executions, some of which deadlock, the model will report only on the 1982non-deadlocking executions. For example: 1983 1984 int x, y; 1985 1986 P0() 1987 { 1988 int r0; 1989 1990 WRITE_ONCE(x, 1); 1991 r0 = READ_ONCE(y); 1992 } 1993 1994 P1() 1995 { 1996 rcu_read_lock(); 1997 if (READ_ONCE(x) > 0) { 1998 WRITE_ONCE(y, 36); 1999 synchronize_rcu(); 2000 } 2001 rcu_read_unlock(); 2002 } 2003 2004Is it possible to end up with r0 = 36 at the end? The LKMM will tell 2005you it is not, but the model won't mention that this is because P1 2006will self-deadlock in the executions where it stores 36 in y. 2007