Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 1 | Explanation of the Linux-Kernel Memory Consistency Model |
| 2 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 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 |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 30 | 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb |
Alan Stern | 6e89e83 | 2018-09-26 11:29:17 -0700 | [diff] [blame] | 31 | 23. LOCKING |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 32 | 24. PLAIN ACCESSES AND DATA RACES |
| 33 | 25. ODDS AND ENDS |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 34 | |
| 35 | |
| 36 | |
| 37 | INTRODUCTION |
| 38 | ------------ |
| 39 | |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 40 | The Linux-kernel memory consistency model (LKMM) is rather complex and |
| 41 | obscure. This is particularly evident if you read through the |
| 42 | linux-kernel.bell and linux-kernel.cat files that make up the formal |
| 43 | version of the model; they are extremely terse and their meanings are |
| 44 | far from clear. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 45 | |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 46 | This document describes the ideas underlying the LKMM. It is meant |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 47 | for people who want to understand how the model was designed. It does |
| 48 | not go into the details of the code in the .bell and .cat files; |
| 49 | rather, it explains in English what the code expresses symbolically. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 50 | |
| 51 | Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 52 | toward beginners; they explain what memory consistency models are and |
| 53 | the basic notions shared by all such models. People already familiar |
| 54 | with these concepts can skim or skip over them. Sections 6 (EVENTS) |
| 55 | through 12 (THE FROM_READS RELATION) describe the fundamental |
| 56 | relations used in many models. Starting in Section 13 (AN OPERATIONAL |
| 57 | MODEL), the workings of the LKMM itself are covered. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 58 | |
| 59 | Warning: The code examples in this document are not written in the |
| 60 | proper format for litmus tests. They don't include a header line, the |
| 61 | initializations are not enclosed in braces, the global variables are |
| 62 | not passed by pointers, and they don't have an "exists" clause at the |
| 63 | end. Converting them to the right format is left as an exercise for |
| 64 | the reader. |
| 65 | |
| 66 | |
| 67 | BACKGROUND |
| 68 | ---------- |
| 69 | |
| 70 | A memory consistency model (or just memory model, for short) is |
| 71 | something which predicts, given a piece of computer code running on a |
| 72 | particular kind of system, what values may be obtained by the code's |
| 73 | load instructions. The LKMM makes these predictions for code running |
| 74 | as part of the Linux kernel. |
| 75 | |
| 76 | In practice, people tend to use memory models the other way around. |
| 77 | That is, given a piece of code and a collection of values specified |
| 78 | for the loads, the model will predict whether it is possible for the |
| 79 | code to run in such a way that the loads will indeed obtain the |
| 80 | specified values. Of course, this is just another way of expressing |
| 81 | the same idea. |
| 82 | |
| 83 | For code running on a uniprocessor system, the predictions are easy: |
| 84 | Each load instruction must obtain the value written by the most recent |
| 85 | store instruction accessing the same location (we ignore complicating |
| 86 | factors such as DMA and mixed-size accesses.) But on multiprocessor |
| 87 | systems, with multiple CPUs making concurrent accesses to shared |
| 88 | memory locations, things aren't so simple. |
| 89 | |
| 90 | Different architectures have differing memory models, and the Linux |
| 91 | kernel supports a variety of architectures. The LKMM has to be fairly |
| 92 | permissive, in the sense that any behavior allowed by one of these |
| 93 | architectures also has to be allowed by the LKMM. |
| 94 | |
| 95 | |
| 96 | A SIMPLE EXAMPLE |
| 97 | ---------------- |
| 98 | |
| 99 | Here is a simple example to illustrate the basic concepts. Consider |
| 100 | some code running as part of a device driver for an input device. The |
| 101 | driver might contain an interrupt handler which collects data from the |
| 102 | device, stores it in a buffer, and sets a flag to indicate the buffer |
| 103 | is full. Running concurrently on a different CPU might be a part of |
| 104 | the driver code being executed by a process in the midst of a read(2) |
| 105 | system call. This code tests the flag to see whether the buffer is |
| 106 | ready, and if it is, copies the data back to userspace. The buffer |
| 107 | and the flag are memory locations shared between the two CPUs. |
| 108 | |
| 109 | We 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 |
| 111 | assignment 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 | |
| 131 | Here the P0() function represents the interrupt handler running on one |
| 132 | CPU and P1() represents the read() routine running on another. The |
| 133 | value 1 stored in buf represents input data collected from the device. |
| 134 | Thus, P0 stores the data in buf and then sets flag. Meanwhile, P1 |
| 135 | reads flag into the private variable r1, and if it is set, reads the |
| 136 | data from buf into a second private variable r2 for copying to |
| 137 | userspace. (Presumably if flag is not set then the driver will wait a |
| 138 | while and try again.) |
| 139 | |
| 140 | This pattern of memory accesses, where one CPU stores values to two |
| 141 | shared memory locations and another CPU loads from those locations in |
| 142 | the opposite order, is widely known as the "Message Passing" or MP |
| 143 | pattern. It is typical of memory access patterns in the kernel. |
| 144 | |
| 145 | Please note that this example code is a simplified abstraction. Real |
| 146 | buffers are usually larger than a single integer, real device drivers |
| 147 | usually use sleep and wakeup mechanisms rather than polling for I/O |
| 148 | completion, and real code generally doesn't bother to copy values into |
| 149 | private variables before using them. All that is beside the point; |
| 150 | the idea here is simply to illustrate the overall pattern of memory |
| 151 | accesses by the CPUs. |
| 152 | |
| 153 | A memory model will predict what values P1 might obtain for its loads |
| 154 | from flag and buf, or equivalently, what values r1 and r2 might end up |
| 155 | with after the code has finished running. |
| 156 | |
| 157 | Some predictions are trivial. For instance, no sane memory model would |
| 158 | predict that r1 = 42 or r2 = -7, because neither of those values ever |
| 159 | gets stored in flag or buf. |
| 160 | |
| 161 | Some nontrivial predictions are nonetheless quite simple. For |
| 162 | instance, P1 might run entirely before P0 begins, in which case r1 and |
| 163 | r2 will both be 0 at the end. Or P0 might run entirely before P1 |
| 164 | begins, in which case r1 and r2 will both be 1. |
| 165 | |
| 166 | The interesting predictions concern what might happen when the two |
| 167 | routines run concurrently. One possibility is that P1 runs after P0's |
| 168 | store to buf but before the store to flag. In this case, r1 and r2 |
| 169 | will again both be 0. (If P1 had been designed to read buf |
| 170 | unconditionally then we would instead have r1 = 0 and r2 = 1.) |
| 171 | |
| 172 | However, the most interesting possibility is where r1 = 1 and r2 = 0. |
| 173 | If this were to occur it would mean the driver contains a bug, because |
| 174 | incorrect data would get sent to the user: 0 instead of 1. As it |
| 175 | happens, the LKMM does predict this outcome can occur, and the example |
| 176 | driver code shown above is indeed buggy. |
| 177 | |
| 178 | |
| 179 | A SELECTION OF MEMORY MODELS |
| 180 | ---------------------------- |
| 181 | |
| 182 | The first widely cited memory model, and the simplest to understand, |
| 183 | is Sequential Consistency. According to this model, systems behave as |
| 184 | if each CPU executed its instructions in order but with unspecified |
| 185 | timing. In other words, the instructions from the various CPUs get |
| 186 | interleaved in a nondeterministic way, always according to some single |
| 187 | global order that agrees with the order of the instructions in the |
| 188 | program source for each CPU. The model says that the value obtained |
| 189 | by each load is simply the value written by the most recently executed |
| 190 | store to the same memory location, from any CPU. |
| 191 | |
| 192 | For the MP example code shown above, Sequential Consistency predicts |
| 193 | that the undesired result r1 = 1, r2 = 0 cannot occur. The reasoning |
| 194 | goes 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 | |
Alan Stern | 3321ea1 | 2019-10-01 13:39:47 -0400 | [diff] [blame] | 209 | Since an instruction (in this case, P0's store to flag) cannot |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 210 | execute before itself, the specified outcome is impossible. |
| 211 | |
| 212 | However, real computer hardware almost never follows the Sequential |
| 213 | Consistency memory model; doing so would rule out too many valuable |
| 214 | performance optimizations. On ARM and PowerPC architectures, for |
| 215 | instance, the MP example code really does sometimes yield r1 = 1 and |
| 216 | r2 = 0. |
| 217 | |
| 218 | x86 and SPARC follow yet a different memory model: TSO (Total Store |
| 219 | Ordering). This model predicts that the undesired outcome for the MP |
| 220 | pattern cannot occur, but in other respects it differs from Sequential |
| 221 | Consistency. One example is the Store Buffer (SB) pattern, in which |
| 222 | each CPU stores to its own shared location and then loads from the |
| 223 | other 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 | |
| 243 | Sequential Consistency predicts that the outcome r0 = 0, r1 = 0 is |
| 244 | impossible. (Exercise: Figure out the reasoning.) But TSO allows |
| 245 | this outcome to occur, and in fact it does sometimes occur on x86 and |
| 246 | SPARC systems. |
| 247 | |
| 248 | The LKMM was inspired by the memory models followed by PowerPC, ARM, |
| 249 | x86, Alpha, and other architectures. However, it is different in |
| 250 | detail from each of them. |
| 251 | |
| 252 | |
| 253 | ORDERING AND CYCLES |
| 254 | ------------------- |
| 255 | |
| 256 | Memory 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 |
| 258 | be; consider for example the order of instructions in a program's |
| 259 | source code. We saw above that Sequential Consistency makes an |
| 260 | important assumption that CPUs execute instructions in the same order |
| 261 | as those instructions occur in the code, and there are many other |
| 262 | instances of ordering playing central roles in memory models. |
| 263 | |
| 264 | The counterpart to ordering is a cycle. Ordering rules out cycles: |
| 265 | It's not possible to have X ordered before Y, Y ordered before Z, and |
| 266 | Z ordered before X, because this would mean that X is ordered before |
| 267 | itself. The analysis of the MP example under Sequential Consistency |
| 268 | involved 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 | |
| 276 | In short, if a memory model requires certain accesses to be ordered, |
| 277 | and a certain outcome for the loads in a piece of code can happen only |
| 278 | if those accesses would form a cycle, then the memory model predicts |
| 279 | that outcome cannot occur. |
| 280 | |
| 281 | The LKMM is defined largely in terms of cycles, as we will see. |
| 282 | |
| 283 | |
| 284 | EVENTS |
| 285 | ------ |
| 286 | |
| 287 | The LKMM does not work directly with the C statements that make up |
| 288 | kernel source code. Instead it considers the effects of those |
| 289 | statements in a more abstract form, namely, events. The model |
| 290 | includes 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 | |
| 302 | These categories are not exclusive; a read or write event can also be |
| 303 | a fence. This happens with functions like smp_load_acquire() or |
| 304 | spin_lock(). However, no single event can be both a read and a write. |
| 305 | Atomic read-modify-write accesses, such as atomic_inc() or xchg(), |
| 306 | correspond to a pair of events: a read followed by a write. (The |
| 307 | write event is omitted for executions where it doesn't occur, such as |
| 308 | a cmpxchg() where the comparison fails.) |
| 309 | |
| 310 | Other parts of the code, those which do not involve interaction with |
| 311 | shared memory, do not give rise to events. Thus, arithmetic and |
| 312 | logical computations, control-flow instructions, or accesses to |
| 313 | private memory or CPU registers are not of central interest to the |
| 314 | memory model. They only affect the model's predictions indirectly. |
| 315 | For example, an arithmetic computation might determine the value that |
| 316 | gets stored to a shared memory location (or in the case of an array |
| 317 | index, the address where the value gets stored), but the memory model |
| 318 | is concerned only with the store itself -- its value and its address |
| 319 | -- not the computation leading up to it. |
| 320 | |
| 321 | Events in the LKMM can be linked by various relations, which we will |
| 322 | describe in the following sections. The memory model requires certain |
| 323 | of these relations to be orderings, that is, it requires them not to |
| 324 | have any cycles. |
| 325 | |
| 326 | |
| 327 | THE PROGRAM ORDER RELATION: po AND po-loc |
| 328 | ----------------------------------------- |
| 329 | |
| 330 | The most important relation between events is program order (po). You |
| 331 | can think of it as the order in which statements occur in the source |
| 332 | code after branches are taken into account and loops have been |
| 333 | unrolled. A better description might be the order in which |
| 334 | instructions are presented to a CPU's execution unit. Thus, we say |
| 335 | that X is po-before Y (written as "X ->po Y" in formulas) if X occurs |
| 336 | before Y in the instruction stream. |
| 337 | |
| 338 | This is inherently a single-CPU relation; two instructions executing |
| 339 | on different CPUs are never linked by po. Also, it is by definition |
| 340 | an ordering so it cannot have any cycles. |
| 341 | |
| 342 | po-loc is a sub-relation of po. It links two memory accesses when the |
| 343 | first comes before the second in program order and they access the |
| 344 | same memory location (the "-loc" suffix). |
| 345 | |
| 346 | Although this may seem straightforward, there is one subtle aspect to |
| 347 | program order we need to explain. The LKMM was inspired by low-level |
| 348 | architectural memory models which describe the behavior of machine |
| 349 | code, and it retains their outlook to a considerable extent. The |
| 350 | read, write, and fence events used by the model are close in spirit to |
| 351 | individual machine instructions. Nevertheless, the LKMM describes |
| 352 | kernel code written in C, and the mapping from C to machine code can |
| 353 | be extremely complex. |
| 354 | |
| 355 | Optimizing compilers have great freedom in the way they translate |
| 356 | source code to object code. They are allowed to apply transformations |
| 357 | that add memory accesses, eliminate accesses, combine them, split them |
Andrea Parri | 6738ff8 | 2019-06-29 23:10:44 +0200 | [diff] [blame] | 358 | into pieces, or move them around. The use of READ_ONCE(), WRITE_ONCE(), |
| 359 | or one of the other atomic or synchronization primitives prevents a |
| 360 | large number of compiler optimizations. In particular, it is guaranteed |
| 361 | that 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 |
| 363 | change the order in which they occur in the code (within limits imposed |
| 364 | by the C standard), and it will not introduce extraneous accesses. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 365 | |
Andrea Parri | 6738ff8 | 2019-06-29 23:10:44 +0200 | [diff] [blame] | 366 | The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather |
| 367 | than ordinary memory accesses. Thanks to this usage, we can be certain |
| 368 | that in the MP example, the compiler won't reorder P0's write event to |
| 369 | buf and P0's write event to flag, and similarly for the other shared |
| 370 | memory accesses in the examples. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 371 | |
Andrea Parri | 6738ff8 | 2019-06-29 23:10:44 +0200 | [diff] [blame] | 372 | Since private variables are not shared between CPUs, they can be |
| 373 | accessed normally without READ_ONCE() or WRITE_ONCE(). In fact, they |
| 374 | need not even be stored in normal memory at all -- in principle a |
| 375 | private variable could be stored in a CPU register (hence the convention |
| 376 | that these variables have names starting with the letter 'r'). |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 377 | |
| 378 | |
| 379 | A WARNING |
| 380 | --------- |
| 381 | |
| 382 | The protections provided by READ_ONCE(), WRITE_ONCE(), and others are |
| 383 | not perfect; and under some circumstances it is possible for the |
| 384 | compiler to undermine the memory model. Here is an example. Suppose |
| 385 | both branches of an "if" statement store the same value to the same |
| 386 | location: |
| 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 | |
| 397 | For this code, the LKMM predicts that the load from x will always be |
| 398 | executed before either of the stores to y. However, a compiler could |
| 399 | lift the stores out of the conditional, transforming the code into |
| 400 | something 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 | |
| 410 | Given this version of the code, the LKMM would predict that the load |
| 411 | from x could be executed after the store to y. Thus, the memory |
| 412 | model's original prediction could be invalidated by the compiler. |
| 413 | |
| 414 | Another issue arises from the fact that in C, arguments to many |
| 415 | operators and function calls can be evaluated in any order. For |
| 416 | example: |
| 417 | |
| 418 | r1 = f(5) + g(6); |
| 419 | |
| 420 | The object code might call f(5) either before or after g(6); the |
| 421 | memory model cannot assume there is a fixed program order relation |
Alan Stern | 3321ea1 | 2019-10-01 13:39:47 -0400 | [diff] [blame] | 422 | between them. (In fact, if the function calls are inlined then the |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 423 | compiler might even interleave their object code.) |
| 424 | |
| 425 | |
| 426 | DEPENDENCY RELATIONS: data, addr, and ctrl |
| 427 | ------------------------------------------ |
| 428 | |
| 429 | We say that two events are linked by a dependency relation when the |
| 430 | execution of the second event depends in some way on a value obtained |
| 431 | from memory by the first. The first event must be a read, and the |
| 432 | value it obtains must somehow affect what the second event does. |
| 433 | There are three kinds of dependencies: data, address (addr), and |
| 434 | control (ctrl). |
| 435 | |
| 436 | A read and a write event are linked by a data dependency if the value |
| 437 | obtained by the read affects the value stored by the write. As a very |
| 438 | simple example: |
| 439 | |
| 440 | int x, y; |
| 441 | |
| 442 | r1 = READ_ONCE(x); |
| 443 | WRITE_ONCE(y, r1 + 5); |
| 444 | |
| 445 | The value stored by the WRITE_ONCE obviously depends on the value |
| 446 | loaded by the READ_ONCE. Such dependencies can wind through |
| 447 | arbitrarily complicated computations, and a write can depend on the |
| 448 | values of multiple reads. |
| 449 | |
| 450 | A read event and another memory access event are linked by an address |
| 451 | dependency if the value obtained by the read affects the location |
| 452 | accessed by the other event. The second event can be either a read or |
| 453 | a 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 | |
| 461 | Here the location accessed by the second READ_ONCE() depends on the |
| 462 | index value loaded by the first. Pointer indirection also gives rise |
| 463 | to address dependencies, since the address of a location accessed |
| 464 | through a pointer will depend on the value read earlier from that |
| 465 | pointer. |
| 466 | |
| 467 | Finally, a read event and another memory access event are linked by a |
| 468 | control dependency if the value obtained by the read affects whether |
| 469 | the 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 | |
| 477 | Execution of the WRITE_ONCE() is controlled by a conditional expression |
| 478 | which depends on the value obtained by the READ_ONCE(); hence there is |
| 479 | a control dependency from the load to the store. |
| 480 | |
| 481 | It should be pretty obvious that events can only depend on reads that |
| 482 | come earlier in program order. Symbolically, if we have R ->data X, |
| 483 | R ->addr X, or R ->ctrl X (where R is a read event), then we must also |
| 484 | have R ->po X. It wouldn't make sense for a computation to depend |
| 485 | somehow on a value that doesn't get loaded from shared memory until |
| 486 | later in the code! |
| 487 | |
| 488 | |
| 489 | THE READS-FROM RELATION: rf, rfi, and rfe |
| 490 | ----------------------------------------- |
| 491 | |
| 492 | The reads-from relation (rf) links a write event to a read event when |
| 493 | the value loaded by the read is the value that was stored by the |
| 494 | write. In colloquial terms, the load "reads from" the store. We |
| 495 | write W ->rf R to indicate that the load R reads from the store W. We |
| 496 | further distinguish the cases where the load and the store occur on |
| 497 | the same CPU (internal reads-from, or rfi) and where they occur on |
| 498 | different CPUs (external reads-from, or rfe). |
| 499 | |
| 500 | For our purposes, a memory location's initial value is treated as |
| 501 | though it had been written there by an imaginary initial store that |
Alan Stern | 3321ea1 | 2019-10-01 13:39:47 -0400 | [diff] [blame] | 502 | executes on a separate CPU before the main program runs. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 503 | |
| 504 | Usage of the rf relation implicitly assumes that loads will always |
| 505 | read from a single store. It doesn't apply properly in the presence |
| 506 | of load-tearing, where a load obtains some of its bits from one store |
| 507 | and some of them from another store. Fortunately, use of READ_ONCE() |
| 508 | and 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 | |
| 524 | and end up with r1 = 0x1200 (partly from x's initial value and partly |
| 525 | from the value stored by P0). |
| 526 | |
| 527 | On the other hand, load-tearing is unavoidable when mixed-size |
| 528 | accesses 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 | |
| 548 | If r1 = 0x56781234 (little-endian!) at the end, then P1 must have read |
| 549 | from both of P0's stores. It is possible to handle mixed-size and |
| 550 | unaligned accesses in a memory model, but the LKMM currently does not |
| 551 | attempt to do so. It requires all accesses to be properly aligned and |
| 552 | of the location's actual size. |
| 553 | |
| 554 | |
| 555 | CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe |
| 556 | ------------------------------------------------------------------ |
| 557 | |
| 558 | Cache coherence is a general principle requiring that in a |
| 559 | multi-processor system, the CPUs must share a consistent view of the |
| 560 | memory contents. Specifically, it requires that for each location in |
| 561 | shared memory, the stores to that location must form a single global |
| 562 | ordering which all the CPUs agree on (the coherence order), and this |
| 563 | ordering must be consistent with the program order for accesses to |
| 564 | that location. |
| 565 | |
| 566 | To put it another way, for any variable x, the coherence order (co) of |
| 567 | the stores to x is simply the order in which the stores overwrite one |
| 568 | another. The imaginary store which establishes x's initial value |
| 569 | comes first in the coherence order; the store which directly |
| 570 | overwrites the initial value comes second; the store which overwrites |
| 571 | that value comes third, and so on. |
| 572 | |
| 573 | You can think of the coherence order as being the order in which the |
| 574 | stores reach x's location in memory (or if you prefer a more |
| 575 | hardware-centric view, the order in which the stores get written to |
| 576 | x's cache line). We write W ->co W' if W comes before W' in the |
| 577 | coherence order, that is, if the value stored by W gets overwritten, |
| 578 | directly or indirectly, by the value stored by W'. |
| 579 | |
| 580 | Coherence order is required to be consistent with program order. This |
| 581 | requirement 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 | |
| 600 | This is sometimes referred to as sequential consistency per variable, |
| 601 | because it means that the accesses to any single memory location obey |
| 602 | the rules of the Sequential Consistency memory model. (According to |
| 603 | Wikipedia, sequential consistency per variable and cache coherence |
| 604 | mean the same thing except that cache coherence includes an extra |
| 605 | requirement that every store eventually becomes visible to every CPU.) |
| 606 | |
| 607 | Any reasonable memory model will include cache coherence. Indeed, our |
| 608 | expectation of cache coherence is so deeply ingrained that violations |
| 609 | of its requirements look more like hardware bugs than programming |
| 610 | errors: |
| 611 | |
| 612 | int x; |
| 613 | |
| 614 | P0() |
| 615 | { |
| 616 | WRITE_ONCE(x, 17); |
| 617 | WRITE_ONCE(x, 23); |
| 618 | } |
| 619 | |
| 620 | If the final value stored in x after this code ran was 17, you would |
| 621 | think your computer was broken. It would be a violation of the |
| 622 | write-write coherence rule: Since the store of 23 comes later in |
| 623 | program order, it must also come later in x's coherence order and |
| 624 | thus 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 | |
| 636 | If r1 = 666 at the end, this would violate the read-write coherence |
| 637 | rule: The READ_ONCE() load comes before the WRITE_ONCE() store in |
| 638 | program order, so it must not read from that store but rather from one |
| 639 | coming earlier in the coherence order (in this case, x's initial |
| 640 | value). |
| 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 | |
| 657 | If r1 = 5 (reading from P0's store) and r2 = 0 (reading from the |
| 658 | imaginary store which establishes x's initial value) at the end, this |
| 659 | would violate the read-read coherence rule: The r1 load comes before |
| 660 | the r2 load in program order, so it must not read from a store that |
| 661 | comes later in the coherence order. |
| 662 | |
| 663 | (As a minor curiosity, if this code had used normal loads instead of |
| 664 | READ_ONCE() in P1, on Itanium it sometimes could end up with r1 = 5 |
| 665 | and r2 = 0! This results from parallel execution of the operations |
| 666 | encoded in Itanium's Very-Long-Instruction-Word format, and it is yet |
| 667 | another motivation for using READ_ONCE() when accessing shared memory |
| 668 | locations.) |
| 669 | |
| 670 | Just like the po relation, co is inherently an ordering -- it is not |
| 671 | possible for a store to directly or indirectly overwrite itself! And |
| 672 | just like with the rf relation, we distinguish between stores that |
| 673 | occur on the same CPU (internal coherence order, or coi) and stores |
| 674 | that occur on different CPUs (external coherence order, or coe). |
| 675 | |
| 676 | On the other hand, stores to different memory locations are never |
| 677 | related by co, just as instructions on different CPUs are never |
| 678 | related by po. Coherence order is strictly per-location, or if you |
| 679 | prefer, each location has its own independent coherence order. |
| 680 | |
| 681 | |
| 682 | THE FROM-READS RELATION: fr, fri, and fre |
| 683 | ----------------------------------------- |
| 684 | |
| 685 | The from-reads relation (fr) can be a little difficult for people to |
| 686 | grok. It describes the situation where a load reads a value that gets |
| 687 | overwritten by a store. In other words, we have R ->fr W when the |
| 688 | value that R reads is overwritten (directly or indirectly) by W, or |
| 689 | equivalently, when R reads from a store which comes earlier than W in |
| 690 | the coherence order. |
| 691 | |
| 692 | For 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 | |
| 704 | The value loaded from x will be 0 (assuming cache coherence!), and it |
| 705 | gets overwritten by the value 2. Thus there is an fr link from the |
| 706 | READ_ONCE() to the WRITE_ONCE(). If the code contained any later |
| 707 | stores to x, there would also be fr links from the READ_ONCE() to |
| 708 | them. |
| 709 | |
| 710 | As with rf, rfi, and rfe, we subdivide the fr relation into fri (when |
| 711 | the load and the store are on the same CPU) and fre (when they are on |
| 712 | different CPUs). |
| 713 | |
| 714 | Note that the fr relation is determined entirely by the rf and co |
| 715 | relations; it is not independent. Given a read event R and a write |
| 716 | event W for the same location, we will have R ->fr W if and only if |
| 717 | the 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 | |
| 722 | AN OPERATIONAL MODEL |
| 723 | -------------------- |
| 724 | |
| 725 | The LKMM is based on various operational memory models, meaning that |
| 726 | the models arise from an abstract view of how a computer system |
| 727 | operates. Here are the main ideas, as incorporated into the LKMM. |
| 728 | |
| 729 | The system as a whole is divided into the CPUs and a memory subsystem. |
| 730 | The CPUs are responsible for executing instructions (not necessarily |
| 731 | in program order), and they communicate with the memory subsystem. |
| 732 | For the most part, executing an instruction requires a CPU to perform |
| 733 | only internal operations. However, loads, stores, and fences involve |
| 734 | more. |
| 735 | |
| 736 | When CPU C executes a store instruction, it tells the memory subsystem |
| 737 | to store a certain value at a certain location. The memory subsystem |
| 738 | propagates the store to all the other CPUs as well as to RAM. (As a |
| 739 | special case, we say that the store propagates to its own CPU at the |
| 740 | time it is executed.) The memory subsystem also determines where the |
| 741 | store falls in the location's coherence order. In particular, it must |
| 742 | arrange for the store to be co-later than (i.e., to overwrite) any |
| 743 | other store to the same location which has already propagated to CPU C. |
| 744 | |
| 745 | When a CPU executes a load instruction R, it first checks to see |
| 746 | whether there are any as-yet unexecuted store instructions, for the |
| 747 | same location, that come before R in program order. If there are, it |
| 748 | uses the value of the po-latest such store as the value obtained by R, |
| 749 | and we say that the store's value is forwarded to R. Otherwise, the |
| 750 | CPU asks the memory subsystem for the value to load and we say that R |
| 751 | is satisfied from memory. The memory subsystem hands back the value |
| 752 | of the co-latest store to the location in question which has already |
| 753 | propagated to that CPU. |
| 754 | |
| 755 | (In fact, the picture needs to be a little more complicated than this. |
| 756 | CPUs have local caches, and propagating a store to a CPU really means |
| 757 | propagating it to the CPU's local cache. A local cache can take some |
| 758 | time to process the stores that it receives, and a store can't be used |
| 759 | to satisfy one of the CPU's loads until it has been processed. On |
| 760 | most architectures, the local caches process stores in |
| 761 | First-In-First-Out order, and consequently the processing delay |
| 762 | doesn't matter for the memory model. But on Alpha, the local caches |
| 763 | have a partitioned design that results in non-FIFO behavior. We will |
| 764 | discuss this in more detail later.) |
| 765 | |
| 766 | Note that load instructions may be executed speculatively and may be |
| 767 | restarted under certain circumstances. The memory model ignores these |
| 768 | premature executions; we simply say that the load executes at the |
| 769 | final time it is forwarded or satisfied. |
| 770 | |
| 771 | Executing a fence (or memory barrier) instruction doesn't require a |
| 772 | CPU to do anything special other than informing the memory subsystem |
| 773 | about the fence. However, fences do constrain the way CPUs and the |
| 774 | memory subsystem handle other instructions, in two respects. |
| 775 | |
| 776 | First, a fence forces the CPU to execute various instructions in |
| 777 | program order. Exactly which instructions are ordered depends on the |
| 778 | type 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 | |
| 800 | Second, some types of fence affect the way the memory subsystem |
| 801 | propagates stores. When a fence instruction is executed on CPU C: |
| 802 | |
Yauheni Kaliuta | 0fcff17 | 2018-07-16 11:06:04 -0700 | [diff] [blame] | 803 | For each other CPU C', smp_wmb() forces all po-earlier stores |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 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 | |
| 816 | The propagation ordering enforced by release fences and strong fences |
| 817 | affects stores from other CPUs that propagate to CPU C before the |
| 818 | fence is executed, as well as stores that are executed on C before the |
| 819 | fence. We describe this property by saying that release fences and |
| 820 | strong fences are A-cumulative. By contrast, smp_wmb() fences are not |
| 821 | A-cumulative; they only affect the propagation of stores that are |
| 822 | executed on C before the fence (i.e., those which precede the fence in |
| 823 | program order). |
| 824 | |
Alan Stern | bd5c0ba | 2018-03-07 09:27:40 -0800 | [diff] [blame] | 825 | rcu_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 826 | other properties which we discuss later. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 827 | |
| 828 | |
| 829 | PROPAGATION ORDER RELATION: cumul-fence |
| 830 | --------------------------------------- |
| 831 | |
| 832 | The fences which affect propagation order (i.e., strong, release, and |
| 833 | smp_wmb() fences) are collectively referred to as cumul-fences, even |
| 834 | though smp_wmb() isn't A-cumulative. The cumul-fence relation is |
| 835 | defined 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 | |
| 846 | The operational model requires that whenever W and W' are both stores |
| 847 | and W ->cumul-fence W', then W must propagate to any given CPU |
| 848 | before W' does. However, for different CPUs C and C', it does not |
| 849 | require W to propagate to C before W' propagates to C'. |
| 850 | |
| 851 | |
| 852 | DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL |
| 853 | ------------------------------------------------- |
| 854 | |
| 855 | The LKMM is derived from the restrictions imposed by the design |
| 856 | outlined above. These restrictions involve the necessity of |
| 857 | maintaining cache coherence and the fact that a CPU can't operate on a |
| 858 | value before it knows what that value is, among other things. |
| 859 | |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 860 | The formal version of the LKMM is defined by six requirements, or |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 861 | axioms: |
| 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 | |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 880 | Plain-coherence: This requires that plain memory accesses |
| 881 | (those not using READ_ONCE(), WRITE_ONCE(), etc.) must obey |
| 882 | the operational model's rules regarding cache coherence. |
| 883 | |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 884 | The first and second are quite common; they can be found in many |
| 885 | memory models (such as those for C11/C++11). The "happens-before" and |
| 886 | "propagation" axioms have analogs in other memory models as well. The |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 887 | "rcu" and "plain-coherence" axioms are specific to the LKMM. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 888 | |
| 889 | Each of these axioms is discussed below. |
| 890 | |
| 891 | |
| 892 | SEQUENTIAL CONSISTENCY PER VARIABLE |
| 893 | ----------------------------------- |
| 894 | |
| 895 | According to the principle of cache coherence, the stores to any fixed |
| 896 | shared location in memory form a global ordering. We can imagine |
| 897 | inserting the loads from that location into this ordering, by placing |
| 898 | each load between the store that it reads from and the following |
| 899 | store. This leaves the relative positions of loads that read from the |
| 900 | same store unspecified; let's say they are inserted in program order, |
| 901 | first for CPU 0, then CPU 1, etc. |
| 902 | |
| 903 | You can check that the four coherency rules imply that the rf, co, fr, |
| 904 | and po-loc relations agree with this global ordering; in other words, |
| 905 | whenever we have X ->rf Y or X ->co Y or X ->fr Y or X ->po-loc Y, the |
| 906 | X event comes before the Y event in the global ordering. The LKMM's |
| 907 | "coherence" axiom expresses this by requiring the union of these |
| 908 | relations not to have any cycles. This means it must not be possible |
| 909 | to find events |
| 910 | |
| 911 | X0 -> X1 -> X2 -> ... -> Xn -> X0, |
| 912 | |
| 913 | where each of the links is either rf, co, fr, or po-loc. This has to |
| 914 | hold if the accesses to the fixed memory location can be ordered as |
| 915 | cache coherence demands. |
| 916 | |
| 917 | Although it is not obvious, it can be shown that the converse is also |
| 918 | true: This LKMM axiom implies that the four coherency rules are |
| 919 | obeyed. |
| 920 | |
| 921 | |
| 922 | ATOMIC UPDATES: rmw |
| 923 | ------------------- |
| 924 | |
| 925 | What does it mean to say that a read-modify-write (rmw) update, such |
| 926 | as atomic_inc(&x), is atomic? It means that the memory location (x in |
| 927 | this case) does not get altered between the read and the write events |
| 928 | making up the atomic operation. In particular, if two CPUs perform |
| 929 | atomic_inc(&x) concurrently, it must be guaranteed that the final |
| 930 | value of x will be the initial value plus two. We should never have |
| 931 | the following sequence of events: |
| 932 | |
| 933 | CPU 0 loads x obtaining 13; |
| 934 | CPU 1 loads x obtaining 13; |
| 935 | CPU 0 stores 14 to x; |
| 936 | CPU 1 stores 14 to x; |
| 937 | |
| 938 | where the final value of x is wrong (14 rather than 15). |
| 939 | |
| 940 | In this example, CPU 0's increment effectively gets lost because it |
| 941 | occurs in between CPU 1's load and store. To put it another way, the |
| 942 | problem is that the position of CPU 0's store in x's coherence order |
| 943 | is between the store that CPU 1 reads from and the store that CPU 1 |
| 944 | performs. |
| 945 | |
| 946 | The same analysis applies to all atomic update operations. Therefore, |
| 947 | to enforce atomicity the LKMM requires that atomic updates follow this |
| 948 | rule: Whenever R and W are the read and write events composing an |
| 949 | atomic read-modify-write and W' is the write event which R reads from, |
| 950 | there must not be any stores coming between W' and W in the coherence |
| 951 | order. Equivalently, |
| 952 | |
| 953 | (R ->rmw W) implies (there is no X with R ->fr X and X ->co W), |
| 954 | |
| 955 | where the rmw relation links the read and write events making up each |
| 956 | atomic update. This is what the LKMM's "atomic" axiom says. |
| 957 | |
| 958 | |
| 959 | THE PRESERVED PROGRAM ORDER RELATION: ppo |
| 960 | ----------------------------------------- |
| 961 | |
Alan Stern | 3321ea1 | 2019-10-01 13:39:47 -0400 | [diff] [blame] | 962 | There are many situations where a CPU is obliged to execute two |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 963 | instructions in program order. We amalgamate them into the ppo (for |
| 964 | "preserved program order") relation, which links the po-earlier |
| 965 | instruction to the po-later instruction and is thus a sub-relation of |
| 966 | po. |
| 967 | |
| 968 | The operational model already includes a description of one such |
| 969 | situation: Fences are a source of ppo links. Suppose X and Y are |
| 970 | memory accesses with X ->po Y; then the CPU must execute X before Y if |
| 971 | any of the following hold: |
| 972 | |
| 973 | A strong (smp_mb() or synchronize_rcu()) fence occurs between |
| 974 | X and Y; |
| 975 | |
| 976 | X and Y are both stores and an smp_wmb() fence occurs between |
| 977 | them; |
| 978 | |
| 979 | X and Y are both loads and an smp_rmb() fence occurs between |
| 980 | them; |
| 981 | |
| 982 | X is also an acquire fence, such as smp_load_acquire(); |
| 983 | |
| 984 | Y is also a release fence, such as smp_store_release(). |
| 985 | |
| 986 | Another possibility, not mentioned earlier but discussed in the next |
| 987 | section, is: |
| 988 | |
| 989 | X and Y are both loads, X ->addr Y (i.e., there is an address |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 990 | dependency from X to Y), and X is a READ_ONCE() or an atomic |
| 991 | access. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 992 | |
| 993 | Dependencies can also cause instructions to be executed in program |
| 994 | order. This is uncontroversial when the second instruction is a |
| 995 | store; either a data, address, or control dependency from a load R to |
| 996 | a store W will force the CPU to execute R before W. This is very |
| 997 | simply because the CPU cannot tell the memory subsystem about W's |
| 998 | store before it knows what value should be stored (in the case of a |
| 999 | data dependency), what location it should be stored into (in the case |
| 1000 | of an address dependency), or whether the store should actually take |
| 1001 | place (in the case of a control dependency). |
| 1002 | |
| 1003 | Dependencies to load instructions are more problematic. To begin with, |
| 1004 | there is no such thing as a data dependency to a load. Next, a CPU |
| 1005 | has no reason to respect a control dependency to a load, because it |
| 1006 | can always satisfy the second load speculatively before the first, and |
| 1007 | then ignore the result if it turns out that the second load shouldn't |
| 1008 | be executed after all. And lastly, the real difficulties begin when |
| 1009 | we consider address dependencies to loads. |
| 1010 | |
| 1011 | To be fair about it, all Linux-supported architectures do execute |
| 1012 | loads in program order if there is an address dependency between them. |
| 1013 | After all, a CPU cannot ask the memory subsystem to load a value from |
| 1014 | a particular location before it knows what that location is. However, |
| 1015 | the split-cache design used by Alpha can cause it to behave in a way |
| 1016 | that looks as if the loads were executed out of order (see the next |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 1017 | section for more details). The kernel includes a workaround for this |
| 1018 | problem when the loads come from READ_ONCE(), and therefore the LKMM |
| 1019 | includes address dependencies to loads in the ppo relation. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1020 | |
| 1021 | On the other hand, dependencies can indirectly affect the ordering of |
| 1022 | two loads. This happens when there is a dependency from a load to a |
| 1023 | store and a second, po-later load reads from that store: |
| 1024 | |
| 1025 | R ->dep W ->rfi R', |
| 1026 | |
| 1027 | where the dep link can be either an address or a data dependency. In |
| 1028 | this situation we know it is possible for the CPU to execute R' before |
| 1029 | W, because it can forward the value that W will store to R'. But it |
| 1030 | cannot execute R' before R, because it cannot forward the value before |
| 1031 | it knows what that value is, or that W and R' do access the same |
| 1032 | location. However, if there is merely a control dependency between R |
| 1033 | and W then the CPU can speculatively forward W to R' before executing |
| 1034 | R; if the speculation turns out to be wrong then the CPU merely has to |
| 1035 | restart or abandon R'. |
| 1036 | |
| 1037 | (In theory, a CPU might forward a store to a load when it runs across |
| 1038 | an address dependency like this: |
| 1039 | |
| 1040 | r1 = READ_ONCE(ptr); |
| 1041 | WRITE_ONCE(*r1, 17); |
| 1042 | r2 = READ_ONCE(*r1); |
| 1043 | |
| 1044 | because it could tell that the store and the second load access the |
| 1045 | same location even before it knows what the location's address is. |
| 1046 | However, none of the architectures supported by the Linux kernel do |
| 1047 | this.) |
| 1048 | |
| 1049 | Two memory accesses of the same location must always be executed in |
| 1050 | program order if the second access is a store. Thus, if we have |
| 1051 | |
| 1052 | R ->po-loc W |
| 1053 | |
| 1054 | (the po-loc link says that R comes before W in program order and they |
| 1055 | access the same location), the CPU is obliged to execute W after R. |
| 1056 | If it executed W first then the memory subsystem would respond to R's |
| 1057 | read request with the value stored by W (or an even later store), in |
| 1058 | violation of the read-write coherence rule. Similarly, if we had |
| 1059 | |
| 1060 | W ->po-loc W' |
| 1061 | |
| 1062 | and the CPU executed W' before W, then the memory subsystem would put |
| 1063 | W' before W in the coherence order. It would effectively cause W to |
| 1064 | overwrite W', in violation of the write-write coherence rule. |
| 1065 | (Interestingly, an early ARMv8 memory model, now obsolete, proposed |
| 1066 | allowing out-of-order writes like this to occur. The model avoided |
| 1067 | violating the write-write coherence rule by requiring the CPU not to |
| 1068 | send the W write to the memory subsystem at all!) |
| 1069 | |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1070 | |
| 1071 | AND THEN THERE WAS ALPHA |
| 1072 | ------------------------ |
| 1073 | |
| 1074 | As mentioned above, the Alpha architecture is unique in that it does |
| 1075 | not appear to respect address dependencies to loads. This means that |
| 1076 | code such as the following: |
| 1077 | |
| 1078 | int x = 0; |
| 1079 | int y = -1; |
| 1080 | int *ptr = &y; |
| 1081 | |
| 1082 | P0() |
| 1083 | { |
| 1084 | WRITE_ONCE(x, 1); |
| 1085 | smp_wmb(); |
| 1086 | WRITE_ONCE(ptr, &x); |
| 1087 | } |
| 1088 | |
| 1089 | P1() |
| 1090 | { |
| 1091 | int *r1; |
| 1092 | int r2; |
| 1093 | |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 1094 | r1 = ptr; |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1095 | r2 = READ_ONCE(*r1); |
| 1096 | } |
| 1097 | |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 1098 | can malfunction on Alpha systems (notice that P1 uses an ordinary load |
| 1099 | to read ptr instead of READ_ONCE()). It is quite possible that r1 = &x |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1100 | and r2 = 0 at the end, in spite of the address dependency. |
| 1101 | |
| 1102 | At first glance this doesn't seem to make sense. We know that the |
| 1103 | smp_wmb() forces P0's store to x to propagate to P1 before the store |
| 1104 | to ptr does. And since P1 can't execute its second load |
| 1105 | until it knows what location to load from, i.e., after executing its |
| 1106 | first load, the value x = 1 must have propagated to P1 before the |
| 1107 | second load executed. So why doesn't r2 end up equal to 1? |
| 1108 | |
| 1109 | The answer lies in the Alpha's split local caches. Although the two |
| 1110 | stores do reach P1's local cache in the proper order, it can happen |
| 1111 | that the first store is processed by a busy part of the cache while |
| 1112 | the second store is processed by an idle part. As a result, the x = 1 |
| 1113 | value may not become available for P1's CPU to read until after the |
| 1114 | ptr = &x value does, leading to the undesirable result above. The |
| 1115 | final effect is that even though the two loads really are executed in |
| 1116 | program order, it appears that they aren't. |
| 1117 | |
| 1118 | This could not have happened if the local cache had processed the |
Alan Stern | bd5c0ba | 2018-03-07 09:27:40 -0800 | [diff] [blame] | 1119 | incoming stores in FIFO order. By contrast, other architectures |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1120 | maintain at least the appearance of FIFO order. |
| 1121 | |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 1122 | In practice, this difficulty is solved by inserting a special fence |
| 1123 | between P1's two loads when the kernel is compiled for the Alpha |
| 1124 | architecture. In fact, as of version 4.15, the kernel automatically |
Will Deacon | 628fd55 | 2019-11-07 14:44:06 +0000 | [diff] [blame] | 1125 | adds this fence after every READ_ONCE() and atomic load on Alpha. The |
| 1126 | effect of the fence is to cause the CPU not to execute any po-later |
| 1127 | instructions until after the local cache has finished processing all |
| 1128 | the stores it has already received. Thus, if the code was changed to: |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1129 | |
| 1130 | P1() |
| 1131 | { |
| 1132 | int *r1; |
| 1133 | int r2; |
| 1134 | |
| 1135 | r1 = READ_ONCE(ptr); |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1136 | r2 = READ_ONCE(*r1); |
| 1137 | } |
| 1138 | |
| 1139 | then we would never get r1 = &x and r2 = 0. By the time P1 executed |
| 1140 | its second load, the x = 1 store would already be fully processed by |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 1141 | the local cache and available for satisfying the read request. Thus |
| 1142 | we have yet another reason why shared data should always be read with |
| 1143 | READ_ONCE() or another synchronization primitive rather than accessed |
| 1144 | directly. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1145 | |
| 1146 | The LKMM requires that smp_rmb(), acquire fences, and strong fences |
Will Deacon | 628fd55 | 2019-11-07 14:44:06 +0000 | [diff] [blame] | 1147 | share this property: They do not allow the CPU to execute any po-later |
| 1148 | instructions (or po-later loads in the case of smp_rmb()) until all |
| 1149 | outstanding stores have been processed by the local cache. In the |
| 1150 | case of a strong fence, the CPU first has to wait for all of its |
| 1151 | po-earlier stores to propagate to every other CPU in the system; then |
| 1152 | it has to wait for the local cache to process all the stores received |
| 1153 | as of that time -- not just the stores received when the strong fence |
| 1154 | began. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1155 | |
| 1156 | And of course, none of this matters for any architecture other than |
| 1157 | Alpha. |
| 1158 | |
| 1159 | |
| 1160 | THE HAPPENS-BEFORE RELATION: hb |
| 1161 | ------------------------------- |
| 1162 | |
| 1163 | The happens-before relation (hb) links memory accesses that have to |
| 1164 | execute in a certain order. hb includes the ppo relation and two |
| 1165 | others, one of which is rfe. |
| 1166 | |
| 1167 | W ->rfe R implies that W and R are on different CPUs. It also means |
| 1168 | that W's store must have propagated to R's CPU before R executed; |
| 1169 | otherwise R could not have read the value stored by W. Therefore W |
| 1170 | must have executed before R, and so we have W ->hb R. |
| 1171 | |
| 1172 | The equivalent fact need not hold if W ->rfi R (i.e., W and R are on |
| 1173 | the same CPU). As we have already seen, the operational model allows |
| 1174 | W's value to be forwarded to R in such cases, meaning that R may well |
| 1175 | execute before W does. |
| 1176 | |
| 1177 | It's important to understand that neither coe nor fre is included in |
| 1178 | hb, despite their similarities to rfe. For example, suppose we have |
| 1179 | W ->coe W'. This means that W and W' are stores to the same location, |
| 1180 | they execute on different CPUs, and W comes before W' in the coherence |
| 1181 | order (i.e., W' overwrites W). Nevertheless, it is possible for W' to |
| 1182 | execute before W, because the decision as to which store overwrites |
| 1183 | the other is made later by the memory subsystem. When the stores are |
| 1184 | nearly simultaneous, either one can come out on top. Similarly, |
| 1185 | R ->fre W means that W overwrites the value which R reads, but it |
| 1186 | doesn't mean that W has to execute after R. All that's necessary is |
| 1187 | for the memory subsystem not to propagate W to R's CPU until after R |
| 1188 | has executed, which is possible if W executes shortly before R. |
| 1189 | |
| 1190 | The third relation included in hb is like ppo, in that it only links |
| 1191 | events that are on the same CPU. However it is more difficult to |
| 1192 | explain, because it arises only indirectly from the requirement of |
| 1193 | cache coherence. The relation is called prop, and it links two events |
| 1194 | on CPU C in situations where a store from some other CPU comes after |
| 1195 | the first event in the coherence order and propagates to C before the |
| 1196 | second event executes. |
| 1197 | |
| 1198 | This is best explained with some examples. The simplest case looks |
| 1199 | like this: |
| 1200 | |
| 1201 | int x; |
| 1202 | |
| 1203 | P0() |
| 1204 | { |
| 1205 | int r1; |
| 1206 | |
| 1207 | WRITE_ONCE(x, 1); |
| 1208 | r1 = READ_ONCE(x); |
| 1209 | } |
| 1210 | |
| 1211 | P1() |
| 1212 | { |
| 1213 | WRITE_ONCE(x, 8); |
| 1214 | } |
| 1215 | |
| 1216 | If r1 = 8 at the end then P0's accesses must have executed in program |
| 1217 | order. We can deduce this from the operational model; if P0's load |
| 1218 | had executed before its store then the value of the store would have |
| 1219 | been forwarded to the load, so r1 would have ended up equal to 1, not |
| 1220 | 8. In this case there is a prop link from P0's write event to its read |
| 1221 | event, because P1's store came after P0's store in x's coherence |
| 1222 | order, and P1's store propagated to P0 before P0's load executed. |
| 1223 | |
| 1224 | An equally simple case involves two loads of the same location that |
| 1225 | read from different stores: |
| 1226 | |
| 1227 | int x = 0; |
| 1228 | |
| 1229 | P0() |
| 1230 | { |
| 1231 | int r1, r2; |
| 1232 | |
| 1233 | r1 = READ_ONCE(x); |
| 1234 | r2 = READ_ONCE(x); |
| 1235 | } |
| 1236 | |
| 1237 | P1() |
| 1238 | { |
| 1239 | WRITE_ONCE(x, 9); |
| 1240 | } |
| 1241 | |
| 1242 | If r1 = 0 and r2 = 9 at the end then P0's accesses must have executed |
| 1243 | in program order. If the second load had executed before the first |
| 1244 | then the x = 9 store must have been propagated to P0 before the first |
| 1245 | load executed, and so r1 would have been 9 rather than 0. In this |
| 1246 | case there is a prop link from P0's first read event to its second, |
| 1247 | because P1's store overwrote the value read by P0's first load, and |
| 1248 | P1's store propagated to P0 before P0's second load executed. |
| 1249 | |
| 1250 | Less trivial examples of prop all involve fences. Unlike the simple |
| 1251 | examples above, they can require that some instructions are executed |
| 1252 | out of program order. This next one should look familiar: |
| 1253 | |
| 1254 | int buf = 0, flag = 0; |
| 1255 | |
| 1256 | P0() |
| 1257 | { |
| 1258 | WRITE_ONCE(buf, 1); |
| 1259 | smp_wmb(); |
| 1260 | WRITE_ONCE(flag, 1); |
| 1261 | } |
| 1262 | |
| 1263 | P1() |
| 1264 | { |
| 1265 | int r1; |
| 1266 | int r2; |
| 1267 | |
| 1268 | r1 = READ_ONCE(flag); |
| 1269 | r2 = READ_ONCE(buf); |
| 1270 | } |
| 1271 | |
| 1272 | This is the MP pattern again, with an smp_wmb() fence between the two |
| 1273 | stores. If r1 = 1 and r2 = 0 at the end then there is a prop link |
| 1274 | from P1's second load to its first (backwards!). The reason is |
| 1275 | similar to the previous examples: The value P1 loads from buf gets |
| 1276 | overwritten by P0's store to buf, the fence guarantees that the store |
| 1277 | to buf will propagate to P1 before the store to flag does, and the |
| 1278 | store to flag propagates to P1 before P1 reads flag. |
| 1279 | |
| 1280 | The prop link says that in order to obtain the r1 = 1, r2 = 0 result, |
| 1281 | P1 must execute its second load before the first. Indeed, if the load |
| 1282 | from flag were executed first, then the buf = 1 store would already |
| 1283 | have propagated to P1 by the time P1's load from buf executed, so r2 |
| 1284 | would have been 1 at the end, not 0. (The reasoning holds even for |
| 1285 | Alpha, although the details are more complicated and we will not go |
| 1286 | into them.) |
| 1287 | |
| 1288 | But what if we put an smp_rmb() fence between P1's loads? The fence |
| 1289 | would force the two loads to be executed in program order, and it |
| 1290 | would generate a cycle in the hb relation: The fence would create a ppo |
| 1291 | link (hence an hb link) from the first load to the second, and the |
| 1292 | prop relation would give an hb link from the second load to the first. |
| 1293 | Since an instruction can't execute before itself, we are forced to |
| 1294 | conclude that if an smp_rmb() fence is added, the r1 = 1, r2 = 0 |
| 1295 | outcome is impossible -- as it should be. |
| 1296 | |
| 1297 | The formal definition of the prop relation involves a coe or fre link, |
| 1298 | followed by an arbitrary number of cumul-fence links, ending with an |
| 1299 | rfe link. You can concoct more exotic examples, containing more than |
| 1300 | one fence, although this quickly leads to diminishing returns in terms |
| 1301 | of complexity. For instance, here's an example containing a coe link |
Joel Fernandes (Google) | 6240973 | 2019-07-29 08:36:05 -0400 | [diff] [blame] | 1302 | followed by two cumul-fences and an rfe link, utilizing the fact that |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1303 | release fences are A-cumulative: |
| 1304 | |
| 1305 | int x, y, z; |
| 1306 | |
| 1307 | P0() |
| 1308 | { |
| 1309 | int r0; |
| 1310 | |
| 1311 | WRITE_ONCE(x, 1); |
| 1312 | r0 = READ_ONCE(z); |
| 1313 | } |
| 1314 | |
| 1315 | P1() |
| 1316 | { |
| 1317 | WRITE_ONCE(x, 2); |
| 1318 | smp_wmb(); |
| 1319 | WRITE_ONCE(y, 1); |
| 1320 | } |
| 1321 | |
| 1322 | P2() |
| 1323 | { |
| 1324 | int r2; |
| 1325 | |
| 1326 | r2 = READ_ONCE(y); |
| 1327 | smp_store_release(&z, 1); |
| 1328 | } |
| 1329 | |
| 1330 | If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop |
| 1331 | link from P0's store to its load. This is because P0's store gets |
| 1332 | overwritten by P1's store since x = 2 at the end (a coe link), the |
| 1333 | smp_wmb() ensures that P1's store to x propagates to P2 before the |
Joel Fernandes (Google) | 6240973 | 2019-07-29 08:36:05 -0400 | [diff] [blame] | 1334 | store to y does (the first cumul-fence), the store to y propagates to P2 |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1335 | before P2's load and store execute, P2's smp_store_release() |
| 1336 | guarantees that the stores to x and y both propagate to P0 before the |
Joel Fernandes (Google) | 6240973 | 2019-07-29 08:36:05 -0400 | [diff] [blame] | 1337 | store to z does (the second cumul-fence), and P0's load executes after the |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1338 | store to z has propagated to P0 (an rfe link). |
| 1339 | |
| 1340 | In summary, the fact that the hb relation links memory access events |
| 1341 | in the order they execute means that it must not have cycles. This |
| 1342 | requirement is the content of the LKMM's "happens-before" axiom. |
| 1343 | |
| 1344 | The LKMM defines yet another relation connected to times of |
| 1345 | instruction execution, but it is not included in hb. It relies on the |
| 1346 | particular properties of strong fences, which we cover in the next |
| 1347 | section. |
| 1348 | |
| 1349 | |
| 1350 | THE PROPAGATES-BEFORE RELATION: pb |
| 1351 | ---------------------------------- |
| 1352 | |
| 1353 | The propagates-before (pb) relation capitalizes on the special |
| 1354 | features of strong fences. It links two events E and F whenever some |
| 1355 | store is coherence-later than E and propagates to every CPU and to RAM |
| 1356 | before F executes. The formal definition requires that E be linked to |
| 1357 | F via a coe or fre link, an arbitrary number of cumul-fences, an |
| 1358 | optional rfe link, a strong fence, and an arbitrary number of hb |
| 1359 | links. Let's see how this definition works out. |
| 1360 | |
| 1361 | Consider first the case where E is a store (implying that the sequence |
| 1362 | of links begins with coe). Then there are events W, X, Y, and Z such |
| 1363 | that: |
| 1364 | |
| 1365 | E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F, |
| 1366 | |
| 1367 | where the * suffix indicates an arbitrary number of links of the |
| 1368 | specified type, and the ? suffix indicates the link is optional (Y may |
| 1369 | be equal to X). Because of the cumul-fence links, we know that W will |
| 1370 | propagate to Y's CPU before X does, hence before Y executes and hence |
| 1371 | before the strong fence executes. Because this fence is strong, we |
| 1372 | know that W will propagate to every CPU and to RAM before Z executes. |
| 1373 | And because of the hb links, we know that Z will execute before F. |
| 1374 | Thus W, which comes later than E in the coherence order, will |
| 1375 | propagate to every CPU and to RAM before F executes. |
| 1376 | |
| 1377 | The case where E is a load is exactly the same, except that the first |
| 1378 | link in the sequence is fre instead of coe. |
| 1379 | |
| 1380 | The existence of a pb link from E to F implies that E must execute |
| 1381 | before F. To see why, suppose that F executed first. Then W would |
| 1382 | have propagated to E's CPU before E executed. If E was a store, the |
| 1383 | memory subsystem would then be forced to make E come after W in the |
| 1384 | coherence order, contradicting the fact that E ->coe W. If E was a |
| 1385 | load, the memory subsystem would then be forced to satisfy E's read |
| 1386 | request with the value stored by W or an even later store, |
| 1387 | contradicting the fact that E ->fre W. |
| 1388 | |
| 1389 | A good example illustrating how pb works is the SB pattern with strong |
| 1390 | fences: |
| 1391 | |
| 1392 | int x = 0, y = 0; |
| 1393 | |
| 1394 | P0() |
| 1395 | { |
| 1396 | int r0; |
| 1397 | |
| 1398 | WRITE_ONCE(x, 1); |
| 1399 | smp_mb(); |
| 1400 | r0 = READ_ONCE(y); |
| 1401 | } |
| 1402 | |
| 1403 | P1() |
| 1404 | { |
| 1405 | int r1; |
| 1406 | |
| 1407 | WRITE_ONCE(y, 1); |
| 1408 | smp_mb(); |
| 1409 | r1 = READ_ONCE(x); |
| 1410 | } |
| 1411 | |
| 1412 | If r0 = 0 at the end then there is a pb link from P0's load to P1's |
| 1413 | load: an fre link from P0's load to P1's store (which overwrites the |
| 1414 | value read by P0), and a strong fence between P1's store and its load. |
| 1415 | In this example, the sequences of cumul-fence and hb links are empty. |
| 1416 | Note that this pb link is not included in hb as an instance of prop, |
| 1417 | because it does not start and end on the same CPU. |
| 1418 | |
| 1419 | Similarly, if r1 = 0 at the end then there is a pb link from P1's load |
| 1420 | to P0's. This means that if both r1 and r2 were 0 there would be a |
| 1421 | cycle in pb, which is not possible since an instruction cannot execute |
| 1422 | before itself. Thus, adding smp_mb() fences to the SB pattern |
| 1423 | prevents the r0 = 0, r1 = 0 outcome. |
| 1424 | |
| 1425 | In summary, the fact that the pb relation links events in the order |
| 1426 | they execute means that it cannot have cycles. This requirement is |
| 1427 | the content of the LKMM's "propagation" axiom. |
| 1428 | |
| 1429 | |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1430 | RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb |
| 1431 | ------------------------------------------------------------------------ |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1432 | |
| 1433 | RCU (Read-Copy-Update) is a powerful synchronization mechanism. It |
| 1434 | rests on two concepts: grace periods and read-side critical sections. |
| 1435 | |
| 1436 | A grace period is the span of time occupied by a call to |
| 1437 | synchronize_rcu(). A read-side critical section (or just critical |
| 1438 | section, for short) is a region of code delimited by rcu_read_lock() |
| 1439 | at the start and rcu_read_unlock() at the end. Critical sections can |
| 1440 | be nested, although we won't make use of this fact. |
| 1441 | |
| 1442 | As far as memory models are concerned, RCU's main feature is its |
| 1443 | Grace-Period Guarantee, which states that a critical section can never |
| 1444 | span a full grace period. In more detail, the Guarantee says: |
| 1445 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1446 | For any critical section C and any grace period G, at least |
| 1447 | one of the following statements must hold: |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1448 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1449 | (1) C ends before G does, and in addition, every store that |
| 1450 | propagates to C's CPU before the end of C must propagate to |
| 1451 | every CPU before G ends. |
| 1452 | |
| 1453 | (2) G starts before C does, and in addition, every store that |
| 1454 | propagates to G's CPU before the start of G must propagate |
| 1455 | to every CPU before C starts. |
| 1456 | |
| 1457 | In particular, it is not possible for a critical section to both start |
| 1458 | before and end after a grace period. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1459 | |
| 1460 | Here is a simple example of RCU in action: |
| 1461 | |
| 1462 | int x, y; |
| 1463 | |
| 1464 | P0() |
| 1465 | { |
| 1466 | rcu_read_lock(); |
| 1467 | WRITE_ONCE(x, 1); |
| 1468 | WRITE_ONCE(y, 1); |
| 1469 | rcu_read_unlock(); |
| 1470 | } |
| 1471 | |
| 1472 | P1() |
| 1473 | { |
| 1474 | int r1, r2; |
| 1475 | |
| 1476 | r1 = READ_ONCE(x); |
| 1477 | synchronize_rcu(); |
| 1478 | r2 = READ_ONCE(y); |
| 1479 | } |
| 1480 | |
| 1481 | The Grace Period Guarantee tells us that when this code runs, it will |
| 1482 | never end with r1 = 1 and r2 = 0. The reasoning is as follows. r1 = 1 |
| 1483 | means that P0's store to x propagated to P1 before P1 called |
| 1484 | synchronize_rcu(), so P0's critical section must have started before |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1485 | P1's grace period, contrary to part (2) of the Guarantee. On the |
| 1486 | other hand, r2 = 0 means that P0's store to y, which occurs before the |
| 1487 | end of the critical section, did not propagate to P1 before the end of |
| 1488 | the grace period, contrary to part (1). Together the results violate |
| 1489 | the Guarantee. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1490 | |
Alan Stern | 1ee2da5 | 2018-05-14 16:33:39 -0700 | [diff] [blame] | 1491 | In the kernel's implementations of RCU, the requirements for stores |
| 1492 | to propagate to every CPU are fulfilled by placing strong fences at |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1493 | suitable places in the RCU-related code. Thus, if a critical section |
| 1494 | starts before a grace period does then the critical section's CPU will |
| 1495 | execute an smp_mb() fence after the end of the critical section and |
| 1496 | some time before the grace period's synchronize_rcu() call returns. |
| 1497 | And if a critical section ends after a grace period does then the |
| 1498 | synchronize_rcu() routine will execute an smp_mb() fence at its start |
| 1499 | and some time before the critical section's opening rcu_read_lock() |
| 1500 | executes. |
| 1501 | |
| 1502 | What exactly do we mean by saying that a critical section "starts |
| 1503 | before" or "ends after" a grace period? Some aspects of the meaning |
| 1504 | are pretty obvious, as in the example above, but the details aren't |
Alan Stern | 1ee2da5 | 2018-05-14 16:33:39 -0700 | [diff] [blame] | 1505 | entirely clear. The LKMM formalizes this notion by means of the |
| 1506 | rcu-link relation. rcu-link encompasses a very general notion of |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1507 | "before": If E and F are RCU fence events (i.e., rcu_read_lock(), |
| 1508 | rcu_read_unlock(), or synchronize_rcu()) then among other things, |
| 1509 | E ->rcu-link F includes cases where E is po-before some memory-access |
| 1510 | event X, F is po-after some memory-access event Y, and we have any of |
| 1511 | X ->rfe Y, X ->co Y, or X ->fr Y. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1512 | |
Alan Stern | 1ee2da5 | 2018-05-14 16:33:39 -0700 | [diff] [blame] | 1513 | The formal definition of the rcu-link relation is more than a little |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1514 | obscure, and we won't give it here. It is closely related to the pb |
| 1515 | relation, and the details don't matter unless you want to comb through |
| 1516 | a somewhat lengthy formal proof. Pretty much all you need to know |
Alan Stern | 1ee2da5 | 2018-05-14 16:33:39 -0700 | [diff] [blame] | 1517 | about rcu-link is the information in the preceding paragraph. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1518 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1519 | The LKMM also defines the rcu-gp and rcu-rscsi relations. They bring |
| 1520 | grace periods and read-side critical sections into the picture, in the |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1521 | following way: |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1522 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1523 | E ->rcu-gp F means that E and F are in fact the same event, |
| 1524 | and that event is a synchronize_rcu() fence (i.e., a grace |
| 1525 | period). |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1526 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1527 | E ->rcu-rscsi F means that E and F are the rcu_read_unlock() |
| 1528 | and rcu_read_lock() fence events delimiting some read-side |
| 1529 | critical section. (The 'i' at the end of the name emphasizes |
| 1530 | that this relation is "inverted": It links the end of the |
| 1531 | critical section to the start.) |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1532 | |
Alan Stern | 1ee2da5 | 2018-05-14 16:33:39 -0700 | [diff] [blame] | 1533 | If we think of the rcu-link relation as standing for an extended |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1534 | "before", then X ->rcu-gp Y ->rcu-link Z roughly says that X is a |
| 1535 | grace period which ends before Z begins. (In fact it covers more than |
| 1536 | this, because it also includes cases where some store propagates to |
| 1537 | Z's CPU before Z begins but doesn't propagate to some other CPU until |
| 1538 | after X ends.) Similarly, X ->rcu-rscsi Y ->rcu-link Z says that X is |
| 1539 | the end of a critical section which starts before Z begins. |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1540 | |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1541 | The LKMM goes on to define the rcu-order relation as a sequence of |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1542 | rcu-gp and rcu-rscsi links separated by rcu-link links, in which the |
| 1543 | number of rcu-gp links is >= the number of rcu-rscsi links. For |
| 1544 | example: |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1545 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1546 | X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1547 | |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1548 | would imply that X ->rcu-order V, because this sequence contains two |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1549 | rcu-gp links and one rcu-rscsi link. (It also implies that |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1550 | X ->rcu-order T and Z ->rcu-order V.) On the other hand: |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1551 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1552 | X ->rcu-rscsi Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1553 | |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1554 | does not imply X ->rcu-order V, because the sequence contains only |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1555 | one rcu-gp link but two rcu-rscsi links. |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1556 | |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1557 | The rcu-order relation is important because the Grace Period Guarantee |
| 1558 | means that rcu-order links act kind of like strong fences. In |
| 1559 | particular, E ->rcu-order F implies not only that E begins before F |
| 1560 | ends, but also that any write po-before E will propagate to every CPU |
| 1561 | before any instruction po-after F can execute. (However, it does not |
| 1562 | imply that E must execute before F; in fact, each synchronize_rcu() |
| 1563 | fence event is linked to itself by rcu-order as a degenerate case.) |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1564 | |
| 1565 | To prove this in full generality requires some intellectual effort. |
| 1566 | We'll consider just a very simple case: |
| 1567 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1568 | G ->rcu-gp W ->rcu-link Z ->rcu-rscsi F. |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1569 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1570 | This formula means that G and W are the same event (a grace period), |
| 1571 | and there are events X, Y and a read-side critical section C such that: |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1572 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1573 | 1. G = W is po-before or equal to X; |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1574 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1575 | 2. X comes "before" Y in some sense (including rfe, co and fr); |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1576 | |
Alan Stern | 3321ea1 | 2019-10-01 13:39:47 -0400 | [diff] [blame] | 1577 | 3. Y is po-before Z; |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1578 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1579 | 4. Z is the rcu_read_unlock() event marking the end of C; |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1580 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1581 | 5. F is the rcu_read_lock() event marking the start of C. |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1582 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1583 | From 1 - 4 we deduce that the grace period G ends before the critical |
| 1584 | section C. Then part (2) of the Grace Period Guarantee says not only |
| 1585 | that G starts before C does, but also that any write which executes on |
| 1586 | G's CPU before G starts must propagate to every CPU before C starts. |
| 1587 | In particular, the write propagates to every CPU before F finishes |
| 1588 | executing and hence before any instruction po-after F can execute. |
| 1589 | This sort of reasoning can be extended to handle all the situations |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1590 | covered by rcu-order. |
| 1591 | |
| 1592 | The rcu-fence relation is a simple extension of rcu-order. While |
| 1593 | rcu-order only links certain fence events (calls to synchronize_rcu(), |
| 1594 | rcu_read_lock(), or rcu_read_unlock()), rcu-fence links any events |
| 1595 | that are separated by an rcu-order link. This is analogous to the way |
| 1596 | the strong-fence relation links events that are separated by an |
| 1597 | smp_mb() fence event (as mentioned above, rcu-order links act kind of |
| 1598 | like strong fences). Written symbolically, X ->rcu-fence Y means |
| 1599 | there are fence events E and F such that: |
| 1600 | |
| 1601 | X ->po E ->rcu-order F ->po Y. |
| 1602 | |
| 1603 | From the discussion above, we see this implies not only that X |
| 1604 | executes before Y, but also (if X is a store) that X propagates to |
| 1605 | every CPU before Y executes. Thus rcu-fence is sort of a |
| 1606 | "super-strong" fence: Unlike the original strong fences (smp_mb() and |
| 1607 | synchronize_rcu()), rcu-fence is able to link events on different |
| 1608 | CPUs. (Perhaps this fact should lead us to say that rcu-fence isn't |
| 1609 | really a fence at all!) |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1610 | |
| 1611 | Finally, the LKMM defines the RCU-before (rb) relation in terms of |
| 1612 | rcu-fence. This is done in essentially the same way as the pb |
| 1613 | relation was defined in terms of strong-fence. We will omit the |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1614 | details; the end result is that E ->rb F implies E must execute |
| 1615 | before F, just as E ->pb F does (and for much the same reasons). |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1616 | |
| 1617 | Putting this all together, the LKMM expresses the Grace Period |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1618 | Guarantee by requiring that the rb relation does not contain a cycle. |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1619 | Equivalently, this "rcu" axiom requires that there are no events E |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1620 | and F with E ->rcu-link F ->rcu-order E. Or to put it a third way, |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1621 | the axiom requires that there are no cycles consisting of rcu-gp and |
| 1622 | rcu-rscsi alternating with rcu-link, where the number of rcu-gp links |
| 1623 | is >= the number of rcu-rscsi links. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1624 | |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1625 | Justifying the axiom isn't easy, but it is in fact a valid |
| 1626 | formalization of the Grace Period Guarantee. We won't attempt to go |
| 1627 | through the detailed argument, but the following analysis gives a |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1628 | taste of what is involved. Suppose both parts of the Guarantee are |
| 1629 | violated: A critical section starts before a grace period, and some |
| 1630 | store propagates to the critical section's CPU before the end of the |
| 1631 | critical section but doesn't propagate to some other CPU until after |
| 1632 | the end of the grace period. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1633 | |
| 1634 | Putting symbols to these ideas, let L and U be the rcu_read_lock() and |
| 1635 | rcu_read_unlock() fence events delimiting the critical section in |
| 1636 | question, and let S be the synchronize_rcu() fence event for the grace |
| 1637 | period. Saying that the critical section starts before S means there |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1638 | are events Q and R where Q is po-after L (which marks the start of the |
| 1639 | critical section), Q is "before" R in the sense used by the rcu-link |
| 1640 | relation, and R is po-before the grace period S. Thus we have: |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1641 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1642 | L ->rcu-link S. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1643 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1644 | Let W be the store mentioned above, let Y come before the end of the |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1645 | critical section and witness that W propagates to the critical |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1646 | section's CPU by reading from W, and let Z on some arbitrary CPU be a |
| 1647 | witness that W has not propagated to that CPU, where Z happens after |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1648 | some event X which is po-after S. Symbolically, this amounts to: |
| 1649 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1650 | S ->po X ->hb* Z ->fr W ->rf Y ->po U. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1651 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1652 | The fr link from Z to W indicates that W has not propagated to Z's CPU |
| 1653 | at the time that Z executes. From this, it can be shown (see the |
| 1654 | discussion of the rcu-link relation earlier) that S and U are related |
| 1655 | by rcu-link: |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1656 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1657 | S ->rcu-link U. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1658 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1659 | Since S is a grace period we have S ->rcu-gp S, and since L and U are |
| 1660 | the start and end of the critical section C we have U ->rcu-rscsi L. |
| 1661 | From this we obtain: |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1662 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1663 | S ->rcu-gp S ->rcu-link U ->rcu-rscsi L ->rcu-link S, |
Alan Stern | 9d03688 | 2018-05-14 16:33:40 -0700 | [diff] [blame] | 1664 | |
| 1665 | a forbidden cycle. Thus the "rcu" axiom rules out this violation of |
| 1666 | the Grace Period Guarantee. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1667 | |
| 1668 | For something a little more down-to-earth, let's see how the axiom |
| 1669 | works out in practice. Consider the RCU code example from above, this |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1670 | time with statement labels added: |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1671 | |
| 1672 | int x, y; |
| 1673 | |
| 1674 | P0() |
| 1675 | { |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1676 | L: rcu_read_lock(); |
| 1677 | X: WRITE_ONCE(x, 1); |
| 1678 | Y: WRITE_ONCE(y, 1); |
| 1679 | U: rcu_read_unlock(); |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1680 | } |
| 1681 | |
| 1682 | P1() |
| 1683 | { |
| 1684 | int r1, r2; |
| 1685 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1686 | Z: r1 = READ_ONCE(x); |
| 1687 | S: synchronize_rcu(); |
| 1688 | W: r2 = READ_ONCE(y); |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1689 | } |
| 1690 | |
| 1691 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1692 | If r2 = 0 at the end then P0's store at Y overwrites the value that |
| 1693 | P1's load at W reads from, so we have W ->fre Y. Since S ->po W and |
| 1694 | also Y ->po U, we get S ->rcu-link U. In addition, S ->rcu-gp S |
| 1695 | because S is a grace period. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1696 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1697 | If r1 = 1 at the end then P1's load at Z reads from P0's store at X, |
| 1698 | so we have X ->rfe Z. Together with L ->po X and Z ->po S, this |
| 1699 | yields L ->rcu-link S. And since L and U are the start and end of a |
| 1700 | critical section, we have U ->rcu-rscsi L. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1701 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1702 | Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S ->rcu-link U is a |
| 1703 | forbidden cycle, violating the "rcu" axiom. Hence the outcome is not |
| 1704 | allowed by the LKMM, as we would expect. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1705 | |
| 1706 | For contrast, let's see what can happen in a more complicated example: |
| 1707 | |
| 1708 | int x, y, z; |
| 1709 | |
| 1710 | P0() |
| 1711 | { |
| 1712 | int r0; |
| 1713 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1714 | L0: rcu_read_lock(); |
| 1715 | r0 = READ_ONCE(x); |
| 1716 | WRITE_ONCE(y, 1); |
| 1717 | U0: rcu_read_unlock(); |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1718 | } |
| 1719 | |
| 1720 | P1() |
| 1721 | { |
| 1722 | int r1; |
| 1723 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1724 | r1 = READ_ONCE(y); |
| 1725 | S1: synchronize_rcu(); |
| 1726 | WRITE_ONCE(z, 1); |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1727 | } |
| 1728 | |
| 1729 | P2() |
| 1730 | { |
| 1731 | int r2; |
| 1732 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1733 | L2: rcu_read_lock(); |
| 1734 | r2 = READ_ONCE(z); |
| 1735 | WRITE_ONCE(x, 1); |
| 1736 | U2: rcu_read_unlock(); |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1737 | } |
| 1738 | |
| 1739 | If r0 = r1 = r2 = 1 at the end, then similar reasoning to before shows |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1740 | that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp S1 ->rcu-link U2 ->rcu-rscsi |
| 1741 | L2 ->rcu-link U0. However this cycle is not forbidden, because the |
| 1742 | sequence of relations contains fewer instances of rcu-gp (one) than of |
| 1743 | rcu-rscsi (two). Consequently the outcome is allowed by the LKMM. |
| 1744 | The following instruction timing diagram shows how it might actually |
| 1745 | occur: |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1746 | |
| 1747 | P0 P1 P2 |
| 1748 | -------------------- -------------------- -------------------- |
| 1749 | rcu_read_lock() |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1750 | WRITE_ONCE(y, 1) |
| 1751 | r1 = READ_ONCE(y) |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1752 | synchronize_rcu() starts |
| 1753 | . rcu_read_lock() |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1754 | . WRITE_ONCE(x, 1) |
| 1755 | r0 = READ_ONCE(x) . |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1756 | rcu_read_unlock() . |
| 1757 | synchronize_rcu() ends |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1758 | WRITE_ONCE(z, 1) |
| 1759 | r2 = READ_ONCE(z) |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1760 | rcu_read_unlock() |
| 1761 | |
| 1762 | This requires P0 and P2 to execute their loads and stores out of |
| 1763 | program order, but of course they are allowed to do so. And as you |
| 1764 | can see, the Grace Period Guarantee is not violated: The critical |
| 1765 | section in P0 both starts before P1's grace period does and ends |
| 1766 | before it does, and the critical section in P2 both starts after P1's |
| 1767 | grace period does and ends after it does. |
| 1768 | |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1769 | Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in |
| 1770 | addition to normal RCU. The ideas involved are much the same as |
| 1771 | above, with new relations srcu-gp and srcu-rscsi added to represent |
| 1772 | SRCU grace periods and read-side critical sections. There is a |
| 1773 | restriction on the srcu-gp and srcu-rscsi links that can appear in an |
Alan Stern | ddc8299 | 2019-10-01 13:40:11 -0400 | [diff] [blame] | 1774 | rcu-order sequence (the srcu-rscsi links must be paired with srcu-gp |
Alan Stern | 648e717 | 2018-12-11 11:38:53 -0500 | [diff] [blame] | 1775 | links having the same SRCU domain with proper nesting); the details |
| 1776 | are relatively unimportant. |
| 1777 | |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 1778 | |
Alan Stern | 6e89e83 | 2018-09-26 11:29:17 -0700 | [diff] [blame] | 1779 | LOCKING |
| 1780 | ------- |
| 1781 | |
| 1782 | The LKMM includes locking. In fact, there is special code for locking |
| 1783 | in the formal model, added in order to make tools run faster. |
| 1784 | However, this special code is intended to be more or less equivalent |
| 1785 | to concepts we have already covered. A spinlock_t variable is treated |
| 1786 | the same as an int, and spin_lock(&s) is treated almost the same as: |
| 1787 | |
| 1788 | while (cmpxchg_acquire(&s, 0, 1) != 0) |
| 1789 | cpu_relax(); |
| 1790 | |
| 1791 | This waits until s is equal to 0 and then atomically sets it to 1, |
| 1792 | and the read part of the cmpxchg operation acts as an acquire fence. |
| 1793 | An alternate way to express the same thing would be: |
| 1794 | |
| 1795 | r = xchg_acquire(&s, 1); |
| 1796 | |
| 1797 | along with a requirement that at the end, r = 0. Similarly, |
| 1798 | spin_trylock(&s) is treated almost the same as: |
| 1799 | |
| 1800 | return !cmpxchg_acquire(&s, 0, 1); |
| 1801 | |
| 1802 | which atomically sets s to 1 if it is currently equal to 0 and returns |
| 1803 | true if it succeeds (the read part of the cmpxchg operation acts as an |
| 1804 | acquire fence only if the operation is successful). spin_unlock(&s) |
| 1805 | is treated almost the same as: |
| 1806 | |
| 1807 | smp_store_release(&s, 0); |
| 1808 | |
| 1809 | The "almost" qualifiers above need some explanation. In the LKMM, the |
| 1810 | store-release in a spin_unlock() and the load-acquire which forms the |
| 1811 | first half of the atomic rmw update in a spin_lock() or a successful |
| 1812 | spin_trylock() -- we can call these things lock-releases and |
| 1813 | lock-acquires -- have two properties beyond those of ordinary releases |
| 1814 | and acquires. |
| 1815 | |
| 1816 | First, when a lock-acquire reads from a lock-release, the LKMM |
| 1817 | requires that every instruction po-before the lock-release must |
| 1818 | execute before any instruction po-after the lock-acquire. This would |
| 1819 | naturally hold if the release and acquire operations were on different |
| 1820 | CPUs, but the LKMM says it holds even when they are on the same CPU. |
| 1821 | For example: |
| 1822 | |
| 1823 | int x, y; |
| 1824 | spinlock_t s; |
| 1825 | |
| 1826 | P0() |
| 1827 | { |
| 1828 | int r1, r2; |
| 1829 | |
| 1830 | spin_lock(&s); |
| 1831 | r1 = READ_ONCE(x); |
| 1832 | spin_unlock(&s); |
| 1833 | spin_lock(&s); |
| 1834 | r2 = READ_ONCE(y); |
| 1835 | spin_unlock(&s); |
| 1836 | } |
| 1837 | |
| 1838 | P1() |
| 1839 | { |
| 1840 | WRITE_ONCE(y, 1); |
| 1841 | smp_wmb(); |
| 1842 | WRITE_ONCE(x, 1); |
| 1843 | } |
| 1844 | |
| 1845 | Here the second spin_lock() reads from the first spin_unlock(), and |
| 1846 | therefore the load of x must execute before the load of y. Thus we |
| 1847 | cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the |
| 1848 | MP pattern). |
| 1849 | |
| 1850 | This requirement does not apply to ordinary release and acquire |
| 1851 | fences, only to lock-related operations. For instance, suppose P0() |
| 1852 | in the example had been written as: |
| 1853 | |
| 1854 | P0() |
| 1855 | { |
| 1856 | int r1, r2, r3; |
| 1857 | |
| 1858 | r1 = READ_ONCE(x); |
| 1859 | smp_store_release(&s, 1); |
| 1860 | r3 = smp_load_acquire(&s); |
| 1861 | r2 = READ_ONCE(y); |
| 1862 | } |
| 1863 | |
| 1864 | Then the CPU would be allowed to forward the s = 1 value from the |
| 1865 | smp_store_release() to the smp_load_acquire(), executing the |
| 1866 | instructions in the following order: |
| 1867 | |
| 1868 | r3 = smp_load_acquire(&s); // Obtains r3 = 1 |
| 1869 | r2 = READ_ONCE(y); |
| 1870 | r1 = READ_ONCE(x); |
| 1871 | smp_store_release(&s, 1); // Value is forwarded |
| 1872 | |
| 1873 | and thus it could load y before x, obtaining r2 = 0 and r1 = 1. |
| 1874 | |
| 1875 | Second, when a lock-acquire reads from a lock-release, and some other |
| 1876 | stores W and W' occur po-before the lock-release and po-after the |
| 1877 | lock-acquire respectively, the LKMM requires that W must propagate to |
| 1878 | each CPU before W' does. For example, consider: |
| 1879 | |
| 1880 | int x, y; |
| 1881 | spinlock_t x; |
| 1882 | |
| 1883 | P0() |
| 1884 | { |
| 1885 | spin_lock(&s); |
| 1886 | WRITE_ONCE(x, 1); |
| 1887 | spin_unlock(&s); |
| 1888 | } |
| 1889 | |
| 1890 | P1() |
| 1891 | { |
| 1892 | int r1; |
| 1893 | |
| 1894 | spin_lock(&s); |
| 1895 | r1 = READ_ONCE(x); |
| 1896 | WRITE_ONCE(y, 1); |
| 1897 | spin_unlock(&s); |
| 1898 | } |
| 1899 | |
| 1900 | P2() |
| 1901 | { |
| 1902 | int r2, r3; |
| 1903 | |
| 1904 | r2 = READ_ONCE(y); |
| 1905 | smp_rmb(); |
| 1906 | r3 = READ_ONCE(x); |
| 1907 | } |
| 1908 | |
| 1909 | If r1 = 1 at the end then the spin_lock() in P1 must have read from |
| 1910 | the spin_unlock() in P0. Hence the store to x must propagate to P2 |
| 1911 | before the store to y does, so we cannot have r2 = 1 and r3 = 0. |
| 1912 | |
| 1913 | These two special requirements for lock-release and lock-acquire do |
| 1914 | not arise from the operational model. Nevertheless, kernel developers |
| 1915 | have come to expect and rely on them because they do hold on all |
| 1916 | architectures supported by the Linux kernel, albeit for various |
| 1917 | differing reasons. |
| 1918 | |
| 1919 | |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 1920 | PLAIN ACCESSES AND DATA RACES |
| 1921 | ----------------------------- |
| 1922 | |
| 1923 | In the LKMM, memory accesses such as READ_ONCE(x), atomic_inc(&y), |
| 1924 | smp_load_acquire(&z), and so on are collectively referred to as |
| 1925 | "marked" accesses, because they are all annotated with special |
| 1926 | operations of one kind or another. Ordinary C-language memory |
| 1927 | accesses such as x or y = 0 are simply called "plain" accesses. |
| 1928 | |
| 1929 | Early versions of the LKMM had nothing to say about plain accesses. |
| 1930 | The C standard allows compilers to assume that the variables affected |
| 1931 | by plain accesses are not concurrently read or written by any other |
| 1932 | threads or CPUs. This leaves compilers free to implement all manner |
| 1933 | of transformations or optimizations of code containing plain accesses, |
| 1934 | making such code very difficult for a memory model to handle. |
| 1935 | |
| 1936 | Here is just one example of a possible pitfall: |
| 1937 | |
| 1938 | int a = 6; |
| 1939 | int *x = &a; |
| 1940 | |
| 1941 | P0() |
| 1942 | { |
| 1943 | int *r1; |
| 1944 | int r2 = 0; |
| 1945 | |
| 1946 | r1 = x; |
| 1947 | if (r1 != NULL) |
| 1948 | r2 = READ_ONCE(*r1); |
| 1949 | } |
| 1950 | |
| 1951 | P1() |
| 1952 | { |
| 1953 | WRITE_ONCE(x, NULL); |
| 1954 | } |
| 1955 | |
| 1956 | On the face of it, one would expect that when this code runs, the only |
| 1957 | possible final values for r2 are 6 and 0, depending on whether or not |
| 1958 | P1's store to x propagates to P0 before P0's load from x executes. |
| 1959 | But since P0's load from x is a plain access, the compiler may decide |
| 1960 | to carry out the load twice (for the comparison against NULL, then again |
| 1961 | for the READ_ONCE()) and eliminate the temporary variable r1. The |
| 1962 | object code generated for P0 could therefore end up looking rather |
| 1963 | like this: |
| 1964 | |
| 1965 | P0() |
| 1966 | { |
| 1967 | int r2 = 0; |
| 1968 | |
| 1969 | if (x != NULL) |
| 1970 | r2 = READ_ONCE(*x); |
| 1971 | } |
| 1972 | |
| 1973 | And now it is obvious that this code runs the risk of dereferencing a |
| 1974 | NULL pointer, because P1's store to x might propagate to P0 after the |
| 1975 | test against NULL has been made but before the READ_ONCE() executes. |
| 1976 | If the original code had said "r1 = READ_ONCE(x)" instead of "r1 = x", |
| 1977 | the compiler would not have performed this optimization and there |
| 1978 | would be no possibility of a NULL-pointer dereference. |
| 1979 | |
| 1980 | Given the possibility of transformations like this one, the LKMM |
| 1981 | doesn't try to predict all possible outcomes of code containing plain |
| 1982 | accesses. It is instead content to determine whether the code |
| 1983 | violates the compiler's assumptions, which would render the ultimate |
| 1984 | outcome undefined. |
| 1985 | |
| 1986 | In technical terms, the compiler is allowed to assume that when the |
| 1987 | program executes, there will not be any data races. A "data race" |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 1988 | occurs when there are two memory accesses such that: |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 1989 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 1990 | 1. they access the same location, |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 1991 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 1992 | 2. at least one of them is a store, |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 1993 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 1994 | 3. at least one of them is plain, |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 1995 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 1996 | 4. they occur on different CPUs (or in different threads on the |
| 1997 | same CPU), and |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 1998 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 1999 | 5. they execute concurrently. |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2000 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 2001 | In the literature, two accesses are said to "conflict" if they satisfy |
| 2002 | 1 and 2 above. We'll go a little farther and say that two accesses |
| 2003 | are "race candidates" if they satisfy 1 - 4. Thus, whether or not two |
| 2004 | race candidates actually do race in a given execution depends on |
| 2005 | whether they are concurrent. |
| 2006 | |
| 2007 | The LKMM tries to determine whether a program contains race candidates |
| 2008 | which may execute concurrently; if it does then the LKMM says there is |
| 2009 | a potential data race and makes no predictions about the program's |
| 2010 | outcome. |
| 2011 | |
| 2012 | Determining whether two accesses are race candidates is easy; you can |
| 2013 | see that all the concepts involved in the definition above are already |
| 2014 | part of the memory model. The hard part is telling whether they may |
| 2015 | execute concurrently. The LKMM takes a conservative attitude, |
| 2016 | assuming that accesses may be concurrent unless it can prove they |
| 2017 | are not. |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2018 | |
| 2019 | If two memory accesses aren't concurrent then one must execute before |
| 2020 | the other. Therefore the LKMM decides two accesses aren't concurrent |
| 2021 | if they can be connected by a sequence of hb, pb, and rb links |
| 2022 | (together referred to as xb, for "executes before"). However, there |
| 2023 | are two complicating factors. |
| 2024 | |
| 2025 | If X is a load and X executes before a store Y, then indeed there is |
| 2026 | no danger of X and Y being concurrent. After all, Y can't have any |
| 2027 | effect on the value obtained by X until the memory subsystem has |
| 2028 | propagated Y from its own CPU to X's CPU, which won't happen until |
| 2029 | some time after Y executes and thus after X executes. But if X is a |
| 2030 | store, then even if X executes before Y it is still possible that X |
| 2031 | will propagate to Y's CPU just as Y is executing. In such a case X |
| 2032 | could very well interfere somehow with Y, and we would have to |
| 2033 | consider X and Y to be concurrent. |
| 2034 | |
| 2035 | Therefore when X is a store, for X and Y to be non-concurrent the LKMM |
| 2036 | requires not only that X must execute before Y but also that X must |
| 2037 | propagate to Y's CPU before Y executes. (Or vice versa, of course, if |
| 2038 | Y executes before X -- then Y must propagate to X's CPU before X |
| 2039 | executes if Y is a store.) This is expressed by the visibility |
| 2040 | relation (vis), where X ->vis Y is defined to hold if there is an |
| 2041 | intermediate event Z such that: |
| 2042 | |
| 2043 | X is connected to Z by a possibly empty sequence of |
| 2044 | cumul-fence links followed by an optional rfe link (if none of |
| 2045 | these links are present, X and Z are the same event), |
| 2046 | |
| 2047 | and either: |
| 2048 | |
| 2049 | Z is connected to Y by a strong-fence link followed by a |
| 2050 | possibly empty sequence of xb links, |
| 2051 | |
| 2052 | or: |
| 2053 | |
| 2054 | Z is on the same CPU as Y and is connected to Y by a possibly |
| 2055 | empty sequence of xb links (again, if the sequence is empty it |
| 2056 | means Z and Y are the same event). |
| 2057 | |
| 2058 | The motivations behind this definition are straightforward: |
| 2059 | |
| 2060 | cumul-fence memory barriers force stores that are po-before |
| 2061 | the barrier to propagate to other CPUs before stores that are |
| 2062 | po-after the barrier. |
| 2063 | |
| 2064 | An rfe link from an event W to an event R says that R reads |
| 2065 | from W, which certainly means that W must have propagated to |
| 2066 | R's CPU before R executed. |
| 2067 | |
| 2068 | strong-fence memory barriers force stores that are po-before |
| 2069 | the barrier, or that propagate to the barrier's CPU before the |
| 2070 | barrier executes, to propagate to all CPUs before any events |
| 2071 | po-after the barrier can execute. |
| 2072 | |
| 2073 | To see how this works out in practice, consider our old friend, the MP |
| 2074 | pattern (with fences and statement labels, but without the conditional |
| 2075 | test): |
| 2076 | |
| 2077 | int buf = 0, flag = 0; |
| 2078 | |
| 2079 | P0() |
| 2080 | { |
| 2081 | X: WRITE_ONCE(buf, 1); |
| 2082 | smp_wmb(); |
| 2083 | W: WRITE_ONCE(flag, 1); |
| 2084 | } |
| 2085 | |
| 2086 | P1() |
| 2087 | { |
| 2088 | int r1; |
| 2089 | int r2 = 0; |
| 2090 | |
| 2091 | Z: r1 = READ_ONCE(flag); |
| 2092 | smp_rmb(); |
| 2093 | Y: r2 = READ_ONCE(buf); |
| 2094 | } |
| 2095 | |
| 2096 | The smp_wmb() memory barrier gives a cumul-fence link from X to W, and |
| 2097 | assuming r1 = 1 at the end, there is an rfe link from W to Z. This |
| 2098 | means that the store to buf must propagate from P0 to P1 before Z |
| 2099 | executes. Next, Z and Y are on the same CPU and the smp_rmb() fence |
| 2100 | provides an xb link from Z to Y (i.e., it forces Z to execute before |
| 2101 | Y). Therefore we have X ->vis Y: X must propagate to Y's CPU before Y |
| 2102 | executes. |
| 2103 | |
| 2104 | The second complicating factor mentioned above arises from the fact |
| 2105 | that when we are considering data races, some of the memory accesses |
| 2106 | are plain. Now, although we have not said so explicitly, up to this |
| 2107 | point most of the relations defined by the LKMM (ppo, hb, prop, |
| 2108 | cumul-fence, pb, and so on -- including vis) apply only to marked |
| 2109 | accesses. |
| 2110 | |
| 2111 | There are good reasons for this restriction. The compiler is not |
| 2112 | allowed to apply fancy transformations to marked accesses, and |
| 2113 | consequently each such access in the source code corresponds more or |
| 2114 | less directly to a single machine instruction in the object code. But |
| 2115 | plain accesses are a different story; the compiler may combine them, |
| 2116 | split them up, duplicate them, eliminate them, invent new ones, and |
| 2117 | who knows what else. Seeing a plain access in the source code tells |
| 2118 | you almost nothing about what machine instructions will end up in the |
| 2119 | object code. |
| 2120 | |
| 2121 | Fortunately, the compiler isn't completely free; it is subject to some |
| 2122 | limitations. For one, it is not allowed to introduce a data race into |
| 2123 | the object code if the source code does not already contain a data |
| 2124 | race (if it could, memory models would be useless and no multithreaded |
| 2125 | code would be safe!). For another, it cannot move a plain access past |
| 2126 | a compiler barrier. |
| 2127 | |
| 2128 | A compiler barrier is a kind of fence, but as the name implies, it |
| 2129 | only affects the compiler; it does not necessarily have any effect on |
| 2130 | how instructions are executed by the CPU. In Linux kernel source |
| 2131 | code, the barrier() function is a compiler barrier. It doesn't give |
| 2132 | rise directly to any machine instructions in the object code; rather, |
| 2133 | it affects how the compiler generates the rest of the object code. |
| 2134 | Given source code like this: |
| 2135 | |
| 2136 | ... some memory accesses ... |
| 2137 | barrier(); |
| 2138 | ... some other memory accesses ... |
| 2139 | |
| 2140 | the barrier() function ensures that the machine instructions |
| 2141 | corresponding to the first group of accesses will all end po-before |
| 2142 | any machine instructions corresponding to the second group of accesses |
| 2143 | -- even if some of the accesses are plain. (Of course, the CPU may |
| 2144 | then execute some of those accesses out of program order, but we |
| 2145 | already know how to deal with such issues.) Without the barrier() |
| 2146 | there would be no such guarantee; the two groups of accesses could be |
| 2147 | intermingled or even reversed in the object code. |
| 2148 | |
| 2149 | The LKMM doesn't say much about the barrier() function, but it does |
| 2150 | require that all fences are also compiler barriers. In addition, it |
| 2151 | requires that the ordering properties of memory barriers such as |
| 2152 | smp_rmb() or smp_store_release() apply to plain accesses as well as to |
| 2153 | marked accesses. |
| 2154 | |
| 2155 | This is the key to analyzing data races. Consider the MP pattern |
| 2156 | again, now using plain accesses for buf: |
| 2157 | |
| 2158 | int buf = 0, flag = 0; |
| 2159 | |
| 2160 | P0() |
| 2161 | { |
| 2162 | U: buf = 1; |
| 2163 | smp_wmb(); |
| 2164 | X: WRITE_ONCE(flag, 1); |
| 2165 | } |
| 2166 | |
| 2167 | P1() |
| 2168 | { |
| 2169 | int r1; |
| 2170 | int r2 = 0; |
| 2171 | |
| 2172 | Y: r1 = READ_ONCE(flag); |
| 2173 | if (r1) { |
| 2174 | smp_rmb(); |
| 2175 | V: r2 = buf; |
| 2176 | } |
| 2177 | } |
| 2178 | |
| 2179 | This program does not contain a data race. Although the U and V |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 2180 | accesses are race candidates, the LKMM can prove they are not |
| 2181 | concurrent as follows: |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2182 | |
| 2183 | The smp_wmb() fence in P0 is both a compiler barrier and a |
| 2184 | cumul-fence. It guarantees that no matter what hash of |
| 2185 | machine instructions the compiler generates for the plain |
| 2186 | access U, all those instructions will be po-before the fence. |
| 2187 | Consequently U's store to buf, no matter how it is carried out |
| 2188 | at the machine level, must propagate to P1 before X's store to |
| 2189 | flag does. |
| 2190 | |
| 2191 | X and Y are both marked accesses. Hence an rfe link from X to |
| 2192 | Y is a valid indicator that X propagated to P1 before Y |
| 2193 | executed, i.e., X ->vis Y. (And if there is no rfe link then |
| 2194 | r1 will be 0, so V will not be executed and ipso facto won't |
| 2195 | race with U.) |
| 2196 | |
| 2197 | The smp_rmb() fence in P1 is a compiler barrier as well as a |
| 2198 | fence. It guarantees that all the machine-level instructions |
| 2199 | corresponding to the access V will be po-after the fence, and |
| 2200 | therefore any loads among those instructions will execute |
| 2201 | after the fence does and hence after Y does. |
| 2202 | |
| 2203 | Thus U's store to buf is forced to propagate to P1 before V's load |
| 2204 | executes (assuming V does execute), ruling out the possibility of a |
| 2205 | data race between them. |
| 2206 | |
| 2207 | This analysis illustrates how the LKMM deals with plain accesses in |
| 2208 | general. Suppose R is a plain load and we want to show that R |
| 2209 | executes before some marked access E. We can do this by finding a |
| 2210 | marked access X such that R and X are ordered by a suitable fence and |
| 2211 | X ->xb* E. If E was also a plain access, we would also look for a |
| 2212 | marked access Y such that X ->xb* Y, and Y and E are ordered by a |
| 2213 | fence. We describe this arrangement by saying that R is |
| 2214 | "post-bounded" by X and E is "pre-bounded" by Y. |
| 2215 | |
| 2216 | In fact, we go one step further: Since R is a read, we say that R is |
| 2217 | "r-post-bounded" by X. Similarly, E would be "r-pre-bounded" or |
| 2218 | "w-pre-bounded" by Y, depending on whether E was a store or a load. |
| 2219 | This distinction is needed because some fences affect only loads |
| 2220 | (i.e., smp_rmb()) and some affect only stores (smp_wmb()); otherwise |
| 2221 | the two types of bounds are the same. And as a degenerate case, we |
| 2222 | say that a marked access pre-bounds and post-bounds itself (e.g., if R |
| 2223 | above were a marked load then X could simply be taken to be R itself.) |
| 2224 | |
| 2225 | The need to distinguish between r- and w-bounding raises yet another |
| 2226 | issue. When the source code contains a plain store, the compiler is |
| 2227 | allowed to put plain loads of the same location into the object code. |
| 2228 | For example, given the source code: |
| 2229 | |
| 2230 | x = 1; |
| 2231 | |
| 2232 | the compiler is theoretically allowed to generate object code that |
| 2233 | looks like: |
| 2234 | |
| 2235 | if (x != 1) |
| 2236 | x = 1; |
| 2237 | |
| 2238 | thereby adding a load (and possibly replacing the store entirely). |
| 2239 | For this reason, whenever the LKMM requires a plain store to be |
| 2240 | w-pre-bounded or w-post-bounded by a marked access, it also requires |
| 2241 | the store to be r-pre-bounded or r-post-bounded, so as to handle cases |
| 2242 | where the compiler adds a load. |
| 2243 | |
| 2244 | (This may be overly cautious. We don't know of any examples where a |
| 2245 | compiler has augmented a store with a load in this fashion, and the |
| 2246 | Linux kernel developers would probably fight pretty hard to change a |
| 2247 | compiler if it ever did this. Still, better safe than sorry.) |
| 2248 | |
| 2249 | Incidentally, the other tranformation -- augmenting a plain load by |
| 2250 | adding in a store to the same location -- is not allowed. This is |
| 2251 | because the compiler cannot know whether any other CPUs might perform |
| 2252 | a concurrent load from that location. Two concurrent loads don't |
| 2253 | constitute a race (they can't interfere with each other), but a store |
| 2254 | does race with a concurrent load. Thus adding a store might create a |
| 2255 | data race where one was not already present in the source code, |
| 2256 | something the compiler is forbidden to do. Augmenting a store with a |
| 2257 | load, on the other hand, is acceptable because doing so won't create a |
| 2258 | data race unless one already existed. |
| 2259 | |
| 2260 | The LKMM includes a second way to pre-bound plain accesses, in |
| 2261 | addition to fences: an address dependency from a marked load. That |
| 2262 | is, in the sequence: |
| 2263 | |
| 2264 | p = READ_ONCE(ptr); |
| 2265 | r = *p; |
| 2266 | |
| 2267 | the LKMM says that the marked load of ptr pre-bounds the plain load of |
| 2268 | *p; the marked load must execute before any of the machine |
| 2269 | instructions corresponding to the plain load. This is a reasonable |
| 2270 | stipulation, since after all, the CPU can't perform the load of *p |
| 2271 | until it knows what value p will hold. Furthermore, without some |
| 2272 | assumption like this one, some usages typical of RCU would count as |
| 2273 | data races. For example: |
| 2274 | |
| 2275 | int a = 1, b; |
| 2276 | int *ptr = &a; |
| 2277 | |
| 2278 | P0() |
| 2279 | { |
| 2280 | b = 2; |
| 2281 | rcu_assign_pointer(ptr, &b); |
| 2282 | } |
| 2283 | |
| 2284 | P1() |
| 2285 | { |
| 2286 | int *p; |
| 2287 | int r; |
| 2288 | |
| 2289 | rcu_read_lock(); |
| 2290 | p = rcu_dereference(ptr); |
| 2291 | r = *p; |
| 2292 | rcu_read_unlock(); |
| 2293 | } |
| 2294 | |
| 2295 | (In this example the rcu_read_lock() and rcu_read_unlock() calls don't |
| 2296 | really do anything, because there aren't any grace periods. They are |
| 2297 | included merely for the sake of good form; typically P0 would call |
| 2298 | synchronize_rcu() somewhere after the rcu_assign_pointer().) |
| 2299 | |
| 2300 | rcu_assign_pointer() performs a store-release, so the plain store to b |
| 2301 | is definitely w-post-bounded before the store to ptr, and the two |
| 2302 | stores will propagate to P1 in that order. However, rcu_dereference() |
| 2303 | is only equivalent to READ_ONCE(). While it is a marked access, it is |
| 2304 | not a fence or compiler barrier. Hence the only guarantee we have |
| 2305 | that the load of ptr in P1 is r-pre-bounded before the load of *p |
| 2306 | (thus avoiding a race) is the assumption about address dependencies. |
| 2307 | |
| 2308 | This is a situation where the compiler can undermine the memory model, |
| 2309 | and a certain amount of care is required when programming constructs |
| 2310 | like this one. In particular, comparisons between the pointer and |
| 2311 | other known addresses can cause trouble. If you have something like: |
| 2312 | |
| 2313 | p = rcu_dereference(ptr); |
| 2314 | if (p == &x) |
| 2315 | r = *p; |
| 2316 | |
| 2317 | then the compiler just might generate object code resembling: |
| 2318 | |
| 2319 | p = rcu_dereference(ptr); |
| 2320 | if (p == &x) |
| 2321 | r = x; |
| 2322 | |
| 2323 | or even: |
| 2324 | |
| 2325 | rtemp = x; |
| 2326 | p = rcu_dereference(ptr); |
| 2327 | if (p == &x) |
| 2328 | r = rtemp; |
| 2329 | |
| 2330 | which would invalidate the memory model's assumption, since the CPU |
| 2331 | could now perform the load of x before the load of ptr (there might be |
| 2332 | a control dependency but no address dependency at the machine level). |
| 2333 | |
| 2334 | Finally, it turns out there is a situation in which a plain write does |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 2335 | not need to be w-post-bounded: when it is separated from the other |
| 2336 | race-candidate access by a fence. At first glance this may seem |
| 2337 | impossible. After all, to be race candidates the two accesses must |
| 2338 | be on different CPUs, and fences don't link events on different CPUs. |
| 2339 | Well, normal fences don't -- but rcu-fence can! Here's an example: |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2340 | |
| 2341 | int x, y; |
| 2342 | |
| 2343 | P0() |
| 2344 | { |
| 2345 | WRITE_ONCE(x, 1); |
| 2346 | synchronize_rcu(); |
| 2347 | y = 3; |
| 2348 | } |
| 2349 | |
| 2350 | P1() |
| 2351 | { |
| 2352 | rcu_read_lock(); |
| 2353 | if (READ_ONCE(x) == 0) |
| 2354 | y = 2; |
| 2355 | rcu_read_unlock(); |
| 2356 | } |
| 2357 | |
| 2358 | Do the plain stores to y race? Clearly not if P1 reads a non-zero |
| 2359 | value for x, so let's assume the READ_ONCE(x) does obtain 0. This |
| 2360 | means that the read-side critical section in P1 must finish executing |
| 2361 | before the grace period in P0 does, because RCU's Grace-Period |
| 2362 | Guarantee says that otherwise P0's store to x would have propagated to |
| 2363 | P1 before the critical section started and so would have been visible |
| 2364 | to the READ_ONCE(). (Another way of putting it is that the fre link |
| 2365 | from the READ_ONCE() to the WRITE_ONCE() gives rise to an rcu-link |
| 2366 | between those two events.) |
| 2367 | |
| 2368 | This means there is an rcu-fence link from P1's "y = 2" store to P0's |
| 2369 | "y = 3" store, and consequently the first must propagate from P1 to P0 |
| 2370 | before the second can execute. Therefore the two stores cannot be |
| 2371 | concurrent and there is no race, even though P1's plain store to y |
| 2372 | isn't w-post-bounded by any marked accesses. |
| 2373 | |
| 2374 | Putting all this material together yields the following picture. For |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 2375 | race-candidate stores W and W', where W ->co W', the LKMM says the |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2376 | stores don't race if W can be linked to W' by a |
| 2377 | |
| 2378 | w-post-bounded ; vis ; w-pre-bounded |
| 2379 | |
| 2380 | sequence. If W is plain then they also have to be linked by an |
| 2381 | |
| 2382 | r-post-bounded ; xb* ; w-pre-bounded |
| 2383 | |
| 2384 | sequence, and if W' is plain then they also have to be linked by a |
| 2385 | |
| 2386 | w-post-bounded ; vis ; r-pre-bounded |
| 2387 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 2388 | sequence. For race-candidate load R and store W, the LKMM says the |
| 2389 | two accesses don't race if R can be linked to W by an |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2390 | |
| 2391 | r-post-bounded ; xb* ; w-pre-bounded |
| 2392 | |
| 2393 | sequence or if W can be linked to R by a |
| 2394 | |
| 2395 | w-post-bounded ; vis ; r-pre-bounded |
| 2396 | |
| 2397 | sequence. For the cases involving a vis link, the LKMM also accepts |
| 2398 | sequences in which W is linked to W' or R by a |
| 2399 | |
| 2400 | strong-fence ; xb* ; {w and/or r}-pre-bounded |
| 2401 | |
| 2402 | sequence with no post-bounding, and in every case the LKMM also allows |
| 2403 | the link simply to be a fence with no bounding at all. If no sequence |
| 2404 | of the appropriate sort exists, the LKMM says that the accesses race. |
| 2405 | |
| 2406 | There is one more part of the LKMM related to plain accesses (although |
| 2407 | not to data races) we should discuss. Recall that many relations such |
| 2408 | as hb are limited to marked accesses only. As a result, the |
| 2409 | happens-before, propagates-before, and rcu axioms (which state that |
| 2410 | various relation must not contain a cycle) doesn't apply to plain |
| 2411 | accesses. Nevertheless, we do want to rule out such cycles, because |
| 2412 | they don't make sense even for plain accesses. |
| 2413 | |
| 2414 | To this end, the LKMM imposes three extra restrictions, together |
| 2415 | called the "plain-coherence" axiom because of their resemblance to the |
| 2416 | rules used by the operational model to ensure cache coherence (that |
| 2417 | is, the rules governing the memory subsystem's choice of a store to |
| 2418 | satisfy a load request and its determination of where a store will |
| 2419 | fall in the coherence order): |
| 2420 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 2421 | If R and W are race candidates and it is possible to link R to |
| 2422 | W by one of the xb* sequences listed above, then W ->rfe R is |
| 2423 | not allowed (i.e., a load cannot read from a store that it |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2424 | executes before, even if one or both is plain). |
| 2425 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 2426 | If W and R are race candidates and it is possible to link W to |
| 2427 | R by one of the vis sequences listed above, then R ->fre W is |
| 2428 | not allowed (i.e., if a store is visible to a load then the |
| 2429 | load must read from that store or one coherence-after it). |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2430 | |
Marco Elver | c1b1460 | 2020-03-02 18:21:01 +0100 | [diff] [blame] | 2431 | If W and W' are race candidates and it is possible to link W |
| 2432 | to W' by one of the vis sequences listed above, then W' ->co W |
| 2433 | is not allowed (i.e., if one store is visible to a second then |
| 2434 | the second must come after the first in the coherence order). |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2435 | |
| 2436 | This is the extent to which the LKMM deals with plain accesses. |
| 2437 | Perhaps it could say more (for example, plain accesses might |
| 2438 | contribute to the ppo relation), but at the moment it seems that this |
| 2439 | minimal, conservative approach is good enough. |
| 2440 | |
| 2441 | |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 2442 | ODDS AND ENDS |
| 2443 | ------------- |
| 2444 | |
| 2445 | This section covers material that didn't quite fit anywhere in the |
| 2446 | earlier sections. |
| 2447 | |
| 2448 | The descriptions in this document don't always match the formal |
| 2449 | version of the LKMM exactly. For example, the actual formal |
| 2450 | definition of the prop relation makes the initial coe or fre part |
| 2451 | optional, and it doesn't require the events linked by the relation to |
| 2452 | be on the same CPU. These differences are very unimportant; indeed, |
| 2453 | instances where the coe/fre part of prop is missing are of no interest |
| 2454 | because all the other parts (fences and rfe) are already included in |
| 2455 | hb anyway, and where the formal model adds prop into hb, it includes |
| 2456 | an explicit requirement that the events being linked are on the same |
| 2457 | CPU. |
| 2458 | |
| 2459 | Another minor difference has to do with events that are both memory |
| 2460 | accesses and fences, such as those corresponding to smp_load_acquire() |
| 2461 | calls. In the formal model, these events aren't actually both reads |
| 2462 | and fences; rather, they are read events with an annotation marking |
| 2463 | them as acquires. (Or write events annotated as releases, in the case |
| 2464 | smp_store_release().) The final effect is the same. |
| 2465 | |
| 2466 | Although we didn't mention it above, the instruction execution |
| 2467 | ordering provided by the smp_rmb() fence doesn't apply to read events |
| 2468 | that are part of a non-value-returning atomic update. For instance, |
| 2469 | given: |
| 2470 | |
| 2471 | atomic_inc(&x); |
| 2472 | smp_rmb(); |
| 2473 | r1 = READ_ONCE(y); |
| 2474 | |
| 2475 | it is not guaranteed that the load from y will execute after the |
| 2476 | update to x. This is because the ARMv8 architecture allows |
| 2477 | non-value-returning atomic operations effectively to be executed off |
| 2478 | the CPU. Basically, the CPU tells the memory subsystem to increment |
| 2479 | x, and then the increment is carried out by the memory hardware with |
| 2480 | no further involvement from the CPU. Since the CPU doesn't ever read |
| 2481 | the value of x, there is nothing for the smp_rmb() fence to act on. |
| 2482 | |
| 2483 | The LKMM defines a few extra synchronization operations in terms of |
Alan Stern | bf28ae5 | 2018-02-20 15:25:12 -0800 | [diff] [blame] | 2484 | things we have already covered. In particular, rcu_dereference() is |
| 2485 | treated as READ_ONCE() and rcu_assign_pointer() is treated as |
| 2486 | smp_store_release() -- which is basically how the Linux kernel treats |
| 2487 | them. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 2488 | |
Alan Stern | c58a801 | 2019-10-01 13:40:19 -0400 | [diff] [blame] | 2489 | Although we said that plain accesses are not linked by the ppo |
| 2490 | relation, they do contribute to it indirectly. Namely, when there is |
| 2491 | an address dependency from a marked load R to a plain store W, |
| 2492 | followed by smp_wmb() and then a marked store W', the LKMM creates a |
| 2493 | ppo link from R to W'. The reasoning behind this is perhaps a little |
| 2494 | shaky, but essentially it says there is no way to generate object code |
| 2495 | for this source code in which W' could execute before R. Just as with |
| 2496 | pre-bounding by address dependencies, it is possible for the compiler |
| 2497 | to undermine this relation if sufficient care is not taken. |
| 2498 | |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 2499 | There are a few oddball fences which need special treatment: |
| 2500 | smp_mb__before_atomic(), smp_mb__after_atomic(), and |
| 2501 | smp_mb__after_spinlock(). The LKMM uses fence events with special |
| 2502 | annotations for them; they act as strong fences just like smp_mb() |
| 2503 | except for the sets of events that they order. Instead of ordering |
| 2504 | all po-earlier events against all po-later events, as smp_mb() does, |
| 2505 | they behave as follows: |
| 2506 | |
| 2507 | smp_mb__before_atomic() orders all po-earlier events against |
| 2508 | po-later atomic updates and the events following them; |
| 2509 | |
| 2510 | smp_mb__after_atomic() orders po-earlier atomic updates and |
| 2511 | the events preceding them against all po-later events; |
| 2512 | |
Björn Töpel | d25fba0 | 2021-03-05 11:28:23 +0100 | [diff] [blame] | 2513 | smp_mb__after_spinlock() orders po-earlier lock acquisition |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 2514 | events and the events preceding them against all po-later |
| 2515 | events. |
| 2516 | |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 2517 | Interestingly, RCU and locking each introduce the possibility of |
| 2518 | deadlock. When faced with code sequences such as: |
| 2519 | |
| 2520 | spin_lock(&s); |
| 2521 | spin_lock(&s); |
| 2522 | spin_unlock(&s); |
| 2523 | spin_unlock(&s); |
| 2524 | |
| 2525 | or: |
| 2526 | |
| 2527 | rcu_read_lock(); |
| 2528 | synchronize_rcu(); |
| 2529 | rcu_read_unlock(); |
| 2530 | |
| 2531 | what does the LKMM have to say? Answer: It says there are no allowed |
| 2532 | executions at all, which makes sense. But this can also lead to |
| 2533 | misleading results, because if a piece of code has multiple possible |
| 2534 | executions, some of which deadlock, the model will report only on the |
| 2535 | non-deadlocking executions. For example: |
| 2536 | |
| 2537 | int x, y; |
| 2538 | |
| 2539 | P0() |
| 2540 | { |
| 2541 | int r0; |
| 2542 | |
| 2543 | WRITE_ONCE(x, 1); |
| 2544 | r0 = READ_ONCE(y); |
| 2545 | } |
| 2546 | |
| 2547 | P1() |
| 2548 | { |
| 2549 | rcu_read_lock(); |
| 2550 | if (READ_ONCE(x) > 0) { |
| 2551 | WRITE_ONCE(y, 36); |
| 2552 | synchronize_rcu(); |
| 2553 | } |
| 2554 | rcu_read_unlock(); |
| 2555 | } |
| 2556 | |
| 2557 | Is it possible to end up with r0 = 36 at the end? The LKMM will tell |
| 2558 | you it is not, but the model won't mention that this is because P1 |
| 2559 | will self-deadlock in the executions where it stores 36 in y. |