brintos / linux-shallow public Read only

1Explanation of the Linux-Kernel Memory Consistency Model2~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~3 4:Author: Alan Stern <stern@rowland.harvard.edu>5:Created: October 20176 7.. Contents8 9  1. INTRODUCTION10  2. BACKGROUND11  3. A SIMPLE EXAMPLE12  4. A SELECTION OF MEMORY MODELS13  5. ORDERING AND CYCLES14  6. EVENTS15  7. THE PROGRAM ORDER RELATION: po AND po-loc16  8. A WARNING17  9. DEPENDENCY RELATIONS: data, addr, and ctrl18  10. THE READS-FROM RELATION: rf, rfi, and rfe19  11. CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe20  12. THE FROM-READS RELATION: fr, fri, and fre21  13. AN OPERATIONAL MODEL22  14. PROPAGATION ORDER RELATION: cumul-fence23  15. DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL24  16. SEQUENTIAL CONSISTENCY PER VARIABLE25  17. ATOMIC UPDATES: rmw26  18. THE PRESERVED PROGRAM ORDER RELATION: ppo27  19. AND THEN THERE WAS ALPHA28  20. THE HAPPENS-BEFORE RELATION: hb29  21. THE PROPAGATES-BEFORE RELATION: pb30  22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb31  23. SRCU READ-SIDE CRITICAL SECTIONS32  24. LOCKING33  25. PLAIN ACCESSES AND DATA RACES34  26. ODDS AND ENDS35 36 37 38INTRODUCTION39------------40 41The Linux-kernel memory consistency model (LKMM) is rather complex and42obscure.  This is particularly evident if you read through the43linux-kernel.bell and linux-kernel.cat files that make up the formal44version of the model; they are extremely terse and their meanings are45far from clear.46 47This document describes the ideas underlying the LKMM.  It is meant48for people who want to understand how the model was designed.  It does49not go into the details of the code in the .bell and .cat files;50rather, it explains in English what the code expresses symbolically.51 52Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed53toward beginners; they explain what memory consistency models are and54the basic notions shared by all such models.  People already familiar55with these concepts can skim or skip over them.  Sections 6 (EVENTS)56through 12 (THE FROM_READS RELATION) describe the fundamental57relations used in many models.  Starting in Section 13 (AN OPERATIONAL58MODEL), the workings of the LKMM itself are covered.59 60Warning: The code examples in this document are not written in the61proper format for litmus tests.  They don't include a header line, the62initializations are not enclosed in braces, the global variables are63not passed by pointers, and they don't have an "exists" clause at the64end.  Converting them to the right format is left as an exercise for65the reader.66 67 68BACKGROUND69----------70 71A memory consistency model (or just memory model, for short) is72something which predicts, given a piece of computer code running on a73particular kind of system, what values may be obtained by the code's74load instructions.  The LKMM makes these predictions for code running75as part of the Linux kernel.76 77In practice, people tend to use memory models the other way around.78That is, given a piece of code and a collection of values specified79for the loads, the model will predict whether it is possible for the80code to run in such a way that the loads will indeed obtain the81specified values.  Of course, this is just another way of expressing82the same idea.83 84For code running on a uniprocessor system, the predictions are easy:85Each load instruction must obtain the value written by the most recent86store instruction accessing the same location (we ignore complicating87factors such as DMA and mixed-size accesses.)  But on multiprocessor88systems, with multiple CPUs making concurrent accesses to shared89memory locations, things aren't so simple.90 91Different architectures have differing memory models, and the Linux92kernel supports a variety of architectures.  The LKMM has to be fairly93permissive, in the sense that any behavior allowed by one of these94architectures also has to be allowed by the LKMM.95 96 97A SIMPLE EXAMPLE98----------------99 100Here is a simple example to illustrate the basic concepts.  Consider101some code running as part of a device driver for an input device.  The102driver might contain an interrupt handler which collects data from the103device, stores it in a buffer, and sets a flag to indicate the buffer104is full.  Running concurrently on a different CPU might be a part of105the driver code being executed by a process in the midst of a read(2)106system call.  This code tests the flag to see whether the buffer is107ready, and if it is, copies the data back to userspace.  The buffer108and the flag are memory locations shared between the two CPUs.109 110We can abstract out the important pieces of the driver code as follows111(the reason for using WRITE_ONCE() and READ_ONCE() instead of simple112assignment statements is discussed later):113 114	int buf = 0, flag = 0;115 116	P0()117	{118		WRITE_ONCE(buf, 1);119		WRITE_ONCE(flag, 1);120	}121 122	P1()123	{124		int r1;125		int r2 = 0;126 127		r1 = READ_ONCE(flag);128		if (r1)129			r2 = READ_ONCE(buf);130	}131 132Here the P0() function represents the interrupt handler running on one133CPU and P1() represents the read() routine running on another.  The134value 1 stored in buf represents input data collected from the device.135Thus, P0 stores the data in buf and then sets flag.  Meanwhile, P1136reads flag into the private variable r1, and if it is set, reads the137data from buf into a second private variable r2 for copying to138userspace.  (Presumably if flag is not set then the driver will wait a139while and try again.)140 141This pattern of memory accesses, where one CPU stores values to two142shared memory locations and another CPU loads from those locations in143the opposite order, is widely known as the "Message Passing" or MP144pattern.  It is typical of memory access patterns in the kernel.145 146Please note that this example code is a simplified abstraction.  Real147buffers are usually larger than a single integer, real device drivers148usually use sleep and wakeup mechanisms rather than polling for I/O149completion, and real code generally doesn't bother to copy values into150private variables before using them.  All that is beside the point;151the idea here is simply to illustrate the overall pattern of memory152accesses by the CPUs.153 154A memory model will predict what values P1 might obtain for its loads155from flag and buf, or equivalently, what values r1 and r2 might end up156with after the code has finished running.157 158Some predictions are trivial.  For instance, no sane memory model would159predict that r1 = 42 or r2 = -7, because neither of those values ever160gets stored in flag or buf.161 162Some nontrivial predictions are nonetheless quite simple.  For163instance, P1 might run entirely before P0 begins, in which case r1 and164r2 will both be 0 at the end.  Or P0 might run entirely before P1165begins, in which case r1 and r2 will both be 1.166 167The interesting predictions concern what might happen when the two168routines run concurrently.  One possibility is that P1 runs after P0's169store to buf but before the store to flag.  In this case, r1 and r2170will again both be 0.  (If P1 had been designed to read buf171unconditionally then we would instead have r1 = 0 and r2 = 1.)172 173However, the most interesting possibility is where r1 = 1 and r2 = 0.174If this were to occur it would mean the driver contains a bug, because175incorrect data would get sent to the user: 0 instead of 1.  As it176happens, the LKMM does predict this outcome can occur, and the example177driver code shown above is indeed buggy.178 179 180A SELECTION OF MEMORY MODELS181----------------------------182 183The first widely cited memory model, and the simplest to understand,184is Sequential Consistency.  According to this model, systems behave as185if each CPU executed its instructions in order but with unspecified186timing.  In other words, the instructions from the various CPUs get187interleaved in a nondeterministic way, always according to some single188global order that agrees with the order of the instructions in the189program source for each CPU.  The model says that the value obtained190by each load is simply the value written by the most recently executed191store to the same memory location, from any CPU.192 193For the MP example code shown above, Sequential Consistency predicts194that the undesired result r1 = 1, r2 = 0 cannot occur.  The reasoning195goes like this:196 197	Since r1 = 1, P0 must store 1 to flag before P1 loads 1 from198	it, as loads can obtain values only from earlier stores.199 200	P1 loads from flag before loading from buf, since CPUs execute201	their instructions in order.202 203	P1 must load 0 from buf before P0 stores 1 to it; otherwise r2204	would be 1 since a load obtains its value from the most recent205	store to the same address.206 207	P0 stores 1 to buf before storing 1 to flag, since it executes208	its instructions in order.209 210	Since an instruction (in this case, P0's store to flag) cannot211	execute before itself, the specified outcome is impossible.212 213However, real computer hardware almost never follows the Sequential214Consistency memory model; doing so would rule out too many valuable215performance optimizations.  On ARM and PowerPC architectures, for216instance, the MP example code really does sometimes yield r1 = 1 and217r2 = 0.218 219x86 and SPARC follow yet a different memory model: TSO (Total Store220Ordering).  This model predicts that the undesired outcome for the MP221pattern cannot occur, but in other respects it differs from Sequential222Consistency.  One example is the Store Buffer (SB) pattern, in which223each CPU stores to its own shared location and then loads from the224other CPU's location:225 226	int x = 0, y = 0;227 228	P0()229	{230		int r0;231 232		WRITE_ONCE(x, 1);233		r0 = READ_ONCE(y);234	}235 236	P1()237	{238		int r1;239 240		WRITE_ONCE(y, 1);241		r1 = READ_ONCE(x);242	}243 244Sequential Consistency predicts that the outcome r0 = 0, r1 = 0 is245impossible.  (Exercise: Figure out the reasoning.)  But TSO allows246this outcome to occur, and in fact it does sometimes occur on x86 and247SPARC systems.248 249The LKMM was inspired by the memory models followed by PowerPC, ARM,250x86, Alpha, and other architectures.  However, it is different in251detail from each of them.252 253 254ORDERING AND CYCLES255-------------------256 257Memory models are all about ordering.  Often this is temporal ordering258(i.e., the order in which certain events occur) but it doesn't have to259be; consider for example the order of instructions in a program's260source code.  We saw above that Sequential Consistency makes an261important assumption that CPUs execute instructions in the same order262as those instructions occur in the code, and there are many other263instances of ordering playing central roles in memory models.264 265The counterpart to ordering is a cycle.  Ordering rules out cycles:266It's not possible to have X ordered before Y, Y ordered before Z, and267Z ordered before X, because this would mean that X is ordered before268itself.  The analysis of the MP example under Sequential Consistency269involved just such an impossible cycle:270 271	W: P0 stores 1 to flag   executes before272	X: P1 loads 1 from flag  executes before273	Y: P1 loads 0 from buf   executes before274	Z: P0 stores 1 to buf    executes before275	W: P0 stores 1 to flag.276 277In short, if a memory model requires certain accesses to be ordered,278and a certain outcome for the loads in a piece of code can happen only279if those accesses would form a cycle, then the memory model predicts280that outcome cannot occur.281 282The LKMM is defined largely in terms of cycles, as we will see.283 284 285EVENTS286------287 288The LKMM does not work directly with the C statements that make up289kernel source code.  Instead it considers the effects of those290statements in a more abstract form, namely, events.  The model291includes three types of events:292 293	Read events correspond to loads from shared memory, such as294	calls to READ_ONCE(), smp_load_acquire(), or295	rcu_dereference().296 297	Write events correspond to stores to shared memory, such as298	calls to WRITE_ONCE(), smp_store_release(), or atomic_set().299 300	Fence events correspond to memory barriers (also known as301	fences), such as calls to smp_rmb() or rcu_read_lock().302 303These categories are not exclusive; a read or write event can also be304a fence.  This happens with functions like smp_load_acquire() or305spin_lock().  However, no single event can be both a read and a write.306Atomic read-modify-write accesses, such as atomic_inc() or xchg(),307correspond to a pair of events: a read followed by a write.  (The308write event is omitted for executions where it doesn't occur, such as309a cmpxchg() where the comparison fails.)310 311Other parts of the code, those which do not involve interaction with312shared memory, do not give rise to events.  Thus, arithmetic and313logical computations, control-flow instructions, or accesses to314private memory or CPU registers are not of central interest to the315memory model.  They only affect the model's predictions indirectly.316For example, an arithmetic computation might determine the value that317gets stored to a shared memory location (or in the case of an array318index, the address where the value gets stored), but the memory model319is concerned only with the store itself -- its value and its address320-- not the computation leading up to it.321 322Events in the LKMM can be linked by various relations, which we will323describe in the following sections.  The memory model requires certain324of these relations to be orderings, that is, it requires them not to325have any cycles.326 327 328THE PROGRAM ORDER RELATION: po AND po-loc329-----------------------------------------330 331The most important relation between events is program order (po).  You332can think of it as the order in which statements occur in the source333code after branches are taken into account and loops have been334unrolled.  A better description might be the order in which335instructions are presented to a CPU's execution unit.  Thus, we say336that X is po-before Y (written as "X ->po Y" in formulas) if X occurs337before Y in the instruction stream.338 339This is inherently a single-CPU relation; two instructions executing340on different CPUs are never linked by po.  Also, it is by definition341an ordering so it cannot have any cycles.342 343po-loc is a sub-relation of po.  It links two memory accesses when the344first comes before the second in program order and they access the345same memory location (the "-loc" suffix).346 347Although this may seem straightforward, there is one subtle aspect to348program order we need to explain.  The LKMM was inspired by low-level349architectural memory models which describe the behavior of machine350code, and it retains their outlook to a considerable extent.  The351read, write, and fence events used by the model are close in spirit to352individual machine instructions.  Nevertheless, the LKMM describes353kernel code written in C, and the mapping from C to machine code can354be extremely complex.355 356Optimizing compilers have great freedom in the way they translate357source code to object code.  They are allowed to apply transformations358that add memory accesses, eliminate accesses, combine them, split them359into pieces, or move them around.  The use of READ_ONCE(), WRITE_ONCE(),360or one of the other atomic or synchronization primitives prevents a361large number of compiler optimizations.  In particular, it is guaranteed362that the compiler will not remove such accesses from the generated code363(unless it can prove the accesses will never be executed), it will not364change the order in which they occur in the code (within limits imposed365by the C standard), and it will not introduce extraneous accesses.366 367The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather368than ordinary memory accesses.  Thanks to this usage, we can be certain369that in the MP example, the compiler won't reorder P0's write event to370buf and P0's write event to flag, and similarly for the other shared371memory accesses in the examples.372 373Since private variables are not shared between CPUs, they can be374accessed normally without READ_ONCE() or WRITE_ONCE().  In fact, they375need not even be stored in normal memory at all -- in principle a376private variable could be stored in a CPU register (hence the convention377that these variables have names starting with the letter 'r').378 379 380A WARNING381---------382 383The protections provided by READ_ONCE(), WRITE_ONCE(), and others are384not perfect; and under some circumstances it is possible for the385compiler to undermine the memory model.  Here is an example.  Suppose386both branches of an "if" statement store the same value to the same387location:388 389	r1 = READ_ONCE(x);390	if (r1) {391		WRITE_ONCE(y, 2);392		...  /* do something */393	} else {394		WRITE_ONCE(y, 2);395		...  /* do something else */396	}397 398For this code, the LKMM predicts that the load from x will always be399executed before either of the stores to y.  However, a compiler could400lift the stores out of the conditional, transforming the code into401something resembling:402 403	r1 = READ_ONCE(x);404	WRITE_ONCE(y, 2);405	if (r1) {406		...  /* do something */407	} else {408		...  /* do something else */409	}410 411Given this version of the code, the LKMM would predict that the load412from x could be executed after the store to y.  Thus, the memory413model's original prediction could be invalidated by the compiler.414 415Another issue arises from the fact that in C, arguments to many416operators and function calls can be evaluated in any order.  For417example:418 419	r1 = f(5) + g(6);420 421The object code might call f(5) either before or after g(6); the422memory model cannot assume there is a fixed program order relation423between them.  (In fact, if the function calls are inlined then the424compiler might even interleave their object code.)425 426 427DEPENDENCY RELATIONS: data, addr, and ctrl428------------------------------------------429 430We say that two events are linked by a dependency relation when the431execution of the second event depends in some way on a value obtained432from memory by the first.  The first event must be a read, and the433value it obtains must somehow affect what the second event does.434There are three kinds of dependencies: data, address (addr), and435control (ctrl).436 437A read and a write event are linked by a data dependency if the value438obtained by the read affects the value stored by the write.  As a very439simple example:440 441	int x, y;442 443	r1 = READ_ONCE(x);444	WRITE_ONCE(y, r1 + 5);445 446The value stored by the WRITE_ONCE obviously depends on the value447loaded by the READ_ONCE.  Such dependencies can wind through448arbitrarily complicated computations, and a write can depend on the449values of multiple reads.450 451A read event and another memory access event are linked by an address452dependency if the value obtained by the read affects the location453accessed by the other event.  The second event can be either a read or454a write.  Here's another simple example:455 456	int a[20];457	int i;458 459	r1 = READ_ONCE(i);460	r2 = READ_ONCE(a[r1]);461 462Here the location accessed by the second READ_ONCE() depends on the463index value loaded by the first.  Pointer indirection also gives rise464to address dependencies, since the address of a location accessed465through a pointer will depend on the value read earlier from that466pointer.467 468Finally, a read event X and a write event Y are linked by a control469dependency if Y syntactically lies within an arm of an if statement and470X affects the evaluation of the if condition via a data or address471dependency (or similarly for a switch statement).  Simple example:472 473	int x, y;474 475	r1 = READ_ONCE(x);476	if (r1)477		WRITE_ONCE(y, 1984);478 479Execution of the WRITE_ONCE() is controlled by a conditional expression480which depends on the value obtained by the READ_ONCE(); hence there is481a control dependency from the load to the store.482 483It should be pretty obvious that events can only depend on reads that484come earlier in program order.  Symbolically, if we have R ->data X,485R ->addr X, or R ->ctrl X (where R is a read event), then we must also486have R ->po X.  It wouldn't make sense for a computation to depend487somehow on a value that doesn't get loaded from shared memory until488later in the code!489 490Here's a trick question: When is a dependency not a dependency?  Answer:491When it is purely syntactic rather than semantic.  We say a dependency492between two accesses is purely syntactic if the second access doesn't493actually depend on the result of the first.  Here is a trivial example:494 495	r1 = READ_ONCE(x);496	WRITE_ONCE(y, r1 * 0);497 498There appears to be a data dependency from the load of x to the store499of y, since the value to be stored is computed from the value that was500loaded.  But in fact, the value stored does not really depend on501anything since it will always be 0.  Thus the data dependency is only502syntactic (it appears to exist in the code) but not semantic (the503second access will always be the same, regardless of the value of the504first access).  Given code like this, a compiler could simply discard505the value returned by the load from x, which would certainly destroy506any dependency.  (The compiler is not permitted to eliminate entirely507the load generated for a READ_ONCE() -- that's one of the nice508properties of READ_ONCE() -- but it is allowed to ignore the load's509value.)510 511It's natural to object that no one in their right mind would write512code like the above.  However, macro expansions can easily give rise513to this sort of thing, in ways that often are not apparent to the514programmer.515 516Another mechanism that can lead to purely syntactic dependencies is517related to the notion of "undefined behavior".  Certain program518behaviors are called "undefined" in the C language specification,519which means that when they occur there are no guarantees at all about520the outcome.  Consider the following example:521 522	int a[1];523	int i;524 525	r1 = READ_ONCE(i);526	r2 = READ_ONCE(a[r1]);527 528Access beyond the end or before the beginning of an array is one kind529of undefined behavior.  Therefore the compiler doesn't have to worry530about what will happen if r1 is nonzero, and it can assume that r1531will always be zero regardless of the value actually loaded from i.532(If the assumption turns out to be wrong the resulting behavior will533be undefined anyway, so the compiler doesn't care!)  Thus the value534from the load can be discarded, breaking the address dependency.535 536The LKMM is unaware that purely syntactic dependencies are different537from semantic dependencies and therefore mistakenly predicts that the538accesses in the two examples above will be ordered.  This is another539example of how the compiler can undermine the memory model.  Be warned.540 541 542THE READS-FROM RELATION: rf, rfi, and rfe543-----------------------------------------544 545The reads-from relation (rf) links a write event to a read event when546the value loaded by the read is the value that was stored by the547write.  In colloquial terms, the load "reads from" the store.  We548write W ->rf R to indicate that the load R reads from the store W.  We549further distinguish the cases where the load and the store occur on550the same CPU (internal reads-from, or rfi) and where they occur on551different CPUs (external reads-from, or rfe).552 553For our purposes, a memory location's initial value is treated as554though it had been written there by an imaginary initial store that555executes on a separate CPU before the main program runs.556 557Usage of the rf relation implicitly assumes that loads will always558read from a single store.  It doesn't apply properly in the presence559of load-tearing, where a load obtains some of its bits from one store560and some of them from another store.  Fortunately, use of READ_ONCE()561and WRITE_ONCE() will prevent load-tearing; it's not possible to have:562 563	int x = 0;564 565	P0()566	{567		WRITE_ONCE(x, 0x1234);568	}569 570	P1()571	{572		int r1;573 574		r1 = READ_ONCE(x);575	}576 577and end up with r1 = 0x1200 (partly from x's initial value and partly578from the value stored by P0).579 580On the other hand, load-tearing is unavoidable when mixed-size581accesses are used.  Consider this example:582 583	union {584		u32	w;585		u16	h[2];586	} x;587 588	P0()589	{590		WRITE_ONCE(x.h[0], 0x1234);591		WRITE_ONCE(x.h[1], 0x5678);592	}593 594	P1()595	{596		int r1;597 598		r1 = READ_ONCE(x.w);599	}600 601If r1 = 0x56781234 (little-endian!) at the end, then P1 must have read602from both of P0's stores.  It is possible to handle mixed-size and603unaligned accesses in a memory model, but the LKMM currently does not604attempt to do so.  It requires all accesses to be properly aligned and605of the location's actual size.606 607 608CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe609------------------------------------------------------------------610 611Cache coherence is a general principle requiring that in a612multi-processor system, the CPUs must share a consistent view of the613memory contents.  Specifically, it requires that for each location in614shared memory, the stores to that location must form a single global615ordering which all the CPUs agree on (the coherence order), and this616ordering must be consistent with the program order for accesses to617that location.618 619To put it another way, for any variable x, the coherence order (co) of620the stores to x is simply the order in which the stores overwrite one621another.  The imaginary store which establishes x's initial value622comes first in the coherence order; the store which directly623overwrites the initial value comes second; the store which overwrites624that value comes third, and so on.625 626You can think of the coherence order as being the order in which the627stores reach x's location in memory (or if you prefer a more628hardware-centric view, the order in which the stores get written to629x's cache line).  We write W ->co W' if W comes before W' in the630coherence order, that is, if the value stored by W gets overwritten,631directly or indirectly, by the value stored by W'.632 633Coherence order is required to be consistent with program order.  This634requirement takes the form of four coherency rules:635 636	Write-write coherence: If W ->po-loc W' (i.e., W comes before637	W' in program order and they access the same location), where W638	and W' are two stores, then W ->co W'.639 640	Write-read coherence: If W ->po-loc R, where W is a store and R641	is a load, then R must read from W or from some other store642	which comes after W in the coherence order.643 644	Read-write coherence: If R ->po-loc W, where R is a load and W645	is a store, then the store which R reads from must come before646	W in the coherence order.647 648	Read-read coherence: If R ->po-loc R', where R and R' are two649	loads, then either they read from the same store or else the650	store read by R comes before the store read by R' in the651	coherence order.652 653This is sometimes referred to as sequential consistency per variable,654because it means that the accesses to any single memory location obey655the rules of the Sequential Consistency memory model.  (According to656Wikipedia, sequential consistency per variable and cache coherence657mean the same thing except that cache coherence includes an extra658requirement that every store eventually becomes visible to every CPU.)659 660Any reasonable memory model will include cache coherence.  Indeed, our661expectation of cache coherence is so deeply ingrained that violations662of its requirements look more like hardware bugs than programming663errors:664 665	int x;666 667	P0()668	{669		WRITE_ONCE(x, 17);670		WRITE_ONCE(x, 23);671	}672 673If the final value stored in x after this code ran was 17, you would674think your computer was broken.  It would be a violation of the675write-write coherence rule: Since the store of 23 comes later in676program order, it must also come later in x's coherence order and677thus must overwrite the store of 17.678 679	int x = 0;680 681	P0()682	{683		int r1;684 685		r1 = READ_ONCE(x);686		WRITE_ONCE(x, 666);687	}688 689If r1 = 666 at the end, this would violate the read-write coherence690rule: The READ_ONCE() load comes before the WRITE_ONCE() store in691program order, so it must not read from that store but rather from one692coming earlier in the coherence order (in this case, x's initial693value).694 695	int x = 0;696 697	P0()698	{699		WRITE_ONCE(x, 5);700	}701 702	P1()703	{704		int r1, r2;705 706		r1 = READ_ONCE(x);707		r2 = READ_ONCE(x);708	}709 710If r1 = 5 (reading from P0's store) and r2 = 0 (reading from the711imaginary store which establishes x's initial value) at the end, this712would violate the read-read coherence rule: The r1 load comes before713the r2 load in program order, so it must not read from a store that714comes later in the coherence order.715 716(As a minor curiosity, if this code had used normal loads instead of717READ_ONCE() in P1, on Itanium it sometimes could end up with r1 = 5718and r2 = 0!  This results from parallel execution of the operations719encoded in Itanium's Very-Long-Instruction-Word format, and it is yet720another motivation for using READ_ONCE() when accessing shared memory721locations.)722 723Just like the po relation, co is inherently an ordering -- it is not724possible for a store to directly or indirectly overwrite itself!  And725just like with the rf relation, we distinguish between stores that726occur on the same CPU (internal coherence order, or coi) and stores727that occur on different CPUs (external coherence order, or coe).728 729On the other hand, stores to different memory locations are never730related by co, just as instructions on different CPUs are never731related by po.  Coherence order is strictly per-location, or if you732prefer, each location has its own independent coherence order.733 734 735THE FROM-READS RELATION: fr, fri, and fre736-----------------------------------------737 738The from-reads relation (fr) can be a little difficult for people to739grok.  It describes the situation where a load reads a value that gets740overwritten by a store.  In other words, we have R ->fr W when the741value that R reads is overwritten (directly or indirectly) by W, or742equivalently, when R reads from a store which comes earlier than W in743the coherence order.744 745For example:746 747	int x = 0;748 749	P0()750	{751		int r1;752 753		r1 = READ_ONCE(x);754		WRITE_ONCE(x, 2);755	}756 757The value loaded from x will be 0 (assuming cache coherence!), and it758gets overwritten by the value 2.  Thus there is an fr link from the759READ_ONCE() to the WRITE_ONCE().  If the code contained any later760stores to x, there would also be fr links from the READ_ONCE() to761them.762 763As with rf, rfi, and rfe, we subdivide the fr relation into fri (when764the load and the store are on the same CPU) and fre (when they are on765different CPUs).766 767Note that the fr relation is determined entirely by the rf and co768relations; it is not independent.  Given a read event R and a write769event W for the same location, we will have R ->fr W if and only if770the write which R reads from is co-before W.  In symbols,771 772	(R ->fr W) := (there exists W' with W' ->rf R and W' ->co W).773 774 775AN OPERATIONAL MODEL776--------------------777 778The LKMM is based on various operational memory models, meaning that779the models arise from an abstract view of how a computer system780operates.  Here are the main ideas, as incorporated into the LKMM.781 782The system as a whole is divided into the CPUs and a memory subsystem.783The CPUs are responsible for executing instructions (not necessarily784in program order), and they communicate with the memory subsystem.785For the most part, executing an instruction requires a CPU to perform786only internal operations.  However, loads, stores, and fences involve787more.788 789When CPU C executes a store instruction, it tells the memory subsystem790to store a certain value at a certain location.  The memory subsystem791propagates the store to all the other CPUs as well as to RAM.  (As a792special case, we say that the store propagates to its own CPU at the793time it is executed.)  The memory subsystem also determines where the794store falls in the location's coherence order.  In particular, it must795arrange for the store to be co-later than (i.e., to overwrite) any796other store to the same location which has already propagated to CPU C.797 798When a CPU executes a load instruction R, it first checks to see799whether there are any as-yet unexecuted store instructions, for the800same location, that come before R in program order.  If there are, it801uses the value of the po-latest such store as the value obtained by R,802and we say that the store's value is forwarded to R.  Otherwise, the803CPU asks the memory subsystem for the value to load and we say that R804is satisfied from memory.  The memory subsystem hands back the value805of the co-latest store to the location in question which has already806propagated to that CPU.807 808(In fact, the picture needs to be a little more complicated than this.809CPUs have local caches, and propagating a store to a CPU really means810propagating it to the CPU's local cache.  A local cache can take some811time to process the stores that it receives, and a store can't be used812to satisfy one of the CPU's loads until it has been processed.  On813most architectures, the local caches process stores in814First-In-First-Out order, and consequently the processing delay815doesn't matter for the memory model.  But on Alpha, the local caches816have a partitioned design that results in non-FIFO behavior.  We will817discuss this in more detail later.)818 819Note that load instructions may be executed speculatively and may be820restarted under certain circumstances.  The memory model ignores these821premature executions; we simply say that the load executes at the822final time it is forwarded or satisfied.823 824Executing a fence (or memory barrier) instruction doesn't require a825CPU to do anything special other than informing the memory subsystem826about the fence.  However, fences do constrain the way CPUs and the827memory subsystem handle other instructions, in two respects.828 829First, a fence forces the CPU to execute various instructions in830program order.  Exactly which instructions are ordered depends on the831type of fence:832 833	Strong fences, including smp_mb() and synchronize_rcu(), force834	the CPU to execute all po-earlier instructions before any835	po-later instructions;836 837	smp_rmb() forces the CPU to execute all po-earlier loads838	before any po-later loads;839 840	smp_wmb() forces the CPU to execute all po-earlier stores841	before any po-later stores;842 843	Acquire fences, such as smp_load_acquire(), force the CPU to844	execute the load associated with the fence (e.g., the load845	part of an smp_load_acquire()) before any po-later846	instructions;847 848	Release fences, such as smp_store_release(), force the CPU to849	execute all po-earlier instructions before the store850	associated with the fence (e.g., the store part of an851	smp_store_release()).852 853Second, some types of fence affect the way the memory subsystem854propagates stores.  When a fence instruction is executed on CPU C:855 856	For each other CPU C', smp_wmb() forces all po-earlier stores857	on C to propagate to C' before any po-later stores do.858 859	For each other CPU C', any store which propagates to C before860	a release fence is executed (including all po-earlier861	stores executed on C) is forced to propagate to C' before the862	store associated with the release fence does.863 864	Any store which propagates to C before a strong fence is865	executed (including all po-earlier stores on C) is forced to866	propagate to all other CPUs before any instructions po-after867	the strong fence are executed on C.868 869The propagation ordering enforced by release fences and strong fences870affects stores from other CPUs that propagate to CPU C before the871fence is executed, as well as stores that are executed on C before the872fence.  We describe this property by saying that release fences and873strong fences are A-cumulative.  By contrast, smp_wmb() fences are not874A-cumulative; they only affect the propagation of stores that are875executed on C before the fence (i.e., those which precede the fence in876program order).877 878rcu_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have879other properties which we discuss later.880 881 882PROPAGATION ORDER RELATION: cumul-fence883---------------------------------------884 885The fences which affect propagation order (i.e., strong, release, and886smp_wmb() fences) are collectively referred to as cumul-fences, even887though smp_wmb() isn't A-cumulative.  The cumul-fence relation is888defined to link memory access events E and F whenever:889 890	E and F are both stores on the same CPU and an smp_wmb() fence891	event occurs between them in program order; or892 893	F is a release fence and some X comes before F in program order,894	where either X = E or else E ->rf X; or895 896	A strong fence event occurs between some X and F in program897	order, where either X = E or else E ->rf X.898 899The operational model requires that whenever W and W' are both stores900and W ->cumul-fence W', then W must propagate to any given CPU901before W' does.  However, for different CPUs C and C', it does not902require W to propagate to C before W' propagates to C'.903 904 905DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL906-------------------------------------------------907 908The LKMM is derived from the restrictions imposed by the design909outlined above.  These restrictions involve the necessity of910maintaining cache coherence and the fact that a CPU can't operate on a911value before it knows what that value is, among other things.912 913The formal version of the LKMM is defined by six requirements, or914axioms:915 916	Sequential consistency per variable: This requires that the917	system obey the four coherency rules.918 919	Atomicity: This requires that atomic read-modify-write920	operations really are atomic, that is, no other stores can921	sneak into the middle of such an update.922 923	Happens-before: This requires that certain instructions are924	executed in a specific order.925 926	Propagation: This requires that certain stores propagate to927	CPUs and to RAM in a specific order.928 929	Rcu: This requires that RCU read-side critical sections and930	grace periods obey the rules of RCU, in particular, the931	Grace-Period Guarantee.932 933	Plain-coherence: This requires that plain memory accesses934	(those not using READ_ONCE(), WRITE_ONCE(), etc.) must obey935	the operational model's rules regarding cache coherence.936 937The first and second are quite common; they can be found in many938memory models (such as those for C11/C++11).  The "happens-before" and939"propagation" axioms have analogs in other memory models as well.  The940"rcu" and "plain-coherence" axioms are specific to the LKMM.941 942Each of these axioms is discussed below.943 944 945SEQUENTIAL CONSISTENCY PER VARIABLE946-----------------------------------947 948According to the principle of cache coherence, the stores to any fixed949shared location in memory form a global ordering.  We can imagine950inserting the loads from that location into this ordering, by placing951each load between the store that it reads from and the following952store.  This leaves the relative positions of loads that read from the953same store unspecified; let's say they are inserted in program order,954first for CPU 0, then CPU 1, etc.955 956You can check that the four coherency rules imply that the rf, co, fr,957and po-loc relations agree with this global ordering; in other words,958whenever we have X ->rf Y or X ->co Y or X ->fr Y or X ->po-loc Y, the959X event comes before the Y event in the global ordering.  The LKMM's960"coherence" axiom expresses this by requiring the union of these961relations not to have any cycles.  This means it must not be possible962to find events963 964	X0 -> X1 -> X2 -> ... -> Xn -> X0,965 966where each of the links is either rf, co, fr, or po-loc.  This has to967hold if the accesses to the fixed memory location can be ordered as968cache coherence demands.969 970Although it is not obvious, it can be shown that the converse is also971true: This LKMM axiom implies that the four coherency rules are972obeyed.973 974 975ATOMIC UPDATES: rmw976-------------------977 978What does it mean to say that a read-modify-write (rmw) update, such979as atomic_inc(&x), is atomic?  It means that the memory location (x in980this case) does not get altered between the read and the write events981making up the atomic operation.  In particular, if two CPUs perform982atomic_inc(&x) concurrently, it must be guaranteed that the final983value of x will be the initial value plus two.  We should never have984the following sequence of events:985 986	CPU 0 loads x obtaining 13;987					CPU 1 loads x obtaining 13;988	CPU 0 stores 14 to x;989					CPU 1 stores 14 to x;990 991where the final value of x is wrong (14 rather than 15).992 993In this example, CPU 0's increment effectively gets lost because it994occurs in between CPU 1's load and store.  To put it another way, the995problem is that the position of CPU 0's store in x's coherence order996is between the store that CPU 1 reads from and the store that CPU 1997performs.998 999The same analysis applies to all atomic update operations.  Therefore,1000to enforce atomicity the LKMM requires that atomic updates follow this1001rule: Whenever R and W are the read and write events composing an1002atomic read-modify-write and W' is the write event which R reads from,1003there must not be any stores coming between W' and W in the coherence1004order.  Equivalently,1005 1006	(R ->rmw W) implies (there is no X with R ->fr X and X ->co W),1007 1008where the rmw relation links the read and write events making up each1009atomic update.  This is what the LKMM's "atomic" axiom says.1010 1011Atomic rmw updates play one more role in the LKMM: They can form "rmw1012sequences".  An rmw sequence is simply a bunch of atomic updates where1013each update reads from the previous one.  Written using events, it1014looks like this:1015 1016	Z0 ->rf Y1 ->rmw Z1 ->rf ... ->rf Yn ->rmw Zn,1017 1018where Z0 is some store event and n can be any number (even 0, in the1019degenerate case).  We write this relation as: Z0 ->rmw-sequence Zn.1020Note that this implies Z0 and Zn are stores to the same variable.1021 1022Rmw sequences have a special property in the LKMM: They can extend the1023cumul-fence relation.  That is, if we have:1024 1025	U ->cumul-fence X -> rmw-sequence Y1026 1027then also U ->cumul-fence Y.  Thinking about this in terms of the1028operational model, U ->cumul-fence X says that the store U propagates1029to each CPU before the store X does.  Then the fact that X and Y are1030linked by an rmw sequence means that U also propagates to each CPU1031before Y does.  In an analogous way, rmw sequences can also extend1032the w-post-bounded relation defined below in the PLAIN ACCESSES AND1033DATA RACES section.1034 1035(The notion of rmw sequences in the LKMM is similar to, but not quite1036the same as, that of release sequences in the C11 memory model.  They1037were added to the LKMM to fix an obscure bug; without them, atomic1038updates with full-barrier semantics did not always guarantee ordering1039at least as strong as atomic updates with release-barrier semantics.)1040 1041 1042THE PRESERVED PROGRAM ORDER RELATION: ppo1043-----------------------------------------1044 1045There are many situations where a CPU is obliged to execute two1046instructions in program order.  We amalgamate them into the ppo (for1047"preserved program order") relation, which links the po-earlier1048instruction to the po-later instruction and is thus a sub-relation of1049po.1050 1051The operational model already includes a description of one such1052situation: Fences are a source of ppo links.  Suppose X and Y are1053memory accesses with X ->po Y; then the CPU must execute X before Y if1054any of the following hold:1055 1056	A strong (smp_mb() or synchronize_rcu()) fence occurs between1057	X and Y;1058 1059	X and Y are both stores and an smp_wmb() fence occurs between1060	them;1061 1062	X and Y are both loads and an smp_rmb() fence occurs between1063	them;1064 1065	X is also an acquire fence, such as smp_load_acquire();1066 1067	Y is also a release fence, such as smp_store_release().1068 1069Another possibility, not mentioned earlier but discussed in the next1070section, is:1071 1072	X and Y are both loads, X ->addr Y (i.e., there is an address1073	dependency from X to Y), and X is a READ_ONCE() or an atomic1074	access.1075 1076Dependencies can also cause instructions to be executed in program1077order.  This is uncontroversial when the second instruction is a1078store; either a data, address, or control dependency from a load R to1079a store W will force the CPU to execute R before W.  This is very1080simply because the CPU cannot tell the memory subsystem about W's1081store before it knows what value should be stored (in the case of a1082data dependency), what location it should be stored into (in the case1083of an address dependency), or whether the store should actually take1084place (in the case of a control dependency).1085 1086Dependencies to load instructions are more problematic.  To begin with,1087there is no such thing as a data dependency to a load.  Next, a CPU1088has no reason to respect a control dependency to a load, because it1089can always satisfy the second load speculatively before the first, and1090then ignore the result if it turns out that the second load shouldn't1091be executed after all.  And lastly, the real difficulties begin when1092we consider address dependencies to loads.1093 1094To be fair about it, all Linux-supported architectures do execute1095loads in program order if there is an address dependency between them.1096After all, a CPU cannot ask the memory subsystem to load a value from1097a particular location before it knows what that location is.  However,1098the split-cache design used by Alpha can cause it to behave in a way1099that looks as if the loads were executed out of order (see the next1100section for more details).  The kernel includes a workaround for this1101problem when the loads come from READ_ONCE(), and therefore the LKMM1102includes address dependencies to loads in the ppo relation.1103 1104On the other hand, dependencies can indirectly affect the ordering of1105two loads.  This happens when there is a dependency from a load to a1106store and a second, po-later load reads from that store:1107 1108	R ->dep W ->rfi R',1109 1110where the dep link can be either an address or a data dependency.  In1111this situation we know it is possible for the CPU to execute R' before1112W, because it can forward the value that W will store to R'.  But it1113cannot execute R' before R, because it cannot forward the value before1114it knows what that value is, or that W and R' do access the same1115location.  However, if there is merely a control dependency between R1116and W then the CPU can speculatively forward W to R' before executing1117R; if the speculation turns out to be wrong then the CPU merely has to1118restart or abandon R'.1119 1120(In theory, a CPU might forward a store to a load when it runs across1121an address dependency like this:1122 1123	r1 = READ_ONCE(ptr);1124	WRITE_ONCE(*r1, 17);1125	r2 = READ_ONCE(*r1);1126 1127because it could tell that the store and the second load access the1128same location even before it knows what the location's address is.1129However, none of the architectures supported by the Linux kernel do1130this.)1131 1132Two memory accesses of the same location must always be executed in1133program order if the second access is a store.  Thus, if we have1134 1135	R ->po-loc W1136 1137(the po-loc link says that R comes before W in program order and they1138access the same location), the CPU is obliged to execute W after R.1139If it executed W first then the memory subsystem would respond to R's1140read request with the value stored by W (or an even later store), in1141violation of the read-write coherence rule.  Similarly, if we had1142 1143	W ->po-loc W'1144 1145and the CPU executed W' before W, then the memory subsystem would put1146W' before W in the coherence order.  It would effectively cause W to1147overwrite W', in violation of the write-write coherence rule.1148(Interestingly, an early ARMv8 memory model, now obsolete, proposed1149allowing out-of-order writes like this to occur.  The model avoided1150violating the write-write coherence rule by requiring the CPU not to1151send the W write to the memory subsystem at all!)1152 1153 1154AND THEN THERE WAS ALPHA1155------------------------1156 1157As mentioned above, the Alpha architecture is unique in that it does1158not appear to respect address dependencies to loads.  This means that1159code such as the following:1160 1161	int x = 0;1162	int y = -1;1163	int *ptr = &y;1164 1165	P0()1166	{1167		WRITE_ONCE(x, 1);1168		smp_wmb();1169		WRITE_ONCE(ptr, &x);1170	}1171 1172	P1()1173	{1174		int *r1;1175		int r2;1176 1177		r1 = ptr;1178		r2 = READ_ONCE(*r1);1179	}1180 1181can malfunction on Alpha systems (notice that P1 uses an ordinary load1182to read ptr instead of READ_ONCE()).  It is quite possible that r1 = &x1183and r2 = 0 at the end, in spite of the address dependency.1184 1185At first glance this doesn't seem to make sense.  We know that the1186smp_wmb() forces P0's store to x to propagate to P1 before the store1187to ptr does.  And since P1 can't execute its second load1188until it knows what location to load from, i.e., after executing its1189first load, the value x = 1 must have propagated to P1 before the1190second load executed.  So why doesn't r2 end up equal to 1?1191 1192The answer lies in the Alpha's split local caches.  Although the two1193stores do reach P1's local cache in the proper order, it can happen1194that the first store is processed by a busy part of the cache while1195the second store is processed by an idle part.  As a result, the x = 11196value may not become available for P1's CPU to read until after the1197ptr = &x value does, leading to the undesirable result above.  The1198final effect is that even though the two loads really are executed in1199program order, it appears that they aren't.1200 1201This could not have happened if the local cache had processed the1202incoming stores in FIFO order.  By contrast, other architectures1203maintain at least the appearance of FIFO order.1204 1205In practice, this difficulty is solved by inserting a special fence1206between P1's two loads when the kernel is compiled for the Alpha1207architecture.  In fact, as of version 4.15, the kernel automatically1208adds this fence after every READ_ONCE() and atomic load on Alpha.  The1209effect of the fence is to cause the CPU not to execute any po-later1210instructions until after the local cache has finished processing all1211the stores it has already received.  Thus, if the code was changed to:1212 1213	P1()1214	{1215		int *r1;1216		int r2;1217 1218		r1 = READ_ONCE(ptr);1219		r2 = READ_ONCE(*r1);1220	}1221 1222then we would never get r1 = &x and r2 = 0.  By the time P1 executed1223its second load, the x = 1 store would already be fully processed by1224the local cache and available for satisfying the read request.  Thus1225we have yet another reason why shared data should always be read with1226READ_ONCE() or another synchronization primitive rather than accessed1227directly.1228 1229The LKMM requires that smp_rmb(), acquire fences, and strong fences1230share this property: They do not allow the CPU to execute any po-later1231instructions (or po-later loads in the case of smp_rmb()) until all1232outstanding stores have been processed by the local cache.  In the1233case of a strong fence, the CPU first has to wait for all of its1234po-earlier stores to propagate to every other CPU in the system; then1235it has to wait for the local cache to process all the stores received1236as of that time -- not just the stores received when the strong fence1237began.1238 1239And of course, none of this matters for any architecture other than1240Alpha.1241 1242 1243THE HAPPENS-BEFORE RELATION: hb1244-------------------------------1245 1246The happens-before relation (hb) links memory accesses that have to1247execute in a certain order.  hb includes the ppo relation and two1248others, one of which is rfe.1249 1250W ->rfe R implies that W and R are on different CPUs.  It also means1251that W's store must have propagated to R's CPU before R executed;1252otherwise R could not have read the value stored by W.  Therefore W1253must have executed before R, and so we have W ->hb R.1254 1255The equivalent fact need not hold if W ->rfi R (i.e., W and R are on1256the same CPU).  As we have already seen, the operational model allows1257W's value to be forwarded to R in such cases, meaning that R may well1258execute before W does.1259 1260It's important to understand that neither coe nor fre is included in1261hb, despite their similarities to rfe.  For example, suppose we have1262W ->coe W'.  This means that W and W' are stores to the same location,1263they execute on different CPUs, and W comes before W' in the coherence1264order (i.e., W' overwrites W).  Nevertheless, it is possible for W' to1265execute before W, because the decision as to which store overwrites1266the other is made later by the memory subsystem.  When the stores are1267nearly simultaneous, either one can come out on top.  Similarly,1268R ->fre W means that W overwrites the value which R reads, but it1269doesn't mean that W has to execute after R.  All that's necessary is1270for the memory subsystem not to propagate W to R's CPU until after R1271has executed, which is possible if W executes shortly before R.1272 1273The third relation included in hb is like ppo, in that it only links1274events that are on the same CPU.  However it is more difficult to1275explain, because it arises only indirectly from the requirement of1276cache coherence.  The relation is called prop, and it links two events1277on CPU C in situations where a store from some other CPU comes after1278the first event in the coherence order and propagates to C before the1279second event executes.1280 1281This is best explained with some examples.  The simplest case looks1282like this:1283 1284	int x;1285 1286	P0()1287	{1288		int r1;1289 1290		WRITE_ONCE(x, 1);1291		r1 = READ_ONCE(x);1292	}1293 1294	P1()1295	{1296		WRITE_ONCE(x, 8);1297	}1298 1299If r1 = 8 at the end then P0's accesses must have executed in program1300order.  We can deduce this from the operational model; if P0's load1301had executed before its store then the value of the store would have1302been forwarded to the load, so r1 would have ended up equal to 1, not13038.  In this case there is a prop link from P0's write event to its read1304event, because P1's store came after P0's store in x's coherence1305order, and P1's store propagated to P0 before P0's load executed.1306 1307An equally simple case involves two loads of the same location that1308read from different stores:1309 1310	int x = 0;1311 1312	P0()1313	{1314		int r1, r2;1315 1316		r1 = READ_ONCE(x);1317		r2 = READ_ONCE(x);1318	}1319 1320	P1()1321	{1322		WRITE_ONCE(x, 9);1323	}1324 1325If r1 = 0 and r2 = 9 at the end then P0's accesses must have executed1326in program order.  If the second load had executed before the first1327then the x = 9 store must have been propagated to P0 before the first1328load executed, and so r1 would have been 9 rather than 0.  In this1329case there is a prop link from P0's first read event to its second,1330because P1's store overwrote the value read by P0's first load, and1331P1's store propagated to P0 before P0's second load executed.1332 1333Less trivial examples of prop all involve fences.  Unlike the simple1334examples above, they can require that some instructions are executed1335out of program order.  This next one should look familiar:1336 1337	int buf = 0, flag = 0;1338 1339	P0()1340	{1341		WRITE_ONCE(buf, 1);1342		smp_wmb();1343		WRITE_ONCE(flag, 1);1344	}1345 1346	P1()1347	{1348		int r1;1349		int r2;1350 1351		r1 = READ_ONCE(flag);1352		r2 = READ_ONCE(buf);1353	}1354 1355This is the MP pattern again, with an smp_wmb() fence between the two1356stores.  If r1 = 1 and r2 = 0 at the end then there is a prop link1357from P1's second load to its first (backwards!).  The reason is1358similar to the previous examples: The value P1 loads from buf gets1359overwritten by P0's store to buf, the fence guarantees that the store1360to buf will propagate to P1 before the store to flag does, and the1361store to flag propagates to P1 before P1 reads flag.1362 1363The prop link says that in order to obtain the r1 = 1, r2 = 0 result,1364P1 must execute its second load before the first.  Indeed, if the load1365from flag were executed first, then the buf = 1 store would already1366have propagated to P1 by the time P1's load from buf executed, so r21367would have been 1 at the end, not 0.  (The reasoning holds even for1368Alpha, although the details are more complicated and we will not go1369into them.)1370 1371But what if we put an smp_rmb() fence between P1's loads?  The fence1372would force the two loads to be executed in program order, and it1373would generate a cycle in the hb relation: The fence would create a ppo1374link (hence an hb link) from the first load to the second, and the1375prop relation would give an hb link from the second load to the first.1376Since an instruction can't execute before itself, we are forced to1377conclude that if an smp_rmb() fence is added, the r1 = 1, r2 = 01378outcome is impossible -- as it should be.1379 1380The formal definition of the prop relation involves a coe or fre link,1381followed by an arbitrary number of cumul-fence links, ending with an1382rfe link.  You can concoct more exotic examples, containing more than1383one fence, although this quickly leads to diminishing returns in terms1384of complexity.  For instance, here's an example containing a coe link1385followed by two cumul-fences and an rfe link, utilizing the fact that1386release fences are A-cumulative:1387 1388	int x, y, z;1389 1390	P0()1391	{1392		int r0;1393 1394		WRITE_ONCE(x, 1);1395		r0 = READ_ONCE(z);1396	}1397 1398	P1()1399	{1400		WRITE_ONCE(x, 2);1401		smp_wmb();1402		WRITE_ONCE(y, 1);1403	}1404 1405	P2()1406	{1407		int r2;1408 1409		r2 = READ_ONCE(y);1410		smp_store_release(&z, 1);1411	}1412 1413If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop1414link from P0's store to its load.  This is because P0's store gets1415overwritten by P1's store since x = 2 at the end (a coe link), the1416smp_wmb() ensures that P1's store to x propagates to P2 before the1417store to y does (the first cumul-fence), the store to y propagates to P21418before P2's load and store execute, P2's smp_store_release()1419guarantees that the stores to x and y both propagate to P0 before the1420store to z does (the second cumul-fence), and P0's load executes after the1421store to z has propagated to P0 (an rfe link).1422 1423In summary, the fact that the hb relation links memory access events1424in the order they execute means that it must not have cycles.  This1425requirement is the content of the LKMM's "happens-before" axiom.1426 1427The LKMM defines yet another relation connected to times of1428instruction execution, but it is not included in hb.  It relies on the1429particular properties of strong fences, which we cover in the next1430section.1431 1432 1433THE PROPAGATES-BEFORE RELATION: pb1434----------------------------------1435 1436The propagates-before (pb) relation capitalizes on the special1437features of strong fences.  It links two events E and F whenever some1438store is coherence-later than E and propagates to every CPU and to RAM1439before F executes.  The formal definition requires that E be linked to1440F via a coe or fre link, an arbitrary number of cumul-fences, an1441optional rfe link, a strong fence, and an arbitrary number of hb1442links.  Let's see how this definition works out.1443 1444Consider first the case where E is a store (implying that the sequence1445of links begins with coe).  Then there are events W, X, Y, and Z such1446that:1447 1448	E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F,1449 1450where the * suffix indicates an arbitrary number of links of the1451specified type, and the ? suffix indicates the link is optional (Y may1452be equal to X).  Because of the cumul-fence links, we know that W will1453propagate to Y's CPU before X does, hence before Y executes and hence1454before the strong fence executes.  Because this fence is strong, we1455know that W will propagate to every CPU and to RAM before Z executes.1456And because of the hb links, we know that Z will execute before F.1457Thus W, which comes later than E in the coherence order, will1458propagate to every CPU and to RAM before F executes.1459 1460The case where E is a load is exactly the same, except that the first1461link in the sequence is fre instead of coe.1462 1463The existence of a pb link from E to F implies that E must execute1464before F.  To see why, suppose that F executed first.  Then W would1465have propagated to E's CPU before E executed.  If E was a store, the1466memory subsystem would then be forced to make E come after W in the1467coherence order, contradicting the fact that E ->coe W.  If E was a1468load, the memory subsystem would then be forced to satisfy E's read1469request with the value stored by W or an even later store,1470contradicting the fact that E ->fre W.1471 1472A good example illustrating how pb works is the SB pattern with strong1473fences:1474 1475	int x = 0, y = 0;1476 1477	P0()1478	{1479		int r0;1480 1481		WRITE_ONCE(x, 1);1482		smp_mb();1483		r0 = READ_ONCE(y);1484	}1485 1486	P1()1487	{1488		int r1;1489 1490		WRITE_ONCE(y, 1);1491		smp_mb();1492		r1 = READ_ONCE(x);1493	}1494 1495If r0 = 0 at the end then there is a pb link from P0's load to P1's1496load: an fre link from P0's load to P1's store (which overwrites the1497value read by P0), and a strong fence between P1's store and its load.1498In this example, the sequences of cumul-fence and hb links are empty.1499Note that this pb link is not included in hb as an instance of prop,1500because it does not start and end on the same CPU.1501 1502Similarly, if r1 = 0 at the end then there is a pb link from P1's load1503to P0's.  This means that if both r1 and r2 were 0 there would be a1504cycle in pb, which is not possible since an instruction cannot execute1505before itself.  Thus, adding smp_mb() fences to the SB pattern1506prevents the r0 = 0, r1 = 0 outcome.1507 1508In summary, the fact that the pb relation links events in the order1509they execute means that it cannot have cycles.  This requirement is1510the content of the LKMM's "propagation" axiom.1511 1512 1513RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb1514------------------------------------------------------------------------1515 1516RCU (Read-Copy-Update) is a powerful synchronization mechanism.  It1517rests on two concepts: grace periods and read-side critical sections.1518 1519A grace period is the span of time occupied by a call to1520synchronize_rcu().  A read-side critical section (or just critical1521section, for short) is a region of code delimited by rcu_read_lock()1522at the start and rcu_read_unlock() at the end.  Critical sections can1523be nested, although we won't make use of this fact.1524 1525As far as memory models are concerned, RCU's main feature is its1526Grace-Period Guarantee, which states that a critical section can never1527span a full grace period.  In more detail, the Guarantee says:1528 1529	For any critical section C and any grace period G, at least1530	one of the following statements must hold:1531 1532(1)	C ends before G does, and in addition, every store that1533	propagates to C's CPU before the end of C must propagate to1534	every CPU before G ends.1535 1536(2)	G starts before C does, and in addition, every store that1537	propagates to G's CPU before the start of G must propagate1538	to every CPU before C starts.1539 1540In particular, it is not possible for a critical section to both start1541before and end after a grace period.1542 1543Here is a simple example of RCU in action:1544 1545	int x, y;1546 1547	P0()1548	{1549		rcu_read_lock();1550		WRITE_ONCE(x, 1);1551		WRITE_ONCE(y, 1);1552		rcu_read_unlock();1553	}1554 1555	P1()1556	{1557		int r1, r2;1558 1559		r1 = READ_ONCE(x);1560		synchronize_rcu();1561		r2 = READ_ONCE(y);1562	}1563 1564The Grace Period Guarantee tells us that when this code runs, it will1565never end with r1 = 1 and r2 = 0.  The reasoning is as follows.  r1 = 11566means that P0's store to x propagated to P1 before P1 called1567synchronize_rcu(), so P0's critical section must have started before1568P1's grace period, contrary to part (2) of the Guarantee.  On the1569other hand, r2 = 0 means that P0's store to y, which occurs before the1570end of the critical section, did not propagate to P1 before the end of1571the grace period, contrary to part (1).  Together the results violate1572the Guarantee.1573 1574In the kernel's implementations of RCU, the requirements for stores1575to propagate to every CPU are fulfilled by placing strong fences at1576suitable places in the RCU-related code.  Thus, if a critical section1577starts before a grace period does then the critical section's CPU will1578execute an smp_mb() fence after the end of the critical section and1579some time before the grace period's synchronize_rcu() call returns.1580And if a critical section ends after a grace period does then the1581synchronize_rcu() routine will execute an smp_mb() fence at its start1582and some time before the critical section's opening rcu_read_lock()1583executes.1584 1585What exactly do we mean by saying that a critical section "starts1586before" or "ends after" a grace period?  Some aspects of the meaning1587are pretty obvious, as in the example above, but the details aren't1588entirely clear.  The LKMM formalizes this notion by means of the1589rcu-link relation.  rcu-link encompasses a very general notion of1590"before": If E and F are RCU fence events (i.e., rcu_read_lock(),1591rcu_read_unlock(), or synchronize_rcu()) then among other things,1592E ->rcu-link F includes cases where E is po-before some memory-access1593event X, F is po-after some memory-access event Y, and we have any of1594X ->rfe Y, X ->co Y, or X ->fr Y.1595 1596The formal definition of the rcu-link relation is more than a little1597obscure, and we won't give it here.  It is closely related to the pb1598relation, and the details don't matter unless you want to comb through1599a somewhat lengthy formal proof.  Pretty much all you need to know1600about rcu-link is the information in the preceding paragraph.1601 1602The LKMM also defines the rcu-gp and rcu-rscsi relations.  They bring1603grace periods and read-side critical sections into the picture, in the1604following way:1605 1606	E ->rcu-gp F means that E and F are in fact the same event,1607	and that event is a synchronize_rcu() fence (i.e., a grace1608	period).1609 1610	E ->rcu-rscsi F means that E and F are the rcu_read_unlock()1611	and rcu_read_lock() fence events delimiting some read-side1612	critical section.  (The 'i' at the end of the name emphasizes1613	that this relation is "inverted": It links the end of the1614	critical section to the start.)1615 1616If we think of the rcu-link relation as standing for an extended1617"before", then X ->rcu-gp Y ->rcu-link Z roughly says that X is a1618grace period which ends before Z begins.  (In fact it covers more than1619this, because it also includes cases where some store propagates to1620Z's CPU before Z begins but doesn't propagate to some other CPU until1621after X ends.)  Similarly, X ->rcu-rscsi Y ->rcu-link Z says that X is1622the end of a critical section which starts before Z begins.1623 1624The LKMM goes on to define the rcu-order relation as a sequence of1625rcu-gp and rcu-rscsi links separated by rcu-link links, in which the1626number of rcu-gp links is >= the number of rcu-rscsi links.  For1627example:1628 1629	X ->rcu-gp Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V1630 1631would imply that X ->rcu-order V, because this sequence contains two1632rcu-gp links and one rcu-rscsi link.  (It also implies that1633X ->rcu-order T and Z ->rcu-order V.)  On the other hand:1634 1635	X ->rcu-rscsi Y ->rcu-link Z ->rcu-rscsi T ->rcu-link U ->rcu-gp V1636 1637does not imply X ->rcu-order V, because the sequence contains only1638one rcu-gp link but two rcu-rscsi links.1639 1640The rcu-order relation is important because the Grace Period Guarantee1641means that rcu-order links act kind of like strong fences.  In1642particular, E ->rcu-order F implies not only that E begins before F1643ends, but also that any write po-before E will propagate to every CPU1644before any instruction po-after F can execute.  (However, it does not1645imply that E must execute before F; in fact, each synchronize_rcu()1646fence event is linked to itself by rcu-order as a degenerate case.)1647 1648To prove this in full generality requires some intellectual effort.1649We'll consider just a very simple case:1650 1651	G ->rcu-gp W ->rcu-link Z ->rcu-rscsi F.1652 1653This formula means that G and W are the same event (a grace period),1654and there are events X, Y and a read-side critical section C such that:1655 1656	1. G = W is po-before or equal to X;1657 1658	2. X comes "before" Y in some sense (including rfe, co and fr);1659 1660	3. Y is po-before Z;1661 1662	4. Z is the rcu_read_unlock() event marking the end of C;1663 1664	5. F is the rcu_read_lock() event marking the start of C.1665 1666From 1 - 4 we deduce that the grace period G ends before the critical1667section C.  Then part (2) of the Grace Period Guarantee says not only1668that G starts before C does, but also that any write which executes on1669G's CPU before G starts must propagate to every CPU before C starts.1670In particular, the write propagates to every CPU before F finishes1671executing and hence before any instruction po-after F can execute.1672This sort of reasoning can be extended to handle all the situations1673covered by rcu-order.1674 1675The rcu-fence relation is a simple extension of rcu-order.  While1676rcu-order only links certain fence events (calls to synchronize_rcu(),1677rcu_read_lock(), or rcu_read_unlock()), rcu-fence links any events1678that are separated by an rcu-order link.  This is analogous to the way1679the strong-fence relation links events that are separated by an1680smp_mb() fence event (as mentioned above, rcu-order links act kind of1681like strong fences).  Written symbolically, X ->rcu-fence Y means1682there are fence events E and F such that:1683 1684	X ->po E ->rcu-order F ->po Y.1685 1686From the discussion above, we see this implies not only that X1687executes before Y, but also (if X is a store) that X propagates to1688every CPU before Y executes.  Thus rcu-fence is sort of a1689"super-strong" fence: Unlike the original strong fences (smp_mb() and1690synchronize_rcu()), rcu-fence is able to link events on different1691CPUs.  (Perhaps this fact should lead us to say that rcu-fence isn't1692really a fence at all!)1693 1694Finally, the LKMM defines the RCU-before (rb) relation in terms of1695rcu-fence.  This is done in essentially the same way as the pb1696relation was defined in terms of strong-fence.  We will omit the1697details; the end result is that E ->rb F implies E must execute1698before F, just as E ->pb F does (and for much the same reasons).1699 1700Putting this all together, the LKMM expresses the Grace Period1701Guarantee by requiring that the rb relation does not contain a cycle.1702Equivalently, this "rcu" axiom requires that there are no events E1703and F with E ->rcu-link F ->rcu-order E.  Or to put it a third way,1704the axiom requires that there are no cycles consisting of rcu-gp and1705rcu-rscsi alternating with rcu-link, where the number of rcu-gp links1706is >= the number of rcu-rscsi links.1707 1708Justifying the axiom isn't easy, but it is in fact a valid1709formalization of the Grace Period Guarantee.  We won't attempt to go1710through the detailed argument, but the following analysis gives a1711taste of what is involved.  Suppose both parts of the Guarantee are1712violated: A critical section starts before a grace period, and some1713store propagates to the critical section's CPU before the end of the1714critical section but doesn't propagate to some other CPU until after1715the end of the grace period.1716 1717Putting symbols to these ideas, let L and U be the rcu_read_lock() and1718rcu_read_unlock() fence events delimiting the critical section in1719question, and let S be the synchronize_rcu() fence event for the grace1720period.  Saying that the critical section starts before S means there1721are events Q and R where Q is po-after L (which marks the start of the1722critical section), Q is "before" R in the sense used by the rcu-link1723relation, and R is po-before the grace period S.  Thus we have:1724 1725	L ->rcu-link S.1726 1727Let W be the store mentioned above, let Y come before the end of the1728critical section and witness that W propagates to the critical1729section's CPU by reading from W, and let Z on some arbitrary CPU be a1730witness that W has not propagated to that CPU, where Z happens after1731some event X which is po-after S.  Symbolically, this amounts to:1732 1733	S ->po X ->hb* Z ->fr W ->rf Y ->po U.1734 1735The fr link from Z to W indicates that W has not propagated to Z's CPU1736at the time that Z executes.  From this, it can be shown (see the1737discussion of the rcu-link relation earlier) that S and U are related1738by rcu-link:1739 1740	S ->rcu-link U.1741 1742Since S is a grace period we have S ->rcu-gp S, and since L and U are1743the start and end of the critical section C we have U ->rcu-rscsi L.1744From this we obtain:1745 1746	S ->rcu-gp S ->rcu-link U ->rcu-rscsi L ->rcu-link S,1747 1748a forbidden cycle.  Thus the "rcu" axiom rules out this violation of1749the Grace Period Guarantee.1750 1751For something a little more down-to-earth, let's see how the axiom1752works out in practice.  Consider the RCU code example from above, this1753time with statement labels added:1754 1755	int x, y;1756 1757	P0()1758	{1759		L: rcu_read_lock();1760		X: WRITE_ONCE(x, 1);1761		Y: WRITE_ONCE(y, 1);1762		U: rcu_read_unlock();1763	}1764 1765	P1()1766	{1767		int r1, r2;1768 1769		Z: r1 = READ_ONCE(x);1770		S: synchronize_rcu();1771		W: r2 = READ_ONCE(y);1772	}1773 1774 1775If r2 = 0 at the end then P0's store at Y overwrites the value that1776P1's load at W reads from, so we have W ->fre Y.  Since S ->po W and1777also Y ->po U, we get S ->rcu-link U.  In addition, S ->rcu-gp S1778because S is a grace period.1779 1780If r1 = 1 at the end then P1's load at Z reads from P0's store at X,1781so we have X ->rfe Z.  Together with L ->po X and Z ->po S, this1782yields L ->rcu-link S.  And since L and U are the start and end of a1783critical section, we have U ->rcu-rscsi L.1784 1785Then U ->rcu-rscsi L ->rcu-link S ->rcu-gp S ->rcu-link U is a1786forbidden cycle, violating the "rcu" axiom.  Hence the outcome is not1787allowed by the LKMM, as we would expect.1788 1789For contrast, let's see what can happen in a more complicated example:1790 1791	int x, y, z;1792 1793	P0()1794	{1795		int r0;1796 1797		L0: rcu_read_lock();1798		    r0 = READ_ONCE(x);1799		    WRITE_ONCE(y, 1);1800		U0: rcu_read_unlock();1801	}1802 1803	P1()1804	{1805		int r1;1806 1807		    r1 = READ_ONCE(y);1808		S1: synchronize_rcu();1809		    WRITE_ONCE(z, 1);1810	}1811 1812	P2()1813	{1814		int r2;1815 1816		L2: rcu_read_lock();1817		    r2 = READ_ONCE(z);1818		    WRITE_ONCE(x, 1);1819		U2: rcu_read_unlock();1820	}1821 1822If r0 = r1 = r2 = 1 at the end, then similar reasoning to before shows1823that U0 ->rcu-rscsi L0 ->rcu-link S1 ->rcu-gp S1 ->rcu-link U2 ->rcu-rscsi1824L2 ->rcu-link U0.  However this cycle is not forbidden, because the1825sequence of relations contains fewer instances of rcu-gp (one) than of1826rcu-rscsi (two).  Consequently the outcome is allowed by the LKMM.1827The following instruction timing diagram shows how it might actually1828occur:1829 1830P0			P1			P21831--------------------	--------------------	--------------------1832rcu_read_lock()1833WRITE_ONCE(y, 1)1834			r1 = READ_ONCE(y)1835			synchronize_rcu() starts1836			.			rcu_read_lock()1837			.			WRITE_ONCE(x, 1)1838r0 = READ_ONCE(x)	.1839rcu_read_unlock()	.1840			synchronize_rcu() ends1841			WRITE_ONCE(z, 1)1842						r2 = READ_ONCE(z)1843						rcu_read_unlock()1844 1845This requires P0 and P2 to execute their loads and stores out of1846program order, but of course they are allowed to do so.  And as you1847can see, the Grace Period Guarantee is not violated: The critical1848section in P0 both starts before P1's grace period does and ends1849before it does, and the critical section in P2 both starts after P1's1850grace period does and ends after it does.1851 1852The LKMM supports SRCU (Sleepable Read-Copy-Update) in addition to1853normal RCU.  The ideas involved are much the same as above, with new1854relations srcu-gp and srcu-rscsi added to represent SRCU grace periods1855and read-side critical sections.  However, there are some significant1856differences between RCU read-side critical sections and their SRCU1857counterparts, as described in the next section.1858 1859 1860SRCU READ-SIDE CRITICAL SECTIONS1861--------------------------------1862 1863The LKMM uses the srcu-rscsi relation to model SRCU read-side critical1864sections.  They differ from RCU read-side critical sections in the1865following respects:1866 18671.	Unlike the analogous RCU primitives, synchronize_srcu(),1868	srcu_read_lock(), and srcu_read_unlock() take a pointer to a1869	struct srcu_struct as an argument.  This structure is called1870	an SRCU domain, and calls linked by srcu-rscsi must have the1871	same domain.  Read-side critical sections and grace periods1872	associated with different domains are independent of one1873	another; the SRCU version of the RCU Guarantee applies only1874	to pairs of critical sections and grace periods having the1875	same domain.1876 18772.	srcu_read_lock() returns a value, called the index, which must1878	be passed to the matching srcu_read_unlock() call.  Unlike1879	rcu_read_lock() and rcu_read_unlock(), an srcu_read_lock()1880	call does not always have to match the next unpaired1881	srcu_read_unlock().  In fact, it is possible for two SRCU1882	read-side critical sections to overlap partially, as in the1883	following example (where s is an srcu_struct and idx1 and idx21884	are integer variables):1885 1886		idx1 = srcu_read_lock(&s);	// Start of first RSCS1887		idx2 = srcu_read_lock(&s);	// Start of second RSCS1888		srcu_read_unlock(&s, idx1);	// End of first RSCS1889		srcu_read_unlock(&s, idx2);	// End of second RSCS1890 1891	The matching is determined entirely by the domain pointer and1892	index value.  By contrast, if the calls had been1893	rcu_read_lock() and rcu_read_unlock() then they would have1894	created two nested (fully overlapping) read-side critical1895	sections: an inner one and an outer one.1896 18973.	The srcu_down_read() and srcu_up_read() primitives work1898	exactly like srcu_read_lock() and srcu_read_unlock(), except1899	that matching calls don't have to execute on the same CPU.1900	(The names are meant to be suggestive of operations on1901	semaphores.)  Since the matching is determined by the domain1902	pointer and index value, these primitives make it possible for1903	an SRCU read-side critical section to start on one CPU and end1904	on another, so to speak.1905 1906In order to account for these properties of SRCU, the LKMM models1907srcu_read_lock() as a special type of load event (which is1908appropriate, since it takes a memory location as argument and returns1909a value, just as a load does) and srcu_read_unlock() as a special type1910of store event (again appropriate, since it takes as arguments a1911memory location and a value).  These loads and stores are annotated as1912belonging to the "srcu-lock" and "srcu-unlock" event classes1913respectively.1914 1915This approach allows the LKMM to tell whether two events are1916associated with the same SRCU domain, simply by checking whether they1917access the same memory location (i.e., they are linked by the loc1918relation).  It also gives a way to tell which unlock matches a1919particular lock, by checking for the presence of a data dependency1920from the load (srcu-lock) to the store (srcu-unlock).  For example,1921given the situation outlined earlier (with statement labels added):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 1928the LKMM will treat A and B as loads from s yielding values saved in1929idx1 and idx2 respectively.  Similarly, it will treat C and D as1930though they stored the values from idx1 and idx2 in s.  The end result1931is 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 1938except for the presence of the special srcu-lock and srcu-unlock1939annotations.  You can see at once that we have A ->data C and1940B ->data D.  These dependencies tell the LKMM that C is the1941srcu-unlock event matching srcu-lock event A, and D is the1942srcu-unlock event matching srcu-lock event B.1943 1944This approach is admittedly a hack, and it has the potential to lead1945to 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 1952the LKMM will believe that idx2 must have the same value as idx1,1953since it reads from the immediately preceding store of idx1 in s.1954Fortunately this won't matter, assuming that litmus tests never do1955anything with SRCU index values other than pass them to1956srcu_read_unlock() or srcu_up_read() calls.1957 1958However, sometimes it is necessary to store an index value in a1959shared variable temporarily.  In fact, this is the only way for1960srcu_down_read() to pass the index it gets to an srcu_up_read() call1961on a different CPU.  In more detail, we might have soething like: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 1982Assuming that P1 executes after P0 and does read the index value1983stored in x, we can write this (using brackets to represent event1984annotations) as:1985 1986	A[srcu-lock] ->data B[once] ->rf C[once] ->data D[srcu-unlock].1987 1988The LKMM defines a carry-srcu-data relation to express this pattern;1989it permits an arbitrarily long sequence of1990 1991	data ; rf1992 1993pairs (that is, a data link followed by an rf link) to occur between1994an srcu-lock event and the final data dependency leading to the1995matching srcu-unlock event.  carry-srcu-data is complicated by the1996need to ensure that none of the intermediate store events in this1997sequence are instances of srcu-unlock.  This is necessary because in a1998pattern 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 2005the LKMM treats B as a store to the variable s and C as a load from2006that variable, creating an undesirable rf link from B to C:2007 2008	A ->data B ->rf C ->data D.2009 2010This would cause carry-srcu-data to mistakenly extend a data2011dependency from A to D, giving the impression that D was the2012srcu-unlock event matching A's srcu-lock.  To avoid such problems,2013carry-srcu-data does not accept sequences in which the ends of any of2014the intermediate ->data links (B above) is an srcu-unlock event.2015 2016 2017LOCKING2018-------2019 2020The LKMM includes locking.  In fact, there is special code for locking2021in the formal model, added in order to make tools run faster.2022However, this special code is intended to be more or less equivalent2023to concepts we have already covered.  A spinlock_t variable is treated2024the same as an int, and spin_lock(&s) is treated almost the same as:2025 2026	while (cmpxchg_acquire(&s, 0, 1) != 0)2027		cpu_relax();2028 2029This waits until s is equal to 0 and then atomically sets it to 1,2030and the read part of the cmpxchg operation acts as an acquire fence.2031An alternate way to express the same thing would be:2032 2033	r = xchg_acquire(&s, 1);2034 2035along with a requirement that at the end, r = 0.  Similarly,2036spin_trylock(&s) is treated almost the same as:2037 2038	return !cmpxchg_acquire(&s, 0, 1);2039 2040which atomically sets s to 1 if it is currently equal to 0 and returns2041true if it succeeds (the read part of the cmpxchg operation acts as an2042acquire fence only if the operation is successful).  spin_unlock(&s)2043is treated almost the same as:2044 2045	smp_store_release(&s, 0);2046 2047The "almost" qualifiers above need some explanation.  In the LKMM, the2048store-release in a spin_unlock() and the load-acquire which forms the2049first half of the atomic rmw update in a spin_lock() or a successful2050spin_trylock() -- we can call these things lock-releases and2051lock-acquires -- have two properties beyond those of ordinary releases2052and acquires.2053 2054First, when a lock-acquire reads from or is po-after a lock-release,2055the LKMM requires that every instruction po-before the lock-release2056must execute before any instruction po-after the lock-acquire.  This2057would naturally hold if the release and acquire operations were on2058different CPUs and accessed the same lock variable, but the LKMM says2059it also holds when they are on the same CPU, even if they access2060different lock variables.  For example:2061 2062	int x, y;2063	spinlock_t s, t;2064 2065	P0()2066	{2067		int r1, r2;2068 2069		spin_lock(&s);2070		r1 = READ_ONCE(x);2071		spin_unlock(&s);2072		spin_lock(&t);2073		r2 = READ_ONCE(y);2074		spin_unlock(&t);2075	}2076 2077	P1()2078	{2079		WRITE_ONCE(y, 1);2080		smp_wmb();2081		WRITE_ONCE(x, 1);2082	}2083 2084Here the second spin_lock() is po-after the first spin_unlock(), and2085therefore the load of x must execute before the load of y, even though2086the two locking operations use different locks.  Thus we cannot have2087r1 = 1 and r2 = 0 at the end (this is an instance of the MP pattern).2088 2089This requirement does not apply to ordinary release and acquire2090fences, only to lock-related operations.  For instance, suppose P0()2091in the example had been written as:2092 2093	P0()2094	{2095		int r1, r2, r3;2096 2097		r1 = READ_ONCE(x);2098		smp_store_release(&s, 1);2099		r3 = smp_load_acquire(&s);2100		r2 = READ_ONCE(y);2101	}2102 2103Then the CPU would be allowed to forward the s = 1 value from the2104smp_store_release() to the smp_load_acquire(), executing the2105instructions in the following order:2106 2107		r3 = smp_load_acquire(&s);	// Obtains r3 = 12108		r2 = READ_ONCE(y);2109		r1 = READ_ONCE(x);2110		smp_store_release(&s, 1);	// Value is forwarded2111 2112and thus it could load y before x, obtaining r2 = 0 and r1 = 1.2113 2114Second, when a lock-acquire reads from or is po-after a lock-release,2115and some other stores W and W' occur po-before the lock-release and2116po-after the lock-acquire respectively, the LKMM requires that W must2117propagate to each CPU before W' does.  For example, consider:2118 2119	int x, y;2120	spinlock_t s;2121 2122	P0()2123	{2124		spin_lock(&s);2125		WRITE_ONCE(x, 1);2126		spin_unlock(&s);2127	}2128 2129	P1()2130	{2131		int r1;2132 2133		spin_lock(&s);2134		r1 = READ_ONCE(x);2135		WRITE_ONCE(y, 1);2136		spin_unlock(&s);2137	}2138 2139	P2()2140	{2141		int r2, r3;2142 2143		r2 = READ_ONCE(y);2144		smp_rmb();2145		r3 = READ_ONCE(x);2146	}2147 2148If r1 = 1 at the end then the spin_lock() in P1 must have read from2149the spin_unlock() in P0.  Hence the store to x must propagate to P22150before the store to y does, so we cannot have r2 = 1 and r3 = 0.  But2151if P1 had used a lock variable different from s, the writes could have2152propagated in either order.  (On the other hand, if the code in P0 and2153P1 had all executed on a single CPU, as in the example before this2154one, then the writes would have propagated in order even if the two2155critical sections used different lock variables.)2156 2157These two special requirements for lock-release and lock-acquire do2158not arise from the operational model.  Nevertheless, kernel developers2159have come to expect and rely on them because they do hold on all2160architectures supported by the Linux kernel, albeit for various2161differing reasons.2162 2163 2164PLAIN ACCESSES AND DATA RACES2165-----------------------------2166 2167In the LKMM, memory accesses such as READ_ONCE(x), atomic_inc(&y),2168smp_load_acquire(&z), and so on are collectively referred to as2169"marked" accesses, because they are all annotated with special2170operations of one kind or another.  Ordinary C-language memory2171accesses such as x or y = 0 are simply called "plain" accesses.2172 2173Early versions of the LKMM had nothing to say about plain accesses.2174The C standard allows compilers to assume that the variables affected2175by plain accesses are not concurrently read or written by any other2176threads or CPUs.  This leaves compilers free to implement all manner2177of transformations or optimizations of code containing plain accesses,2178making such code very difficult for a memory model to handle.2179 2180Here is just one example of a possible pitfall:2181 2182	int a = 6;2183	int *x = &a;2184 2185	P0()2186	{2187		int *r1;2188		int r2 = 0;2189 2190		r1 = x;2191		if (r1 != NULL)2192			r2 = READ_ONCE(*r1);2193	}2194 2195	P1()2196	{2197		WRITE_ONCE(x, NULL);2198	}2199 2200On the face of it, one would expect that when this code runs, the only2201possible final values for r2 are 6 and 0, depending on whether or not2202P1's store to x propagates to P0 before P0's load from x executes.2203But since P0's load from x is a plain access, the compiler may decide2204to carry out the load twice (for the comparison against NULL, then again2205for the READ_ONCE()) and eliminate the temporary variable r1.  The2206object code generated for P0 could therefore end up looking rather2207like this:2208 2209	P0()2210	{2211		int r2 = 0;2212 2213		if (x != NULL)2214			r2 = READ_ONCE(*x);2215	}2216 2217And now it is obvious that this code runs the risk of dereferencing a2218NULL pointer, because P1's store to x might propagate to P0 after the2219test against NULL has been made but before the READ_ONCE() executes.2220If the original code had said "r1 = READ_ONCE(x)" instead of "r1 = x",2221the compiler would not have performed this optimization and there2222would be no possibility of a NULL-pointer dereference.2223 2224Given the possibility of transformations like this one, the LKMM2225doesn't try to predict all possible outcomes of code containing plain2226accesses.  It is instead content to determine whether the code2227violates the compiler's assumptions, which would render the ultimate2228outcome undefined.2229 2230In technical terms, the compiler is allowed to assume that when the2231program executes, there will not be any data races.  A "data race"2232occurs when there are two memory accesses such that:2233 22341.	they access the same location,2235 22362.	at least one of them is a store,2237 22383.	at least one of them is plain,2239 22404.	they occur on different CPUs (or in different threads on the2241	same CPU), and2242 22435.	they execute concurrently.2244 2245In the literature, two accesses are said to "conflict" if they satisfy22461 and 2 above.  We'll go a little farther and say that two accesses2247are "race candidates" if they satisfy 1 - 4.  Thus, whether or not two2248race candidates actually do race in a given execution depends on2249whether they are concurrent.2250 2251The LKMM tries to determine whether a program contains race candidates2252which may execute concurrently; if it does then the LKMM says there is2253a potential data race and makes no predictions about the program's2254outcome.2255 2256Determining whether two accesses are race candidates is easy; you can2257see that all the concepts involved in the definition above are already2258part of the memory model.  The hard part is telling whether they may2259execute concurrently.  The LKMM takes a conservative attitude,2260assuming that accesses may be concurrent unless it can prove they2261are not.2262 2263If two memory accesses aren't concurrent then one must execute before2264the other.  Therefore the LKMM decides two accesses aren't concurrent2265if they can be connected by a sequence of hb, pb, and rb links2266(together referred to as xb, for "executes before").  However, there2267are two complicating factors.2268 2269If X is a load and X executes before a store Y, then indeed there is2270no danger of X and Y being concurrent.  After all, Y can't have any2271effect on the value obtained by X until the memory subsystem has2272propagated Y from its own CPU to X's CPU, which won't happen until2273some time after Y executes and thus after X executes.  But if X is a2274store, then even if X executes before Y it is still possible that X2275will propagate to Y's CPU just as Y is executing.  In such a case X2276could very well interfere somehow with Y, and we would have to2277consider X and Y to be concurrent.2278 2279Therefore when X is a store, for X and Y to be non-concurrent the LKMM2280requires not only that X must execute before Y but also that X must2281propagate to Y's CPU before Y executes.  (Or vice versa, of course, if2282Y executes before X -- then Y must propagate to X's CPU before X2283executes if Y is a store.)  This is expressed by the visibility2284relation (vis), where X ->vis Y is defined to hold if there is an2285intermediate event Z such that:2286 2287	X is connected to Z by a possibly empty sequence of2288	cumul-fence links followed by an optional rfe link (if none of2289	these links are present, X and Z are the same event),2290 2291and either:2292 2293	Z is connected to Y by a strong-fence link followed by a2294	possibly empty sequence of xb links,2295 2296or:2297 2298	Z is on the same CPU as Y and is connected to Y by a possibly2299	empty sequence of xb links (again, if the sequence is empty it2300	means Z and Y are the same event).2301 2302The motivations behind this definition are straightforward:2303 2304	cumul-fence memory barriers force stores that are po-before2305	the barrier to propagate to other CPUs before stores that are2306	po-after the barrier.2307 2308	An rfe link from an event W to an event R says that R reads2309	from W, which certainly means that W must have propagated to2310	R's CPU before R executed.2311 2312	strong-fence memory barriers force stores that are po-before2313	the barrier, or that propagate to the barrier's CPU before the2314	barrier executes, to propagate to all CPUs before any events2315	po-after the barrier can execute.2316 2317To see how this works out in practice, consider our old friend, the MP2318pattern (with fences and statement labels, but without the conditional2319test):2320 2321	int buf = 0, flag = 0;2322 2323	P0()2324	{2325		X: WRITE_ONCE(buf, 1);2326		   smp_wmb();2327		W: WRITE_ONCE(flag, 1);2328	}2329 2330	P1()2331	{2332		int r1;2333		int r2 = 0;2334 2335		Z: r1 = READ_ONCE(flag);2336		   smp_rmb();2337		Y: r2 = READ_ONCE(buf);2338	}2339 2340The smp_wmb() memory barrier gives a cumul-fence link from X to W, and2341assuming r1 = 1 at the end, there is an rfe link from W to Z.  This2342means that the store to buf must propagate from P0 to P1 before Z2343executes.  Next, Z and Y are on the same CPU and the smp_rmb() fence2344provides an xb link from Z to Y (i.e., it forces Z to execute before2345Y).  Therefore we have X ->vis Y: X must propagate to Y's CPU before Y2346executes.2347 2348The second complicating factor mentioned above arises from the fact2349that when we are considering data races, some of the memory accesses2350are plain.  Now, although we have not said so explicitly, up to this2351point most of the relations defined by the LKMM (ppo, hb, prop,2352cumul-fence, pb, and so on -- including vis) apply only to marked2353accesses.2354 2355There are good reasons for this restriction.  The compiler is not2356allowed to apply fancy transformations to marked accesses, and2357consequently each such access in the source code corresponds more or2358less directly to a single machine instruction in the object code.  But2359plain accesses are a different story; the compiler may combine them,2360split them up, duplicate them, eliminate them, invent new ones, and2361who knows what else.  Seeing a plain access in the source code tells2362you almost nothing about what machine instructions will end up in the2363object code.2364 2365Fortunately, the compiler isn't completely free; it is subject to some2366limitations.  For one, it is not allowed to introduce a data race into2367the object code if the source code does not already contain a data2368race (if it could, memory models would be useless and no multithreaded2369code would be safe!).  For another, it cannot move a plain access past2370a compiler barrier.2371 2372A compiler barrier is a kind of fence, but as the name implies, it2373only affects the compiler; it does not necessarily have any effect on2374how instructions are executed by the CPU.  In Linux kernel source2375code, the barrier() function is a compiler barrier.  It doesn't give2376rise directly to any machine instructions in the object code; rather,2377it affects how the compiler generates the rest of the object code.2378Given source code like this:2379 2380	... some memory accesses ...2381	barrier();2382	... some other memory accesses ...2383 2384the barrier() function ensures that the machine instructions2385corresponding to the first group of accesses will all end po-before2386any machine instructions corresponding to the second group of accesses2387-- even if some of the accesses are plain.  (Of course, the CPU may2388then execute some of those accesses out of program order, but we2389already know how to deal with such issues.)  Without the barrier()2390there would be no such guarantee; the two groups of accesses could be2391intermingled or even reversed in the object code.2392 2393The LKMM doesn't say much about the barrier() function, but it does2394require that all fences are also compiler barriers.  In addition, it2395requires that the ordering properties of memory barriers such as2396smp_rmb() or smp_store_release() apply to plain accesses as well as to2397marked accesses.2398 2399This is the key to analyzing data races.  Consider the MP pattern2400again, now using plain accesses for buf:2401 2402	int buf = 0, flag = 0;2403 2404	P0()2405	{2406		U: buf = 1;2407		   smp_wmb();2408		X: WRITE_ONCE(flag, 1);2409	}2410 2411	P1()2412	{2413		int r1;2414		int r2 = 0;2415 2416		Y: r1 = READ_ONCE(flag);2417		   if (r1) {2418			   smp_rmb();2419			V: r2 = buf;2420		   }2421	}2422 2423This program does not contain a data race.  Although the U and V2424accesses are race candidates, the LKMM can prove they are not2425concurrent as follows:2426 2427	The smp_wmb() fence in P0 is both a compiler barrier and a2428	cumul-fence.  It guarantees that no matter what hash of2429	machine instructions the compiler generates for the plain2430	access U, all those instructions will be po-before the fence.2431	Consequently U's store to buf, no matter how it is carried out2432	at the machine level, must propagate to P1 before X's store to2433	flag does.2434 2435	X and Y are both marked accesses.  Hence an rfe link from X to2436	Y is a valid indicator that X propagated to P1 before Y2437	executed, i.e., X ->vis Y.  (And if there is no rfe link then2438	r1 will be 0, so V will not be executed and ipso facto won't2439	race with U.)2440 2441	The smp_rmb() fence in P1 is a compiler barrier as well as a2442	fence.  It guarantees that all the machine-level instructions2443	corresponding to the access V will be po-after the fence, and2444	therefore any loads among those instructions will execute2445	after the fence does and hence after Y does.2446 2447Thus U's store to buf is forced to propagate to P1 before V's load2448executes (assuming V does execute), ruling out the possibility of a2449data race between them.2450 2451This analysis illustrates how the LKMM deals with plain accesses in2452general.  Suppose R is a plain load and we want to show that R2453executes before some marked access E.  We can do this by finding a2454marked access X such that R and X are ordered by a suitable fence and2455X ->xb* E.  If E was also a plain access, we would also look for a2456marked access Y such that X ->xb* Y, and Y and E are ordered by a2457fence.  We describe this arrangement by saying that R is2458"post-bounded" by X and E is "pre-bounded" by Y.2459 2460In fact, we go one step further: Since R is a read, we say that R is2461"r-post-bounded" by X.  Similarly, E would be "r-pre-bounded" or2462"w-pre-bounded" by Y, depending on whether E was a store or a load.2463This distinction is needed because some fences affect only loads2464(i.e., smp_rmb()) and some affect only stores (smp_wmb()); otherwise2465the two types of bounds are the same.  And as a degenerate case, we2466say that a marked access pre-bounds and post-bounds itself (e.g., if R2467above were a marked load then X could simply be taken to be R itself.)2468 2469The need to distinguish between r- and w-bounding raises yet another2470issue.  When the source code contains a plain store, the compiler is2471allowed to put plain loads of the same location into the object code.2472For example, given the source code:2473 2474	x = 1;2475 2476the compiler is theoretically allowed to generate object code that2477looks like:2478 2479	if (x != 1)2480		x = 1;2481 2482thereby adding a load (and possibly replacing the store entirely).2483For this reason, whenever the LKMM requires a plain store to be2484w-pre-bounded or w-post-bounded by a marked access, it also requires2485the store to be r-pre-bounded or r-post-bounded, so as to handle cases2486where the compiler adds a load.2487 2488(This may be overly cautious.  We don't know of any examples where a2489compiler has augmented a store with a load in this fashion, and the2490Linux kernel developers would probably fight pretty hard to change a2491compiler if it ever did this.  Still, better safe than sorry.)2492 2493Incidentally, the other tranformation -- augmenting a plain load by2494adding in a store to the same location -- is not allowed.  This is2495because the compiler cannot know whether any other CPUs might perform2496a concurrent load from that location.  Two concurrent loads don't2497constitute a race (they can't interfere with each other), but a store2498does race with a concurrent load.  Thus adding a store might create a2499data race where one was not already present in the source code,2500something the compiler is forbidden to do.  Augmenting a store with a2501load, on the other hand, is acceptable because doing so won't create a2502data race unless one already existed.2503 2504The LKMM includes a second way to pre-bound plain accesses, in2505addition to fences: an address dependency from a marked load.  That2506is, in the sequence:2507 2508	p = READ_ONCE(ptr);2509	r = *p;2510 2511the LKMM says that the marked load of ptr pre-bounds the plain load of2512*p; the marked load must execute before any of the machine2513instructions corresponding to the plain load.  This is a reasonable2514stipulation, since after all, the CPU can't perform the load of *p2515until it knows what value p will hold.  Furthermore, without some2516assumption like this one, some usages typical of RCU would count as2517data races.  For example:2518 2519	int a = 1, b;2520	int *ptr = &a;2521 2522	P0()2523	{2524		b = 2;2525		rcu_assign_pointer(ptr, &b);2526	}2527 2528	P1()2529	{2530		int *p;2531		int r;2532 2533		rcu_read_lock();2534		p = rcu_dereference(ptr);2535		r = *p;2536		rcu_read_unlock();2537	}2538 2539(In this example the rcu_read_lock() and rcu_read_unlock() calls don't2540really do anything, because there aren't any grace periods.  They are2541included merely for the sake of good form; typically P0 would call2542synchronize_rcu() somewhere after the rcu_assign_pointer().)2543 2544rcu_assign_pointer() performs a store-release, so the plain store to b2545is definitely w-post-bounded before the store to ptr, and the two2546stores will propagate to P1 in that order.  However, rcu_dereference()2547is only equivalent to READ_ONCE().  While it is a marked access, it is2548not a fence or compiler barrier.  Hence the only guarantee we have2549that the load of ptr in P1 is r-pre-bounded before the load of *p2550(thus avoiding a race) is the assumption about address dependencies.2551 2552This is a situation where the compiler can undermine the memory model,2553and a certain amount of care is required when programming constructs2554like this one.  In particular, comparisons between the pointer and2555other known addresses can cause trouble.  If you have something like:2556 2557	p = rcu_dereference(ptr);2558	if (p == &x)2559		r = *p;2560 2561then the compiler just might generate object code resembling:2562 2563	p = rcu_dereference(ptr);2564	if (p == &x)2565		r = x;2566 2567or even:2568 2569	rtemp = x;2570	p = rcu_dereference(ptr);2571	if (p == &x)2572		r = rtemp;2573 2574which would invalidate the memory model's assumption, since the CPU2575could now perform the load of x before the load of ptr (there might be2576a control dependency but no address dependency at the machine level).2577 2578Finally, it turns out there is a situation in which a plain write does2579not need to be w-post-bounded: when it is separated from the other2580race-candidate access by a fence.  At first glance this may seem2581impossible.  After all, to be race candidates the two accesses must2582be on different CPUs, and fences don't link events on different CPUs.2583Well, normal fences don't -- but rcu-fence can!  Here's an example:2584 2585	int x, y;2586 2587	P0()2588	{2589		WRITE_ONCE(x, 1);2590		synchronize_rcu();2591		y = 3;2592	}2593 2594	P1()2595	{2596		rcu_read_lock();2597		if (READ_ONCE(x) == 0)2598			y = 2;2599		rcu_read_unlock();2600	}2601 2602Do the plain stores to y race?  Clearly not if P1 reads a non-zero2603value for x, so let's assume the READ_ONCE(x) does obtain 0.  This2604means that the read-side critical section in P1 must finish executing2605before the grace period in P0 does, because RCU's Grace-Period2606Guarantee says that otherwise P0's store to x would have propagated to2607P1 before the critical section started and so would have been visible2608to the READ_ONCE().  (Another way of putting it is that the fre link2609from the READ_ONCE() to the WRITE_ONCE() gives rise to an rcu-link2610between those two events.)2611 2612This means there is an rcu-fence link from P1's "y = 2" store to P0's2613"y = 3" store, and consequently the first must propagate from P1 to P02614before the second can execute.  Therefore the two stores cannot be2615concurrent and there is no race, even though P1's plain store to y2616isn't w-post-bounded by any marked accesses.2617 2618Putting all this material together yields the following picture.  For2619race-candidate stores W and W', where W ->co W', the LKMM says the2620stores don't race if W can be linked to W' by a2621 2622	w-post-bounded ; vis ; w-pre-bounded2623 2624sequence.  If W is plain then they also have to be linked by an2625 2626	r-post-bounded ; xb* ; w-pre-bounded2627 2628sequence, and if W' is plain then they also have to be linked by a2629 2630	w-post-bounded ; vis ; r-pre-bounded2631 2632sequence.  For race-candidate load R and store W, the LKMM says the2633two accesses don't race if R can be linked to W by an2634 2635	r-post-bounded ; xb* ; w-pre-bounded2636 2637sequence or if W can be linked to R by a2638 2639	w-post-bounded ; vis ; r-pre-bounded2640 2641sequence.  For the cases involving a vis link, the LKMM also accepts2642sequences in which W is linked to W' or R by a2643 2644	strong-fence ; xb* ; {w and/or r}-pre-bounded2645 2646sequence with no post-bounding, and in every case the LKMM also allows2647the link simply to be a fence with no bounding at all.  If no sequence2648of the appropriate sort exists, the LKMM says that the accesses race.2649 2650There is one more part of the LKMM related to plain accesses (although2651not to data races) we should discuss.  Recall that many relations such2652as hb are limited to marked accesses only.  As a result, the2653happens-before, propagates-before, and rcu axioms (which state that2654various relation must not contain a cycle) doesn't apply to plain2655accesses.  Nevertheless, we do want to rule out such cycles, because2656they don't make sense even for plain accesses.2657 2658To this end, the LKMM imposes three extra restrictions, together2659called the "plain-coherence" axiom because of their resemblance to the2660rules used by the operational model to ensure cache coherence (that2661is, the rules governing the memory subsystem's choice of a store to2662satisfy a load request and its determination of where a store will2663fall in the coherence order):2664 2665	If R and W are race candidates and it is possible to link R to2666	W by one of the xb* sequences listed above, then W ->rfe R is2667	not allowed (i.e., a load cannot read from a store that it2668	executes before, even if one or both is plain).2669 2670	If W and R are race candidates and it is possible to link W to2671	R by one of the vis sequences listed above, then R ->fre W is2672	not allowed (i.e., if a store is visible to a load then the2673	load must read from that store or one coherence-after it).2674 2675	If W and W' are race candidates and it is possible to link W2676	to W' by one of the vis sequences listed above, then W' ->co W2677	is not allowed (i.e., if one store is visible to a second then2678	the second must come after the first in the coherence order).2679 2680This is the extent to which the LKMM deals with plain accesses.2681Perhaps it could say more (for example, plain accesses might2682contribute to the ppo relation), but at the moment it seems that this2683minimal, conservative approach is good enough.2684 2685 2686ODDS AND ENDS2687-------------2688 2689This section covers material that didn't quite fit anywhere in the2690earlier sections.2691 2692The descriptions in this document don't always match the formal2693version of the LKMM exactly.  For example, the actual formal2694definition of the prop relation makes the initial coe or fre part2695optional, and it doesn't require the events linked by the relation to2696be on the same CPU.  These differences are very unimportant; indeed,2697instances where the coe/fre part of prop is missing are of no interest2698because all the other parts (fences and rfe) are already included in2699hb anyway, and where the formal model adds prop into hb, it includes2700an explicit requirement that the events being linked are on the same2701CPU.2702 2703Another minor difference has to do with events that are both memory2704accesses and fences, such as those corresponding to smp_load_acquire()2705calls.  In the formal model, these events aren't actually both reads2706and fences; rather, they are read events with an annotation marking2707them as acquires.  (Or write events annotated as releases, in the case2708smp_store_release().)  The final effect is the same.2709 2710Although we didn't mention it above, the instruction execution2711ordering provided by the smp_rmb() fence doesn't apply to read events2712that are part of a non-value-returning atomic update.  For instance,2713given:2714 2715	atomic_inc(&x);2716	smp_rmb();2717	r1 = READ_ONCE(y);2718 2719it is not guaranteed that the load from y will execute after the2720update to x.  This is because the ARMv8 architecture allows2721non-value-returning atomic operations effectively to be executed off2722the CPU.  Basically, the CPU tells the memory subsystem to increment2723x, and then the increment is carried out by the memory hardware with2724no further involvement from the CPU.  Since the CPU doesn't ever read2725the value of x, there is nothing for the smp_rmb() fence to act on.2726 2727The LKMM defines a few extra synchronization operations in terms of2728things we have already covered.  In particular, rcu_dereference() is2729treated as READ_ONCE() and rcu_assign_pointer() is treated as2730smp_store_release() -- which is basically how the Linux kernel treats2731them.2732 2733Although we said that plain accesses are not linked by the ppo2734relation, they do contribute to it indirectly.  Firstly, when there is2735an address dependency from a marked load R to a plain store W,2736followed by smp_wmb() and then a marked store W', the LKMM creates a2737ppo link from R to W'.  The reasoning behind this is perhaps a little2738shaky, but essentially it says there is no way to generate object code2739for this source code in which W' could execute before R.  Just as with2740pre-bounding by address dependencies, it is possible for the compiler2741to undermine this relation if sufficient care is not taken.2742 2743Secondly, plain accesses can carry dependencies: If a data dependency2744links a marked load R to a store W, and the store is read by a load R'2745from the same thread, then the data loaded by R' depends on the data2746loaded originally by R. Thus, if R' is linked to any access X by a2747dependency, R is also linked to access X by the same dependency, even2748if W' or R' (or both!) are plain.2749 2750There are a few oddball fences which need special treatment:2751smp_mb__before_atomic(), smp_mb__after_atomic(), and2752smp_mb__after_spinlock().  The LKMM uses fence events with special2753annotations for them; they act as strong fences just like smp_mb()2754except for the sets of events that they order.  Instead of ordering2755all po-earlier events against all po-later events, as smp_mb() does,2756they behave as follows:2757 2758	smp_mb__before_atomic() orders all po-earlier events against2759	po-later atomic updates and the events following them;2760 2761	smp_mb__after_atomic() orders po-earlier atomic updates and2762	the events preceding them against all po-later events;2763 2764	smp_mb__after_spinlock() orders po-earlier lock acquisition2765	events and the events preceding them against all po-later2766	events.2767 2768Interestingly, RCU and locking each introduce the possibility of2769deadlock.  When faced with code sequences such as:2770 2771	spin_lock(&s);2772	spin_lock(&s);2773	spin_unlock(&s);2774	spin_unlock(&s);2775 2776or:2777 2778	rcu_read_lock();2779	synchronize_rcu();2780	rcu_read_unlock();2781 2782what does the LKMM have to say?  Answer: It says there are no allowed2783executions at all, which makes sense.  But this can also lead to2784misleading results, because if a piece of code has multiple possible2785executions, some of which deadlock, the model will report only on the2786non-deadlocking executions.  For example:2787 2788	int x, y;2789 2790	P0()2791	{2792		int r0;2793 2794		WRITE_ONCE(x, 1);2795		r0 = READ_ONCE(y);2796	}2797 2798	P1()2799	{2800		rcu_read_lock();2801		if (READ_ONCE(x) > 0) {2802			WRITE_ONCE(y, 36);2803			synchronize_rcu();2804		}2805		rcu_read_unlock();2806	}2807 2808Is it possible to end up with r0 = 36 at the end?  The LKMM will tell2809you it is not, but the model won't mention that this is because P12810will self-deadlock in the executions where it stores 36 in y.2811