1 Explanation of the Linux-Kernel Memory Consist 1 Explanation of the Linux-Kernel Memory Consistency Model 2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3 3 4 :Author: Alan Stern <stern@rowland.harvard.edu> 4 :Author: Alan Stern <stern@rowland.harvard.edu> 5 :Created: October 2017 5 :Created: October 2017 6 6 7 .. Contents 7 .. Contents 8 8 9 1. INTRODUCTION 9 1. INTRODUCTION 10 2. BACKGROUND 10 2. BACKGROUND 11 3. A SIMPLE EXAMPLE 11 3. A SIMPLE EXAMPLE 12 4. A SELECTION OF MEMORY MODELS 12 4. A SELECTION OF MEMORY MODELS 13 5. ORDERING AND CYCLES 13 5. ORDERING AND CYCLES 14 6. EVENTS 14 6. EVENTS 15 7. THE PROGRAM ORDER RELATION: po AND po-loc 15 7. THE PROGRAM ORDER RELATION: po AND po-loc 16 8. A WARNING 16 8. A WARNING 17 9. DEPENDENCY RELATIONS: data, addr, and ctr 17 9. DEPENDENCY RELATIONS: data, addr, and ctrl 18 10. THE READS-FROM RELATION: rf, rfi, and rf 18 10. THE READS-FROM RELATION: rf, rfi, and rfe 19 11. CACHE COHERENCE AND THE COHERENCE ORDER 19 11. CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe 20 12. THE FROM-READS RELATION: fr, fri, and fr 20 12. THE FROM-READS RELATION: fr, fri, and fre 21 13. AN OPERATIONAL MODEL 21 13. AN OPERATIONAL MODEL 22 14. PROPAGATION ORDER RELATION: cumul-fence 22 14. PROPAGATION ORDER RELATION: cumul-fence 23 15. DERIVATION OF THE LKMM FROM THE OPERATIO 23 15. DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL 24 16. SEQUENTIAL CONSISTENCY PER VARIABLE 24 16. SEQUENTIAL CONSISTENCY PER VARIABLE 25 17. ATOMIC UPDATES: rmw 25 17. ATOMIC UPDATES: rmw 26 18. THE PRESERVED PROGRAM ORDER RELATION: pp 26 18. THE PRESERVED PROGRAM ORDER RELATION: ppo 27 19. AND THEN THERE WAS ALPHA 27 19. AND THEN THERE WAS ALPHA 28 20. THE HAPPENS-BEFORE RELATION: hb 28 20. THE HAPPENS-BEFORE RELATION: hb 29 21. THE PROPAGATES-BEFORE RELATION: pb 29 21. THE PROPAGATES-BEFORE RELATION: pb 30 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rsc 30 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb 31 23. SRCU READ-SIDE CRITICAL SECTIONS !! 31 23. LOCKING 32 24. LOCKING !! 32 24. PLAIN ACCESSES AND DATA RACES 33 25. PLAIN ACCESSES AND DATA RACES !! 33 25. ODDS AND ENDS 34 26. ODDS AND ENDS << 35 34 36 35 37 36 38 INTRODUCTION 37 INTRODUCTION 39 ------------ 38 ------------ 40 39 41 The Linux-kernel memory consistency model (LKM 40 The Linux-kernel memory consistency model (LKMM) is rather complex and 42 obscure. This is particularly evident if you 41 obscure. This is particularly evident if you read through the 43 linux-kernel.bell and linux-kernel.cat files t 42 linux-kernel.bell and linux-kernel.cat files that make up the formal 44 version of the model; they are extremely terse 43 version of the model; they are extremely terse and their meanings are 45 far from clear. 44 far from clear. 46 45 47 This document describes the ideas underlying t 46 This document describes the ideas underlying the LKMM. It is meant 48 for people who want to understand how the mode 47 for people who want to understand how the model was designed. It does 49 not go into the details of the code in the .be 48 not go into the details of the code in the .bell and .cat files; 50 rather, it explains in English what the code e 49 rather, it explains in English what the code expresses symbolically. 51 50 52 Sections 2 (BACKGROUND) through 5 (ORDERING AN 51 Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed 53 toward beginners; they explain what memory con 52 toward beginners; they explain what memory consistency models are and 54 the basic notions shared by all such models. 53 the basic notions shared by all such models. People already familiar 55 with these concepts can skim or skip over them 54 with these concepts can skim or skip over them. Sections 6 (EVENTS) 56 through 12 (THE FROM_READS RELATION) describe 55 through 12 (THE FROM_READS RELATION) describe the fundamental 57 relations used in many models. Starting in Se 56 relations used in many models. Starting in Section 13 (AN OPERATIONAL 58 MODEL), the workings of the LKMM itself are co 57 MODEL), the workings of the LKMM itself are covered. 59 58 60 Warning: The code examples in this document ar 59 Warning: The code examples in this document are not written in the 61 proper format for litmus tests. They don't in 60 proper format for litmus tests. They don't include a header line, the 62 initializations are not enclosed in braces, th 61 initializations are not enclosed in braces, the global variables are 63 not passed by pointers, and they don't have an 62 not passed by pointers, and they don't have an "exists" clause at the 64 end. Converting them to the right format is l 63 end. Converting them to the right format is left as an exercise for 65 the reader. 64 the reader. 66 65 67 66 68 BACKGROUND 67 BACKGROUND 69 ---------- 68 ---------- 70 69 71 A memory consistency model (or just memory mod 70 A memory consistency model (or just memory model, for short) is 72 something which predicts, given a piece of com 71 something which predicts, given a piece of computer code running on a 73 particular kind of system, what values may be 72 particular kind of system, what values may be obtained by the code's 74 load instructions. The LKMM makes these predi 73 load instructions. The LKMM makes these predictions for code running 75 as part of the Linux kernel. 74 as part of the Linux kernel. 76 75 77 In practice, people tend to use memory models 76 In practice, people tend to use memory models the other way around. 78 That is, given a piece of code and a collectio 77 That is, given a piece of code and a collection of values specified 79 for the loads, the model will predict whether 78 for the loads, the model will predict whether it is possible for the 80 code to run in such a way that the loads will 79 code to run in such a way that the loads will indeed obtain the 81 specified values. Of course, this is just ano 80 specified values. Of course, this is just another way of expressing 82 the same idea. 81 the same idea. 83 82 84 For code running on a uniprocessor system, the 83 For code running on a uniprocessor system, the predictions are easy: 85 Each load instruction must obtain the value wr 84 Each load instruction must obtain the value written by the most recent 86 store instruction accessing the same location 85 store instruction accessing the same location (we ignore complicating 87 factors such as DMA and mixed-size accesses.) 86 factors such as DMA and mixed-size accesses.) But on multiprocessor 88 systems, with multiple CPUs making concurrent 87 systems, with multiple CPUs making concurrent accesses to shared 89 memory locations, things aren't so simple. 88 memory locations, things aren't so simple. 90 89 91 Different architectures have differing memory 90 Different architectures have differing memory models, and the Linux 92 kernel supports a variety of architectures. T 91 kernel supports a variety of architectures. The LKMM has to be fairly 93 permissive, in the sense that any behavior all 92 permissive, in the sense that any behavior allowed by one of these 94 architectures also has to be allowed by the LK 93 architectures also has to be allowed by the LKMM. 95 94 96 95 97 A SIMPLE EXAMPLE 96 A SIMPLE EXAMPLE 98 ---------------- 97 ---------------- 99 98 100 Here is a simple example to illustrate the bas 99 Here is a simple example to illustrate the basic concepts. Consider 101 some code running as part of a device driver f 100 some code running as part of a device driver for an input device. The 102 driver might contain an interrupt handler whic 101 driver might contain an interrupt handler which collects data from the 103 device, stores it in a buffer, and sets a flag 102 device, stores it in a buffer, and sets a flag to indicate the buffer 104 is full. Running concurrently on a different 103 is full. Running concurrently on a different CPU might be a part of 105 the driver code being executed by a process in 104 the driver code being executed by a process in the midst of a read(2) 106 system call. This code tests the flag to see 105 system call. This code tests the flag to see whether the buffer is 107 ready, and if it is, copies the data back to u 106 ready, and if it is, copies the data back to userspace. The buffer 108 and the flag are memory locations shared betwe 107 and the flag are memory locations shared between the two CPUs. 109 108 110 We can abstract out the important pieces of th 109 We can abstract out the important pieces of the driver code as follows 111 (the reason for using WRITE_ONCE() and READ_ON 110 (the reason for using WRITE_ONCE() and READ_ONCE() instead of simple 112 assignment statements is discussed later): 111 assignment statements is discussed later): 113 112 114 int buf = 0, flag = 0; 113 int buf = 0, flag = 0; 115 114 116 P0() 115 P0() 117 { 116 { 118 WRITE_ONCE(buf, 1); 117 WRITE_ONCE(buf, 1); 119 WRITE_ONCE(flag, 1); 118 WRITE_ONCE(flag, 1); 120 } 119 } 121 120 122 P1() 121 P1() 123 { 122 { 124 int r1; 123 int r1; 125 int r2 = 0; 124 int r2 = 0; 126 125 127 r1 = READ_ONCE(flag); 126 r1 = READ_ONCE(flag); 128 if (r1) 127 if (r1) 129 r2 = READ_ONCE(buf); 128 r2 = READ_ONCE(buf); 130 } 129 } 131 130 132 Here the P0() function represents the interrup 131 Here the P0() function represents the interrupt handler running on one 133 CPU and P1() represents the read() routine run 132 CPU and P1() represents the read() routine running on another. The 134 value 1 stored in buf represents input data co 133 value 1 stored in buf represents input data collected from the device. 135 Thus, P0 stores the data in buf and then sets 134 Thus, P0 stores the data in buf and then sets flag. Meanwhile, P1 136 reads flag into the private variable r1, and i 135 reads flag into the private variable r1, and if it is set, reads the 137 data from buf into a second private variable r 136 data from buf into a second private variable r2 for copying to 138 userspace. (Presumably if flag is not set the 137 userspace. (Presumably if flag is not set then the driver will wait a 139 while and try again.) 138 while and try again.) 140 139 141 This pattern of memory accesses, where one CPU 140 This pattern of memory accesses, where one CPU stores values to two 142 shared memory locations and another CPU loads 141 shared memory locations and another CPU loads from those locations in 143 the opposite order, is widely known as the "Me 142 the opposite order, is widely known as the "Message Passing" or MP 144 pattern. It is typical of memory access patte 143 pattern. It is typical of memory access patterns in the kernel. 145 144 146 Please note that this example code is a simpli 145 Please note that this example code is a simplified abstraction. Real 147 buffers are usually larger than a single integ 146 buffers are usually larger than a single integer, real device drivers 148 usually use sleep and wakeup mechanisms rather 147 usually use sleep and wakeup mechanisms rather than polling for I/O 149 completion, and real code generally doesn't bo 148 completion, and real code generally doesn't bother to copy values into 150 private variables before using them. All that 149 private variables before using them. All that is beside the point; 151 the idea here is simply to illustrate the over 150 the idea here is simply to illustrate the overall pattern of memory 152 accesses by the CPUs. 151 accesses by the CPUs. 153 152 154 A memory model will predict what values P1 mig 153 A memory model will predict what values P1 might obtain for its loads 155 from flag and buf, or equivalently, what value 154 from flag and buf, or equivalently, what values r1 and r2 might end up 156 with after the code has finished running. 155 with after the code has finished running. 157 156 158 Some predictions are trivial. For instance, n 157 Some predictions are trivial. For instance, no sane memory model would 159 predict that r1 = 42 or r2 = -7, because neith 158 predict that r1 = 42 or r2 = -7, because neither of those values ever 160 gets stored in flag or buf. 159 gets stored in flag or buf. 161 160 162 Some nontrivial predictions are nonetheless qu 161 Some nontrivial predictions are nonetheless quite simple. For 163 instance, P1 might run entirely before P0 begi 162 instance, P1 might run entirely before P0 begins, in which case r1 and 164 r2 will both be 0 at the end. Or P0 might run 163 r2 will both be 0 at the end. Or P0 might run entirely before P1 165 begins, in which case r1 and r2 will both be 1 164 begins, in which case r1 and r2 will both be 1. 166 165 167 The interesting predictions concern what might 166 The interesting predictions concern what might happen when the two 168 routines run concurrently. One possibility is 167 routines run concurrently. One possibility is that P1 runs after P0's 169 store to buf but before the store to flag. In 168 store to buf but before the store to flag. In this case, r1 and r2 170 will again both be 0. (If P1 had been designe 169 will again both be 0. (If P1 had been designed to read buf 171 unconditionally then we would instead have r1 170 unconditionally then we would instead have r1 = 0 and r2 = 1.) 172 171 173 However, the most interesting possibility is w 172 However, the most interesting possibility is where r1 = 1 and r2 = 0. 174 If this were to occur it would mean the driver 173 If this were to occur it would mean the driver contains a bug, because 175 incorrect data would get sent to the user: 0 i 174 incorrect data would get sent to the user: 0 instead of 1. As it 176 happens, the LKMM does predict this outcome ca 175 happens, the LKMM does predict this outcome can occur, and the example 177 driver code shown above is indeed buggy. 176 driver code shown above is indeed buggy. 178 177 179 178 180 A SELECTION OF MEMORY MODELS 179 A SELECTION OF MEMORY MODELS 181 ---------------------------- 180 ---------------------------- 182 181 183 The first widely cited memory model, and the s 182 The first widely cited memory model, and the simplest to understand, 184 is Sequential Consistency. According to this 183 is Sequential Consistency. According to this model, systems behave as 185 if each CPU executed its instructions in order 184 if each CPU executed its instructions in order but with unspecified 186 timing. In other words, the instructions from 185 timing. In other words, the instructions from the various CPUs get 187 interleaved in a nondeterministic way, always 186 interleaved in a nondeterministic way, always according to some single 188 global order that agrees with the order of the 187 global order that agrees with the order of the instructions in the 189 program source for each CPU. The model says t 188 program source for each CPU. The model says that the value obtained 190 by each load is simply the value written by th 189 by each load is simply the value written by the most recently executed 191 store to the same memory location, from any CP 190 store to the same memory location, from any CPU. 192 191 193 For the MP example code shown above, Sequentia 192 For the MP example code shown above, Sequential Consistency predicts 194 that the undesired result r1 = 1, r2 = 0 canno 193 that the undesired result r1 = 1, r2 = 0 cannot occur. The reasoning 195 goes like this: 194 goes like this: 196 195 197 Since r1 = 1, P0 must store 1 to flag 196 Since r1 = 1, P0 must store 1 to flag before P1 loads 1 from 198 it, as loads can obtain values only fr 197 it, as loads can obtain values only from earlier stores. 199 198 200 P1 loads from flag before loading from 199 P1 loads from flag before loading from buf, since CPUs execute 201 their instructions in order. 200 their instructions in order. 202 201 203 P1 must load 0 from buf before P0 stor 202 P1 must load 0 from buf before P0 stores 1 to it; otherwise r2 204 would be 1 since a load obtains its va 203 would be 1 since a load obtains its value from the most recent 205 store to the same address. 204 store to the same address. 206 205 207 P0 stores 1 to buf before storing 1 to 206 P0 stores 1 to buf before storing 1 to flag, since it executes 208 its instructions in order. 207 its instructions in order. 209 208 210 Since an instruction (in this case, P0 209 Since an instruction (in this case, P0's store to flag) cannot 211 execute before itself, the specified o 210 execute before itself, the specified outcome is impossible. 212 211 213 However, real computer hardware almost never f 212 However, real computer hardware almost never follows the Sequential 214 Consistency memory model; doing so would rule 213 Consistency memory model; doing so would rule out too many valuable 215 performance optimizations. On ARM and PowerPC 214 performance optimizations. On ARM and PowerPC architectures, for 216 instance, the MP example code really does some 215 instance, the MP example code really does sometimes yield r1 = 1 and 217 r2 = 0. 216 r2 = 0. 218 217 219 x86 and SPARC follow yet a different memory mo 218 x86 and SPARC follow yet a different memory model: TSO (Total Store 220 Ordering). This model predicts that the undes 219 Ordering). This model predicts that the undesired outcome for the MP 221 pattern cannot occur, but in other respects it 220 pattern cannot occur, but in other respects it differs from Sequential 222 Consistency. One example is the Store Buffer 221 Consistency. One example is the Store Buffer (SB) pattern, in which 223 each CPU stores to its own shared location and 222 each CPU stores to its own shared location and then loads from the 224 other CPU's location: 223 other CPU's location: 225 224 226 int x = 0, y = 0; 225 int x = 0, y = 0; 227 226 228 P0() 227 P0() 229 { 228 { 230 int r0; 229 int r0; 231 230 232 WRITE_ONCE(x, 1); 231 WRITE_ONCE(x, 1); 233 r0 = READ_ONCE(y); 232 r0 = READ_ONCE(y); 234 } 233 } 235 234 236 P1() 235 P1() 237 { 236 { 238 int r1; 237 int r1; 239 238 240 WRITE_ONCE(y, 1); 239 WRITE_ONCE(y, 1); 241 r1 = READ_ONCE(x); 240 r1 = READ_ONCE(x); 242 } 241 } 243 242 244 Sequential Consistency predicts that the outco 243 Sequential Consistency predicts that the outcome r0 = 0, r1 = 0 is 245 impossible. (Exercise: Figure out the reasoni 244 impossible. (Exercise: Figure out the reasoning.) But TSO allows 246 this outcome to occur, and in fact it does som 245 this outcome to occur, and in fact it does sometimes occur on x86 and 247 SPARC systems. 246 SPARC systems. 248 247 249 The LKMM was inspired by the memory models fol 248 The LKMM was inspired by the memory models followed by PowerPC, ARM, 250 x86, Alpha, and other architectures. However, 249 x86, Alpha, and other architectures. However, it is different in 251 detail from each of them. 250 detail from each of them. 252 251 253 252 254 ORDERING AND CYCLES 253 ORDERING AND CYCLES 255 ------------------- 254 ------------------- 256 255 257 Memory models are all about ordering. Often t 256 Memory models are all about ordering. Often this is temporal ordering 258 (i.e., the order in which certain events occur 257 (i.e., the order in which certain events occur) but it doesn't have to 259 be; consider for example the order of instruct 258 be; consider for example the order of instructions in a program's 260 source code. We saw above that Sequential Con 259 source code. We saw above that Sequential Consistency makes an 261 important assumption that CPUs execute instruc 260 important assumption that CPUs execute instructions in the same order 262 as those instructions occur in the code, and t 261 as those instructions occur in the code, and there are many other 263 instances of ordering playing central roles in 262 instances of ordering playing central roles in memory models. 264 263 265 The counterpart to ordering is a cycle. Order 264 The counterpart to ordering is a cycle. Ordering rules out cycles: 266 It's not possible to have X ordered before Y, 265 It's not possible to have X ordered before Y, Y ordered before Z, and 267 Z ordered before X, because this would mean th 266 Z ordered before X, because this would mean that X is ordered before 268 itself. The analysis of the MP example under 267 itself. The analysis of the MP example under Sequential Consistency 269 involved just such an impossible cycle: 268 involved just such an impossible cycle: 270 269 271 W: P0 stores 1 to flag executes befo 270 W: P0 stores 1 to flag executes before 272 X: P1 loads 1 from flag executes befo 271 X: P1 loads 1 from flag executes before 273 Y: P1 loads 0 from buf executes befo 272 Y: P1 loads 0 from buf executes before 274 Z: P0 stores 1 to buf executes befo 273 Z: P0 stores 1 to buf executes before 275 W: P0 stores 1 to flag. 274 W: P0 stores 1 to flag. 276 275 277 In short, if a memory model requires certain a 276 In short, if a memory model requires certain accesses to be ordered, 278 and a certain outcome for the loads in a piece 277 and a certain outcome for the loads in a piece of code can happen only 279 if those accesses would form a cycle, then the 278 if those accesses would form a cycle, then the memory model predicts 280 that outcome cannot occur. 279 that outcome cannot occur. 281 280 282 The LKMM is defined largely in terms of cycles 281 The LKMM is defined largely in terms of cycles, as we will see. 283 282 284 283 285 EVENTS 284 EVENTS 286 ------ 285 ------ 287 286 288 The LKMM does not work directly with the C sta 287 The LKMM does not work directly with the C statements that make up 289 kernel source code. Instead it considers the 288 kernel source code. Instead it considers the effects of those 290 statements in a more abstract form, namely, ev 289 statements in a more abstract form, namely, events. The model 291 includes three types of events: 290 includes three types of events: 292 291 293 Read events correspond to loads from s 292 Read events correspond to loads from shared memory, such as 294 calls to READ_ONCE(), smp_load_acquire 293 calls to READ_ONCE(), smp_load_acquire(), or 295 rcu_dereference(). 294 rcu_dereference(). 296 295 297 Write events correspond to stores to s 296 Write events correspond to stores to shared memory, such as 298 calls to WRITE_ONCE(), smp_store_relea 297 calls to WRITE_ONCE(), smp_store_release(), or atomic_set(). 299 298 300 Fence events correspond to memory barr 299 Fence events correspond to memory barriers (also known as 301 fences), such as calls to smp_rmb() or 300 fences), such as calls to smp_rmb() or rcu_read_lock(). 302 301 303 These categories are not exclusive; a read or 302 These categories are not exclusive; a read or write event can also be 304 a fence. This happens with functions like smp 303 a fence. This happens with functions like smp_load_acquire() or 305 spin_lock(). However, no single event can be 304 spin_lock(). However, no single event can be both a read and a write. 306 Atomic read-modify-write accesses, such as ato 305 Atomic read-modify-write accesses, such as atomic_inc() or xchg(), 307 correspond to a pair of events: a read followe 306 correspond to a pair of events: a read followed by a write. (The 308 write event is omitted for executions where it 307 write event is omitted for executions where it doesn't occur, such as 309 a cmpxchg() where the comparison fails.) 308 a cmpxchg() where the comparison fails.) 310 309 311 Other parts of the code, those which do not in 310 Other parts of the code, those which do not involve interaction with 312 shared memory, do not give rise to events. Th 311 shared memory, do not give rise to events. Thus, arithmetic and 313 logical computations, control-flow instruction 312 logical computations, control-flow instructions, or accesses to 314 private memory or CPU registers are not of cen 313 private memory or CPU registers are not of central interest to the 315 memory model. They only affect the model's pr 314 memory model. They only affect the model's predictions indirectly. 316 For example, an arithmetic computation might d 315 For example, an arithmetic computation might determine the value that 317 gets stored to a shared memory location (or in 316 gets stored to a shared memory location (or in the case of an array 318 index, the address where the value gets stored 317 index, the address where the value gets stored), but the memory model 319 is concerned only with the store itself -- its 318 is concerned only with the store itself -- its value and its address 320 -- not the computation leading up to it. 319 -- not the computation leading up to it. 321 320 322 Events in the LKMM can be linked by various re 321 Events in the LKMM can be linked by various relations, which we will 323 describe in the following sections. The memor 322 describe in the following sections. The memory model requires certain 324 of these relations to be orderings, that is, i 323 of these relations to be orderings, that is, it requires them not to 325 have any cycles. 324 have any cycles. 326 325 327 326 328 THE PROGRAM ORDER RELATION: po AND po-loc 327 THE PROGRAM ORDER RELATION: po AND po-loc 329 ----------------------------------------- 328 ----------------------------------------- 330 329 331 The most important relation between events is 330 The most important relation between events is program order (po). You 332 can think of it as the order in which statemen 331 can think of it as the order in which statements occur in the source 333 code after branches are taken into account and 332 code after branches are taken into account and loops have been 334 unrolled. A better description might be the o 333 unrolled. A better description might be the order in which 335 instructions are presented to a CPU's executio 334 instructions are presented to a CPU's execution unit. Thus, we say 336 that X is po-before Y (written as "X ->po Y" i 335 that X is po-before Y (written as "X ->po Y" in formulas) if X occurs 337 before Y in the instruction stream. 336 before Y in the instruction stream. 338 337 339 This is inherently a single-CPU relation; two 338 This is inherently a single-CPU relation; two instructions executing 340 on different CPUs are never linked by po. Als 339 on different CPUs are never linked by po. Also, it is by definition 341 an ordering so it cannot have any cycles. 340 an ordering so it cannot have any cycles. 342 341 343 po-loc is a sub-relation of po. It links two 342 po-loc is a sub-relation of po. It links two memory accesses when the 344 first comes before the second in program order 343 first comes before the second in program order and they access the 345 same memory location (the "-loc" suffix). 344 same memory location (the "-loc" suffix). 346 345 347 Although this may seem straightforward, there 346 Although this may seem straightforward, there is one subtle aspect to 348 program order we need to explain. The LKMM wa 347 program order we need to explain. The LKMM was inspired by low-level 349 architectural memory models which describe the 348 architectural memory models which describe the behavior of machine 350 code, and it retains their outlook to a consid 349 code, and it retains their outlook to a considerable extent. The 351 read, write, and fence events used by the mode 350 read, write, and fence events used by the model are close in spirit to 352 individual machine instructions. Nevertheless 351 individual machine instructions. Nevertheless, the LKMM describes 353 kernel code written in C, and the mapping from 352 kernel code written in C, and the mapping from C to machine code can 354 be extremely complex. 353 be extremely complex. 355 354 356 Optimizing compilers have great freedom in the 355 Optimizing compilers have great freedom in the way they translate 357 source code to object code. They are allowed 356 source code to object code. They are allowed to apply transformations 358 that add memory accesses, eliminate accesses, 357 that add memory accesses, eliminate accesses, combine them, split them 359 into pieces, or move them around. The use of 358 into pieces, or move them around. The use of READ_ONCE(), WRITE_ONCE(), 360 or one of the other atomic or synchronization 359 or one of the other atomic or synchronization primitives prevents a 361 large number of compiler optimizations. In pa 360 large number of compiler optimizations. In particular, it is guaranteed 362 that the compiler will not remove such accesse 361 that the compiler will not remove such accesses from the generated code 363 (unless it can prove the accesses will never b 362 (unless it can prove the accesses will never be executed), it will not 364 change the order in which they occur in the co 363 change the order in which they occur in the code (within limits imposed 365 by the C standard), and it will not introduce 364 by the C standard), and it will not introduce extraneous accesses. 366 365 367 The MP and SB examples above used READ_ONCE() 366 The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather 368 than ordinary memory accesses. Thanks to this 367 than ordinary memory accesses. Thanks to this usage, we can be certain 369 that in the MP example, the compiler won't reo 368 that in the MP example, the compiler won't reorder P0's write event to 370 buf and P0's write event to flag, and similarl 369 buf and P0's write event to flag, and similarly for the other shared 371 memory accesses in the examples. 370 memory accesses in the examples. 372 371 373 Since private variables are not shared between 372 Since private variables are not shared between CPUs, they can be 374 accessed normally without READ_ONCE() or WRITE 373 accessed normally without READ_ONCE() or WRITE_ONCE(). In fact, they 375 need not even be stored in normal memory at al 374 need not even be stored in normal memory at all -- in principle a 376 private variable could be stored in a CPU regi 375 private variable could be stored in a CPU register (hence the convention 377 that these variables have names starting with 376 that these variables have names starting with the letter 'r'). 378 377 379 378 380 A WARNING 379 A WARNING 381 --------- 380 --------- 382 381 383 The protections provided by READ_ONCE(), WRITE 382 The protections provided by READ_ONCE(), WRITE_ONCE(), and others are 384 not perfect; and under some circumstances it i 383 not perfect; and under some circumstances it is possible for the 385 compiler to undermine the memory model. Here 384 compiler to undermine the memory model. Here is an example. Suppose 386 both branches of an "if" statement store the s 385 both branches of an "if" statement store the same value to the same 387 location: 386 location: 388 387 389 r1 = READ_ONCE(x); 388 r1 = READ_ONCE(x); 390 if (r1) { 389 if (r1) { 391 WRITE_ONCE(y, 2); 390 WRITE_ONCE(y, 2); 392 ... /* do something */ 391 ... /* do something */ 393 } else { 392 } else { 394 WRITE_ONCE(y, 2); 393 WRITE_ONCE(y, 2); 395 ... /* do something else */ 394 ... /* do something else */ 396 } 395 } 397 396 398 For this code, the LKMM predicts that the load 397 For this code, the LKMM predicts that the load from x will always be 399 executed before either of the stores to y. Ho 398 executed before either of the stores to y. However, a compiler could 400 lift the stores out of the conditional, transf 399 lift the stores out of the conditional, transforming the code into 401 something resembling: 400 something resembling: 402 401 403 r1 = READ_ONCE(x); 402 r1 = READ_ONCE(x); 404 WRITE_ONCE(y, 2); 403 WRITE_ONCE(y, 2); 405 if (r1) { 404 if (r1) { 406 ... /* do something */ 405 ... /* do something */ 407 } else { 406 } else { 408 ... /* do something else */ 407 ... /* do something else */ 409 } 408 } 410 409 411 Given this version of the code, the LKMM would 410 Given this version of the code, the LKMM would predict that the load 412 from x could be executed after the store to y. 411 from x could be executed after the store to y. Thus, the memory 413 model's original prediction could be invalidat 412 model's original prediction could be invalidated by the compiler. 414 413 415 Another issue arises from the fact that in C, 414 Another issue arises from the fact that in C, arguments to many 416 operators and function calls can be evaluated 415 operators and function calls can be evaluated in any order. For 417 example: 416 example: 418 417 419 r1 = f(5) + g(6); 418 r1 = f(5) + g(6); 420 419 421 The object code might call f(5) either before 420 The object code might call f(5) either before or after g(6); the 422 memory model cannot assume there is a fixed pr 421 memory model cannot assume there is a fixed program order relation 423 between them. (In fact, if the function calls 422 between them. (In fact, if the function calls are inlined then the 424 compiler might even interleave their object co 423 compiler might even interleave their object code.) 425 424 426 425 427 DEPENDENCY RELATIONS: data, addr, and ctrl 426 DEPENDENCY RELATIONS: data, addr, and ctrl 428 ------------------------------------------ 427 ------------------------------------------ 429 428 430 We say that two events are linked by a depende 429 We say that two events are linked by a dependency relation when the 431 execution of the second event depends in some 430 execution of the second event depends in some way on a value obtained 432 from memory by the first. The first event mus 431 from memory by the first. The first event must be a read, and the 433 value it obtains must somehow affect what the 432 value it obtains must somehow affect what the second event does. 434 There are three kinds of dependencies: data, a 433 There are three kinds of dependencies: data, address (addr), and 435 control (ctrl). 434 control (ctrl). 436 435 437 A read and a write event are linked by a data 436 A read and a write event are linked by a data dependency if the value 438 obtained by the read affects the value stored 437 obtained by the read affects the value stored by the write. As a very 439 simple example: 438 simple example: 440 439 441 int x, y; 440 int x, y; 442 441 443 r1 = READ_ONCE(x); 442 r1 = READ_ONCE(x); 444 WRITE_ONCE(y, r1 + 5); 443 WRITE_ONCE(y, r1 + 5); 445 444 446 The value stored by the WRITE_ONCE obviously d 445 The value stored by the WRITE_ONCE obviously depends on the value 447 loaded by the READ_ONCE. Such dependencies ca 446 loaded by the READ_ONCE. Such dependencies can wind through 448 arbitrarily complicated computations, and a wr 447 arbitrarily complicated computations, and a write can depend on the 449 values of multiple reads. 448 values of multiple reads. 450 449 451 A read event and another memory access event a 450 A read event and another memory access event are linked by an address 452 dependency if the value obtained by the read a 451 dependency if the value obtained by the read affects the location 453 accessed by the other event. The second event 452 accessed by the other event. The second event can be either a read or 454 a write. Here's another simple example: 453 a write. Here's another simple example: 455 454 456 int a[20]; 455 int a[20]; 457 int i; 456 int i; 458 457 459 r1 = READ_ONCE(i); 458 r1 = READ_ONCE(i); 460 r2 = READ_ONCE(a[r1]); 459 r2 = READ_ONCE(a[r1]); 461 460 462 Here the location accessed by the second READ_ 461 Here the location accessed by the second READ_ONCE() depends on the 463 index value loaded by the first. Pointer indi 462 index value loaded by the first. Pointer indirection also gives rise 464 to address dependencies, since the address of 463 to address dependencies, since the address of a location accessed 465 through a pointer will depend on the value rea 464 through a pointer will depend on the value read earlier from that 466 pointer. 465 pointer. 467 466 468 Finally, a read event X and a write event Y ar 467 Finally, a read event X and a write event Y are linked by a control 469 dependency if Y syntactically lies within an a 468 dependency if Y syntactically lies within an arm of an if statement and 470 X affects the evaluation of the if condition v 469 X affects the evaluation of the if condition via a data or address 471 dependency (or similarly for a switch statemen 470 dependency (or similarly for a switch statement). Simple example: 472 471 473 int x, y; 472 int x, y; 474 473 475 r1 = READ_ONCE(x); 474 r1 = READ_ONCE(x); 476 if (r1) 475 if (r1) 477 WRITE_ONCE(y, 1984); 476 WRITE_ONCE(y, 1984); 478 477 479 Execution of the WRITE_ONCE() is controlled by 478 Execution of the WRITE_ONCE() is controlled by a conditional expression 480 which depends on the value obtained by the REA 479 which depends on the value obtained by the READ_ONCE(); hence there is 481 a control dependency from the load to the stor 480 a control dependency from the load to the store. 482 481 483 It should be pretty obvious that events can on 482 It should be pretty obvious that events can only depend on reads that 484 come earlier in program order. Symbolically, 483 come earlier in program order. Symbolically, if we have R ->data X, 485 R ->addr X, or R ->ctrl X (where R is a read e 484 R ->addr X, or R ->ctrl X (where R is a read event), then we must also 486 have R ->po X. It wouldn't make sense for a c 485 have R ->po X. It wouldn't make sense for a computation to depend 487 somehow on a value that doesn't get loaded fro 486 somehow on a value that doesn't get loaded from shared memory until 488 later in the code! 487 later in the code! 489 488 490 Here's a trick question: When is a dependency 489 Here's a trick question: When is a dependency not a dependency? Answer: 491 When it is purely syntactic rather than semant 490 When it is purely syntactic rather than semantic. We say a dependency 492 between two accesses is purely syntactic if th 491 between two accesses is purely syntactic if the second access doesn't 493 actually depend on the result of the first. H 492 actually depend on the result of the first. Here is a trivial example: 494 493 495 r1 = READ_ONCE(x); 494 r1 = READ_ONCE(x); 496 WRITE_ONCE(y, r1 * 0); 495 WRITE_ONCE(y, r1 * 0); 497 496 498 There appears to be a data dependency from the 497 There appears to be a data dependency from the load of x to the store 499 of y, since the value to be stored is computed 498 of y, since the value to be stored is computed from the value that was 500 loaded. But in fact, the value stored does no 499 loaded. But in fact, the value stored does not really depend on 501 anything since it will always be 0. Thus the 500 anything since it will always be 0. Thus the data dependency is only 502 syntactic (it appears to exist in the code) bu 501 syntactic (it appears to exist in the code) but not semantic (the 503 second access will always be the same, regardl 502 second access will always be the same, regardless of the value of the 504 first access). Given code like this, a compil 503 first access). Given code like this, a compiler could simply discard 505 the value returned by the load from x, which w 504 the value returned by the load from x, which would certainly destroy 506 any dependency. (The compiler is not permitte 505 any dependency. (The compiler is not permitted to eliminate entirely 507 the load generated for a READ_ONCE() -- that's 506 the load generated for a READ_ONCE() -- that's one of the nice 508 properties of READ_ONCE() -- but it is allowed 507 properties of READ_ONCE() -- but it is allowed to ignore the load's 509 value.) 508 value.) 510 509 511 It's natural to object that no one in their ri 510 It's natural to object that no one in their right mind would write 512 code like the above. However, macro expansion 511 code like the above. However, macro expansions can easily give rise 513 to this sort of thing, in ways that often are 512 to this sort of thing, in ways that often are not apparent to the 514 programmer. 513 programmer. 515 514 516 Another mechanism that can lead to purely synt 515 Another mechanism that can lead to purely syntactic dependencies is 517 related to the notion of "undefined behavior". 516 related to the notion of "undefined behavior". Certain program 518 behaviors are called "undefined" in the C lang 517 behaviors are called "undefined" in the C language specification, 519 which means that when they occur there are no 518 which means that when they occur there are no guarantees at all about 520 the outcome. Consider the following example: 519 the outcome. Consider the following example: 521 520 522 int a[1]; 521 int a[1]; 523 int i; 522 int i; 524 523 525 r1 = READ_ONCE(i); 524 r1 = READ_ONCE(i); 526 r2 = READ_ONCE(a[r1]); 525 r2 = READ_ONCE(a[r1]); 527 526 528 Access beyond the end or before the beginning 527 Access beyond the end or before the beginning of an array is one kind 529 of undefined behavior. Therefore the compiler 528 of undefined behavior. Therefore the compiler doesn't have to worry 530 about what will happen if r1 is nonzero, and i 529 about what will happen if r1 is nonzero, and it can assume that r1 531 will always be zero regardless of the value ac 530 will always be zero regardless of the value actually loaded from i. 532 (If the assumption turns out to be wrong the r 531 (If the assumption turns out to be wrong the resulting behavior will 533 be undefined anyway, so the compiler doesn't c 532 be undefined anyway, so the compiler doesn't care!) Thus the value 534 from the load can be discarded, breaking the a 533 from the load can be discarded, breaking the address dependency. 535 534 536 The LKMM is unaware that purely syntactic depe 535 The LKMM is unaware that purely syntactic dependencies are different 537 from semantic dependencies and therefore mista 536 from semantic dependencies and therefore mistakenly predicts that the 538 accesses in the two examples above will be ord 537 accesses in the two examples above will be ordered. This is another 539 example of how the compiler can undermine the 538 example of how the compiler can undermine the memory model. Be warned. 540 539 541 540 542 THE READS-FROM RELATION: rf, rfi, and rfe 541 THE READS-FROM RELATION: rf, rfi, and rfe 543 ----------------------------------------- 542 ----------------------------------------- 544 543 545 The reads-from relation (rf) links a write eve 544 The reads-from relation (rf) links a write event to a read event when 546 the value loaded by the read is the value that 545 the value loaded by the read is the value that was stored by the 547 write. In colloquial terms, the load "reads f 546 write. In colloquial terms, the load "reads from" the store. We 548 write W ->rf R to indicate that the load R rea 547 write W ->rf R to indicate that the load R reads from the store W. We 549 further distinguish the cases where the load a 548 further distinguish the cases where the load and the store occur on 550 the same CPU (internal reads-from, or rfi) and 549 the same CPU (internal reads-from, or rfi) and where they occur on 551 different CPUs (external reads-from, or rfe). 550 different CPUs (external reads-from, or rfe). 552 551 553 For our purposes, a memory location's initial 552 For our purposes, a memory location's initial value is treated as 554 though it had been written there by an imagina 553 though it had been written there by an imaginary initial store that 555 executes on a separate CPU before the main pro 554 executes on a separate CPU before the main program runs. 556 555 557 Usage of the rf relation implicitly assumes th 556 Usage of the rf relation implicitly assumes that loads will always 558 read from a single store. It doesn't apply pr 557 read from a single store. It doesn't apply properly in the presence 559 of load-tearing, where a load obtains some of 558 of load-tearing, where a load obtains some of its bits from one store 560 and some of them from another store. Fortunat 559 and some of them from another store. Fortunately, use of READ_ONCE() 561 and WRITE_ONCE() will prevent load-tearing; it 560 and WRITE_ONCE() will prevent load-tearing; it's not possible to have: 562 561 563 int x = 0; 562 int x = 0; 564 563 565 P0() 564 P0() 566 { 565 { 567 WRITE_ONCE(x, 0x1234); 566 WRITE_ONCE(x, 0x1234); 568 } 567 } 569 568 570 P1() 569 P1() 571 { 570 { 572 int r1; 571 int r1; 573 572 574 r1 = READ_ONCE(x); 573 r1 = READ_ONCE(x); 575 } 574 } 576 575 577 and end up with r1 = 0x1200 (partly from x's i 576 and end up with r1 = 0x1200 (partly from x's initial value and partly 578 from the value stored by P0). 577 from the value stored by P0). 579 578 580 On the other hand, load-tearing is unavoidable 579 On the other hand, load-tearing is unavoidable when mixed-size 581 accesses are used. Consider this example: 580 accesses are used. Consider this example: 582 581 583 union { 582 union { 584 u32 w; 583 u32 w; 585 u16 h[2]; 584 u16 h[2]; 586 } x; 585 } x; 587 586 588 P0() 587 P0() 589 { 588 { 590 WRITE_ONCE(x.h[0], 0x1234); 589 WRITE_ONCE(x.h[0], 0x1234); 591 WRITE_ONCE(x.h[1], 0x5678); 590 WRITE_ONCE(x.h[1], 0x5678); 592 } 591 } 593 592 594 P1() 593 P1() 595 { 594 { 596 int r1; 595 int r1; 597 596 598 r1 = READ_ONCE(x.w); 597 r1 = READ_ONCE(x.w); 599 } 598 } 600 599 601 If r1 = 0x56781234 (little-endian!) at the end 600 If r1 = 0x56781234 (little-endian!) at the end, then P1 must have read 602 from both of P0's stores. It is possible to h 601 from both of P0's stores. It is possible to handle mixed-size and 603 unaligned accesses in a memory model, but the 602 unaligned accesses in a memory model, but the LKMM currently does not 604 attempt to do so. It requires all accesses to 603 attempt to do so. It requires all accesses to be properly aligned and 605 of the location's actual size. 604 of the location's actual size. 606 605 607 606 608 CACHE COHERENCE AND THE COHERENCE ORDER RELATI 607 CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe 609 ---------------------------------------------- 608 ------------------------------------------------------------------ 610 609 611 Cache coherence is a general principle requiri 610 Cache coherence is a general principle requiring that in a 612 multi-processor system, the CPUs must share a 611 multi-processor system, the CPUs must share a consistent view of the 613 memory contents. Specifically, it requires th 612 memory contents. Specifically, it requires that for each location in 614 shared memory, the stores to that location mus 613 shared memory, the stores to that location must form a single global 615 ordering which all the CPUs agree on (the cohe 614 ordering which all the CPUs agree on (the coherence order), and this 616 ordering must be consistent with the program o 615 ordering must be consistent with the program order for accesses to 617 that location. 616 that location. 618 617 619 To put it another way, for any variable x, the 618 To put it another way, for any variable x, the coherence order (co) of 620 the stores to x is simply the order in which t 619 the stores to x is simply the order in which the stores overwrite one 621 another. The imaginary store which establishe 620 another. The imaginary store which establishes x's initial value 622 comes first in the coherence order; the store 621 comes first in the coherence order; the store which directly 623 overwrites the initial value comes second; the 622 overwrites the initial value comes second; the store which overwrites 624 that value comes third, and so on. 623 that value comes third, and so on. 625 624 626 You can think of the coherence order as being 625 You can think of the coherence order as being the order in which the 627 stores reach x's location in memory (or if you 626 stores reach x's location in memory (or if you prefer a more 628 hardware-centric view, the order in which the 627 hardware-centric view, the order in which the stores get written to 629 x's cache line). We write W ->co W' if W come 628 x's cache line). We write W ->co W' if W comes before W' in the 630 coherence order, that is, if the value stored 629 coherence order, that is, if the value stored by W gets overwritten, 631 directly or indirectly, by the value stored by 630 directly or indirectly, by the value stored by W'. 632 631 633 Coherence order is required to be consistent w 632 Coherence order is required to be consistent with program order. This 634 requirement takes the form of four coherency r 633 requirement takes the form of four coherency rules: 635 634 636 Write-write coherence: If W ->po-loc W 635 Write-write coherence: If W ->po-loc W' (i.e., W comes before 637 W' in program order and they access th 636 W' in program order and they access the same location), where W 638 and W' are two stores, then W ->co W'. 637 and W' are two stores, then W ->co W'. 639 638 640 Write-read coherence: If W ->po-loc R, 639 Write-read coherence: If W ->po-loc R, where W is a store and R 641 is a load, then R must read from W or 640 is a load, then R must read from W or from some other store 642 which comes after W in the coherence o 641 which comes after W in the coherence order. 643 642 644 Read-write coherence: If R ->po-loc W, 643 Read-write coherence: If R ->po-loc W, where R is a load and W 645 is a store, then the store which R rea 644 is a store, then the store which R reads from must come before 646 W in the coherence order. 645 W in the coherence order. 647 646 648 Read-read coherence: If R ->po-loc R', 647 Read-read coherence: If R ->po-loc R', where R and R' are two 649 loads, then either they read from the 648 loads, then either they read from the same store or else the 650 store read by R comes before the store 649 store read by R comes before the store read by R' in the 651 coherence order. 650 coherence order. 652 651 653 This is sometimes referred to as sequential co 652 This is sometimes referred to as sequential consistency per variable, 654 because it means that the accesses to any sing 653 because it means that the accesses to any single memory location obey 655 the rules of the Sequential Consistency memory 654 the rules of the Sequential Consistency memory model. (According to 656 Wikipedia, sequential consistency per variable 655 Wikipedia, sequential consistency per variable and cache coherence 657 mean the same thing except that cache coherenc 656 mean the same thing except that cache coherence includes an extra 658 requirement that every store eventually become 657 requirement that every store eventually becomes visible to every CPU.) 659 658 660 Any reasonable memory model will include cache 659 Any reasonable memory model will include cache coherence. Indeed, our 661 expectation of cache coherence is so deeply in 660 expectation of cache coherence is so deeply ingrained that violations 662 of its requirements look more like hardware bu 661 of its requirements look more like hardware bugs than programming 663 errors: 662 errors: 664 663 665 int x; 664 int x; 666 665 667 P0() 666 P0() 668 { 667 { 669 WRITE_ONCE(x, 17); 668 WRITE_ONCE(x, 17); 670 WRITE_ONCE(x, 23); 669 WRITE_ONCE(x, 23); 671 } 670 } 672 671 673 If the final value stored in x after this code 672 If the final value stored in x after this code ran was 17, you would 674 think your computer was broken. It would be a 673 think your computer was broken. It would be a violation of the 675 write-write coherence rule: Since the store of 674 write-write coherence rule: Since the store of 23 comes later in 676 program order, it must also come later in x's 675 program order, it must also come later in x's coherence order and 677 thus must overwrite the store of 17. 676 thus must overwrite the store of 17. 678 677 679 int x = 0; 678 int x = 0; 680 679 681 P0() 680 P0() 682 { 681 { 683 int r1; 682 int r1; 684 683 685 r1 = READ_ONCE(x); 684 r1 = READ_ONCE(x); 686 WRITE_ONCE(x, 666); 685 WRITE_ONCE(x, 666); 687 } 686 } 688 687 689 If r1 = 666 at the end, this would violate the 688 If r1 = 666 at the end, this would violate the read-write coherence 690 rule: The READ_ONCE() load comes before the WR 689 rule: The READ_ONCE() load comes before the WRITE_ONCE() store in 691 program order, so it must not read from that s 690 program order, so it must not read from that store but rather from one 692 coming earlier in the coherence order (in this 691 coming earlier in the coherence order (in this case, x's initial 693 value). 692 value). 694 693 695 int x = 0; 694 int x = 0; 696 695 697 P0() 696 P0() 698 { 697 { 699 WRITE_ONCE(x, 5); 698 WRITE_ONCE(x, 5); 700 } 699 } 701 700 702 P1() 701 P1() 703 { 702 { 704 int r1, r2; 703 int r1, r2; 705 704 706 r1 = READ_ONCE(x); 705 r1 = READ_ONCE(x); 707 r2 = READ_ONCE(x); 706 r2 = READ_ONCE(x); 708 } 707 } 709 708 710 If r1 = 5 (reading from P0's store) and r2 = 0 709 If r1 = 5 (reading from P0's store) and r2 = 0 (reading from the 711 imaginary store which establishes x's initial 710 imaginary store which establishes x's initial value) at the end, this 712 would violate the read-read coherence rule: Th 711 would violate the read-read coherence rule: The r1 load comes before 713 the r2 load in program order, so it must not r 712 the r2 load in program order, so it must not read from a store that 714 comes later in the coherence order. 713 comes later in the coherence order. 715 714 716 (As a minor curiosity, if this code had used n 715 (As a minor curiosity, if this code had used normal loads instead of 717 READ_ONCE() in P1, on Itanium it sometimes cou 716 READ_ONCE() in P1, on Itanium it sometimes could end up with r1 = 5 718 and r2 = 0! This results from parallel execut 717 and r2 = 0! This results from parallel execution of the operations 719 encoded in Itanium's Very-Long-Instruction-Wor 718 encoded in Itanium's Very-Long-Instruction-Word format, and it is yet 720 another motivation for using READ_ONCE() when 719 another motivation for using READ_ONCE() when accessing shared memory 721 locations.) 720 locations.) 722 721 723 Just like the po relation, co is inherently an 722 Just like the po relation, co is inherently an ordering -- it is not 724 possible for a store to directly or indirectly 723 possible for a store to directly or indirectly overwrite itself! And 725 just like with the rf relation, we distinguish 724 just like with the rf relation, we distinguish between stores that 726 occur on the same CPU (internal coherence orde 725 occur on the same CPU (internal coherence order, or coi) and stores 727 that occur on different CPUs (external coheren 726 that occur on different CPUs (external coherence order, or coe). 728 727 729 On the other hand, stores to different memory 728 On the other hand, stores to different memory locations are never 730 related by co, just as instructions on differe 729 related by co, just as instructions on different CPUs are never 731 related by po. Coherence order is strictly pe 730 related by po. Coherence order is strictly per-location, or if you 732 prefer, each location has its own independent 731 prefer, each location has its own independent coherence order. 733 732 734 733 735 THE FROM-READS RELATION: fr, fri, and fre 734 THE FROM-READS RELATION: fr, fri, and fre 736 ----------------------------------------- 735 ----------------------------------------- 737 736 738 The from-reads relation (fr) can be a little d 737 The from-reads relation (fr) can be a little difficult for people to 739 grok. It describes the situation where a load 738 grok. It describes the situation where a load reads a value that gets 740 overwritten by a store. In other words, we ha 739 overwritten by a store. In other words, we have R ->fr W when the 741 value that R reads is overwritten (directly or 740 value that R reads is overwritten (directly or indirectly) by W, or 742 equivalently, when R reads from a store which 741 equivalently, when R reads from a store which comes earlier than W in 743 the coherence order. 742 the coherence order. 744 743 745 For example: 744 For example: 746 745 747 int x = 0; 746 int x = 0; 748 747 749 P0() 748 P0() 750 { 749 { 751 int r1; 750 int r1; 752 751 753 r1 = READ_ONCE(x); 752 r1 = READ_ONCE(x); 754 WRITE_ONCE(x, 2); 753 WRITE_ONCE(x, 2); 755 } 754 } 756 755 757 The value loaded from x will be 0 (assuming ca 756 The value loaded from x will be 0 (assuming cache coherence!), and it 758 gets overwritten by the value 2. Thus there i 757 gets overwritten by the value 2. Thus there is an fr link from the 759 READ_ONCE() to the WRITE_ONCE(). If the code 758 READ_ONCE() to the WRITE_ONCE(). If the code contained any later 760 stores to x, there would also be fr links from 759 stores to x, there would also be fr links from the READ_ONCE() to 761 them. 760 them. 762 761 763 As with rf, rfi, and rfe, we subdivide the fr 762 As with rf, rfi, and rfe, we subdivide the fr relation into fri (when 764 the load and the store are on the same CPU) an 763 the load and the store are on the same CPU) and fre (when they are on 765 different CPUs). 764 different CPUs). 766 765 767 Note that the fr relation is determined entire 766 Note that the fr relation is determined entirely by the rf and co 768 relations; it is not independent. Given a rea 767 relations; it is not independent. Given a read event R and a write 769 event W for the same location, we will have R 768 event W for the same location, we will have R ->fr W if and only if 770 the write which R reads from is co-before W. 769 the write which R reads from is co-before W. In symbols, 771 770 772 (R ->fr W) := (there exists W' with W' 771 (R ->fr W) := (there exists W' with W' ->rf R and W' ->co W). 773 772 774 773 775 AN OPERATIONAL MODEL 774 AN OPERATIONAL MODEL 776 -------------------- 775 -------------------- 777 776 778 The LKMM is based on various operational memor 777 The LKMM is based on various operational memory models, meaning that 779 the models arise from an abstract view of how 778 the models arise from an abstract view of how a computer system 780 operates. Here are the main ideas, as incorpo 779 operates. Here are the main ideas, as incorporated into the LKMM. 781 780 782 The system as a whole is divided into the CPUs 781 The system as a whole is divided into the CPUs and a memory subsystem. 783 The CPUs are responsible for executing instruc 782 The CPUs are responsible for executing instructions (not necessarily 784 in program order), and they communicate with t 783 in program order), and they communicate with the memory subsystem. 785 For the most part, executing an instruction re 784 For the most part, executing an instruction requires a CPU to perform 786 only internal operations. However, loads, sto 785 only internal operations. However, loads, stores, and fences involve 787 more. 786 more. 788 787 789 When CPU C executes a store instruction, it te 788 When CPU C executes a store instruction, it tells the memory subsystem 790 to store a certain value at a certain location 789 to store a certain value at a certain location. The memory subsystem 791 propagates the store to all the other CPUs as 790 propagates the store to all the other CPUs as well as to RAM. (As a 792 special case, we say that the store propagates 791 special case, we say that the store propagates to its own CPU at the 793 time it is executed.) The memory subsystem al 792 time it is executed.) The memory subsystem also determines where the 794 store falls in the location's coherence order. 793 store falls in the location's coherence order. In particular, it must 795 arrange for the store to be co-later than (i.e 794 arrange for the store to be co-later than (i.e., to overwrite) any 796 other store to the same location which has alr 795 other store to the same location which has already propagated to CPU C. 797 796 798 When a CPU executes a load instruction R, it f 797 When a CPU executes a load instruction R, it first checks to see 799 whether there are any as-yet unexecuted store 798 whether there are any as-yet unexecuted store instructions, for the 800 same location, that come before R in program o 799 same location, that come before R in program order. If there are, it 801 uses the value of the po-latest such store as 800 uses the value of the po-latest such store as the value obtained by R, 802 and we say that the store's value is forwarded 801 and we say that the store's value is forwarded to R. Otherwise, the 803 CPU asks the memory subsystem for the value to 802 CPU asks the memory subsystem for the value to load and we say that R 804 is satisfied from memory. The memory subsyste 803 is satisfied from memory. The memory subsystem hands back the value 805 of the co-latest store to the location in ques 804 of the co-latest store to the location in question which has already 806 propagated to that CPU. 805 propagated to that CPU. 807 806 808 (In fact, the picture needs to be a little mor 807 (In fact, the picture needs to be a little more complicated than this. 809 CPUs have local caches, and propagating a stor 808 CPUs have local caches, and propagating a store to a CPU really means 810 propagating it to the CPU's local cache. A lo 809 propagating it to the CPU's local cache. A local cache can take some 811 time to process the stores that it receives, a 810 time to process the stores that it receives, and a store can't be used 812 to satisfy one of the CPU's loads until it has 811 to satisfy one of the CPU's loads until it has been processed. On 813 most architectures, the local caches process s 812 most architectures, the local caches process stores in 814 First-In-First-Out order, and consequently the 813 First-In-First-Out order, and consequently the processing delay 815 doesn't matter for the memory model. But on A 814 doesn't matter for the memory model. But on Alpha, the local caches 816 have a partitioned design that results in non- 815 have a partitioned design that results in non-FIFO behavior. We will 817 discuss this in more detail later.) 816 discuss this in more detail later.) 818 817 819 Note that load instructions may be executed sp 818 Note that load instructions may be executed speculatively and may be 820 restarted under certain circumstances. The me 819 restarted under certain circumstances. The memory model ignores these 821 premature executions; we simply say that the l 820 premature executions; we simply say that the load executes at the 822 final time it is forwarded or satisfied. 821 final time it is forwarded or satisfied. 823 822 824 Executing a fence (or memory barrier) instruct 823 Executing a fence (or memory barrier) instruction doesn't require a 825 CPU to do anything special other than informin 824 CPU to do anything special other than informing the memory subsystem 826 about the fence. However, fences do constrain 825 about the fence. However, fences do constrain the way CPUs and the 827 memory subsystem handle other instructions, in 826 memory subsystem handle other instructions, in two respects. 828 827 829 First, a fence forces the CPU to execute vario 828 First, a fence forces the CPU to execute various instructions in 830 program order. Exactly which instructions are 829 program order. Exactly which instructions are ordered depends on the 831 type of fence: 830 type of fence: 832 831 833 Strong fences, including smp_mb() and 832 Strong fences, including smp_mb() and synchronize_rcu(), force 834 the CPU to execute all po-earlier inst 833 the CPU to execute all po-earlier instructions before any 835 po-later instructions; 834 po-later instructions; 836 835 837 smp_rmb() forces the CPU to execute al 836 smp_rmb() forces the CPU to execute all po-earlier loads 838 before any po-later loads; 837 before any po-later loads; 839 838 840 smp_wmb() forces the CPU to execute al 839 smp_wmb() forces the CPU to execute all po-earlier stores 841 before any po-later stores; 840 before any po-later stores; 842 841 843 Acquire fences, such as smp_load_acqui 842 Acquire fences, such as smp_load_acquire(), force the CPU to 844 execute the load associated with the f 843 execute the load associated with the fence (e.g., the load 845 part of an smp_load_acquire()) before 844 part of an smp_load_acquire()) before any po-later 846 instructions; 845 instructions; 847 846 848 Release fences, such as smp_store_rele 847 Release fences, such as smp_store_release(), force the CPU to 849 execute all po-earlier instructions be 848 execute all po-earlier instructions before the store 850 associated with the fence (e.g., the s 849 associated with the fence (e.g., the store part of an 851 smp_store_release()). 850 smp_store_release()). 852 851 853 Second, some types of fence affect the way the 852 Second, some types of fence affect the way the memory subsystem 854 propagates stores. When a fence instruction i 853 propagates stores. When a fence instruction is executed on CPU C: 855 854 856 For each other CPU C', smp_wmb() force 855 For each other CPU C', smp_wmb() forces all po-earlier stores 857 on C to propagate to C' before any po- 856 on C to propagate to C' before any po-later stores do. 858 857 859 For each other CPU C', any store which 858 For each other CPU C', any store which propagates to C before 860 a release fence is executed (including 859 a release fence is executed (including all po-earlier 861 stores executed on C) is forced to pro 860 stores executed on C) is forced to propagate to C' before the 862 store associated with the release fenc 861 store associated with the release fence does. 863 862 864 Any store which propagates to C before 863 Any store which propagates to C before a strong fence is 865 executed (including all po-earlier sto 864 executed (including all po-earlier stores on C) is forced to 866 propagate to all other CPUs before any 865 propagate to all other CPUs before any instructions po-after 867 the strong fence are executed on C. 866 the strong fence are executed on C. 868 867 869 The propagation ordering enforced by release f 868 The propagation ordering enforced by release fences and strong fences 870 affects stores from other CPUs that propagate 869 affects stores from other CPUs that propagate to CPU C before the 871 fence is executed, as well as stores that are 870 fence is executed, as well as stores that are executed on C before the 872 fence. We describe this property by saying th 871 fence. We describe this property by saying that release fences and 873 strong fences are A-cumulative. By contrast, 872 strong fences are A-cumulative. By contrast, smp_wmb() fences are not 874 A-cumulative; they only affect the propagation 873 A-cumulative; they only affect the propagation of stores that are 875 executed on C before the fence (i.e., those wh 874 executed on C before the fence (i.e., those which precede the fence in 876 program order). 875 program order). 877 876 878 rcu_read_lock(), rcu_read_unlock(), and synchr 877 rcu_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have 879 other properties which we discuss later. 878 other properties which we discuss later. 880 879 881 880 882 PROPAGATION ORDER RELATION: cumul-fence 881 PROPAGATION ORDER RELATION: cumul-fence 883 --------------------------------------- 882 --------------------------------------- 884 883 885 The fences which affect propagation order (i.e 884 The fences which affect propagation order (i.e., strong, release, and 886 smp_wmb() fences) are collectively referred to 885 smp_wmb() fences) are collectively referred to as cumul-fences, even 887 though smp_wmb() isn't A-cumulative. The cumu 886 though smp_wmb() isn't A-cumulative. The cumul-fence relation is 888 defined to link memory access events E and F w 887 defined to link memory access events E and F whenever: 889 888 890 E and F are both stores on the same CP 889 E and F are both stores on the same CPU and an smp_wmb() fence 891 event occurs between them in program o 890 event occurs between them in program order; or 892 891 893 F is a release fence and some X comes 892 F is a release fence and some X comes before F in program order, 894 where either X = E or else E ->rf X; o 893 where either X = E or else E ->rf X; or 895 894 896 A strong fence event occurs between so 895 A strong fence event occurs between some X and F in program 897 order, where either X = E or else E -> 896 order, where either X = E or else E ->rf X. 898 897 899 The operational model requires that whenever W 898 The operational model requires that whenever W and W' are both stores 900 and W ->cumul-fence W', then W must propagate 899 and W ->cumul-fence W', then W must propagate to any given CPU 901 before W' does. However, for different CPUs C 900 before W' does. However, for different CPUs C and C', it does not 902 require W to propagate to C before W' propagat 901 require W to propagate to C before W' propagates to C'. 903 902 904 903 905 DERIVATION OF THE LKMM FROM THE OPERATIONAL MO 904 DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL 906 ---------------------------------------------- 905 ------------------------------------------------- 907 906 908 The LKMM is derived from the restrictions impo 907 The LKMM is derived from the restrictions imposed by the design 909 outlined above. These restrictions involve th 908 outlined above. These restrictions involve the necessity of 910 maintaining cache coherence and the fact that 909 maintaining cache coherence and the fact that a CPU can't operate on a 911 value before it knows what that value is, amon 910 value before it knows what that value is, among other things. 912 911 913 The formal version of the LKMM is defined by s 912 The formal version of the LKMM is defined by six requirements, or 914 axioms: 913 axioms: 915 914 916 Sequential consistency per variable: T 915 Sequential consistency per variable: This requires that the 917 system obey the four coherency rules. 916 system obey the four coherency rules. 918 917 919 Atomicity: This requires that atomic r 918 Atomicity: This requires that atomic read-modify-write 920 operations really are atomic, that is, 919 operations really are atomic, that is, no other stores can 921 sneak into the middle of such an updat 920 sneak into the middle of such an update. 922 921 923 Happens-before: This requires that cer 922 Happens-before: This requires that certain instructions are 924 executed in a specific order. 923 executed in a specific order. 925 924 926 Propagation: This requires that certai 925 Propagation: This requires that certain stores propagate to 927 CPUs and to RAM in a specific order. 926 CPUs and to RAM in a specific order. 928 927 929 Rcu: This requires that RCU read-side 928 Rcu: This requires that RCU read-side critical sections and 930 grace periods obey the rules of RCU, i 929 grace periods obey the rules of RCU, in particular, the 931 Grace-Period Guarantee. 930 Grace-Period Guarantee. 932 931 933 Plain-coherence: This requires that pl 932 Plain-coherence: This requires that plain memory accesses 934 (those not using READ_ONCE(), WRITE_ON 933 (those not using READ_ONCE(), WRITE_ONCE(), etc.) must obey 935 the operational model's rules regardin 934 the operational model's rules regarding cache coherence. 936 935 937 The first and second are quite common; they ca 936 The first and second are quite common; they can be found in many 938 memory models (such as those for C11/C++11). 937 memory models (such as those for C11/C++11). The "happens-before" and 939 "propagation" axioms have analogs in other mem 938 "propagation" axioms have analogs in other memory models as well. The 940 "rcu" and "plain-coherence" axioms are specifi 939 "rcu" and "plain-coherence" axioms are specific to the LKMM. 941 940 942 Each of these axioms is discussed below. 941 Each of these axioms is discussed below. 943 942 944 943 945 SEQUENTIAL CONSISTENCY PER VARIABLE 944 SEQUENTIAL CONSISTENCY PER VARIABLE 946 ----------------------------------- 945 ----------------------------------- 947 946 948 According to the principle of cache coherence, 947 According to the principle of cache coherence, the stores to any fixed 949 shared location in memory form a global orderi 948 shared location in memory form a global ordering. We can imagine 950 inserting the loads from that location into th 949 inserting the loads from that location into this ordering, by placing 951 each load between the store that it reads from 950 each load between the store that it reads from and the following 952 store. This leaves the relative positions of 951 store. This leaves the relative positions of loads that read from the 953 same store unspecified; let's say they are ins 952 same store unspecified; let's say they are inserted in program order, 954 first for CPU 0, then CPU 1, etc. 953 first for CPU 0, then CPU 1, etc. 955 954 956 You can check that the four coherency rules im 955 You can check that the four coherency rules imply that the rf, co, fr, 957 and po-loc relations agree with this global or 956 and po-loc relations agree with this global ordering; in other words, 958 whenever we have X ->rf Y or X ->co Y or X ->f 957 whenever we have X ->rf Y or X ->co Y or X ->fr Y or X ->po-loc Y, the 959 X event comes before the Y event in the global 958 X event comes before the Y event in the global ordering. The LKMM's 960 "coherence" axiom expresses this by requiring 959 "coherence" axiom expresses this by requiring the union of these 961 relations not to have any cycles. This means 960 relations not to have any cycles. This means it must not be possible 962 to find events 961 to find events 963 962 964 X0 -> X1 -> X2 -> ... -> Xn -> X0, 963 X0 -> X1 -> X2 -> ... -> Xn -> X0, 965 964 966 where each of the links is either rf, co, fr, 965 where each of the links is either rf, co, fr, or po-loc. This has to 967 hold if the accesses to the fixed memory locat 966 hold if the accesses to the fixed memory location can be ordered as 968 cache coherence demands. 967 cache coherence demands. 969 968 970 Although it is not obvious, it can be shown th 969 Although it is not obvious, it can be shown that the converse is also 971 true: This LKMM axiom implies that the four co 970 true: This LKMM axiom implies that the four coherency rules are 972 obeyed. 971 obeyed. 973 972 974 973 975 ATOMIC UPDATES: rmw 974 ATOMIC UPDATES: rmw 976 ------------------- 975 ------------------- 977 976 978 What does it mean to say that a read-modify-wr 977 What does it mean to say that a read-modify-write (rmw) update, such 979 as atomic_inc(&x), is atomic? It means that t 978 as atomic_inc(&x), is atomic? It means that the memory location (x in 980 this case) does not get altered between the re 979 this case) does not get altered between the read and the write events 981 making up the atomic operation. In particular 980 making up the atomic operation. In particular, if two CPUs perform 982 atomic_inc(&x) concurrently, it must be guaran 981 atomic_inc(&x) concurrently, it must be guaranteed that the final 983 value of x will be the initial value plus two. 982 value of x will be the initial value plus two. We should never have 984 the following sequence of events: 983 the following sequence of events: 985 984 986 CPU 0 loads x obtaining 13; 985 CPU 0 loads x obtaining 13; 987 CPU 1 986 CPU 1 loads x obtaining 13; 988 CPU 0 stores 14 to x; 987 CPU 0 stores 14 to x; 989 CPU 1 988 CPU 1 stores 14 to x; 990 989 991 where the final value of x is wrong (14 rather 990 where the final value of x is wrong (14 rather than 15). 992 991 993 In this example, CPU 0's increment effectively 992 In this example, CPU 0's increment effectively gets lost because it 994 occurs in between CPU 1's load and store. To 993 occurs in between CPU 1's load and store. To put it another way, the 995 problem is that the position of CPU 0's store 994 problem is that the position of CPU 0's store in x's coherence order 996 is between the store that CPU 1 reads from and 995 is between the store that CPU 1 reads from and the store that CPU 1 997 performs. 996 performs. 998 997 999 The same analysis applies to all atomic update 998 The same analysis applies to all atomic update operations. Therefore, 1000 to enforce atomicity the LKMM requires that a 999 to enforce atomicity the LKMM requires that atomic updates follow this 1001 rule: Whenever R and W are the read and write 1000 rule: Whenever R and W are the read and write events composing an 1002 atomic read-modify-write and W' is the write 1001 atomic read-modify-write and W' is the write event which R reads from, 1003 there must not be any stores coming between W 1002 there must not be any stores coming between W' and W in the coherence 1004 order. Equivalently, 1003 order. Equivalently, 1005 1004 1006 (R ->rmw W) implies (there is no X wi 1005 (R ->rmw W) implies (there is no X with R ->fr X and X ->co W), 1007 1006 1008 where the rmw relation links the read and wri 1007 where the rmw relation links the read and write events making up each 1009 atomic update. This is what the LKMM's "atom 1008 atomic update. This is what the LKMM's "atomic" axiom says. 1010 1009 1011 Atomic rmw updates play one more role in the 1010 Atomic rmw updates play one more role in the LKMM: They can form "rmw 1012 sequences". An rmw sequence is simply a bunc 1011 sequences". An rmw sequence is simply a bunch of atomic updates where 1013 each update reads from the previous one. Wri 1012 each update reads from the previous one. Written using events, it 1014 looks like this: 1013 looks like this: 1015 1014 1016 Z0 ->rf Y1 ->rmw Z1 ->rf ... ->rf Yn 1015 Z0 ->rf Y1 ->rmw Z1 ->rf ... ->rf Yn ->rmw Zn, 1017 1016 1018 where Z0 is some store event and n can be any 1017 where Z0 is some store event and n can be any number (even 0, in the 1019 degenerate case). We write this relation as: 1018 degenerate case). We write this relation as: Z0 ->rmw-sequence Zn. 1020 Note that this implies Z0 and Zn are stores t 1019 Note that this implies Z0 and Zn are stores to the same variable. 1021 1020 1022 Rmw sequences have a special property in the 1021 Rmw sequences have a special property in the LKMM: They can extend the 1023 cumul-fence relation. That is, if we have: 1022 cumul-fence relation. That is, if we have: 1024 1023 1025 U ->cumul-fence X -> rmw-sequence Y 1024 U ->cumul-fence X -> rmw-sequence Y 1026 1025 1027 then also U ->cumul-fence Y. Thinking about 1026 then also U ->cumul-fence Y. Thinking about this in terms of the 1028 operational model, U ->cumul-fence X says tha 1027 operational model, U ->cumul-fence X says that the store U propagates 1029 to each CPU before the store X does. Then th 1028 to each CPU before the store X does. Then the fact that X and Y are 1030 linked by an rmw sequence means that U also p 1029 linked by an rmw sequence means that U also propagates to each CPU 1031 before Y does. In an analogous way, rmw sequ 1030 before Y does. In an analogous way, rmw sequences can also extend 1032 the w-post-bounded relation defined below in 1031 the w-post-bounded relation defined below in the PLAIN ACCESSES AND 1033 DATA RACES section. 1032 DATA RACES section. 1034 1033 1035 (The notion of rmw sequences in the LKMM is s 1034 (The notion of rmw sequences in the LKMM is similar to, but not quite 1036 the same as, that of release sequences in the 1035 the same as, that of release sequences in the C11 memory model. They 1037 were added to the LKMM to fix an obscure bug; 1036 were added to the LKMM to fix an obscure bug; without them, atomic 1038 updates with full-barrier semantics did not a 1037 updates with full-barrier semantics did not always guarantee ordering 1039 at least as strong as atomic updates with rel 1038 at least as strong as atomic updates with release-barrier semantics.) 1040 1039 1041 1040 1042 THE PRESERVED PROGRAM ORDER RELATION: ppo 1041 THE PRESERVED PROGRAM ORDER RELATION: ppo 1043 ----------------------------------------- 1042 ----------------------------------------- 1044 1043 1045 There are many situations where a CPU is obli 1044 There are many situations where a CPU is obliged to execute two 1046 instructions in program order. We amalgamate 1045 instructions in program order. We amalgamate them into the ppo (for 1047 "preserved program order") relation, which li 1046 "preserved program order") relation, which links the po-earlier 1048 instruction to the po-later instruction and i 1047 instruction to the po-later instruction and is thus a sub-relation of 1049 po. 1048 po. 1050 1049 1051 The operational model already includes a desc 1050 The operational model already includes a description of one such 1052 situation: Fences are a source of ppo links. 1051 situation: Fences are a source of ppo links. Suppose X and Y are 1053 memory accesses with X ->po Y; then the CPU m 1052 memory accesses with X ->po Y; then the CPU must execute X before Y if 1054 any of the following hold: 1053 any of the following hold: 1055 1054 1056 A strong (smp_mb() or synchronize_rcu 1055 A strong (smp_mb() or synchronize_rcu()) fence occurs between 1057 X and Y; 1056 X and Y; 1058 1057 1059 X and Y are both stores and an smp_wm 1058 X and Y are both stores and an smp_wmb() fence occurs between 1060 them; 1059 them; 1061 1060 1062 X and Y are both loads and an smp_rmb 1061 X and Y are both loads and an smp_rmb() fence occurs between 1063 them; 1062 them; 1064 1063 1065 X is also an acquire fence, such as s 1064 X is also an acquire fence, such as smp_load_acquire(); 1066 1065 1067 Y is also a release fence, such as sm 1066 Y is also a release fence, such as smp_store_release(). 1068 1067 1069 Another possibility, not mentioned earlier bu 1068 Another possibility, not mentioned earlier but discussed in the next 1070 section, is: 1069 section, is: 1071 1070 1072 X and Y are both loads, X ->addr Y (i 1071 X and Y are both loads, X ->addr Y (i.e., there is an address 1073 dependency from X to Y), and X is a R 1072 dependency from X to Y), and X is a READ_ONCE() or an atomic 1074 access. 1073 access. 1075 1074 1076 Dependencies can also cause instructions to b 1075 Dependencies can also cause instructions to be executed in program 1077 order. This is uncontroversial when the seco 1076 order. This is uncontroversial when the second instruction is a 1078 store; either a data, address, or control dep 1077 store; either a data, address, or control dependency from a load R to 1079 a store W will force the CPU to execute R bef 1078 a store W will force the CPU to execute R before W. This is very 1080 simply because the CPU cannot tell the memory 1079 simply because the CPU cannot tell the memory subsystem about W's 1081 store before it knows what value should be st 1080 store before it knows what value should be stored (in the case of a 1082 data dependency), what location it should be 1081 data dependency), what location it should be stored into (in the case 1083 of an address dependency), or whether the sto 1082 of an address dependency), or whether the store should actually take 1084 place (in the case of a control dependency). 1083 place (in the case of a control dependency). 1085 1084 1086 Dependencies to load instructions are more pr 1085 Dependencies to load instructions are more problematic. To begin with, 1087 there is no such thing as a data dependency t 1086 there is no such thing as a data dependency to a load. Next, a CPU 1088 has no reason to respect a control dependency 1087 has no reason to respect a control dependency to a load, because it 1089 can always satisfy the second load speculativ 1088 can always satisfy the second load speculatively before the first, and 1090 then ignore the result if it turns out that t 1089 then ignore the result if it turns out that the second load shouldn't 1091 be executed after all. And lastly, the real 1090 be executed after all. And lastly, the real difficulties begin when 1092 we consider address dependencies to loads. 1091 we consider address dependencies to loads. 1093 1092 1094 To be fair about it, all Linux-supported arch 1093 To be fair about it, all Linux-supported architectures do execute 1095 loads in program order if there is an address 1094 loads in program order if there is an address dependency between them. 1096 After all, a CPU cannot ask the memory subsys 1095 After all, a CPU cannot ask the memory subsystem to load a value from 1097 a particular location before it knows what th 1096 a particular location before it knows what that location is. However, 1098 the split-cache design used by Alpha can caus 1097 the split-cache design used by Alpha can cause it to behave in a way 1099 that looks as if the loads were executed out 1098 that looks as if the loads were executed out of order (see the next 1100 section for more details). The kernel includ 1099 section for more details). The kernel includes a workaround for this 1101 problem when the loads come from READ_ONCE(), 1100 problem when the loads come from READ_ONCE(), and therefore the LKMM 1102 includes address dependencies to loads in the 1101 includes address dependencies to loads in the ppo relation. 1103 1102 1104 On the other hand, dependencies can indirectl 1103 On the other hand, dependencies can indirectly affect the ordering of 1105 two loads. This happens when there is a depe 1104 two loads. This happens when there is a dependency from a load to a 1106 store and a second, po-later load reads from 1105 store and a second, po-later load reads from that store: 1107 1106 1108 R ->dep W ->rfi R', 1107 R ->dep W ->rfi R', 1109 1108 1110 where the dep link can be either an address o 1109 where the dep link can be either an address or a data dependency. In 1111 this situation we know it is possible for the 1110 this situation we know it is possible for the CPU to execute R' before 1112 W, because it can forward the value that W wi 1111 W, because it can forward the value that W will store to R'. But it 1113 cannot execute R' before R, because it cannot 1112 cannot execute R' before R, because it cannot forward the value before 1114 it knows what that value is, or that W and R' 1113 it knows what that value is, or that W and R' do access the same 1115 location. However, if there is merely a cont 1114 location. However, if there is merely a control dependency between R 1116 and W then the CPU can speculatively forward 1115 and W then the CPU can speculatively forward W to R' before executing 1117 R; if the speculation turns out to be wrong t 1116 R; if the speculation turns out to be wrong then the CPU merely has to 1118 restart or abandon R'. 1117 restart or abandon R'. 1119 1118 1120 (In theory, a CPU might forward a store to a 1119 (In theory, a CPU might forward a store to a load when it runs across 1121 an address dependency like this: 1120 an address dependency like this: 1122 1121 1123 r1 = READ_ONCE(ptr); 1122 r1 = READ_ONCE(ptr); 1124 WRITE_ONCE(*r1, 17); 1123 WRITE_ONCE(*r1, 17); 1125 r2 = READ_ONCE(*r1); 1124 r2 = READ_ONCE(*r1); 1126 1125 1127 because it could tell that the store and the 1126 because it could tell that the store and the second load access the 1128 same location even before it knows what the l 1127 same location even before it knows what the location's address is. 1129 However, none of the architectures supported 1128 However, none of the architectures supported by the Linux kernel do 1130 this.) 1129 this.) 1131 1130 1132 Two memory accesses of the same location must 1131 Two memory accesses of the same location must always be executed in 1133 program order if the second access is a store 1132 program order if the second access is a store. Thus, if we have 1134 1133 1135 R ->po-loc W 1134 R ->po-loc W 1136 1135 1137 (the po-loc link says that R comes before W i 1136 (the po-loc link says that R comes before W in program order and they 1138 access the same location), the CPU is obliged 1137 access the same location), the CPU is obliged to execute W after R. 1139 If it executed W first then the memory subsys 1138 If it executed W first then the memory subsystem would respond to R's 1140 read request with the value stored by W (or a 1139 read request with the value stored by W (or an even later store), in 1141 violation of the read-write coherence rule. 1140 violation of the read-write coherence rule. Similarly, if we had 1142 1141 1143 W ->po-loc W' 1142 W ->po-loc W' 1144 1143 1145 and the CPU executed W' before W, then the me 1144 and the CPU executed W' before W, then the memory subsystem would put 1146 W' before W in the coherence order. It would 1145 W' before W in the coherence order. It would effectively cause W to 1147 overwrite W', in violation of the write-write 1146 overwrite W', in violation of the write-write coherence rule. 1148 (Interestingly, an early ARMv8 memory model, 1147 (Interestingly, an early ARMv8 memory model, now obsolete, proposed 1149 allowing out-of-order writes like this to occ 1148 allowing out-of-order writes like this to occur. The model avoided 1150 violating the write-write coherence rule by r 1149 violating the write-write coherence rule by requiring the CPU not to 1151 send the W write to the memory subsystem at a 1150 send the W write to the memory subsystem at all!) 1152 1151 1153 1152 1154 AND THEN THERE WAS ALPHA 1153 AND THEN THERE WAS ALPHA 1155 ------------------------ 1154 ------------------------ 1156 1155 1157 As mentioned above, the Alpha architecture is 1156 As mentioned above, the Alpha architecture is unique in that it does 1158 not appear to respect address dependencies to 1157 not appear to respect address dependencies to loads. This means that 1159 code such as the following: 1158 code such as the following: 1160 1159 1161 int x = 0; 1160 int x = 0; 1162 int y = -1; 1161 int y = -1; 1163 int *ptr = &y; 1162 int *ptr = &y; 1164 1163 1165 P0() 1164 P0() 1166 { 1165 { 1167 WRITE_ONCE(x, 1); 1166 WRITE_ONCE(x, 1); 1168 smp_wmb(); 1167 smp_wmb(); 1169 WRITE_ONCE(ptr, &x); 1168 WRITE_ONCE(ptr, &x); 1170 } 1169 } 1171 1170 1172 P1() 1171 P1() 1173 { 1172 { 1174 int *r1; 1173 int *r1; 1175 int r2; 1174 int r2; 1176 1175 1177 r1 = ptr; 1176 r1 = ptr; 1178 r2 = READ_ONCE(*r1); 1177 r2 = READ_ONCE(*r1); 1179 } 1178 } 1180 1179 1181 can malfunction on Alpha systems (notice that 1180 can malfunction on Alpha systems (notice that P1 uses an ordinary load 1182 to read ptr instead of READ_ONCE()). It is q 1181 to read ptr instead of READ_ONCE()). It is quite possible that r1 = &x 1183 and r2 = 0 at the end, in spite of the addres 1182 and r2 = 0 at the end, in spite of the address dependency. 1184 1183 1185 At first glance this doesn't seem to make sen 1184 At first glance this doesn't seem to make sense. We know that the 1186 smp_wmb() forces P0's store to x to propagate 1185 smp_wmb() forces P0's store to x to propagate to P1 before the store 1187 to ptr does. And since P1 can't execute its 1186 to ptr does. And since P1 can't execute its second load 1188 until it knows what location to load from, i. 1187 until it knows what location to load from, i.e., after executing its 1189 first load, the value x = 1 must have propaga 1188 first load, the value x = 1 must have propagated to P1 before the 1190 second load executed. So why doesn't r2 end 1189 second load executed. So why doesn't r2 end up equal to 1? 1191 1190 1192 The answer lies in the Alpha's split local ca 1191 The answer lies in the Alpha's split local caches. Although the two 1193 stores do reach P1's local cache in the prope 1192 stores do reach P1's local cache in the proper order, it can happen 1194 that the first store is processed by a busy p 1193 that the first store is processed by a busy part of the cache while 1195 the second store is processed by an idle part 1194 the second store is processed by an idle part. As a result, the x = 1 1196 value may not become available for P1's CPU t 1195 value may not become available for P1's CPU to read until after the 1197 ptr = &x value does, leading to the undesirab 1196 ptr = &x value does, leading to the undesirable result above. The 1198 final effect is that even though the two load 1197 final effect is that even though the two loads really are executed in 1199 program order, it appears that they aren't. 1198 program order, it appears that they aren't. 1200 1199 1201 This could not have happened if the local cac 1200 This could not have happened if the local cache had processed the 1202 incoming stores in FIFO order. By contrast, 1201 incoming stores in FIFO order. By contrast, other architectures 1203 maintain at least the appearance of FIFO orde 1202 maintain at least the appearance of FIFO order. 1204 1203 1205 In practice, this difficulty is solved by ins 1204 In practice, this difficulty is solved by inserting a special fence 1206 between P1's two loads when the kernel is com 1205 between P1's two loads when the kernel is compiled for the Alpha 1207 architecture. In fact, as of version 4.15, t 1206 architecture. In fact, as of version 4.15, the kernel automatically 1208 adds this fence after every READ_ONCE() and a 1207 adds this fence after every READ_ONCE() and atomic load on Alpha. The 1209 effect of the fence is to cause the CPU not t 1208 effect of the fence is to cause the CPU not to execute any po-later 1210 instructions until after the local cache has 1209 instructions until after the local cache has finished processing all 1211 the stores it has already received. Thus, if 1210 the stores it has already received. Thus, if the code was changed to: 1212 1211 1213 P1() 1212 P1() 1214 { 1213 { 1215 int *r1; 1214 int *r1; 1216 int r2; 1215 int r2; 1217 1216 1218 r1 = READ_ONCE(ptr); 1217 r1 = READ_ONCE(ptr); 1219 r2 = READ_ONCE(*r1); 1218 r2 = READ_ONCE(*r1); 1220 } 1219 } 1221 1220 1222 then we would never get r1 = &x and r2 = 0. 1221 then we would never get r1 = &x and r2 = 0. By the time P1 executed 1223 its second load, the x = 1 store would alread 1222 its second load, the x = 1 store would already be fully processed by 1224 the local cache and available for satisfying 1223 the local cache and available for satisfying the read request. Thus 1225 we have yet another reason why shared data sh 1224 we have yet another reason why shared data should always be read with 1226 READ_ONCE() or another synchronization primit 1225 READ_ONCE() or another synchronization primitive rather than accessed 1227 directly. 1226 directly. 1228 1227 1229 The LKMM requires that smp_rmb(), acquire fen 1228 The LKMM requires that smp_rmb(), acquire fences, and strong fences 1230 share this property: They do not allow the CP 1229 share this property: They do not allow the CPU to execute any po-later 1231 instructions (or po-later loads in the case o 1230 instructions (or po-later loads in the case of smp_rmb()) until all 1232 outstanding stores have been processed by the 1231 outstanding stores have been processed by the local cache. In the 1233 case of a strong fence, the CPU first has to 1232 case of a strong fence, the CPU first has to wait for all of its 1234 po-earlier stores to propagate to every other 1233 po-earlier stores to propagate to every other CPU in the system; then 1235 it has to wait for the local cache to process 1234 it has to wait for the local cache to process all the stores received 1236 as of that time -- not just the stores receiv 1235 as of that time -- not just the stores received when the strong fence 1237 began. 1236 began. 1238 1237 1239 And of course, none of this matters for any a 1238 And of course, none of this matters for any architecture other than 1240 Alpha. 1239 Alpha. 1241 1240 1242 1241 1243 THE HAPPENS-BEFORE RELATION: hb 1242 THE HAPPENS-BEFORE RELATION: hb 1244 ------------------------------- 1243 ------------------------------- 1245 1244 1246 The happens-before relation (hb) links memory 1245 The happens-before relation (hb) links memory accesses that have to 1247 execute in a certain order. hb includes the 1246 execute in a certain order. hb includes the ppo relation and two 1248 others, one of which is rfe. 1247 others, one of which is rfe. 1249 1248 1250 W ->rfe R implies that W and R are on differe 1249 W ->rfe R implies that W and R are on different CPUs. It also means 1251 that W's store must have propagated to R's CP 1250 that W's store must have propagated to R's CPU before R executed; 1252 otherwise R could not have read the value sto 1251 otherwise R could not have read the value stored by W. Therefore W 1253 must have executed before R, and so we have W 1252 must have executed before R, and so we have W ->hb R. 1254 1253 1255 The equivalent fact need not hold if W ->rfi 1254 The equivalent fact need not hold if W ->rfi R (i.e., W and R are on 1256 the same CPU). As we have already seen, the 1255 the same CPU). As we have already seen, the operational model allows 1257 W's value to be forwarded to R in such cases, 1256 W's value to be forwarded to R in such cases, meaning that R may well 1258 execute before W does. 1257 execute before W does. 1259 1258 1260 It's important to understand that neither coe 1259 It's important to understand that neither coe nor fre is included in 1261 hb, despite their similarities to rfe. For e 1260 hb, despite their similarities to rfe. For example, suppose we have 1262 W ->coe W'. This means that W and W' are sto 1261 W ->coe W'. This means that W and W' are stores to the same location, 1263 they execute on different CPUs, and W comes b 1262 they execute on different CPUs, and W comes before W' in the coherence 1264 order (i.e., W' overwrites W). Nevertheless, 1263 order (i.e., W' overwrites W). Nevertheless, it is possible for W' to 1265 execute before W, because the decision as to 1264 execute before W, because the decision as to which store overwrites 1266 the other is made later by the memory subsyst 1265 the other is made later by the memory subsystem. When the stores are 1267 nearly simultaneous, either one can come out 1266 nearly simultaneous, either one can come out on top. Similarly, 1268 R ->fre W means that W overwrites the value w 1267 R ->fre W means that W overwrites the value which R reads, but it 1269 doesn't mean that W has to execute after R. 1268 doesn't mean that W has to execute after R. All that's necessary is 1270 for the memory subsystem not to propagate W t 1269 for the memory subsystem not to propagate W to R's CPU until after R 1271 has executed, which is possible if W executes 1270 has executed, which is possible if W executes shortly before R. 1272 1271 1273 The third relation included in hb is like ppo 1272 The third relation included in hb is like ppo, in that it only links 1274 events that are on the same CPU. However it 1273 events that are on the same CPU. However it is more difficult to 1275 explain, because it arises only indirectly fr 1274 explain, because it arises only indirectly from the requirement of 1276 cache coherence. The relation is called prop 1275 cache coherence. The relation is called prop, and it links two events 1277 on CPU C in situations where a store from som 1276 on CPU C in situations where a store from some other CPU comes after 1278 the first event in the coherence order and pr 1277 the first event in the coherence order and propagates to C before the 1279 second event executes. 1278 second event executes. 1280 1279 1281 This is best explained with some examples. T 1280 This is best explained with some examples. The simplest case looks 1282 like this: 1281 like this: 1283 1282 1284 int x; 1283 int x; 1285 1284 1286 P0() 1285 P0() 1287 { 1286 { 1288 int r1; 1287 int r1; 1289 1288 1290 WRITE_ONCE(x, 1); 1289 WRITE_ONCE(x, 1); 1291 r1 = READ_ONCE(x); 1290 r1 = READ_ONCE(x); 1292 } 1291 } 1293 1292 1294 P1() 1293 P1() 1295 { 1294 { 1296 WRITE_ONCE(x, 8); 1295 WRITE_ONCE(x, 8); 1297 } 1296 } 1298 1297 1299 If r1 = 8 at the end then P0's accesses must 1298 If r1 = 8 at the end then P0's accesses must have executed in program 1300 order. We can deduce this from the operation 1299 order. We can deduce this from the operational model; if P0's load 1301 had executed before its store then the value 1300 had executed before its store then the value of the store would have 1302 been forwarded to the load, so r1 would have 1301 been forwarded to the load, so r1 would have ended up equal to 1, not 1303 8. In this case there is a prop link from P0 1302 8. In this case there is a prop link from P0's write event to its read 1304 event, because P1's store came after P0's sto 1303 event, because P1's store came after P0's store in x's coherence 1305 order, and P1's store propagated to P0 before 1304 order, and P1's store propagated to P0 before P0's load executed. 1306 1305 1307 An equally simple case involves two loads of 1306 An equally simple case involves two loads of the same location that 1308 read from different stores: 1307 read from different stores: 1309 1308 1310 int x = 0; 1309 int x = 0; 1311 1310 1312 P0() 1311 P0() 1313 { 1312 { 1314 int r1, r2; 1313 int r1, r2; 1315 1314 1316 r1 = READ_ONCE(x); 1315 r1 = READ_ONCE(x); 1317 r2 = READ_ONCE(x); 1316 r2 = READ_ONCE(x); 1318 } 1317 } 1319 1318 1320 P1() 1319 P1() 1321 { 1320 { 1322 WRITE_ONCE(x, 9); 1321 WRITE_ONCE(x, 9); 1323 } 1322 } 1324 1323 1325 If r1 = 0 and r2 = 9 at the end then P0's acc 1324 If r1 = 0 and r2 = 9 at the end then P0's accesses must have executed 1326 in program order. If the second load had exe 1325 in program order. If the second load had executed before the first 1327 then the x = 9 store must have been propagate 1326 then the x = 9 store must have been propagated to P0 before the first 1328 load executed, and so r1 would have been 9 ra 1327 load executed, and so r1 would have been 9 rather than 0. In this 1329 case there is a prop link from P0's first rea 1328 case there is a prop link from P0's first read event to its second, 1330 because P1's store overwrote the value read b 1329 because P1's store overwrote the value read by P0's first load, and 1331 P1's store propagated to P0 before P0's secon 1330 P1's store propagated to P0 before P0's second load executed. 1332 1331 1333 Less trivial examples of prop all involve fen 1332 Less trivial examples of prop all involve fences. Unlike the simple 1334 examples above, they can require that some in 1333 examples above, they can require that some instructions are executed 1335 out of program order. This next one should l 1334 out of program order. This next one should look familiar: 1336 1335 1337 int buf = 0, flag = 0; 1336 int buf = 0, flag = 0; 1338 1337 1339 P0() 1338 P0() 1340 { 1339 { 1341 WRITE_ONCE(buf, 1); 1340 WRITE_ONCE(buf, 1); 1342 smp_wmb(); 1341 smp_wmb(); 1343 WRITE_ONCE(flag, 1); 1342 WRITE_ONCE(flag, 1); 1344 } 1343 } 1345 1344 1346 P1() 1345 P1() 1347 { 1346 { 1348 int r1; 1347 int r1; 1349 int r2; 1348 int r2; 1350 1349 1351 r1 = READ_ONCE(flag); 1350 r1 = READ_ONCE(flag); 1352 r2 = READ_ONCE(buf); 1351 r2 = READ_ONCE(buf); 1353 } 1352 } 1354 1353 1355 This is the MP pattern again, with an smp_wmb 1354 This is the MP pattern again, with an smp_wmb() fence between the two 1356 stores. If r1 = 1 and r2 = 0 at the end then 1355 stores. If r1 = 1 and r2 = 0 at the end then there is a prop link 1357 from P1's second load to its first (backwards 1356 from P1's second load to its first (backwards!). The reason is 1358 similar to the previous examples: The value P 1357 similar to the previous examples: The value P1 loads from buf gets 1359 overwritten by P0's store to buf, the fence g 1358 overwritten by P0's store to buf, the fence guarantees that the store 1360 to buf will propagate to P1 before the store 1359 to buf will propagate to P1 before the store to flag does, and the 1361 store to flag propagates to P1 before P1 read 1360 store to flag propagates to P1 before P1 reads flag. 1362 1361 1363 The prop link says that in order to obtain th 1362 The prop link says that in order to obtain the r1 = 1, r2 = 0 result, 1364 P1 must execute its second load before the fi 1363 P1 must execute its second load before the first. Indeed, if the load 1365 from flag were executed first, then the buf = 1364 from flag were executed first, then the buf = 1 store would already 1366 have propagated to P1 by the time P1's load f 1365 have propagated to P1 by the time P1's load from buf executed, so r2 1367 would have been 1 at the end, not 0. (The re 1366 would have been 1 at the end, not 0. (The reasoning holds even for 1368 Alpha, although the details are more complica 1367 Alpha, although the details are more complicated and we will not go 1369 into them.) 1368 into them.) 1370 1369 1371 But what if we put an smp_rmb() fence between 1370 But what if we put an smp_rmb() fence between P1's loads? The fence 1372 would force the two loads to be executed in p 1371 would force the two loads to be executed in program order, and it 1373 would generate a cycle in the hb relation: Th 1372 would generate a cycle in the hb relation: The fence would create a ppo 1374 link (hence an hb link) from the first load t 1373 link (hence an hb link) from the first load to the second, and the 1375 prop relation would give an hb link from the 1374 prop relation would give an hb link from the second load to the first. 1376 Since an instruction can't execute before its 1375 Since an instruction can't execute before itself, we are forced to 1377 conclude that if an smp_rmb() fence is added, 1376 conclude that if an smp_rmb() fence is added, the r1 = 1, r2 = 0 1378 outcome is impossible -- as it should be. 1377 outcome is impossible -- as it should be. 1379 1378 1380 The formal definition of the prop relation in 1379 The formal definition of the prop relation involves a coe or fre link, 1381 followed by an arbitrary number of cumul-fenc 1380 followed by an arbitrary number of cumul-fence links, ending with an 1382 rfe link. You can concoct more exotic exampl 1381 rfe link. You can concoct more exotic examples, containing more than 1383 one fence, although this quickly leads to dim 1382 one fence, although this quickly leads to diminishing returns in terms 1384 of complexity. For instance, here's an examp 1383 of complexity. For instance, here's an example containing a coe link 1385 followed by two cumul-fences and an rfe link, 1384 followed by two cumul-fences and an rfe link, utilizing the fact that 1386 release fences are A-cumulative: 1385 release fences are A-cumulative: 1387 1386 1388 int x, y, z; 1387 int x, y, z; 1389 1388 1390 P0() 1389 P0() 1391 { 1390 { 1392 int r0; 1391 int r0; 1393 1392 1394 WRITE_ONCE(x, 1); 1393 WRITE_ONCE(x, 1); 1395 r0 = READ_ONCE(z); 1394 r0 = READ_ONCE(z); 1396 } 1395 } 1397 1396 1398 P1() 1397 P1() 1399 { 1398 { 1400 WRITE_ONCE(x, 2); 1399 WRITE_ONCE(x, 2); 1401 smp_wmb(); 1400 smp_wmb(); 1402 WRITE_ONCE(y, 1); 1401 WRITE_ONCE(y, 1); 1403 } 1402 } 1404 1403 1405 P2() 1404 P2() 1406 { 1405 { 1407 int r2; 1406 int r2; 1408 1407 1409 r2 = READ_ONCE(y); 1408 r2 = READ_ONCE(y); 1410 smp_store_release(&z, 1); 1409 smp_store_release(&z, 1); 1411 } 1410 } 1412 1411 1413 If x = 2, r0 = 1, and r2 = 1 after this code 1412 If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop 1414 link from P0's store to its load. This is be 1413 link from P0's store to its load. This is because P0's store gets 1415 overwritten by P1's store since x = 2 at the 1414 overwritten by P1's store since x = 2 at the end (a coe link), the 1416 smp_wmb() ensures that P1's store to x propag 1415 smp_wmb() ensures that P1's store to x propagates to P2 before the 1417 store to y does (the first cumul-fence), the 1416 store to y does (the first cumul-fence), the store to y propagates to P2 1418 before P2's load and store execute, P2's smp_ 1417 before P2's load and store execute, P2's smp_store_release() 1419 guarantees that the stores to x and y both pr 1418 guarantees that the stores to x and y both propagate to P0 before the 1420 store to z does (the second cumul-fence), and 1419 store to z does (the second cumul-fence), and P0's load executes after the 1421 store to z has propagated to P0 (an rfe link) 1420 store to z has propagated to P0 (an rfe link). 1422 1421 1423 In summary, the fact that the hb relation lin 1422 In summary, the fact that the hb relation links memory access events 1424 in the order they execute means that it must 1423 in the order they execute means that it must not have cycles. This 1425 requirement is the content of the LKMM's "hap 1424 requirement is the content of the LKMM's "happens-before" axiom. 1426 1425 1427 The LKMM defines yet another relation connect 1426 The LKMM defines yet another relation connected to times of 1428 instruction execution, but it is not included 1427 instruction execution, but it is not included in hb. It relies on the 1429 particular properties of strong fences, which 1428 particular properties of strong fences, which we cover in the next 1430 section. 1429 section. 1431 1430 1432 1431 1433 THE PROPAGATES-BEFORE RELATION: pb 1432 THE PROPAGATES-BEFORE RELATION: pb 1434 ---------------------------------- 1433 ---------------------------------- 1435 1434 1436 The propagates-before (pb) relation capitaliz 1435 The propagates-before (pb) relation capitalizes on the special 1437 features of strong fences. It links two even 1436 features of strong fences. It links two events E and F whenever some 1438 store is coherence-later than E and propagate 1437 store is coherence-later than E and propagates to every CPU and to RAM 1439 before F executes. The formal definition req 1438 before F executes. The formal definition requires that E be linked to 1440 F via a coe or fre link, an arbitrary number 1439 F via a coe or fre link, an arbitrary number of cumul-fences, an 1441 optional rfe link, a strong fence, and an arb 1440 optional rfe link, a strong fence, and an arbitrary number of hb 1442 links. Let's see how this definition works o 1441 links. Let's see how this definition works out. 1443 1442 1444 Consider first the case where E is a store (i 1443 Consider first the case where E is a store (implying that the sequence 1445 of links begins with coe). Then there are ev 1444 of links begins with coe). Then there are events W, X, Y, and Z such 1446 that: 1445 that: 1447 1446 1448 E ->coe W ->cumul-fence* X ->rfe? Y - 1447 E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F, 1449 1448 1450 where the * suffix indicates an arbitrary num 1449 where the * suffix indicates an arbitrary number of links of the 1451 specified type, and the ? suffix indicates th 1450 specified type, and the ? suffix indicates the link is optional (Y may 1452 be equal to X). Because of the cumul-fence l 1451 be equal to X). Because of the cumul-fence links, we know that W will 1453 propagate to Y's CPU before X does, hence bef 1452 propagate to Y's CPU before X does, hence before Y executes and hence 1454 before the strong fence executes. Because th 1453 before the strong fence executes. Because this fence is strong, we 1455 know that W will propagate to every CPU and t 1454 know that W will propagate to every CPU and to RAM before Z executes. 1456 And because of the hb links, we know that Z w 1455 And because of the hb links, we know that Z will execute before F. 1457 Thus W, which comes later than E in the coher 1456 Thus W, which comes later than E in the coherence order, will 1458 propagate to every CPU and to RAM before F ex 1457 propagate to every CPU and to RAM before F executes. 1459 1458 1460 The case where E is a load is exactly the sam 1459 The case where E is a load is exactly the same, except that the first 1461 link in the sequence is fre instead of coe. 1460 link in the sequence is fre instead of coe. 1462 1461 1463 The existence of a pb link from E to F implie 1462 The existence of a pb link from E to F implies that E must execute 1464 before F. To see why, suppose that F execute 1463 before F. To see why, suppose that F executed first. Then W would 1465 have propagated to E's CPU before E executed. 1464 have propagated to E's CPU before E executed. If E was a store, the 1466 memory subsystem would then be forced to make 1465 memory subsystem would then be forced to make E come after W in the 1467 coherence order, contradicting the fact that 1466 coherence order, contradicting the fact that E ->coe W. If E was a 1468 load, the memory subsystem would then be forc 1467 load, the memory subsystem would then be forced to satisfy E's read 1469 request with the value stored by W or an even 1468 request with the value stored by W or an even later store, 1470 contradicting the fact that E ->fre W. 1469 contradicting the fact that E ->fre W. 1471 1470 1472 A good example illustrating how pb works is t 1471 A good example illustrating how pb works is the SB pattern with strong 1473 fences: 1472 fences: 1474 1473 1475 int x = 0, y = 0; 1474 int x = 0, y = 0; 1476 1475 1477 P0() 1476 P0() 1478 { 1477 { 1479 int r0; 1478 int r0; 1480 1479 1481 WRITE_ONCE(x, 1); 1480 WRITE_ONCE(x, 1); 1482 smp_mb(); 1481 smp_mb(); 1483 r0 = READ_ONCE(y); 1482 r0 = READ_ONCE(y); 1484 } 1483 } 1485 1484 1486 P1() 1485 P1() 1487 { 1486 { 1488 int r1; 1487 int r1; 1489 1488 1490 WRITE_ONCE(y, 1); 1489 WRITE_ONCE(y, 1); 1491 smp_mb(); 1490 smp_mb(); 1492 r1 = READ_ONCE(x); 1491 r1 = READ_ONCE(x); 1493 } 1492 } 1494 1493 1495 If r0 = 0 at the end then there is a pb link 1494 If r0 = 0 at the end then there is a pb link from P0's load to P1's 1496 load: an fre link from P0's load to P1's stor 1495 load: an fre link from P0's load to P1's store (which overwrites the 1497 value read by P0), and a strong fence between 1496 value read by P0), and a strong fence between P1's store and its load. 1498 In this example, the sequences of cumul-fence 1497 In this example, the sequences of cumul-fence and hb links are empty. 1499 Note that this pb link is not included in hb 1498 Note that this pb link is not included in hb as an instance of prop, 1500 because it does not start and end on the same 1499 because it does not start and end on the same CPU. 1501 1500 1502 Similarly, if r1 = 0 at the end then there is 1501 Similarly, if r1 = 0 at the end then there is a pb link from P1's load 1503 to P0's. This means that if both r1 and r2 w 1502 to P0's. This means that if both r1 and r2 were 0 there would be a 1504 cycle in pb, which is not possible since an i 1503 cycle in pb, which is not possible since an instruction cannot execute 1505 before itself. Thus, adding smp_mb() fences 1504 before itself. Thus, adding smp_mb() fences to the SB pattern 1506 prevents the r0 = 0, r1 = 0 outcome. 1505 prevents the r0 = 0, r1 = 0 outcome. 1507 1506 1508 In summary, the fact that the pb relation lin 1507 In summary, the fact that the pb relation links events in the order 1509 they execute means that it cannot have cycles 1508 they execute means that it cannot have cycles. This requirement is 1510 the content of the LKMM's "propagation" axiom 1509 the content of the LKMM's "propagation" axiom. 1511 1510 1512 1511 1513 RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, r 1512 RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb 1514 --------------------------------------------- 1513 ------------------------------------------------------------------------ 1515 1514 1516 RCU (Read-Copy-Update) is a powerful synchron 1515 RCU (Read-Copy-Update) is a powerful synchronization mechanism. It 1517 rests on two concepts: grace periods and read 1516 rests on two concepts: grace periods and read-side critical sections. 1518 1517 1519 A grace period is the span of time occupied b 1518 A grace period is the span of time occupied by a call to 1520 synchronize_rcu(). A read-side critical sect 1519 synchronize_rcu(). A read-side critical section (or just critical 1521 section, for short) is a region of code delim 1520 section, for short) is a region of code delimited by rcu_read_lock() 1522 at the start and rcu_read_unlock() at the end 1521 at the start and rcu_read_unlock() at the end. Critical sections can 1523 be nested, although we won't make use of this 1522 be nested, although we won't make use of this fact. 1524 1523 1525 As far as memory models are concerned, RCU's 1524 As far as memory models are concerned, RCU's main feature is its 1526 Grace-Period Guarantee, which states that a c 1525 Grace-Period Guarantee, which states that a critical section can never 1527 span a full grace period. In more detail, th 1526 span a full grace period. In more detail, the Guarantee says: 1528 1527 1529 For any critical section C and any gr 1528 For any critical section C and any grace period G, at least 1530 one of the following statements must 1529 one of the following statements must hold: 1531 1530 1532 (1) C ends before G does, and in addition 1531 (1) C ends before G does, and in addition, every store that 1533 propagates to C's CPU before the end 1532 propagates to C's CPU before the end of C must propagate to 1534 every CPU before G ends. 1533 every CPU before G ends. 1535 1534 1536 (2) G starts before C does, and in additi 1535 (2) G starts before C does, and in addition, every store that 1537 propagates to G's CPU before the star 1536 propagates to G's CPU before the start of G must propagate 1538 to every CPU before C starts. 1537 to every CPU before C starts. 1539 1538 1540 In particular, it is not possible for a criti 1539 In particular, it is not possible for a critical section to both start 1541 before and end after a grace period. 1540 before and end after a grace period. 1542 1541 1543 Here is a simple example of RCU in action: 1542 Here is a simple example of RCU in action: 1544 1543 1545 int x, y; 1544 int x, y; 1546 1545 1547 P0() 1546 P0() 1548 { 1547 { 1549 rcu_read_lock(); 1548 rcu_read_lock(); 1550 WRITE_ONCE(x, 1); 1549 WRITE_ONCE(x, 1); 1551 WRITE_ONCE(y, 1); 1550 WRITE_ONCE(y, 1); 1552 rcu_read_unlock(); 1551 rcu_read_unlock(); 1553 } 1552 } 1554 1553 1555 P1() 1554 P1() 1556 { 1555 { 1557 int r1, r2; 1556 int r1, r2; 1558 1557 1559 r1 = READ_ONCE(x); 1558 r1 = READ_ONCE(x); 1560 synchronize_rcu(); 1559 synchronize_rcu(); 1561 r2 = READ_ONCE(y); 1560 r2 = READ_ONCE(y); 1562 } 1561 } 1563 1562 1564 The Grace Period Guarantee tells us that when 1563 The Grace Period Guarantee tells us that when this code runs, it will 1565 never end with r1 = 1 and r2 = 0. The reason 1564 never end with r1 = 1 and r2 = 0. The reasoning is as follows. r1 = 1 1566 means that P0's store to x propagated to P1 b 1565 means that P0's store to x propagated to P1 before P1 called 1567 synchronize_rcu(), so P0's critical section m 1566 synchronize_rcu(), so P0's critical section must have started before 1568 P1's grace period, contrary to part (2) of th 1567 P1's grace period, contrary to part (2) of the Guarantee. On the 1569 other hand, r2 = 0 means that P0's store to y 1568 other hand, r2 = 0 means that P0's store to y, which occurs before the 1570 end of the critical section, did not propagat 1569 end of the critical section, did not propagate to P1 before the end of 1571 the grace period, contrary to part (1). Toge 1570 the grace period, contrary to part (1). Together the results violate 1572 the Guarantee. 1571 the Guarantee. 1573 1572 1574 In the kernel's implementations of RCU, the r 1573 In the kernel's implementations of RCU, the requirements for stores 1575 to propagate to every CPU are fulfilled by pl 1574 to propagate to every CPU are fulfilled by placing strong fences at 1576 suitable places in the RCU-related code. Thu 1575 suitable places in the RCU-related code. Thus, if a critical section 1577 starts before a grace period does then the cr 1576 starts before a grace period does then the critical section's CPU will 1578 execute an smp_mb() fence after the end of th 1577 execute an smp_mb() fence after the end of the critical section and 1579 some time before the grace period's synchroni 1578 some time before the grace period's synchronize_rcu() call returns. 1580 And if a critical section ends after a grace 1579 And if a critical section ends after a grace period does then the 1581 synchronize_rcu() routine will execute an smp 1580 synchronize_rcu() routine will execute an smp_mb() fence at its start 1582 and some time before the critical section's o 1581 and some time before the critical section's opening rcu_read_lock() 1583 executes. 1582 executes. 1584 1583 1585 What exactly do we mean by saying that a crit 1584 What exactly do we mean by saying that a critical section "starts 1586 before" or "ends after" a grace period? Some 1585 before" or "ends after" a grace period? Some aspects of the meaning 1587 are pretty obvious, as in the example above, 1586 are pretty obvious, as in the example above, but the details aren't 1588 entirely clear. The LKMM formalizes this not 1587 entirely clear. The LKMM formalizes this notion by means of the 1589 rcu-link relation. rcu-link encompasses a ve 1588 rcu-link relation. rcu-link encompasses a very general notion of 1590 "before": If E and F are RCU fence events (i. 1589 "before": If E and F are RCU fence events (i.e., rcu_read_lock(), 1591 rcu_read_unlock(), or synchronize_rcu()) then 1590 rcu_read_unlock(), or synchronize_rcu()) then among other things, 1592 E ->rcu-link F includes cases where E is po-b 1591 E ->rcu-link F includes cases where E is po-before some memory-access 1593 event X, F is po-after some memory-access eve 1592 event X, F is po-after some memory-access event Y, and we have any of 1594 X ->rfe Y, X ->co Y, or X ->fr Y. 1593 X ->rfe Y, X ->co Y, or X ->fr Y. 1595 1594 1596 The formal definition of the rcu-link relatio 1595 The formal definition of the rcu-link relation is more than a little 1597 obscure, and we won't give it here. It is cl 1596 obscure, and we won't give it here. It is closely related to the pb 1598 relation, and the details don't matter unless 1597 relation, and the details don't matter unless you want to comb through 1599 a somewhat lengthy formal proof. Pretty much 1598 a somewhat lengthy formal proof. Pretty much all you need to know 1600 about rcu-link is the information in the prec 1599 about rcu-link is the information in the preceding paragraph. 1601 1600 1602 The LKMM also defines the rcu-gp and rcu-rscs 1601 The LKMM also defines the rcu-gp and rcu-rscsi relations. They bring 1603 grace periods and read-side critical sections 1602 grace periods and read-side critical sections into the picture, in the 1604 following way: 1603 following way: 1605 1604 1606 E ->rcu-gp F means that E and F are i 1605 E ->rcu-gp F means that E and F are in fact the same event, 1607 and that event is a synchronize_rcu() 1606 and that event is a synchronize_rcu() fence (i.e., a grace 1608 period). 1607 period). 1609 1608 1610 E ->rcu-rscsi F means that E and F ar 1609 E ->rcu-rscsi F means that E and F are the rcu_read_unlock() 1611 and rcu_read_lock() fence events deli 1610 and rcu_read_lock() fence events delimiting some read-side 1612 critical section. (The 'i' at the en 1611 critical section. (The 'i' at the end of the name emphasizes 1613 that this relation is "inverted": It 1612 that this relation is "inverted": It links the end of the 1614 critical section to the start.) 1613 critical section to the start.) 1615 1614 1616 If we think of the rcu-link relation as stand 1615 If we think of the rcu-link relation as standing for an extended 1617 "before", then X ->rcu-gp Y ->rcu-link Z roug 1616 "before", then X ->rcu-gp Y ->rcu-link Z roughly says that X is a 1618 grace period which ends before Z begins. (In 1617 grace period which ends before Z begins. (In fact it covers more than 1619 this, because it also includes cases where so 1618 this, because it also includes cases where some store propagates to 1620 Z's CPU before Z begins but doesn't propagate 1619 Z's CPU before Z begins but doesn't propagate to some other CPU until 1621 after X ends.) Similarly, X ->rcu-rscsi Y -> 1620 after X ends.) Similarly, X ->rcu-rscsi Y ->rcu-link Z says that X is 1622 the end of a critical section which starts be 1621 the end of a critical section which starts before Z begins. 1623 1622 1624 The LKMM goes on to define the rcu-order rela 1623 The LKMM goes on to define the rcu-order relation as a sequence of 1625 rcu-gp and rcu-rscsi links separated by rcu-l 1624 rcu-gp and rcu-rscsi links separated by rcu-link links, in which the 1626 number of rcu-gp links is >= the number of rc 1625 number of rcu-gp links is >= the number of rcu-rscsi links. For 1627 example: 1626 example: 1628 1627 1629 X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi 1628 X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V 1630 1629 1631 would imply that X ->rcu-order V, because thi 1630 would imply that X ->rcu-order V, because this sequence contains two 1632 rcu-gp links and one rcu-rscsi link. (It als 1631 rcu-gp links and one rcu-rscsi link. (It also implies that 1633 X ->rcu-order T and Z ->rcu-order V.) On the 1632 X ->rcu-order T and Z ->rcu-order V.) On the other hand: 1634 1633 1635 X ->rcu-rscsi Y ->rcu-link Z ->rcu-rs 1634 X ->rcu-rscsi Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V 1636 1635 1637 does not imply X ->rcu-order V, because the s 1636 does not imply X ->rcu-order V, because the sequence contains only 1638 one rcu-gp link but two rcu-rscsi links. 1637 one rcu-gp link but two rcu-rscsi links. 1639 1638 1640 The rcu-order relation is important because t 1639 The rcu-order relation is important because the Grace Period Guarantee 1641 means that rcu-order links act kind of like s 1640 means that rcu-order links act kind of like strong fences. In 1642 particular, E ->rcu-order F implies not only 1641 particular, E ->rcu-order F implies not only that E begins before F 1643 ends, but also that any write po-before E wil 1642 ends, but also that any write po-before E will propagate to every CPU 1644 before any instruction po-after F can execute 1643 before any instruction po-after F can execute. (However, it does not 1645 imply that E must execute before F; in fact, 1644 imply that E must execute before F; in fact, each synchronize_rcu() 1646 fence event is linked to itself by rcu-order 1645 fence event is linked to itself by rcu-order as a degenerate case.) 1647 1646 1648 To prove this in full generality requires som 1647 To prove this in full generality requires some intellectual effort. 1649 We'll consider just a very simple case: 1648 We'll consider just a very simple case: 1650 1649 1651 G ->rcu-gp W ->rcu-link Z ->rcu-rscsi 1650 G ->rcu-gp W ->rcu-link Z ->rcu-rscsi F. 1652 1651 1653 This formula means that G and W are the same 1652 This formula means that G and W are the same event (a grace period), 1654 and there are events X, Y and a read-side cri 1653 and there are events X, Y and a read-side critical section C such that: 1655 1654 1656 1. G = W is po-before or equal to X; 1655 1. G = W is po-before or equal to X; 1657 1656 1658 2. X comes "before" Y in some sense ( 1657 2. X comes "before" Y in some sense (including rfe, co and fr); 1659 1658 1660 3. Y is po-before Z; 1659 3. Y is po-before Z; 1661 1660 1662 4. Z is the rcu_read_unlock() event m 1661 4. Z is the rcu_read_unlock() event marking the end of C; 1663 1662 1664 5. F is the rcu_read_lock() event mar 1663 5. F is the rcu_read_lock() event marking the start of C. 1665 1664 1666 From 1 - 4 we deduce that the grace period G 1665 From 1 - 4 we deduce that the grace period G ends before the critical 1667 section C. Then part (2) of the Grace Period 1666 section C. Then part (2) of the Grace Period Guarantee says not only 1668 that G starts before C does, but also that an 1667 that G starts before C does, but also that any write which executes on 1669 G's CPU before G starts must propagate to eve 1668 G's CPU before G starts must propagate to every CPU before C starts. 1670 In particular, the write propagates to every 1669 In particular, the write propagates to every CPU before F finishes 1671 executing and hence before any instruction po 1670 executing and hence before any instruction po-after F can execute. 1672 This sort of reasoning can be extended to han 1671 This sort of reasoning can be extended to handle all the situations 1673 covered by rcu-order. 1672 covered by rcu-order. 1674 1673 1675 The rcu-fence relation is a simple extension 1674 The rcu-fence relation is a simple extension of rcu-order. While 1676 rcu-order only links certain fence events (ca 1675 rcu-order only links certain fence events (calls to synchronize_rcu(), 1677 rcu_read_lock(), or rcu_read_unlock()), rcu-f 1676 rcu_read_lock(), or rcu_read_unlock()), rcu-fence links any events 1678 that are separated by an rcu-order link. Thi 1677 that are separated by an rcu-order link. This is analogous to the way 1679 the strong-fence relation links events that a 1678 the strong-fence relation links events that are separated by an 1680 smp_mb() fence event (as mentioned above, rcu 1679 smp_mb() fence event (as mentioned above, rcu-order links act kind of 1681 like strong fences). Written symbolically, X 1680 like strong fences). Written symbolically, X ->rcu-fence Y means 1682 there are fence events E and F such that: 1681 there are fence events E and F such that: 1683 1682 1684 X ->po E ->rcu-order F ->po Y. 1683 X ->po E ->rcu-order F ->po Y. 1685 1684 1686 From the discussion above, we see this implie 1685 From the discussion above, we see this implies not only that X 1687 executes before Y, but also (if X is a store) 1686 executes before Y, but also (if X is a store) that X propagates to 1688 every CPU before Y executes. Thus rcu-fence 1687 every CPU before Y executes. Thus rcu-fence is sort of a 1689 "super-strong" fence: Unlike the original str 1688 "super-strong" fence: Unlike the original strong fences (smp_mb() and 1690 synchronize_rcu()), rcu-fence is able to link 1689 synchronize_rcu()), rcu-fence is able to link events on different 1691 CPUs. (Perhaps this fact should lead us to s 1690 CPUs. (Perhaps this fact should lead us to say that rcu-fence isn't 1692 really a fence at all!) 1691 really a fence at all!) 1693 1692 1694 Finally, the LKMM defines the RCU-before (rb) 1693 Finally, the LKMM defines the RCU-before (rb) relation in terms of 1695 rcu-fence. This is done in essentially the s 1694 rcu-fence. This is done in essentially the same way as the pb 1696 relation was defined in terms of strong-fence 1695 relation was defined in terms of strong-fence. We will omit the 1697 details; the end result is that E ->rb F impl 1696 details; the end result is that E ->rb F implies E must execute 1698 before F, just as E ->pb F does (and for much 1697 before F, just as E ->pb F does (and for much the same reasons). 1699 1698 1700 Putting this all together, the LKMM expresses 1699 Putting this all together, the LKMM expresses the Grace Period 1701 Guarantee by requiring that the rb relation d 1700 Guarantee by requiring that the rb relation does not contain a cycle. 1702 Equivalently, this "rcu" axiom requires that 1701 Equivalently, this "rcu" axiom requires that there are no events E 1703 and F with E ->rcu-link F ->rcu-order E. Or 1702 and F with E ->rcu-link F ->rcu-order E. Or to put it a third way, 1704 the axiom requires that there are no cycles c 1703 the axiom requires that there are no cycles consisting of rcu-gp and 1705 rcu-rscsi alternating with rcu-link, where th 1704 rcu-rscsi alternating with rcu-link, where the number of rcu-gp links 1706 is >= the number of rcu-rscsi links. 1705 is >= the number of rcu-rscsi links. 1707 1706 1708 Justifying the axiom isn't easy, but it is in 1707 Justifying the axiom isn't easy, but it is in fact a valid 1709 formalization of the Grace Period Guarantee. 1708 formalization of the Grace Period Guarantee. We won't attempt to go 1710 through the detailed argument, but the follow 1709 through the detailed argument, but the following analysis gives a 1711 taste of what is involved. Suppose both part 1710 taste of what is involved. Suppose both parts of the Guarantee are 1712 violated: A critical section starts before a 1711 violated: A critical section starts before a grace period, and some 1713 store propagates to the critical section's CP 1712 store propagates to the critical section's CPU before the end of the 1714 critical section but doesn't propagate to som 1713 critical section but doesn't propagate to some other CPU until after 1715 the end of the grace period. 1714 the end of the grace period. 1716 1715 1717 Putting symbols to these ideas, let L and U b 1716 Putting symbols to these ideas, let L and U be the rcu_read_lock() and 1718 rcu_read_unlock() fence events delimiting the 1717 rcu_read_unlock() fence events delimiting the critical section in 1719 question, and let S be the synchronize_rcu() 1718 question, and let S be the synchronize_rcu() fence event for the grace 1720 period. Saying that the critical section sta 1719 period. Saying that the critical section starts before S means there 1721 are events Q and R where Q is po-after L (whi 1720 are events Q and R where Q is po-after L (which marks the start of the 1722 critical section), Q is "before" R in the sen 1721 critical section), Q is "before" R in the sense used by the rcu-link 1723 relation, and R is po-before the grace period 1722 relation, and R is po-before the grace period S. Thus we have: 1724 1723 1725 L ->rcu-link S. 1724 L ->rcu-link S. 1726 1725 1727 Let W be the store mentioned above, let Y com 1726 Let W be the store mentioned above, let Y come before the end of the 1728 critical section and witness that W propagate 1727 critical section and witness that W propagates to the critical 1729 section's CPU by reading from W, and let Z on 1728 section's CPU by reading from W, and let Z on some arbitrary CPU be a 1730 witness that W has not propagated to that CPU 1729 witness that W has not propagated to that CPU, where Z happens after 1731 some event X which is po-after S. Symbolical 1730 some event X which is po-after S. Symbolically, this amounts to: 1732 1731 1733 S ->po X ->hb* Z ->fr W ->rf Y ->po U 1732 S ->po X ->hb* Z ->fr W ->rf Y ->po U. 1734 1733 1735 The fr link from Z to W indicates that W has 1734 The fr link from Z to W indicates that W has not propagated to Z's CPU 1736 at the time that Z executes. From this, it c 1735 at the time that Z executes. From this, it can be shown (see the 1737 discussion of the rcu-link relation earlier) 1736 discussion of the rcu-link relation earlier) that S and U are related 1738 by rcu-link: 1737 by rcu-link: 1739 1738 1740 S ->rcu-link U. 1739 S ->rcu-link U. 1741 1740 1742 Since S is a grace period we have S ->rcu-gp 1741 Since S is a grace period we have S ->rcu-gp S, and since L and U are 1743 the start and end of the critical section C w 1742 the start and end of the critical section C we have U ->rcu-rscsi L. 1744 From this we obtain: 1743 From this we obtain: 1745 1744 1746 S ->rcu-gp S ->rcu-link U ->rcu-rscsi 1745 S ->rcu-gp S ->rcu-link U ->rcu-rscsi L ->rcu-link S, 1747 1746 1748 a forbidden cycle. Thus the "rcu" axiom rule 1747 a forbidden cycle. Thus the "rcu" axiom rules out this violation of 1749 the Grace Period Guarantee. 1748 the Grace Period Guarantee. 1750 1749 1751 For something a little more down-to-earth, le 1750 For something a little more down-to-earth, let's see how the axiom 1752 works out in practice. Consider the RCU code 1751 works out in practice. Consider the RCU code example from above, this 1753 time with statement labels added: 1752 time with statement labels added: 1754 1753 1755 int x, y; 1754 int x, y; 1756 1755 1757 P0() 1756 P0() 1758 { 1757 { 1759 L: rcu_read_lock(); 1758 L: rcu_read_lock(); 1760 X: WRITE_ONCE(x, 1); 1759 X: WRITE_ONCE(x, 1); 1761 Y: WRITE_ONCE(y, 1); 1760 Y: WRITE_ONCE(y, 1); 1762 U: rcu_read_unlock(); 1761 U: rcu_read_unlock(); 1763 } 1762 } 1764 1763 1765 P1() 1764 P1() 1766 { 1765 { 1767 int r1, r2; 1766 int r1, r2; 1768 1767 1769 Z: r1 = READ_ONCE(x); 1768 Z: r1 = READ_ONCE(x); 1770 S: synchronize_rcu(); 1769 S: synchronize_rcu(); 1771 W: r2 = READ_ONCE(y); 1770 W: r2 = READ_ONCE(y); 1772 } 1771 } 1773 1772 1774 1773 1775 If r2 = 0 at the end then P0's store at Y ove 1774 If r2 = 0 at the end then P0's store at Y overwrites the value that 1776 P1's load at W reads from, so we have W ->fre 1775 P1's load at W reads from, so we have W ->fre Y. Since S ->po W and 1777 also Y ->po U, we get S ->rcu-link U. In add 1776 also Y ->po U, we get S ->rcu-link U. In addition, S ->rcu-gp S 1778 because S is a grace period. 1777 because S is a grace period. 1779 1778 1780 If r1 = 1 at the end then P1's load at Z read 1779 If r1 = 1 at the end then P1's load at Z reads from P0's store at X, 1781 so we have X ->rfe Z. Together with L ->po X 1780 so we have X ->rfe Z. Together with L ->po X and Z ->po S, this 1782 yields L ->rcu-link S. And since L and U are 1781 yields L ->rcu-link S. And since L and U are the start and end of a 1783 critical section, we have U ->rcu-rscsi L. 1782 critical section, we have U ->rcu-rscsi L. 1784 1783 1785 Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S 1784 Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S ->rcu-link U is a 1786 forbidden cycle, violating the "rcu" axiom. 1785 forbidden cycle, violating the "rcu" axiom. Hence the outcome is not 1787 allowed by the LKMM, as we would expect. 1786 allowed by the LKMM, as we would expect. 1788 1787 1789 For contrast, let's see what can happen in a 1788 For contrast, let's see what can happen in a more complicated example: 1790 1789 1791 int x, y, z; 1790 int x, y, z; 1792 1791 1793 P0() 1792 P0() 1794 { 1793 { 1795 int r0; 1794 int r0; 1796 1795 1797 L0: rcu_read_lock(); 1796 L0: rcu_read_lock(); 1798 r0 = READ_ONCE(x); 1797 r0 = READ_ONCE(x); 1799 WRITE_ONCE(y, 1); 1798 WRITE_ONCE(y, 1); 1800 U0: rcu_read_unlock(); 1799 U0: rcu_read_unlock(); 1801 } 1800 } 1802 1801 1803 P1() 1802 P1() 1804 { 1803 { 1805 int r1; 1804 int r1; 1806 1805 1807 r1 = READ_ONCE(y); 1806 r1 = READ_ONCE(y); 1808 S1: synchronize_rcu(); 1807 S1: synchronize_rcu(); 1809 WRITE_ONCE(z, 1); 1808 WRITE_ONCE(z, 1); 1810 } 1809 } 1811 1810 1812 P2() 1811 P2() 1813 { 1812 { 1814 int r2; 1813 int r2; 1815 1814 1816 L2: rcu_read_lock(); 1815 L2: rcu_read_lock(); 1817 r2 = READ_ONCE(z); 1816 r2 = READ_ONCE(z); 1818 WRITE_ONCE(x, 1); 1817 WRITE_ONCE(x, 1); 1819 U2: rcu_read_unlock(); 1818 U2: rcu_read_unlock(); 1820 } 1819 } 1821 1820 1822 If r0 = r1 = r2 = 1 at the end, then similar 1821 If r0 = r1 = r2 = 1 at the end, then similar reasoning to before shows 1823 that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp 1822 that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp S1 ->rcu-link U2 ->rcu-rscsi 1824 L2 ->rcu-link U0. However this cycle is not 1823 L2 ->rcu-link U0. However this cycle is not forbidden, because the 1825 sequence of relations contains fewer instance 1824 sequence of relations contains fewer instances of rcu-gp (one) than of 1826 rcu-rscsi (two). Consequently the outcome is 1825 rcu-rscsi (two). Consequently the outcome is allowed by the LKMM. 1827 The following instruction timing diagram show 1826 The following instruction timing diagram shows how it might actually 1828 occur: 1827 occur: 1829 1828 1830 P0 P1 1829 P0 P1 P2 1831 -------------------- -------------------- 1830 -------------------- -------------------- -------------------- 1832 rcu_read_lock() 1831 rcu_read_lock() 1833 WRITE_ONCE(y, 1) 1832 WRITE_ONCE(y, 1) 1834 r1 = READ_ONCE(y) 1833 r1 = READ_ONCE(y) 1835 synchronize_rcu() sta 1834 synchronize_rcu() starts 1836 . 1835 . rcu_read_lock() 1837 . 1836 . WRITE_ONCE(x, 1) 1838 r0 = READ_ONCE(x) . 1837 r0 = READ_ONCE(x) . 1839 rcu_read_unlock() . 1838 rcu_read_unlock() . 1840 synchronize_rcu() end 1839 synchronize_rcu() ends 1841 WRITE_ONCE(z, 1) 1840 WRITE_ONCE(z, 1) 1842 1841 r2 = READ_ONCE(z) 1843 1842 rcu_read_unlock() 1844 1843 1845 This requires P0 and P2 to execute their load 1844 This requires P0 and P2 to execute their loads and stores out of 1846 program order, but of course they are allowed 1845 program order, but of course they are allowed to do so. And as you 1847 can see, the Grace Period Guarantee is not vi 1846 can see, the Grace Period Guarantee is not violated: The critical 1848 section in P0 both starts before P1's grace p 1847 section in P0 both starts before P1's grace period does and ends 1849 before it does, and the critical section in P 1848 before it does, and the critical section in P2 both starts after P1's 1850 grace period does and ends after it does. 1849 grace period does and ends after it does. 1851 1850 1852 The LKMM supports SRCU (Sleepable Read-Copy-U !! 1851 Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in 1853 normal RCU. The ideas involved are much the !! 1852 addition to normal RCU. The ideas involved are much the same as 1854 relations srcu-gp and srcu-rscsi added to rep !! 1853 above, with new relations srcu-gp and srcu-rscsi added to represent 1855 and read-side critical sections. However, th !! 1854 SRCU grace periods and read-side critical sections. There is a 1856 differences between RCU read-side critical se !! 1855 restriction on the srcu-gp and srcu-rscsi links that can appear in an 1857 counterparts, as described in the next sectio !! 1856 rcu-order sequence (the srcu-rscsi links must be paired with srcu-gp 1858 !! 1857 links having the same SRCU domain with proper nesting); the details 1859 !! 1858 are relatively unimportant. 1860 SRCU READ-SIDE CRITICAL SECTIONS << 1861 -------------------------------- << 1862 << 1863 The LKMM uses the srcu-rscsi relation to mode << 1864 sections. They differ from RCU read-side cri << 1865 following respects: << 1866 << 1867 1. Unlike the analogous RCU primitives, << 1868 srcu_read_lock(), and srcu_read_unloc << 1869 struct srcu_struct as an argument. T << 1870 an SRCU domain, and calls linked by s << 1871 same domain. Read-side critical sect << 1872 associated with different domains are << 1873 another; the SRCU version of the RCU << 1874 to pairs of critical sections and gra << 1875 same domain. << 1876 << 1877 2. srcu_read_lock() returns a value, cal << 1878 be passed to the matching srcu_read_u << 1879 rcu_read_lock() and rcu_read_unlock() << 1880 call does not always have to match th << 1881 srcu_read_unlock(). In fact, it is p << 1882 read-side critical sections to overla << 1883 following example (where s is an srcu << 1884 are integer variables): << 1885 << 1886 idx1 = srcu_read_lock(&s); << 1887 idx2 = srcu_read_lock(&s); << 1888 srcu_read_unlock(&s, idx1); << 1889 srcu_read_unlock(&s, idx2); << 1890 << 1891 The matching is determined entirely b << 1892 index value. By contrast, if the cal << 1893 rcu_read_lock() and rcu_read_unlock() << 1894 created two nested (fully overlapping << 1895 sections: an inner one and an outer o << 1896 << 1897 3. The srcu_down_read() and srcu_up_read << 1898 exactly like srcu_read_lock() and src << 1899 that matching calls don't have to exe << 1900 (The names are meant to be suggestive << 1901 semaphores.) Since the matching is d << 1902 pointer and index value, these primit << 1903 an SRCU read-side critical section to << 1904 on another, so to speak. << 1905 << 1906 In order to account for these properties of S << 1907 srcu_read_lock() as a special type of load ev << 1908 appropriate, since it takes a memory location << 1909 a value, just as a load does) and srcu_read_u << 1910 of store event (again appropriate, since it t << 1911 memory location and a value). These loads an << 1912 belonging to the "srcu-lock" and "srcu-unlock << 1913 respectively. << 1914 << 1915 This approach allows the LKMM to tell whether << 1916 associated with the same SRCU domain, simply << 1917 access the same memory location (i.e., they a << 1918 relation). It also gives a way to tell which << 1919 particular lock, by checking for the presence << 1920 from the load (srcu-lock) to the store (srcu- << 1921 given the situation outlined earlier (with st << 1922 << 1923 A: idx1 = srcu_read_lock(&s); << 1924 B: idx2 = srcu_read_lock(&s); << 1925 C: srcu_read_unlock(&s, idx1); << 1926 D: srcu_read_unlock(&s, idx2); << 1927 << 1928 the LKMM will treat A and B as loads from s y << 1929 idx1 and idx2 respectively. Similarly, it wi << 1930 though they stored the values from idx1 and i << 1931 is much as if we had written: << 1932 << 1933 A: idx1 = READ_ONCE(s); << 1934 B: idx2 = READ_ONCE(s); << 1935 C: WRITE_ONCE(s, idx1); << 1936 D: WRITE_ONCE(s, idx2); << 1937 << 1938 except for the presence of the special srcu-l << 1939 annotations. You can see at once that we hav << 1940 B ->data D. These dependencies tell the LKMM << 1941 srcu-unlock event matching srcu-lock event A, << 1942 srcu-unlock event matching srcu-lock event B. << 1943 << 1944 This approach is admittedly a hack, and it ha << 1945 to problems. For example, in: << 1946 << 1947 idx1 = srcu_read_lock(&s); << 1948 srcu_read_unlock(&s, idx1); << 1949 idx2 = srcu_read_lock(&s); << 1950 srcu_read_unlock(&s, idx2); << 1951 << 1952 the LKMM will believe that idx2 must have the << 1953 since it reads from the immediately preceding << 1954 Fortunately this won't matter, assuming that << 1955 anything with SRCU index values other than pa << 1956 srcu_read_unlock() or srcu_up_read() calls. << 1957 << 1958 However, sometimes it is necessary to store a << 1959 shared variable temporarily. In fact, this i << 1960 srcu_down_read() to pass the index it gets to << 1961 on a different CPU. In more detail, we might << 1962 << 1963 struct srcu_struct s; << 1964 int x; << 1965 << 1966 P0() << 1967 { << 1968 int r0; << 1969 << 1970 A: r0 = srcu_down_read(&s); << 1971 B: WRITE_ONCE(x, r0); << 1972 } << 1973 << 1974 P1() << 1975 { << 1976 int r1; << 1977 << 1978 C: r1 = READ_ONCE(x); << 1979 D: srcu_up_read(&s, r1); << 1980 } << 1981 << 1982 Assuming that P1 executes after P0 and does r << 1983 stored in x, we can write this (using bracket << 1984 annotations) as: << 1985 << 1986 A[srcu-lock] ->data B[once] ->rf C[on << 1987 << 1988 The LKMM defines a carry-srcu-data relation t << 1989 it permits an arbitrarily long sequence of << 1990 << 1991 data ; rf << 1992 << 1993 pairs (that is, a data link followed by an rf << 1994 an srcu-lock event and the final data depende << 1995 matching srcu-unlock event. carry-srcu-data << 1996 need to ensure that none of the intermediate << 1997 sequence are instances of srcu-unlock. This << 1998 pattern like the one above: << 1999 << 2000 A: idx1 = srcu_read_lock(&s); << 2001 B: srcu_read_unlock(&s, idx1); << 2002 C: idx2 = srcu_read_lock(&s); << 2003 D: srcu_read_unlock(&s, idx2); << 2004 << 2005 the LKMM treats B as a store to the variable << 2006 that variable, creating an undesirable rf lin << 2007 << 2008 A ->data B ->rf C ->data D. << 2009 << 2010 This would cause carry-srcu-data to mistakenl << 2011 dependency from A to D, giving the impression << 2012 srcu-unlock event matching A's srcu-lock. To << 2013 carry-srcu-data does not accept sequences in << 2014 the intermediate ->data links (B above) is an << 2015 1859 2016 1860 2017 LOCKING 1861 LOCKING 2018 ------- 1862 ------- 2019 1863 2020 The LKMM includes locking. In fact, there is 1864 The LKMM includes locking. In fact, there is special code for locking 2021 in the formal model, added in order to make t 1865 in the formal model, added in order to make tools run faster. 2022 However, this special code is intended to be 1866 However, this special code is intended to be more or less equivalent 2023 to concepts we have already covered. A spinl 1867 to concepts we have already covered. A spinlock_t variable is treated 2024 the same as an int, and spin_lock(&s) is trea 1868 the same as an int, and spin_lock(&s) is treated almost the same as: 2025 1869 2026 while (cmpxchg_acquire(&s, 0, 1) != 0 1870 while (cmpxchg_acquire(&s, 0, 1) != 0) 2027 cpu_relax(); 1871 cpu_relax(); 2028 1872 2029 This waits until s is equal to 0 and then ato 1873 This waits until s is equal to 0 and then atomically sets it to 1, 2030 and the read part of the cmpxchg operation ac 1874 and the read part of the cmpxchg operation acts as an acquire fence. 2031 An alternate way to express the same thing wo 1875 An alternate way to express the same thing would be: 2032 1876 2033 r = xchg_acquire(&s, 1); 1877 r = xchg_acquire(&s, 1); 2034 1878 2035 along with a requirement that at the end, r = 1879 along with a requirement that at the end, r = 0. Similarly, 2036 spin_trylock(&s) is treated almost the same a 1880 spin_trylock(&s) is treated almost the same as: 2037 1881 2038 return !cmpxchg_acquire(&s, 0, 1); 1882 return !cmpxchg_acquire(&s, 0, 1); 2039 1883 2040 which atomically sets s to 1 if it is current 1884 which atomically sets s to 1 if it is currently equal to 0 and returns 2041 true if it succeeds (the read part of the cmp 1885 true if it succeeds (the read part of the cmpxchg operation acts as an 2042 acquire fence only if the operation is succes 1886 acquire fence only if the operation is successful). spin_unlock(&s) 2043 is treated almost the same as: 1887 is treated almost the same as: 2044 1888 2045 smp_store_release(&s, 0); 1889 smp_store_release(&s, 0); 2046 1890 2047 The "almost" qualifiers above need some expla 1891 The "almost" qualifiers above need some explanation. In the LKMM, the 2048 store-release in a spin_unlock() and the load 1892 store-release in a spin_unlock() and the load-acquire which forms the 2049 first half of the atomic rmw update in a spin 1893 first half of the atomic rmw update in a spin_lock() or a successful 2050 spin_trylock() -- we can call these things lo 1894 spin_trylock() -- we can call these things lock-releases and 2051 lock-acquires -- have two properties beyond t 1895 lock-acquires -- have two properties beyond those of ordinary releases 2052 and acquires. 1896 and acquires. 2053 1897 2054 First, when a lock-acquire reads from or is p 1898 First, when a lock-acquire reads from or is po-after a lock-release, 2055 the LKMM requires that every instruction po-b 1899 the LKMM requires that every instruction po-before the lock-release 2056 must execute before any instruction po-after 1900 must execute before any instruction po-after the lock-acquire. This 2057 would naturally hold if the release and acqui 1901 would naturally hold if the release and acquire operations were on 2058 different CPUs and accessed the same lock var 1902 different CPUs and accessed the same lock variable, but the LKMM says 2059 it also holds when they are on the same CPU, 1903 it also holds when they are on the same CPU, even if they access 2060 different lock variables. For example: 1904 different lock variables. For example: 2061 1905 2062 int x, y; 1906 int x, y; 2063 spinlock_t s, t; 1907 spinlock_t s, t; 2064 1908 2065 P0() 1909 P0() 2066 { 1910 { 2067 int r1, r2; 1911 int r1, r2; 2068 1912 2069 spin_lock(&s); 1913 spin_lock(&s); 2070 r1 = READ_ONCE(x); 1914 r1 = READ_ONCE(x); 2071 spin_unlock(&s); 1915 spin_unlock(&s); 2072 spin_lock(&t); 1916 spin_lock(&t); 2073 r2 = READ_ONCE(y); 1917 r2 = READ_ONCE(y); 2074 spin_unlock(&t); 1918 spin_unlock(&t); 2075 } 1919 } 2076 1920 2077 P1() 1921 P1() 2078 { 1922 { 2079 WRITE_ONCE(y, 1); 1923 WRITE_ONCE(y, 1); 2080 smp_wmb(); 1924 smp_wmb(); 2081 WRITE_ONCE(x, 1); 1925 WRITE_ONCE(x, 1); 2082 } 1926 } 2083 1927 2084 Here the second spin_lock() is po-after the f 1928 Here the second spin_lock() is po-after the first spin_unlock(), and 2085 therefore the load of x must execute before t 1929 therefore the load of x must execute before the load of y, even though 2086 the two locking operations use different lock 1930 the two locking operations use different locks. Thus we cannot have 2087 r1 = 1 and r2 = 0 at the end (this is an inst 1931 r1 = 1 and r2 = 0 at the end (this is an instance of the MP pattern). 2088 1932 2089 This requirement does not apply to ordinary r 1933 This requirement does not apply to ordinary release and acquire 2090 fences, only to lock-related operations. For 1934 fences, only to lock-related operations. For instance, suppose P0() 2091 in the example had been written as: 1935 in the example had been written as: 2092 1936 2093 P0() 1937 P0() 2094 { 1938 { 2095 int r1, r2, r3; 1939 int r1, r2, r3; 2096 1940 2097 r1 = READ_ONCE(x); 1941 r1 = READ_ONCE(x); 2098 smp_store_release(&s, 1); 1942 smp_store_release(&s, 1); 2099 r3 = smp_load_acquire(&s); 1943 r3 = smp_load_acquire(&s); 2100 r2 = READ_ONCE(y); 1944 r2 = READ_ONCE(y); 2101 } 1945 } 2102 1946 2103 Then the CPU would be allowed to forward the 1947 Then the CPU would be allowed to forward the s = 1 value from the 2104 smp_store_release() to the smp_load_acquire() 1948 smp_store_release() to the smp_load_acquire(), executing the 2105 instructions in the following order: 1949 instructions in the following order: 2106 1950 2107 r3 = smp_load_acquire(&s); 1951 r3 = smp_load_acquire(&s); // Obtains r3 = 1 2108 r2 = READ_ONCE(y); 1952 r2 = READ_ONCE(y); 2109 r1 = READ_ONCE(x); 1953 r1 = READ_ONCE(x); 2110 smp_store_release(&s, 1); 1954 smp_store_release(&s, 1); // Value is forwarded 2111 1955 2112 and thus it could load y before x, obtaining 1956 and thus it could load y before x, obtaining r2 = 0 and r1 = 1. 2113 1957 2114 Second, when a lock-acquire reads from or is 1958 Second, when a lock-acquire reads from or is po-after a lock-release, 2115 and some other stores W and W' occur po-befor 1959 and some other stores W and W' occur po-before the lock-release and 2116 po-after the lock-acquire respectively, the L 1960 po-after the lock-acquire respectively, the LKMM requires that W must 2117 propagate to each CPU before W' does. For ex 1961 propagate to each CPU before W' does. For example, consider: 2118 1962 2119 int x, y; 1963 int x, y; 2120 spinlock_t s; 1964 spinlock_t s; 2121 1965 2122 P0() 1966 P0() 2123 { 1967 { 2124 spin_lock(&s); 1968 spin_lock(&s); 2125 WRITE_ONCE(x, 1); 1969 WRITE_ONCE(x, 1); 2126 spin_unlock(&s); 1970 spin_unlock(&s); 2127 } 1971 } 2128 1972 2129 P1() 1973 P1() 2130 { 1974 { 2131 int r1; 1975 int r1; 2132 1976 2133 spin_lock(&s); 1977 spin_lock(&s); 2134 r1 = READ_ONCE(x); 1978 r1 = READ_ONCE(x); 2135 WRITE_ONCE(y, 1); 1979 WRITE_ONCE(y, 1); 2136 spin_unlock(&s); 1980 spin_unlock(&s); 2137 } 1981 } 2138 1982 2139 P2() 1983 P2() 2140 { 1984 { 2141 int r2, r3; 1985 int r2, r3; 2142 1986 2143 r2 = READ_ONCE(y); 1987 r2 = READ_ONCE(y); 2144 smp_rmb(); 1988 smp_rmb(); 2145 r3 = READ_ONCE(x); 1989 r3 = READ_ONCE(x); 2146 } 1990 } 2147 1991 2148 If r1 = 1 at the end then the spin_lock() in 1992 If r1 = 1 at the end then the spin_lock() in P1 must have read from 2149 the spin_unlock() in P0. Hence the store to 1993 the spin_unlock() in P0. Hence the store to x must propagate to P2 2150 before the store to y does, so we cannot have 1994 before the store to y does, so we cannot have r2 = 1 and r3 = 0. But 2151 if P1 had used a lock variable different from 1995 if P1 had used a lock variable different from s, the writes could have 2152 propagated in either order. (On the other ha 1996 propagated in either order. (On the other hand, if the code in P0 and 2153 P1 had all executed on a single CPU, as in th 1997 P1 had all executed on a single CPU, as in the example before this 2154 one, then the writes would have propagated in 1998 one, then the writes would have propagated in order even if the two 2155 critical sections used different lock variabl 1999 critical sections used different lock variables.) 2156 2000 2157 These two special requirements for lock-relea 2001 These two special requirements for lock-release and lock-acquire do 2158 not arise from the operational model. Nevert 2002 not arise from the operational model. Nevertheless, kernel developers 2159 have come to expect and rely on them because 2003 have come to expect and rely on them because they do hold on all 2160 architectures supported by the Linux kernel, 2004 architectures supported by the Linux kernel, albeit for various 2161 differing reasons. 2005 differing reasons. 2162 2006 2163 2007 2164 PLAIN ACCESSES AND DATA RACES 2008 PLAIN ACCESSES AND DATA RACES 2165 ----------------------------- 2009 ----------------------------- 2166 2010 2167 In the LKMM, memory accesses such as READ_ONC 2011 In the LKMM, memory accesses such as READ_ONCE(x), atomic_inc(&y), 2168 smp_load_acquire(&z), and so on are collectiv 2012 smp_load_acquire(&z), and so on are collectively referred to as 2169 "marked" accesses, because they are all annot 2013 "marked" accesses, because they are all annotated with special 2170 operations of one kind or another. Ordinary 2014 operations of one kind or another. Ordinary C-language memory 2171 accesses such as x or y = 0 are simply called 2015 accesses such as x or y = 0 are simply called "plain" accesses. 2172 2016 2173 Early versions of the LKMM had nothing to say 2017 Early versions of the LKMM had nothing to say about plain accesses. 2174 The C standard allows compilers to assume tha 2018 The C standard allows compilers to assume that the variables affected 2175 by plain accesses are not concurrently read o 2019 by plain accesses are not concurrently read or written by any other 2176 threads or CPUs. This leaves compilers free 2020 threads or CPUs. This leaves compilers free to implement all manner 2177 of transformations or optimizations of code c 2021 of transformations or optimizations of code containing plain accesses, 2178 making such code very difficult for a memory 2022 making such code very difficult for a memory model to handle. 2179 2023 2180 Here is just one example of a possible pitfal 2024 Here is just one example of a possible pitfall: 2181 2025 2182 int a = 6; 2026 int a = 6; 2183 int *x = &a; 2027 int *x = &a; 2184 2028 2185 P0() 2029 P0() 2186 { 2030 { 2187 int *r1; 2031 int *r1; 2188 int r2 = 0; 2032 int r2 = 0; 2189 2033 2190 r1 = x; 2034 r1 = x; 2191 if (r1 != NULL) 2035 if (r1 != NULL) 2192 r2 = READ_ONCE(*r1); 2036 r2 = READ_ONCE(*r1); 2193 } 2037 } 2194 2038 2195 P1() 2039 P1() 2196 { 2040 { 2197 WRITE_ONCE(x, NULL); 2041 WRITE_ONCE(x, NULL); 2198 } 2042 } 2199 2043 2200 On the face of it, one would expect that when 2044 On the face of it, one would expect that when this code runs, the only 2201 possible final values for r2 are 6 and 0, dep 2045 possible final values for r2 are 6 and 0, depending on whether or not 2202 P1's store to x propagates to P0 before P0's 2046 P1's store to x propagates to P0 before P0's load from x executes. 2203 But since P0's load from x is a plain access, 2047 But since P0's load from x is a plain access, the compiler may decide 2204 to carry out the load twice (for the comparis 2048 to carry out the load twice (for the comparison against NULL, then again 2205 for the READ_ONCE()) and eliminate the tempor 2049 for the READ_ONCE()) and eliminate the temporary variable r1. The 2206 object code generated for P0 could therefore 2050 object code generated for P0 could therefore end up looking rather 2207 like this: 2051 like this: 2208 2052 2209 P0() 2053 P0() 2210 { 2054 { 2211 int r2 = 0; 2055 int r2 = 0; 2212 2056 2213 if (x != NULL) 2057 if (x != NULL) 2214 r2 = READ_ONCE(*x); 2058 r2 = READ_ONCE(*x); 2215 } 2059 } 2216 2060 2217 And now it is obvious that this code runs the 2061 And now it is obvious that this code runs the risk of dereferencing a 2218 NULL pointer, because P1's store to x might p 2062 NULL pointer, because P1's store to x might propagate to P0 after the 2219 test against NULL has been made but before th 2063 test against NULL has been made but before the READ_ONCE() executes. 2220 If the original code had said "r1 = READ_ONCE 2064 If the original code had said "r1 = READ_ONCE(x)" instead of "r1 = x", 2221 the compiler would not have performed this op 2065 the compiler would not have performed this optimization and there 2222 would be no possibility of a NULL-pointer der 2066 would be no possibility of a NULL-pointer dereference. 2223 2067 2224 Given the possibility of transformations like 2068 Given the possibility of transformations like this one, the LKMM 2225 doesn't try to predict all possible outcomes 2069 doesn't try to predict all possible outcomes of code containing plain 2226 accesses. It is instead content to determine 2070 accesses. It is instead content to determine whether the code 2227 violates the compiler's assumptions, which wo 2071 violates the compiler's assumptions, which would render the ultimate 2228 outcome undefined. 2072 outcome undefined. 2229 2073 2230 In technical terms, the compiler is allowed t 2074 In technical terms, the compiler is allowed to assume that when the 2231 program executes, there will not be any data 2075 program executes, there will not be any data races. A "data race" 2232 occurs when there are two memory accesses suc 2076 occurs when there are two memory accesses such that: 2233 2077 2234 1. they access the same location, 2078 1. they access the same location, 2235 2079 2236 2. at least one of them is a store, 2080 2. at least one of them is a store, 2237 2081 2238 3. at least one of them is plain, 2082 3. at least one of them is plain, 2239 2083 2240 4. they occur on different CPUs (or in d 2084 4. they occur on different CPUs (or in different threads on the 2241 same CPU), and 2085 same CPU), and 2242 2086 2243 5. they execute concurrently. 2087 5. they execute concurrently. 2244 2088 2245 In the literature, two accesses are said to " 2089 In the literature, two accesses are said to "conflict" if they satisfy 2246 1 and 2 above. We'll go a little farther and 2090 1 and 2 above. We'll go a little farther and say that two accesses 2247 are "race candidates" if they satisfy 1 - 4. 2091 are "race candidates" if they satisfy 1 - 4. Thus, whether or not two 2248 race candidates actually do race in a given e 2092 race candidates actually do race in a given execution depends on 2249 whether they are concurrent. 2093 whether they are concurrent. 2250 2094 2251 The LKMM tries to determine whether a program 2095 The LKMM tries to determine whether a program contains race candidates 2252 which may execute concurrently; if it does th 2096 which may execute concurrently; if it does then the LKMM says there is 2253 a potential data race and makes no prediction 2097 a potential data race and makes no predictions about the program's 2254 outcome. 2098 outcome. 2255 2099 2256 Determining whether two accesses are race can 2100 Determining whether two accesses are race candidates is easy; you can 2257 see that all the concepts involved in the def 2101 see that all the concepts involved in the definition above are already 2258 part of the memory model. The hard part is t 2102 part of the memory model. The hard part is telling whether they may 2259 execute concurrently. The LKMM takes a conse 2103 execute concurrently. The LKMM takes a conservative attitude, 2260 assuming that accesses may be concurrent unle 2104 assuming that accesses may be concurrent unless it can prove they 2261 are not. 2105 are not. 2262 2106 2263 If two memory accesses aren't concurrent then 2107 If two memory accesses aren't concurrent then one must execute before 2264 the other. Therefore the LKMM decides two ac 2108 the other. Therefore the LKMM decides two accesses aren't concurrent 2265 if they can be connected by a sequence of hb, 2109 if they can be connected by a sequence of hb, pb, and rb links 2266 (together referred to as xb, for "executes be 2110 (together referred to as xb, for "executes before"). However, there 2267 are two complicating factors. 2111 are two complicating factors. 2268 2112 2269 If X is a load and X executes before a store 2113 If X is a load and X executes before a store Y, then indeed there is 2270 no danger of X and Y being concurrent. After 2114 no danger of X and Y being concurrent. After all, Y can't have any 2271 effect on the value obtained by X until the m 2115 effect on the value obtained by X until the memory subsystem has 2272 propagated Y from its own CPU to X's CPU, whi 2116 propagated Y from its own CPU to X's CPU, which won't happen until 2273 some time after Y executes and thus after X e 2117 some time after Y executes and thus after X executes. But if X is a 2274 store, then even if X executes before Y it is 2118 store, then even if X executes before Y it is still possible that X 2275 will propagate to Y's CPU just as Y is execut 2119 will propagate to Y's CPU just as Y is executing. In such a case X 2276 could very well interfere somehow with Y, and 2120 could very well interfere somehow with Y, and we would have to 2277 consider X and Y to be concurrent. 2121 consider X and Y to be concurrent. 2278 2122 2279 Therefore when X is a store, for X and Y to b 2123 Therefore when X is a store, for X and Y to be non-concurrent the LKMM 2280 requires not only that X must execute before 2124 requires not only that X must execute before Y but also that X must 2281 propagate to Y's CPU before Y executes. (Or 2125 propagate to Y's CPU before Y executes. (Or vice versa, of course, if 2282 Y executes before X -- then Y must propagate 2126 Y executes before X -- then Y must propagate to X's CPU before X 2283 executes if Y is a store.) This is expressed 2127 executes if Y is a store.) This is expressed by the visibility 2284 relation (vis), where X ->vis Y is defined to 2128 relation (vis), where X ->vis Y is defined to hold if there is an 2285 intermediate event Z such that: 2129 intermediate event Z such that: 2286 2130 2287 X is connected to Z by a possibly emp 2131 X is connected to Z by a possibly empty sequence of 2288 cumul-fence links followed by an opti 2132 cumul-fence links followed by an optional rfe link (if none of 2289 these links are present, X and Z are 2133 these links are present, X and Z are the same event), 2290 2134 2291 and either: 2135 and either: 2292 2136 2293 Z is connected to Y by a strong-fence 2137 Z is connected to Y by a strong-fence link followed by a 2294 possibly empty sequence of xb links, 2138 possibly empty sequence of xb links, 2295 2139 2296 or: 2140 or: 2297 2141 2298 Z is on the same CPU as Y and is conn 2142 Z is on the same CPU as Y and is connected to Y by a possibly 2299 empty sequence of xb links (again, if 2143 empty sequence of xb links (again, if the sequence is empty it 2300 means Z and Y are the same event). 2144 means Z and Y are the same event). 2301 2145 2302 The motivations behind this definition are st 2146 The motivations behind this definition are straightforward: 2303 2147 2304 cumul-fence memory barriers force sto 2148 cumul-fence memory barriers force stores that are po-before 2305 the barrier to propagate to other CPU 2149 the barrier to propagate to other CPUs before stores that are 2306 po-after the barrier. 2150 po-after the barrier. 2307 2151 2308 An rfe link from an event W to an eve 2152 An rfe link from an event W to an event R says that R reads 2309 from W, which certainly means that W 2153 from W, which certainly means that W must have propagated to 2310 R's CPU before R executed. 2154 R's CPU before R executed. 2311 2155 2312 strong-fence memory barriers force st 2156 strong-fence memory barriers force stores that are po-before 2313 the barrier, or that propagate to the 2157 the barrier, or that propagate to the barrier's CPU before the 2314 barrier executes, to propagate to all 2158 barrier executes, to propagate to all CPUs before any events 2315 po-after the barrier can execute. 2159 po-after the barrier can execute. 2316 2160 2317 To see how this works out in practice, consid 2161 To see how this works out in practice, consider our old friend, the MP 2318 pattern (with fences and statement labels, bu 2162 pattern (with fences and statement labels, but without the conditional 2319 test): 2163 test): 2320 2164 2321 int buf = 0, flag = 0; 2165 int buf = 0, flag = 0; 2322 2166 2323 P0() 2167 P0() 2324 { 2168 { 2325 X: WRITE_ONCE(buf, 1); 2169 X: WRITE_ONCE(buf, 1); 2326 smp_wmb(); 2170 smp_wmb(); 2327 W: WRITE_ONCE(flag, 1); 2171 W: WRITE_ONCE(flag, 1); 2328 } 2172 } 2329 2173 2330 P1() 2174 P1() 2331 { 2175 { 2332 int r1; 2176 int r1; 2333 int r2 = 0; 2177 int r2 = 0; 2334 2178 2335 Z: r1 = READ_ONCE(flag); 2179 Z: r1 = READ_ONCE(flag); 2336 smp_rmb(); 2180 smp_rmb(); 2337 Y: r2 = READ_ONCE(buf); 2181 Y: r2 = READ_ONCE(buf); 2338 } 2182 } 2339 2183 2340 The smp_wmb() memory barrier gives a cumul-fe 2184 The smp_wmb() memory barrier gives a cumul-fence link from X to W, and 2341 assuming r1 = 1 at the end, there is an rfe l 2185 assuming r1 = 1 at the end, there is an rfe link from W to Z. This 2342 means that the store to buf must propagate fr 2186 means that the store to buf must propagate from P0 to P1 before Z 2343 executes. Next, Z and Y are on the same CPU 2187 executes. Next, Z and Y are on the same CPU and the smp_rmb() fence 2344 provides an xb link from Z to Y (i.e., it for 2188 provides an xb link from Z to Y (i.e., it forces Z to execute before 2345 Y). Therefore we have X ->vis Y: X must prop 2189 Y). Therefore we have X ->vis Y: X must propagate to Y's CPU before Y 2346 executes. 2190 executes. 2347 2191 2348 The second complicating factor mentioned abov 2192 The second complicating factor mentioned above arises from the fact 2349 that when we are considering data races, some 2193 that when we are considering data races, some of the memory accesses 2350 are plain. Now, although we have not said so 2194 are plain. Now, although we have not said so explicitly, up to this 2351 point most of the relations defined by the LK 2195 point most of the relations defined by the LKMM (ppo, hb, prop, 2352 cumul-fence, pb, and so on -- including vis) 2196 cumul-fence, pb, and so on -- including vis) apply only to marked 2353 accesses. 2197 accesses. 2354 2198 2355 There are good reasons for this restriction. 2199 There are good reasons for this restriction. The compiler is not 2356 allowed to apply fancy transformations to mar 2200 allowed to apply fancy transformations to marked accesses, and 2357 consequently each such access in the source c 2201 consequently each such access in the source code corresponds more or 2358 less directly to a single machine instruction 2202 less directly to a single machine instruction in the object code. But 2359 plain accesses are a different story; the com 2203 plain accesses are a different story; the compiler may combine them, 2360 split them up, duplicate them, eliminate them 2204 split them up, duplicate them, eliminate them, invent new ones, and 2361 who knows what else. Seeing a plain access i 2205 who knows what else. Seeing a plain access in the source code tells 2362 you almost nothing about what machine instruc 2206 you almost nothing about what machine instructions will end up in the 2363 object code. 2207 object code. 2364 2208 2365 Fortunately, the compiler isn't completely fr 2209 Fortunately, the compiler isn't completely free; it is subject to some 2366 limitations. For one, it is not allowed to i 2210 limitations. For one, it is not allowed to introduce a data race into 2367 the object code if the source code does not a 2211 the object code if the source code does not already contain a data 2368 race (if it could, memory models would be use 2212 race (if it could, memory models would be useless and no multithreaded 2369 code would be safe!). For another, it cannot 2213 code would be safe!). For another, it cannot move a plain access past 2370 a compiler barrier. 2214 a compiler barrier. 2371 2215 2372 A compiler barrier is a kind of fence, but as 2216 A compiler barrier is a kind of fence, but as the name implies, it 2373 only affects the compiler; it does not necess 2217 only affects the compiler; it does not necessarily have any effect on 2374 how instructions are executed by the CPU. In 2218 how instructions are executed by the CPU. In Linux kernel source 2375 code, the barrier() function is a compiler ba 2219 code, the barrier() function is a compiler barrier. It doesn't give 2376 rise directly to any machine instructions in 2220 rise directly to any machine instructions in the object code; rather, 2377 it affects how the compiler generates the res 2221 it affects how the compiler generates the rest of the object code. 2378 Given source code like this: 2222 Given source code like this: 2379 2223 2380 ... some memory accesses ... 2224 ... some memory accesses ... 2381 barrier(); 2225 barrier(); 2382 ... some other memory accesses ... 2226 ... some other memory accesses ... 2383 2227 2384 the barrier() function ensures that the machi 2228 the barrier() function ensures that the machine instructions 2385 corresponding to the first group of accesses 2229 corresponding to the first group of accesses will all end po-before 2386 any machine instructions corresponding to the 2230 any machine instructions corresponding to the second group of accesses 2387 -- even if some of the accesses are plain. ( 2231 -- even if some of the accesses are plain. (Of course, the CPU may 2388 then execute some of those accesses out of pr 2232 then execute some of those accesses out of program order, but we 2389 already know how to deal with such issues.) 2233 already know how to deal with such issues.) Without the barrier() 2390 there would be no such guarantee; the two gro 2234 there would be no such guarantee; the two groups of accesses could be 2391 intermingled or even reversed in the object c 2235 intermingled or even reversed in the object code. 2392 2236 2393 The LKMM doesn't say much about the barrier() 2237 The LKMM doesn't say much about the barrier() function, but it does 2394 require that all fences are also compiler bar 2238 require that all fences are also compiler barriers. In addition, it 2395 requires that the ordering properties of memo 2239 requires that the ordering properties of memory barriers such as 2396 smp_rmb() or smp_store_release() apply to pla 2240 smp_rmb() or smp_store_release() apply to plain accesses as well as to 2397 marked accesses. 2241 marked accesses. 2398 2242 2399 This is the key to analyzing data races. Con 2243 This is the key to analyzing data races. Consider the MP pattern 2400 again, now using plain accesses for buf: 2244 again, now using plain accesses for buf: 2401 2245 2402 int buf = 0, flag = 0; 2246 int buf = 0, flag = 0; 2403 2247 2404 P0() 2248 P0() 2405 { 2249 { 2406 U: buf = 1; 2250 U: buf = 1; 2407 smp_wmb(); 2251 smp_wmb(); 2408 X: WRITE_ONCE(flag, 1); 2252 X: WRITE_ONCE(flag, 1); 2409 } 2253 } 2410 2254 2411 P1() 2255 P1() 2412 { 2256 { 2413 int r1; 2257 int r1; 2414 int r2 = 0; 2258 int r2 = 0; 2415 2259 2416 Y: r1 = READ_ONCE(flag); 2260 Y: r1 = READ_ONCE(flag); 2417 if (r1) { 2261 if (r1) { 2418 smp_rmb(); 2262 smp_rmb(); 2419 V: r2 = buf; 2263 V: r2 = buf; 2420 } 2264 } 2421 } 2265 } 2422 2266 2423 This program does not contain a data race. A 2267 This program does not contain a data race. Although the U and V 2424 accesses are race candidates, the LKMM can pr 2268 accesses are race candidates, the LKMM can prove they are not 2425 concurrent as follows: 2269 concurrent as follows: 2426 2270 2427 The smp_wmb() fence in P0 is both a c 2271 The smp_wmb() fence in P0 is both a compiler barrier and a 2428 cumul-fence. It guarantees that no m 2272 cumul-fence. It guarantees that no matter what hash of 2429 machine instructions the compiler gen 2273 machine instructions the compiler generates for the plain 2430 access U, all those instructions will 2274 access U, all those instructions will be po-before the fence. 2431 Consequently U's store to buf, no mat 2275 Consequently U's store to buf, no matter how it is carried out 2432 at the machine level, must propagate 2276 at the machine level, must propagate to P1 before X's store to 2433 flag does. 2277 flag does. 2434 2278 2435 X and Y are both marked accesses. He 2279 X and Y are both marked accesses. Hence an rfe link from X to 2436 Y is a valid indicator that X propaga 2280 Y is a valid indicator that X propagated to P1 before Y 2437 executed, i.e., X ->vis Y. (And if t 2281 executed, i.e., X ->vis Y. (And if there is no rfe link then 2438 r1 will be 0, so V will not be execut 2282 r1 will be 0, so V will not be executed and ipso facto won't 2439 race with U.) 2283 race with U.) 2440 2284 2441 The smp_rmb() fence in P1 is a compil 2285 The smp_rmb() fence in P1 is a compiler barrier as well as a 2442 fence. It guarantees that all the ma 2286 fence. It guarantees that all the machine-level instructions 2443 corresponding to the access V will be 2287 corresponding to the access V will be po-after the fence, and 2444 therefore any loads among those instr 2288 therefore any loads among those instructions will execute 2445 after the fence does and hence after 2289 after the fence does and hence after Y does. 2446 2290 2447 Thus U's store to buf is forced to propagate 2291 Thus U's store to buf is forced to propagate to P1 before V's load 2448 executes (assuming V does execute), ruling ou 2292 executes (assuming V does execute), ruling out the possibility of a 2449 data race between them. 2293 data race between them. 2450 2294 2451 This analysis illustrates how the LKMM deals 2295 This analysis illustrates how the LKMM deals with plain accesses in 2452 general. Suppose R is a plain load and we wa 2296 general. Suppose R is a plain load and we want to show that R 2453 executes before some marked access E. We can 2297 executes before some marked access E. We can do this by finding a 2454 marked access X such that R and X are ordered 2298 marked access X such that R and X are ordered by a suitable fence and 2455 X ->xb* E. If E was also a plain access, we 2299 X ->xb* E. If E was also a plain access, we would also look for a 2456 marked access Y such that X ->xb* Y, and Y an 2300 marked access Y such that X ->xb* Y, and Y and E are ordered by a 2457 fence. We describe this arrangement by sayin 2301 fence. We describe this arrangement by saying that R is 2458 "post-bounded" by X and E is "pre-bounded" by 2302 "post-bounded" by X and E is "pre-bounded" by Y. 2459 2303 2460 In fact, we go one step further: Since R is a 2304 In fact, we go one step further: Since R is a read, we say that R is 2461 "r-post-bounded" by X. Similarly, E would be 2305 "r-post-bounded" by X. Similarly, E would be "r-pre-bounded" or 2462 "w-pre-bounded" by Y, depending on whether E 2306 "w-pre-bounded" by Y, depending on whether E was a store or a load. 2463 This distinction is needed because some fence 2307 This distinction is needed because some fences affect only loads 2464 (i.e., smp_rmb()) and some affect only stores 2308 (i.e., smp_rmb()) and some affect only stores (smp_wmb()); otherwise 2465 the two types of bounds are the same. And as 2309 the two types of bounds are the same. And as a degenerate case, we 2466 say that a marked access pre-bounds and post- 2310 say that a marked access pre-bounds and post-bounds itself (e.g., if R 2467 above were a marked load then X could simply 2311 above were a marked load then X could simply be taken to be R itself.) 2468 2312 2469 The need to distinguish between r- and w-boun 2313 The need to distinguish between r- and w-bounding raises yet another 2470 issue. When the source code contains a plain 2314 issue. When the source code contains a plain store, the compiler is 2471 allowed to put plain loads of the same locati 2315 allowed to put plain loads of the same location into the object code. 2472 For example, given the source code: 2316 For example, given the source code: 2473 2317 2474 x = 1; 2318 x = 1; 2475 2319 2476 the compiler is theoretically allowed to gene 2320 the compiler is theoretically allowed to generate object code that 2477 looks like: 2321 looks like: 2478 2322 2479 if (x != 1) 2323 if (x != 1) 2480 x = 1; 2324 x = 1; 2481 2325 2482 thereby adding a load (and possibly replacing 2326 thereby adding a load (and possibly replacing the store entirely). 2483 For this reason, whenever the LKMM requires a 2327 For this reason, whenever the LKMM requires a plain store to be 2484 w-pre-bounded or w-post-bounded by a marked a 2328 w-pre-bounded or w-post-bounded by a marked access, it also requires 2485 the store to be r-pre-bounded or r-post-bound 2329 the store to be r-pre-bounded or r-post-bounded, so as to handle cases 2486 where the compiler adds a load. 2330 where the compiler adds a load. 2487 2331 2488 (This may be overly cautious. We don't know 2332 (This may be overly cautious. We don't know of any examples where a 2489 compiler has augmented a store with a load in 2333 compiler has augmented a store with a load in this fashion, and the 2490 Linux kernel developers would probably fight 2334 Linux kernel developers would probably fight pretty hard to change a 2491 compiler if it ever did this. Still, better 2335 compiler if it ever did this. Still, better safe than sorry.) 2492 2336 2493 Incidentally, the other tranformation -- augm 2337 Incidentally, the other tranformation -- augmenting a plain load by 2494 adding in a store to the same location -- is 2338 adding in a store to the same location -- is not allowed. This is 2495 because the compiler cannot know whether any 2339 because the compiler cannot know whether any other CPUs might perform 2496 a concurrent load from that location. Two co 2340 a concurrent load from that location. Two concurrent loads don't 2497 constitute a race (they can't interfere with 2341 constitute a race (they can't interfere with each other), but a store 2498 does race with a concurrent load. Thus addin 2342 does race with a concurrent load. Thus adding a store might create a 2499 data race where one was not already present i 2343 data race where one was not already present in the source code, 2500 something the compiler is forbidden to do. A 2344 something the compiler is forbidden to do. Augmenting a store with a 2501 load, on the other hand, is acceptable becaus 2345 load, on the other hand, is acceptable because doing so won't create a 2502 data race unless one already existed. 2346 data race unless one already existed. 2503 2347 2504 The LKMM includes a second way to pre-bound p 2348 The LKMM includes a second way to pre-bound plain accesses, in 2505 addition to fences: an address dependency fro 2349 addition to fences: an address dependency from a marked load. That 2506 is, in the sequence: 2350 is, in the sequence: 2507 2351 2508 p = READ_ONCE(ptr); 2352 p = READ_ONCE(ptr); 2509 r = *p; 2353 r = *p; 2510 2354 2511 the LKMM says that the marked load of ptr pre 2355 the LKMM says that the marked load of ptr pre-bounds the plain load of 2512 *p; the marked load must execute before any o 2356 *p; the marked load must execute before any of the machine 2513 instructions corresponding to the plain load. 2357 instructions corresponding to the plain load. This is a reasonable 2514 stipulation, since after all, the CPU can't p 2358 stipulation, since after all, the CPU can't perform the load of *p 2515 until it knows what value p will hold. Furth 2359 until it knows what value p will hold. Furthermore, without some 2516 assumption like this one, some usages typical 2360 assumption like this one, some usages typical of RCU would count as 2517 data races. For example: 2361 data races. For example: 2518 2362 2519 int a = 1, b; 2363 int a = 1, b; 2520 int *ptr = &a; 2364 int *ptr = &a; 2521 2365 2522 P0() 2366 P0() 2523 { 2367 { 2524 b = 2; 2368 b = 2; 2525 rcu_assign_pointer(ptr, &b); 2369 rcu_assign_pointer(ptr, &b); 2526 } 2370 } 2527 2371 2528 P1() 2372 P1() 2529 { 2373 { 2530 int *p; 2374 int *p; 2531 int r; 2375 int r; 2532 2376 2533 rcu_read_lock(); 2377 rcu_read_lock(); 2534 p = rcu_dereference(ptr); 2378 p = rcu_dereference(ptr); 2535 r = *p; 2379 r = *p; 2536 rcu_read_unlock(); 2380 rcu_read_unlock(); 2537 } 2381 } 2538 2382 2539 (In this example the rcu_read_lock() and rcu_ 2383 (In this example the rcu_read_lock() and rcu_read_unlock() calls don't 2540 really do anything, because there aren't any 2384 really do anything, because there aren't any grace periods. They are 2541 included merely for the sake of good form; ty 2385 included merely for the sake of good form; typically P0 would call 2542 synchronize_rcu() somewhere after the rcu_ass 2386 synchronize_rcu() somewhere after the rcu_assign_pointer().) 2543 2387 2544 rcu_assign_pointer() performs a store-release 2388 rcu_assign_pointer() performs a store-release, so the plain store to b 2545 is definitely w-post-bounded before the store 2389 is definitely w-post-bounded before the store to ptr, and the two 2546 stores will propagate to P1 in that order. H 2390 stores will propagate to P1 in that order. However, rcu_dereference() 2547 is only equivalent to READ_ONCE(). While it 2391 is only equivalent to READ_ONCE(). While it is a marked access, it is 2548 not a fence or compiler barrier. Hence the o 2392 not a fence or compiler barrier. Hence the only guarantee we have 2549 that the load of ptr in P1 is r-pre-bounded b 2393 that the load of ptr in P1 is r-pre-bounded before the load of *p 2550 (thus avoiding a race) is the assumption abou 2394 (thus avoiding a race) is the assumption about address dependencies. 2551 2395 2552 This is a situation where the compiler can un 2396 This is a situation where the compiler can undermine the memory model, 2553 and a certain amount of care is required when 2397 and a certain amount of care is required when programming constructs 2554 like this one. In particular, comparisons be 2398 like this one. In particular, comparisons between the pointer and 2555 other known addresses can cause trouble. If 2399 other known addresses can cause trouble. If you have something like: 2556 2400 2557 p = rcu_dereference(ptr); 2401 p = rcu_dereference(ptr); 2558 if (p == &x) 2402 if (p == &x) 2559 r = *p; 2403 r = *p; 2560 2404 2561 then the compiler just might generate object 2405 then the compiler just might generate object code resembling: 2562 2406 2563 p = rcu_dereference(ptr); 2407 p = rcu_dereference(ptr); 2564 if (p == &x) 2408 if (p == &x) 2565 r = x; 2409 r = x; 2566 2410 2567 or even: 2411 or even: 2568 2412 2569 rtemp = x; 2413 rtemp = x; 2570 p = rcu_dereference(ptr); 2414 p = rcu_dereference(ptr); 2571 if (p == &x) 2415 if (p == &x) 2572 r = rtemp; 2416 r = rtemp; 2573 2417 2574 which would invalidate the memory model's ass 2418 which would invalidate the memory model's assumption, since the CPU 2575 could now perform the load of x before the lo 2419 could now perform the load of x before the load of ptr (there might be 2576 a control dependency but no address dependenc 2420 a control dependency but no address dependency at the machine level). 2577 2421 2578 Finally, it turns out there is a situation in 2422 Finally, it turns out there is a situation in which a plain write does 2579 not need to be w-post-bounded: when it is sep 2423 not need to be w-post-bounded: when it is separated from the other 2580 race-candidate access by a fence. At first g 2424 race-candidate access by a fence. At first glance this may seem 2581 impossible. After all, to be race candidates 2425 impossible. After all, to be race candidates the two accesses must 2582 be on different CPUs, and fences don't link e 2426 be on different CPUs, and fences don't link events on different CPUs. 2583 Well, normal fences don't -- but rcu-fence ca 2427 Well, normal fences don't -- but rcu-fence can! Here's an example: 2584 2428 2585 int x, y; 2429 int x, y; 2586 2430 2587 P0() 2431 P0() 2588 { 2432 { 2589 WRITE_ONCE(x, 1); 2433 WRITE_ONCE(x, 1); 2590 synchronize_rcu(); 2434 synchronize_rcu(); 2591 y = 3; 2435 y = 3; 2592 } 2436 } 2593 2437 2594 P1() 2438 P1() 2595 { 2439 { 2596 rcu_read_lock(); 2440 rcu_read_lock(); 2597 if (READ_ONCE(x) == 0) 2441 if (READ_ONCE(x) == 0) 2598 y = 2; 2442 y = 2; 2599 rcu_read_unlock(); 2443 rcu_read_unlock(); 2600 } 2444 } 2601 2445 2602 Do the plain stores to y race? Clearly not i 2446 Do the plain stores to y race? Clearly not if P1 reads a non-zero 2603 value for x, so let's assume the READ_ONCE(x) 2447 value for x, so let's assume the READ_ONCE(x) does obtain 0. This 2604 means that the read-side critical section in 2448 means that the read-side critical section in P1 must finish executing 2605 before the grace period in P0 does, because R 2449 before the grace period in P0 does, because RCU's Grace-Period 2606 Guarantee says that otherwise P0's store to x 2450 Guarantee says that otherwise P0's store to x would have propagated to 2607 P1 before the critical section started and so 2451 P1 before the critical section started and so would have been visible 2608 to the READ_ONCE(). (Another way of putting 2452 to the READ_ONCE(). (Another way of putting it is that the fre link 2609 from the READ_ONCE() to the WRITE_ONCE() give 2453 from the READ_ONCE() to the WRITE_ONCE() gives rise to an rcu-link 2610 between those two events.) 2454 between those two events.) 2611 2455 2612 This means there is an rcu-fence link from P1 2456 This means there is an rcu-fence link from P1's "y = 2" store to P0's 2613 "y = 3" store, and consequently the first mus 2457 "y = 3" store, and consequently the first must propagate from P1 to P0 2614 before the second can execute. Therefore the 2458 before the second can execute. Therefore the two stores cannot be 2615 concurrent and there is no race, even though 2459 concurrent and there is no race, even though P1's plain store to y 2616 isn't w-post-bounded by any marked accesses. 2460 isn't w-post-bounded by any marked accesses. 2617 2461 2618 Putting all this material together yields the 2462 Putting all this material together yields the following picture. For 2619 race-candidate stores W and W', where W ->co 2463 race-candidate stores W and W', where W ->co W', the LKMM says the 2620 stores don't race if W can be linked to W' by 2464 stores don't race if W can be linked to W' by a 2621 2465 2622 w-post-bounded ; vis ; w-pre-bounded 2466 w-post-bounded ; vis ; w-pre-bounded 2623 2467 2624 sequence. If W is plain then they also have 2468 sequence. If W is plain then they also have to be linked by an 2625 2469 2626 r-post-bounded ; xb* ; w-pre-bounded 2470 r-post-bounded ; xb* ; w-pre-bounded 2627 2471 2628 sequence, and if W' is plain then they also h 2472 sequence, and if W' is plain then they also have to be linked by a 2629 2473 2630 w-post-bounded ; vis ; r-pre-bounded 2474 w-post-bounded ; vis ; r-pre-bounded 2631 2475 2632 sequence. For race-candidate load R and stor 2476 sequence. For race-candidate load R and store W, the LKMM says the 2633 two accesses don't race if R can be linked to 2477 two accesses don't race if R can be linked to W by an 2634 2478 2635 r-post-bounded ; xb* ; w-pre-bounded 2479 r-post-bounded ; xb* ; w-pre-bounded 2636 2480 2637 sequence or if W can be linked to R by a 2481 sequence or if W can be linked to R by a 2638 2482 2639 w-post-bounded ; vis ; r-pre-bounded 2483 w-post-bounded ; vis ; r-pre-bounded 2640 2484 2641 sequence. For the cases involving a vis link 2485 sequence. For the cases involving a vis link, the LKMM also accepts 2642 sequences in which W is linked to W' or R by 2486 sequences in which W is linked to W' or R by a 2643 2487 2644 strong-fence ; xb* ; {w and/or r}-pre 2488 strong-fence ; xb* ; {w and/or r}-pre-bounded 2645 2489 2646 sequence with no post-bounding, and in every 2490 sequence with no post-bounding, and in every case the LKMM also allows 2647 the link simply to be a fence with no boundin 2491 the link simply to be a fence with no bounding at all. If no sequence 2648 of the appropriate sort exists, the LKMM says 2492 of the appropriate sort exists, the LKMM says that the accesses race. 2649 2493 2650 There is one more part of the LKMM related to 2494 There is one more part of the LKMM related to plain accesses (although 2651 not to data races) we should discuss. Recall 2495 not to data races) we should discuss. Recall that many relations such 2652 as hb are limited to marked accesses only. A 2496 as hb are limited to marked accesses only. As a result, the 2653 happens-before, propagates-before, and rcu ax 2497 happens-before, propagates-before, and rcu axioms (which state that 2654 various relation must not contain a cycle) do 2498 various relation must not contain a cycle) doesn't apply to plain 2655 accesses. Nevertheless, we do want to rule o 2499 accesses. Nevertheless, we do want to rule out such cycles, because 2656 they don't make sense even for plain accesses 2500 they don't make sense even for plain accesses. 2657 2501 2658 To this end, the LKMM imposes three extra res 2502 To this end, the LKMM imposes three extra restrictions, together 2659 called the "plain-coherence" axiom because of 2503 called the "plain-coherence" axiom because of their resemblance to the 2660 rules used by the operational model to ensure 2504 rules used by the operational model to ensure cache coherence (that 2661 is, the rules governing the memory subsystem' 2505 is, the rules governing the memory subsystem's choice of a store to 2662 satisfy a load request and its determination 2506 satisfy a load request and its determination of where a store will 2663 fall in the coherence order): 2507 fall in the coherence order): 2664 2508 2665 If R and W are race candidates and it 2509 If R and W are race candidates and it is possible to link R to 2666 W by one of the xb* sequences listed 2510 W by one of the xb* sequences listed above, then W ->rfe R is 2667 not allowed (i.e., a load cannot read 2511 not allowed (i.e., a load cannot read from a store that it 2668 executes before, even if one or both 2512 executes before, even if one or both is plain). 2669 2513 2670 If W and R are race candidates and it 2514 If W and R are race candidates and it is possible to link W to 2671 R by one of the vis sequences listed 2515 R by one of the vis sequences listed above, then R ->fre W is 2672 not allowed (i.e., if a store is visi 2516 not allowed (i.e., if a store is visible to a load then the 2673 load must read from that store or one 2517 load must read from that store or one coherence-after it). 2674 2518 2675 If W and W' are race candidates and i 2519 If W and W' are race candidates and it is possible to link W 2676 to W' by one of the vis sequences lis 2520 to W' by one of the vis sequences listed above, then W' ->co W 2677 is not allowed (i.e., if one store is 2521 is not allowed (i.e., if one store is visible to a second then 2678 the second must come after the first 2522 the second must come after the first in the coherence order). 2679 2523 2680 This is the extent to which the LKMM deals wi 2524 This is the extent to which the LKMM deals with plain accesses. 2681 Perhaps it could say more (for example, plain 2525 Perhaps it could say more (for example, plain accesses might 2682 contribute to the ppo relation), but at the m 2526 contribute to the ppo relation), but at the moment it seems that this 2683 minimal, conservative approach is good enough 2527 minimal, conservative approach is good enough. 2684 2528 2685 2529 2686 ODDS AND ENDS 2530 ODDS AND ENDS 2687 ------------- 2531 ------------- 2688 2532 2689 This section covers material that didn't quit 2533 This section covers material that didn't quite fit anywhere in the 2690 earlier sections. 2534 earlier sections. 2691 2535 2692 The descriptions in this document don't alway 2536 The descriptions in this document don't always match the formal 2693 version of the LKMM exactly. For example, th 2537 version of the LKMM exactly. For example, the actual formal 2694 definition of the prop relation makes the ini 2538 definition of the prop relation makes the initial coe or fre part 2695 optional, and it doesn't require the events l 2539 optional, and it doesn't require the events linked by the relation to 2696 be on the same CPU. These differences are ve 2540 be on the same CPU. These differences are very unimportant; indeed, 2697 instances where the coe/fre part of prop is m 2541 instances where the coe/fre part of prop is missing are of no interest 2698 because all the other parts (fences and rfe) 2542 because all the other parts (fences and rfe) are already included in 2699 hb anyway, and where the formal model adds pr 2543 hb anyway, and where the formal model adds prop into hb, it includes 2700 an explicit requirement that the events being 2544 an explicit requirement that the events being linked are on the same 2701 CPU. 2545 CPU. 2702 2546 2703 Another minor difference has to do with event 2547 Another minor difference has to do with events that are both memory 2704 accesses and fences, such as those correspond 2548 accesses and fences, such as those corresponding to smp_load_acquire() 2705 calls. In the formal model, these events are 2549 calls. In the formal model, these events aren't actually both reads 2706 and fences; rather, they are read events with 2550 and fences; rather, they are read events with an annotation marking 2707 them as acquires. (Or write events annotated 2551 them as acquires. (Or write events annotated as releases, in the case 2708 smp_store_release().) The final effect is th 2552 smp_store_release().) The final effect is the same. 2709 2553 2710 Although we didn't mention it above, the inst 2554 Although we didn't mention it above, the instruction execution 2711 ordering provided by the smp_rmb() fence does 2555 ordering provided by the smp_rmb() fence doesn't apply to read events 2712 that are part of a non-value-returning atomic 2556 that are part of a non-value-returning atomic update. For instance, 2713 given: 2557 given: 2714 2558 2715 atomic_inc(&x); 2559 atomic_inc(&x); 2716 smp_rmb(); 2560 smp_rmb(); 2717 r1 = READ_ONCE(y); 2561 r1 = READ_ONCE(y); 2718 2562 2719 it is not guaranteed that the load from y wil 2563 it is not guaranteed that the load from y will execute after the 2720 update to x. This is because the ARMv8 archi 2564 update to x. This is because the ARMv8 architecture allows 2721 non-value-returning atomic operations effecti 2565 non-value-returning atomic operations effectively to be executed off 2722 the CPU. Basically, the CPU tells the memory 2566 the CPU. Basically, the CPU tells the memory subsystem to increment 2723 x, and then the increment is carried out by t 2567 x, and then the increment is carried out by the memory hardware with 2724 no further involvement from the CPU. Since t 2568 no further involvement from the CPU. Since the CPU doesn't ever read 2725 the value of x, there is nothing for the smp_ 2569 the value of x, there is nothing for the smp_rmb() fence to act on. 2726 2570 2727 The LKMM defines a few extra synchronization 2571 The LKMM defines a few extra synchronization operations in terms of 2728 things we have already covered. In particula 2572 things we have already covered. In particular, rcu_dereference() is 2729 treated as READ_ONCE() and rcu_assign_pointer 2573 treated as READ_ONCE() and rcu_assign_pointer() is treated as 2730 smp_store_release() -- which is basically how 2574 smp_store_release() -- which is basically how the Linux kernel treats 2731 them. 2575 them. 2732 2576 2733 Although we said that plain accesses are not 2577 Although we said that plain accesses are not linked by the ppo 2734 relation, they do contribute to it indirectly 2578 relation, they do contribute to it indirectly. Firstly, when there is 2735 an address dependency from a marked load R to 2579 an address dependency from a marked load R to a plain store W, 2736 followed by smp_wmb() and then a marked store 2580 followed by smp_wmb() and then a marked store W', the LKMM creates a 2737 ppo link from R to W'. The reasoning behind 2581 ppo link from R to W'. The reasoning behind this is perhaps a little 2738 shaky, but essentially it says there is no wa 2582 shaky, but essentially it says there is no way to generate object code 2739 for this source code in which W' could execut 2583 for this source code in which W' could execute before R. Just as with 2740 pre-bounding by address dependencies, it is p 2584 pre-bounding by address dependencies, it is possible for the compiler 2741 to undermine this relation if sufficient care 2585 to undermine this relation if sufficient care is not taken. 2742 2586 2743 Secondly, plain accesses can carry dependenci 2587 Secondly, plain accesses can carry dependencies: If a data dependency 2744 links a marked load R to a store W, and the s 2588 links a marked load R to a store W, and the store is read by a load R' 2745 from the same thread, then the data loaded by 2589 from the same thread, then the data loaded by R' depends on the data 2746 loaded originally by R. Thus, if R' is linked 2590 loaded originally by R. Thus, if R' is linked to any access X by a 2747 dependency, R is also linked to access X by t 2591 dependency, R is also linked to access X by the same dependency, even 2748 if W' or R' (or both!) are plain. 2592 if W' or R' (or both!) are plain. 2749 2593 2750 There are a few oddball fences which need spe 2594 There are a few oddball fences which need special treatment: 2751 smp_mb__before_atomic(), smp_mb__after_atomic 2595 smp_mb__before_atomic(), smp_mb__after_atomic(), and 2752 smp_mb__after_spinlock(). The LKMM uses fenc 2596 smp_mb__after_spinlock(). The LKMM uses fence events with special 2753 annotations for them; they act as strong fenc 2597 annotations for them; they act as strong fences just like smp_mb() 2754 except for the sets of events that they order 2598 except for the sets of events that they order. Instead of ordering 2755 all po-earlier events against all po-later ev 2599 all po-earlier events against all po-later events, as smp_mb() does, 2756 they behave as follows: 2600 they behave as follows: 2757 2601 2758 smp_mb__before_atomic() orders all po 2602 smp_mb__before_atomic() orders all po-earlier events against 2759 po-later atomic updates and the event 2603 po-later atomic updates and the events following them; 2760 2604 2761 smp_mb__after_atomic() orders po-earl 2605 smp_mb__after_atomic() orders po-earlier atomic updates and 2762 the events preceding them against all 2606 the events preceding them against all po-later events; 2763 2607 2764 smp_mb__after_spinlock() orders po-ea 2608 smp_mb__after_spinlock() orders po-earlier lock acquisition 2765 events and the events preceding them 2609 events and the events preceding them against all po-later 2766 events. 2610 events. 2767 2611 2768 Interestingly, RCU and locking each introduce 2612 Interestingly, RCU and locking each introduce the possibility of 2769 deadlock. When faced with code sequences suc 2613 deadlock. When faced with code sequences such as: 2770 2614 2771 spin_lock(&s); 2615 spin_lock(&s); 2772 spin_lock(&s); 2616 spin_lock(&s); 2773 spin_unlock(&s); 2617 spin_unlock(&s); 2774 spin_unlock(&s); 2618 spin_unlock(&s); 2775 2619 2776 or: 2620 or: 2777 2621 2778 rcu_read_lock(); 2622 rcu_read_lock(); 2779 synchronize_rcu(); 2623 synchronize_rcu(); 2780 rcu_read_unlock(); 2624 rcu_read_unlock(); 2781 2625 2782 what does the LKMM have to say? Answer: It s 2626 what does the LKMM have to say? Answer: It says there are no allowed 2783 executions at all, which makes sense. But th 2627 executions at all, which makes sense. But this can also lead to 2784 misleading results, because if a piece of cod 2628 misleading results, because if a piece of code has multiple possible 2785 executions, some of which deadlock, the model 2629 executions, some of which deadlock, the model will report only on the 2786 non-deadlocking executions. For example: 2630 non-deadlocking executions. For example: 2787 2631 2788 int x, y; 2632 int x, y; 2789 2633 2790 P0() 2634 P0() 2791 { 2635 { 2792 int r0; 2636 int r0; 2793 2637 2794 WRITE_ONCE(x, 1); 2638 WRITE_ONCE(x, 1); 2795 r0 = READ_ONCE(y); 2639 r0 = READ_ONCE(y); 2796 } 2640 } 2797 2641 2798 P1() 2642 P1() 2799 { 2643 { 2800 rcu_read_lock(); 2644 rcu_read_lock(); 2801 if (READ_ONCE(x) > 0) { 2645 if (READ_ONCE(x) > 0) { 2802 WRITE_ONCE(y, 36); 2646 WRITE_ONCE(y, 36); 2803 synchronize_rcu(); 2647 synchronize_rcu(); 2804 } 2648 } 2805 rcu_read_unlock(); 2649 rcu_read_unlock(); 2806 } 2650 } 2807 2651 2808 Is it possible to end up with r0 = 36 at the 2652 Is it possible to end up with r0 = 36 at the end? The LKMM will tell 2809 you it is not, but the model won't mention th 2653 you it is not, but the model won't mention that this is because P1 2810 will self-deadlock in the executions where it 2654 will self-deadlock in the executions where it stores 36 in y.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.