![Alan Stern](/assets/img/avatar_default.png)
This patch reorganizes the definition of rb in the Linux Kernel Memory Consistency Model. The relation is now expressed in terms of rcu-fence, which consists of a sequence of gp and rscs links separated by rcu-link links, in which the number of occurrences of gp is >= the number of occurrences of rscs. Arguments similar to those published in http://diy.inria.fr/linux/long.pdf show that rcu-fence behaves like an inter-CPU strong fence. Furthermore, the definition of rb in terms of rcu-fence is highly analogous to the definition of pb in terms of strong-fence, which can help explain why rcu-path expresses a form of temporal ordering. This change should not affect the semantics of the memory model, just its internal organization. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Reviewed-by: Boqun Feng <boqun.feng@gmail.com> Reviewed-by: Andrea Parri <parri.andrea@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-2-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
1897 lines
72 KiB
Plaintext
1897 lines
72 KiB
Plaintext
Explanation of the Linux-Kernel Memory Consistency Model
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
:Author: Alan Stern <stern@rowland.harvard.edu>
|
|
:Created: October 2017
|
|
|
|
.. Contents
|
|
|
|
1. INTRODUCTION
|
|
2. BACKGROUND
|
|
3. A SIMPLE EXAMPLE
|
|
4. A SELECTION OF MEMORY MODELS
|
|
5. ORDERING AND CYCLES
|
|
6. EVENTS
|
|
7. THE PROGRAM ORDER RELATION: po AND po-loc
|
|
8. A WARNING
|
|
9. DEPENDENCY RELATIONS: data, addr, and ctrl
|
|
10. THE READS-FROM RELATION: rf, rfi, and rfe
|
|
11. CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe
|
|
12. THE FROM-READS RELATION: fr, fri, and fre
|
|
13. AN OPERATIONAL MODEL
|
|
14. PROPAGATION ORDER RELATION: cumul-fence
|
|
15. DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL
|
|
16. SEQUENTIAL CONSISTENCY PER VARIABLE
|
|
17. ATOMIC UPDATES: rmw
|
|
18. THE PRESERVED PROGRAM ORDER RELATION: ppo
|
|
19. AND THEN THERE WAS ALPHA
|
|
20. THE HAPPENS-BEFORE RELATION: hb
|
|
21. THE PROPAGATES-BEFORE RELATION: pb
|
|
22. RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
|
|
23. ODDS AND ENDS
|
|
|
|
|
|
|
|
INTRODUCTION
|
|
------------
|
|
|
|
The Linux-kernel memory consistency model (LKMM) is rather complex and
|
|
obscure. This is particularly evident if you read through the
|
|
linux-kernel.bell and linux-kernel.cat files that make up the formal
|
|
version of the model; they are extremely terse and their meanings are
|
|
far from clear.
|
|
|
|
This document describes the ideas underlying the LKMM. It is meant
|
|
for people who want to understand how the model was designed. It does
|
|
not go into the details of the code in the .bell and .cat files;
|
|
rather, it explains in English what the code expresses symbolically.
|
|
|
|
Sections 2 (BACKGROUND) through 5 (ORDERING AND CYCLES) are aimed
|
|
toward beginners; they explain what memory consistency models are and
|
|
the basic notions shared by all such models. People already familiar
|
|
with these concepts can skim or skip over them. Sections 6 (EVENTS)
|
|
through 12 (THE FROM_READS RELATION) describe the fundamental
|
|
relations used in many models. Starting in Section 13 (AN OPERATIONAL
|
|
MODEL), the workings of the LKMM itself are covered.
|
|
|
|
Warning: The code examples in this document are not written in the
|
|
proper format for litmus tests. They don't include a header line, the
|
|
initializations are not enclosed in braces, the global variables are
|
|
not passed by pointers, and they don't have an "exists" clause at the
|
|
end. Converting them to the right format is left as an exercise for
|
|
the reader.
|
|
|
|
|
|
BACKGROUND
|
|
----------
|
|
|
|
A memory consistency model (or just memory model, for short) is
|
|
something which predicts, given a piece of computer code running on a
|
|
particular kind of system, what values may be obtained by the code's
|
|
load instructions. The LKMM makes these predictions for code running
|
|
as part of the Linux kernel.
|
|
|
|
In practice, people tend to use memory models the other way around.
|
|
That is, given a piece of code and a collection of values specified
|
|
for the loads, the model will predict whether it is possible for the
|
|
code to run in such a way that the loads will indeed obtain the
|
|
specified values. Of course, this is just another way of expressing
|
|
the same idea.
|
|
|
|
For code running on a uniprocessor system, the predictions are easy:
|
|
Each load instruction must obtain the value written by the most recent
|
|
store instruction accessing the same location (we ignore complicating
|
|
factors such as DMA and mixed-size accesses.) But on multiprocessor
|
|
systems, with multiple CPUs making concurrent accesses to shared
|
|
memory locations, things aren't so simple.
|
|
|
|
Different architectures have differing memory models, and the Linux
|
|
kernel supports a variety of architectures. The LKMM has to be fairly
|
|
permissive, in the sense that any behavior allowed by one of these
|
|
architectures also has to be allowed by the LKMM.
|
|
|
|
|
|
A SIMPLE EXAMPLE
|
|
----------------
|
|
|
|
Here is a simple example to illustrate the basic concepts. Consider
|
|
some code running as part of a device driver for an input device. The
|
|
driver might contain an interrupt handler which collects data from the
|
|
device, stores it in a buffer, and sets a flag to indicate the buffer
|
|
is full. Running concurrently on a different CPU might be a part of
|
|
the driver code being executed by a process in the midst of a read(2)
|
|
system call. This code tests the flag to see whether the buffer is
|
|
ready, and if it is, copies the data back to userspace. The buffer
|
|
and the flag are memory locations shared between the two CPUs.
|
|
|
|
We can abstract out the important pieces of the driver code as follows
|
|
(the reason for using WRITE_ONCE() and READ_ONCE() instead of simple
|
|
assignment statements is discussed later):
|
|
|
|
int buf = 0, flag = 0;
|
|
|
|
P0()
|
|
{
|
|
WRITE_ONCE(buf, 1);
|
|
WRITE_ONCE(flag, 1);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1;
|
|
int r2 = 0;
|
|
|
|
r1 = READ_ONCE(flag);
|
|
if (r1)
|
|
r2 = READ_ONCE(buf);
|
|
}
|
|
|
|
Here the P0() function represents the interrupt handler running on one
|
|
CPU and P1() represents the read() routine running on another. The
|
|
value 1 stored in buf represents input data collected from the device.
|
|
Thus, P0 stores the data in buf and then sets flag. Meanwhile, P1
|
|
reads flag into the private variable r1, and if it is set, reads the
|
|
data from buf into a second private variable r2 for copying to
|
|
userspace. (Presumably if flag is not set then the driver will wait a
|
|
while and try again.)
|
|
|
|
This pattern of memory accesses, where one CPU stores values to two
|
|
shared memory locations and another CPU loads from those locations in
|
|
the opposite order, is widely known as the "Message Passing" or MP
|
|
pattern. It is typical of memory access patterns in the kernel.
|
|
|
|
Please note that this example code is a simplified abstraction. Real
|
|
buffers are usually larger than a single integer, real device drivers
|
|
usually use sleep and wakeup mechanisms rather than polling for I/O
|
|
completion, and real code generally doesn't bother to copy values into
|
|
private variables before using them. All that is beside the point;
|
|
the idea here is simply to illustrate the overall pattern of memory
|
|
accesses by the CPUs.
|
|
|
|
A memory model will predict what values P1 might obtain for its loads
|
|
from flag and buf, or equivalently, what values r1 and r2 might end up
|
|
with after the code has finished running.
|
|
|
|
Some predictions are trivial. For instance, no sane memory model would
|
|
predict that r1 = 42 or r2 = -7, because neither of those values ever
|
|
gets stored in flag or buf.
|
|
|
|
Some nontrivial predictions are nonetheless quite simple. For
|
|
instance, P1 might run entirely before P0 begins, in which case r1 and
|
|
r2 will both be 0 at the end. Or P0 might run entirely before P1
|
|
begins, in which case r1 and r2 will both be 1.
|
|
|
|
The interesting predictions concern what might happen when the two
|
|
routines run concurrently. One possibility is that P1 runs after P0's
|
|
store to buf but before the store to flag. In this case, r1 and r2
|
|
will again both be 0. (If P1 had been designed to read buf
|
|
unconditionally then we would instead have r1 = 0 and r2 = 1.)
|
|
|
|
However, the most interesting possibility is where r1 = 1 and r2 = 0.
|
|
If this were to occur it would mean the driver contains a bug, because
|
|
incorrect data would get sent to the user: 0 instead of 1. As it
|
|
happens, the LKMM does predict this outcome can occur, and the example
|
|
driver code shown above is indeed buggy.
|
|
|
|
|
|
A SELECTION OF MEMORY MODELS
|
|
----------------------------
|
|
|
|
The first widely cited memory model, and the simplest to understand,
|
|
is Sequential Consistency. According to this model, systems behave as
|
|
if each CPU executed its instructions in order but with unspecified
|
|
timing. In other words, the instructions from the various CPUs get
|
|
interleaved in a nondeterministic way, always according to some single
|
|
global order that agrees with the order of the instructions in the
|
|
program source for each CPU. The model says that the value obtained
|
|
by each load is simply the value written by the most recently executed
|
|
store to the same memory location, from any CPU.
|
|
|
|
For the MP example code shown above, Sequential Consistency predicts
|
|
that the undesired result r1 = 1, r2 = 0 cannot occur. The reasoning
|
|
goes like this:
|
|
|
|
Since r1 = 1, P0 must store 1 to flag before P1 loads 1 from
|
|
it, as loads can obtain values only from earlier stores.
|
|
|
|
P1 loads from flag before loading from buf, since CPUs execute
|
|
their instructions in order.
|
|
|
|
P1 must load 0 from buf before P0 stores 1 to it; otherwise r2
|
|
would be 1 since a load obtains its value from the most recent
|
|
store to the same address.
|
|
|
|
P0 stores 1 to buf before storing 1 to flag, since it executes
|
|
its instructions in order.
|
|
|
|
Since an instruction (in this case, P1's store to flag) cannot
|
|
execute before itself, the specified outcome is impossible.
|
|
|
|
However, real computer hardware almost never follows the Sequential
|
|
Consistency memory model; doing so would rule out too many valuable
|
|
performance optimizations. On ARM and PowerPC architectures, for
|
|
instance, the MP example code really does sometimes yield r1 = 1 and
|
|
r2 = 0.
|
|
|
|
x86 and SPARC follow yet a different memory model: TSO (Total Store
|
|
Ordering). This model predicts that the undesired outcome for the MP
|
|
pattern cannot occur, but in other respects it differs from Sequential
|
|
Consistency. One example is the Store Buffer (SB) pattern, in which
|
|
each CPU stores to its own shared location and then loads from the
|
|
other CPU's location:
|
|
|
|
int x = 0, y = 0;
|
|
|
|
P0()
|
|
{
|
|
int r0;
|
|
|
|
WRITE_ONCE(x, 1);
|
|
r0 = READ_ONCE(y);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1;
|
|
|
|
WRITE_ONCE(y, 1);
|
|
r1 = READ_ONCE(x);
|
|
}
|
|
|
|
Sequential Consistency predicts that the outcome r0 = 0, r1 = 0 is
|
|
impossible. (Exercise: Figure out the reasoning.) But TSO allows
|
|
this outcome to occur, and in fact it does sometimes occur on x86 and
|
|
SPARC systems.
|
|
|
|
The LKMM was inspired by the memory models followed by PowerPC, ARM,
|
|
x86, Alpha, and other architectures. However, it is different in
|
|
detail from each of them.
|
|
|
|
|
|
ORDERING AND CYCLES
|
|
-------------------
|
|
|
|
Memory models are all about ordering. Often this is temporal ordering
|
|
(i.e., the order in which certain events occur) but it doesn't have to
|
|
be; consider for example the order of instructions in a program's
|
|
source code. We saw above that Sequential Consistency makes an
|
|
important assumption that CPUs execute instructions in the same order
|
|
as those instructions occur in the code, and there are many other
|
|
instances of ordering playing central roles in memory models.
|
|
|
|
The counterpart to ordering is a cycle. Ordering rules out cycles:
|
|
It's not possible to have X ordered before Y, Y ordered before Z, and
|
|
Z ordered before X, because this would mean that X is ordered before
|
|
itself. The analysis of the MP example under Sequential Consistency
|
|
involved just such an impossible cycle:
|
|
|
|
W: P0 stores 1 to flag executes before
|
|
X: P1 loads 1 from flag executes before
|
|
Y: P1 loads 0 from buf executes before
|
|
Z: P0 stores 1 to buf executes before
|
|
W: P0 stores 1 to flag.
|
|
|
|
In short, if a memory model requires certain accesses to be ordered,
|
|
and a certain outcome for the loads in a piece of code can happen only
|
|
if those accesses would form a cycle, then the memory model predicts
|
|
that outcome cannot occur.
|
|
|
|
The LKMM is defined largely in terms of cycles, as we will see.
|
|
|
|
|
|
EVENTS
|
|
------
|
|
|
|
The LKMM does not work directly with the C statements that make up
|
|
kernel source code. Instead it considers the effects of those
|
|
statements in a more abstract form, namely, events. The model
|
|
includes three types of events:
|
|
|
|
Read events correspond to loads from shared memory, such as
|
|
calls to READ_ONCE(), smp_load_acquire(), or
|
|
rcu_dereference().
|
|
|
|
Write events correspond to stores to shared memory, such as
|
|
calls to WRITE_ONCE(), smp_store_release(), or atomic_set().
|
|
|
|
Fence events correspond to memory barriers (also known as
|
|
fences), such as calls to smp_rmb() or rcu_read_lock().
|
|
|
|
These categories are not exclusive; a read or write event can also be
|
|
a fence. This happens with functions like smp_load_acquire() or
|
|
spin_lock(). However, no single event can be both a read and a write.
|
|
Atomic read-modify-write accesses, such as atomic_inc() or xchg(),
|
|
correspond to a pair of events: a read followed by a write. (The
|
|
write event is omitted for executions where it doesn't occur, such as
|
|
a cmpxchg() where the comparison fails.)
|
|
|
|
Other parts of the code, those which do not involve interaction with
|
|
shared memory, do not give rise to events. Thus, arithmetic and
|
|
logical computations, control-flow instructions, or accesses to
|
|
private memory or CPU registers are not of central interest to the
|
|
memory model. They only affect the model's predictions indirectly.
|
|
For example, an arithmetic computation might determine the value that
|
|
gets stored to a shared memory location (or in the case of an array
|
|
index, the address where the value gets stored), but the memory model
|
|
is concerned only with the store itself -- its value and its address
|
|
-- not the computation leading up to it.
|
|
|
|
Events in the LKMM can be linked by various relations, which we will
|
|
describe in the following sections. The memory model requires certain
|
|
of these relations to be orderings, that is, it requires them not to
|
|
have any cycles.
|
|
|
|
|
|
THE PROGRAM ORDER RELATION: po AND po-loc
|
|
-----------------------------------------
|
|
|
|
The most important relation between events is program order (po). You
|
|
can think of it as the order in which statements occur in the source
|
|
code after branches are taken into account and loops have been
|
|
unrolled. A better description might be the order in which
|
|
instructions are presented to a CPU's execution unit. Thus, we say
|
|
that X is po-before Y (written as "X ->po Y" in formulas) if X occurs
|
|
before Y in the instruction stream.
|
|
|
|
This is inherently a single-CPU relation; two instructions executing
|
|
on different CPUs are never linked by po. Also, it is by definition
|
|
an ordering so it cannot have any cycles.
|
|
|
|
po-loc is a sub-relation of po. It links two memory accesses when the
|
|
first comes before the second in program order and they access the
|
|
same memory location (the "-loc" suffix).
|
|
|
|
Although this may seem straightforward, there is one subtle aspect to
|
|
program order we need to explain. The LKMM was inspired by low-level
|
|
architectural memory models which describe the behavior of machine
|
|
code, and it retains their outlook to a considerable extent. The
|
|
read, write, and fence events used by the model are close in spirit to
|
|
individual machine instructions. Nevertheless, the LKMM describes
|
|
kernel code written in C, and the mapping from C to machine code can
|
|
be extremely complex.
|
|
|
|
Optimizing compilers have great freedom in the way they translate
|
|
source code to object code. They are allowed to apply transformations
|
|
that add memory accesses, eliminate accesses, combine them, split them
|
|
into pieces, or move them around. Faced with all these possibilities,
|
|
the LKMM basically gives up. It insists that the code it analyzes
|
|
must contain no ordinary accesses to shared memory; all accesses must
|
|
be performed using READ_ONCE(), WRITE_ONCE(), or one of the other
|
|
atomic or synchronization primitives. These primitives prevent a
|
|
large number of compiler optimizations. In particular, it is
|
|
guaranteed that the compiler will not remove such accesses from the
|
|
generated code (unless it can prove the accesses will never be
|
|
executed), it will not change the order in which they occur in the
|
|
code (within limits imposed by the C standard), and it will not
|
|
introduce extraneous accesses.
|
|
|
|
This explains why the MP and SB examples above used READ_ONCE() and
|
|
WRITE_ONCE() rather than ordinary memory accesses. Thanks to this
|
|
usage, we can be certain that in the MP example, P0's write event to
|
|
buf really is po-before its write event to flag, and similarly for the
|
|
other shared memory accesses in the examples.
|
|
|
|
Private variables are not subject to this restriction. Since they are
|
|
not shared between CPUs, they can be accessed normally without
|
|
READ_ONCE() or WRITE_ONCE(), and there will be no ill effects. In
|
|
fact, they need not even be stored in normal memory at all -- in
|
|
principle a private variable could be stored in a CPU register (hence
|
|
the convention that these variables have names starting with the
|
|
letter 'r').
|
|
|
|
|
|
A WARNING
|
|
---------
|
|
|
|
The protections provided by READ_ONCE(), WRITE_ONCE(), and others are
|
|
not perfect; and under some circumstances it is possible for the
|
|
compiler to undermine the memory model. Here is an example. Suppose
|
|
both branches of an "if" statement store the same value to the same
|
|
location:
|
|
|
|
r1 = READ_ONCE(x);
|
|
if (r1) {
|
|
WRITE_ONCE(y, 2);
|
|
... /* do something */
|
|
} else {
|
|
WRITE_ONCE(y, 2);
|
|
... /* do something else */
|
|
}
|
|
|
|
For this code, the LKMM predicts that the load from x will always be
|
|
executed before either of the stores to y. However, a compiler could
|
|
lift the stores out of the conditional, transforming the code into
|
|
something resembling:
|
|
|
|
r1 = READ_ONCE(x);
|
|
WRITE_ONCE(y, 2);
|
|
if (r1) {
|
|
... /* do something */
|
|
} else {
|
|
... /* do something else */
|
|
}
|
|
|
|
Given this version of the code, the LKMM would predict that the load
|
|
from x could be executed after the store to y. Thus, the memory
|
|
model's original prediction could be invalidated by the compiler.
|
|
|
|
Another issue arises from the fact that in C, arguments to many
|
|
operators and function calls can be evaluated in any order. For
|
|
example:
|
|
|
|
r1 = f(5) + g(6);
|
|
|
|
The object code might call f(5) either before or after g(6); the
|
|
memory model cannot assume there is a fixed program order relation
|
|
between them. (In fact, if the functions are inlined then the
|
|
compiler might even interleave their object code.)
|
|
|
|
|
|
DEPENDENCY RELATIONS: data, addr, and ctrl
|
|
------------------------------------------
|
|
|
|
We say that two events are linked by a dependency relation when the
|
|
execution of the second event depends in some way on a value obtained
|
|
from memory by the first. The first event must be a read, and the
|
|
value it obtains must somehow affect what the second event does.
|
|
There are three kinds of dependencies: data, address (addr), and
|
|
control (ctrl).
|
|
|
|
A read and a write event are linked by a data dependency if the value
|
|
obtained by the read affects the value stored by the write. As a very
|
|
simple example:
|
|
|
|
int x, y;
|
|
|
|
r1 = READ_ONCE(x);
|
|
WRITE_ONCE(y, r1 + 5);
|
|
|
|
The value stored by the WRITE_ONCE obviously depends on the value
|
|
loaded by the READ_ONCE. Such dependencies can wind through
|
|
arbitrarily complicated computations, and a write can depend on the
|
|
values of multiple reads.
|
|
|
|
A read event and another memory access event are linked by an address
|
|
dependency if the value obtained by the read affects the location
|
|
accessed by the other event. The second event can be either a read or
|
|
a write. Here's another simple example:
|
|
|
|
int a[20];
|
|
int i;
|
|
|
|
r1 = READ_ONCE(i);
|
|
r2 = READ_ONCE(a[r1]);
|
|
|
|
Here the location accessed by the second READ_ONCE() depends on the
|
|
index value loaded by the first. Pointer indirection also gives rise
|
|
to address dependencies, since the address of a location accessed
|
|
through a pointer will depend on the value read earlier from that
|
|
pointer.
|
|
|
|
Finally, a read event and another memory access event are linked by a
|
|
control dependency if the value obtained by the read affects whether
|
|
the second event is executed at all. Simple example:
|
|
|
|
int x, y;
|
|
|
|
r1 = READ_ONCE(x);
|
|
if (r1)
|
|
WRITE_ONCE(y, 1984);
|
|
|
|
Execution of the WRITE_ONCE() is controlled by a conditional expression
|
|
which depends on the value obtained by the READ_ONCE(); hence there is
|
|
a control dependency from the load to the store.
|
|
|
|
It should be pretty obvious that events can only depend on reads that
|
|
come earlier in program order. Symbolically, if we have R ->data X,
|
|
R ->addr X, or R ->ctrl X (where R is a read event), then we must also
|
|
have R ->po X. It wouldn't make sense for a computation to depend
|
|
somehow on a value that doesn't get loaded from shared memory until
|
|
later in the code!
|
|
|
|
|
|
THE READS-FROM RELATION: rf, rfi, and rfe
|
|
-----------------------------------------
|
|
|
|
The reads-from relation (rf) links a write event to a read event when
|
|
the value loaded by the read is the value that was stored by the
|
|
write. In colloquial terms, the load "reads from" the store. We
|
|
write W ->rf R to indicate that the load R reads from the store W. We
|
|
further distinguish the cases where the load and the store occur on
|
|
the same CPU (internal reads-from, or rfi) and where they occur on
|
|
different CPUs (external reads-from, or rfe).
|
|
|
|
For our purposes, a memory location's initial value is treated as
|
|
though it had been written there by an imaginary initial store that
|
|
executes on a separate CPU before the program runs.
|
|
|
|
Usage of the rf relation implicitly assumes that loads will always
|
|
read from a single store. It doesn't apply properly in the presence
|
|
of load-tearing, where a load obtains some of its bits from one store
|
|
and some of them from another store. Fortunately, use of READ_ONCE()
|
|
and WRITE_ONCE() will prevent load-tearing; it's not possible to have:
|
|
|
|
int x = 0;
|
|
|
|
P0()
|
|
{
|
|
WRITE_ONCE(x, 0x1234);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1;
|
|
|
|
r1 = READ_ONCE(x);
|
|
}
|
|
|
|
and end up with r1 = 0x1200 (partly from x's initial value and partly
|
|
from the value stored by P0).
|
|
|
|
On the other hand, load-tearing is unavoidable when mixed-size
|
|
accesses are used. Consider this example:
|
|
|
|
union {
|
|
u32 w;
|
|
u16 h[2];
|
|
} x;
|
|
|
|
P0()
|
|
{
|
|
WRITE_ONCE(x.h[0], 0x1234);
|
|
WRITE_ONCE(x.h[1], 0x5678);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1;
|
|
|
|
r1 = READ_ONCE(x.w);
|
|
}
|
|
|
|
If r1 = 0x56781234 (little-endian!) at the end, then P1 must have read
|
|
from both of P0's stores. It is possible to handle mixed-size and
|
|
unaligned accesses in a memory model, but the LKMM currently does not
|
|
attempt to do so. It requires all accesses to be properly aligned and
|
|
of the location's actual size.
|
|
|
|
|
|
CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co, coi, and coe
|
|
------------------------------------------------------------------
|
|
|
|
Cache coherence is a general principle requiring that in a
|
|
multi-processor system, the CPUs must share a consistent view of the
|
|
memory contents. Specifically, it requires that for each location in
|
|
shared memory, the stores to that location must form a single global
|
|
ordering which all the CPUs agree on (the coherence order), and this
|
|
ordering must be consistent with the program order for accesses to
|
|
that location.
|
|
|
|
To put it another way, for any variable x, the coherence order (co) of
|
|
the stores to x is simply the order in which the stores overwrite one
|
|
another. The imaginary store which establishes x's initial value
|
|
comes first in the coherence order; the store which directly
|
|
overwrites the initial value comes second; the store which overwrites
|
|
that value comes third, and so on.
|
|
|
|
You can think of the coherence order as being the order in which the
|
|
stores reach x's location in memory (or if you prefer a more
|
|
hardware-centric view, the order in which the stores get written to
|
|
x's cache line). We write W ->co W' if W comes before W' in the
|
|
coherence order, that is, if the value stored by W gets overwritten,
|
|
directly or indirectly, by the value stored by W'.
|
|
|
|
Coherence order is required to be consistent with program order. This
|
|
requirement takes the form of four coherency rules:
|
|
|
|
Write-write coherence: If W ->po-loc W' (i.e., W comes before
|
|
W' in program order and they access the same location), where W
|
|
and W' are two stores, then W ->co W'.
|
|
|
|
Write-read coherence: If W ->po-loc R, where W is a store and R
|
|
is a load, then R must read from W or from some other store
|
|
which comes after W in the coherence order.
|
|
|
|
Read-write coherence: If R ->po-loc W, where R is a load and W
|
|
is a store, then the store which R reads from must come before
|
|
W in the coherence order.
|
|
|
|
Read-read coherence: If R ->po-loc R', where R and R' are two
|
|
loads, then either they read from the same store or else the
|
|
store read by R comes before the store read by R' in the
|
|
coherence order.
|
|
|
|
This is sometimes referred to as sequential consistency per variable,
|
|
because it means that the accesses to any single memory location obey
|
|
the rules of the Sequential Consistency memory model. (According to
|
|
Wikipedia, sequential consistency per variable and cache coherence
|
|
mean the same thing except that cache coherence includes an extra
|
|
requirement that every store eventually becomes visible to every CPU.)
|
|
|
|
Any reasonable memory model will include cache coherence. Indeed, our
|
|
expectation of cache coherence is so deeply ingrained that violations
|
|
of its requirements look more like hardware bugs than programming
|
|
errors:
|
|
|
|
int x;
|
|
|
|
P0()
|
|
{
|
|
WRITE_ONCE(x, 17);
|
|
WRITE_ONCE(x, 23);
|
|
}
|
|
|
|
If the final value stored in x after this code ran was 17, you would
|
|
think your computer was broken. It would be a violation of the
|
|
write-write coherence rule: Since the store of 23 comes later in
|
|
program order, it must also come later in x's coherence order and
|
|
thus must overwrite the store of 17.
|
|
|
|
int x = 0;
|
|
|
|
P0()
|
|
{
|
|
int r1;
|
|
|
|
r1 = READ_ONCE(x);
|
|
WRITE_ONCE(x, 666);
|
|
}
|
|
|
|
If r1 = 666 at the end, this would violate the read-write coherence
|
|
rule: The READ_ONCE() load comes before the WRITE_ONCE() store in
|
|
program order, so it must not read from that store but rather from one
|
|
coming earlier in the coherence order (in this case, x's initial
|
|
value).
|
|
|
|
int x = 0;
|
|
|
|
P0()
|
|
{
|
|
WRITE_ONCE(x, 5);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1, r2;
|
|
|
|
r1 = READ_ONCE(x);
|
|
r2 = READ_ONCE(x);
|
|
}
|
|
|
|
If r1 = 5 (reading from P0's store) and r2 = 0 (reading from the
|
|
imaginary store which establishes x's initial value) at the end, this
|
|
would violate the read-read coherence rule: The r1 load comes before
|
|
the r2 load in program order, so it must not read from a store that
|
|
comes later in the coherence order.
|
|
|
|
(As a minor curiosity, if this code had used normal loads instead of
|
|
READ_ONCE() in P1, on Itanium it sometimes could end up with r1 = 5
|
|
and r2 = 0! This results from parallel execution of the operations
|
|
encoded in Itanium's Very-Long-Instruction-Word format, and it is yet
|
|
another motivation for using READ_ONCE() when accessing shared memory
|
|
locations.)
|
|
|
|
Just like the po relation, co is inherently an ordering -- it is not
|
|
possible for a store to directly or indirectly overwrite itself! And
|
|
just like with the rf relation, we distinguish between stores that
|
|
occur on the same CPU (internal coherence order, or coi) and stores
|
|
that occur on different CPUs (external coherence order, or coe).
|
|
|
|
On the other hand, stores to different memory locations are never
|
|
related by co, just as instructions on different CPUs are never
|
|
related by po. Coherence order is strictly per-location, or if you
|
|
prefer, each location has its own independent coherence order.
|
|
|
|
|
|
THE FROM-READS RELATION: fr, fri, and fre
|
|
-----------------------------------------
|
|
|
|
The from-reads relation (fr) can be a little difficult for people to
|
|
grok. It describes the situation where a load reads a value that gets
|
|
overwritten by a store. In other words, we have R ->fr W when the
|
|
value that R reads is overwritten (directly or indirectly) by W, or
|
|
equivalently, when R reads from a store which comes earlier than W in
|
|
the coherence order.
|
|
|
|
For example:
|
|
|
|
int x = 0;
|
|
|
|
P0()
|
|
{
|
|
int r1;
|
|
|
|
r1 = READ_ONCE(x);
|
|
WRITE_ONCE(x, 2);
|
|
}
|
|
|
|
The value loaded from x will be 0 (assuming cache coherence!), and it
|
|
gets overwritten by the value 2. Thus there is an fr link from the
|
|
READ_ONCE() to the WRITE_ONCE(). If the code contained any later
|
|
stores to x, there would also be fr links from the READ_ONCE() to
|
|
them.
|
|
|
|
As with rf, rfi, and rfe, we subdivide the fr relation into fri (when
|
|
the load and the store are on the same CPU) and fre (when they are on
|
|
different CPUs).
|
|
|
|
Note that the fr relation is determined entirely by the rf and co
|
|
relations; it is not independent. Given a read event R and a write
|
|
event W for the same location, we will have R ->fr W if and only if
|
|
the write which R reads from is co-before W. In symbols,
|
|
|
|
(R ->fr W) := (there exists W' with W' ->rf R and W' ->co W).
|
|
|
|
|
|
AN OPERATIONAL MODEL
|
|
--------------------
|
|
|
|
The LKMM is based on various operational memory models, meaning that
|
|
the models arise from an abstract view of how a computer system
|
|
operates. Here are the main ideas, as incorporated into the LKMM.
|
|
|
|
The system as a whole is divided into the CPUs and a memory subsystem.
|
|
The CPUs are responsible for executing instructions (not necessarily
|
|
in program order), and they communicate with the memory subsystem.
|
|
For the most part, executing an instruction requires a CPU to perform
|
|
only internal operations. However, loads, stores, and fences involve
|
|
more.
|
|
|
|
When CPU C executes a store instruction, it tells the memory subsystem
|
|
to store a certain value at a certain location. The memory subsystem
|
|
propagates the store to all the other CPUs as well as to RAM. (As a
|
|
special case, we say that the store propagates to its own CPU at the
|
|
time it is executed.) The memory subsystem also determines where the
|
|
store falls in the location's coherence order. In particular, it must
|
|
arrange for the store to be co-later than (i.e., to overwrite) any
|
|
other store to the same location which has already propagated to CPU C.
|
|
|
|
When a CPU executes a load instruction R, it first checks to see
|
|
whether there are any as-yet unexecuted store instructions, for the
|
|
same location, that come before R in program order. If there are, it
|
|
uses the value of the po-latest such store as the value obtained by R,
|
|
and we say that the store's value is forwarded to R. Otherwise, the
|
|
CPU asks the memory subsystem for the value to load and we say that R
|
|
is satisfied from memory. The memory subsystem hands back the value
|
|
of the co-latest store to the location in question which has already
|
|
propagated to that CPU.
|
|
|
|
(In fact, the picture needs to be a little more complicated than this.
|
|
CPUs have local caches, and propagating a store to a CPU really means
|
|
propagating it to the CPU's local cache. A local cache can take some
|
|
time to process the stores that it receives, and a store can't be used
|
|
to satisfy one of the CPU's loads until it has been processed. On
|
|
most architectures, the local caches process stores in
|
|
First-In-First-Out order, and consequently the processing delay
|
|
doesn't matter for the memory model. But on Alpha, the local caches
|
|
have a partitioned design that results in non-FIFO behavior. We will
|
|
discuss this in more detail later.)
|
|
|
|
Note that load instructions may be executed speculatively and may be
|
|
restarted under certain circumstances. The memory model ignores these
|
|
premature executions; we simply say that the load executes at the
|
|
final time it is forwarded or satisfied.
|
|
|
|
Executing a fence (or memory barrier) instruction doesn't require a
|
|
CPU to do anything special other than informing the memory subsystem
|
|
about the fence. However, fences do constrain the way CPUs and the
|
|
memory subsystem handle other instructions, in two respects.
|
|
|
|
First, a fence forces the CPU to execute various instructions in
|
|
program order. Exactly which instructions are ordered depends on the
|
|
type of fence:
|
|
|
|
Strong fences, including smp_mb() and synchronize_rcu(), force
|
|
the CPU to execute all po-earlier instructions before any
|
|
po-later instructions;
|
|
|
|
smp_rmb() forces the CPU to execute all po-earlier loads
|
|
before any po-later loads;
|
|
|
|
smp_wmb() forces the CPU to execute all po-earlier stores
|
|
before any po-later stores;
|
|
|
|
Acquire fences, such as smp_load_acquire(), force the CPU to
|
|
execute the load associated with the fence (e.g., the load
|
|
part of an smp_load_acquire()) before any po-later
|
|
instructions;
|
|
|
|
Release fences, such as smp_store_release(), force the CPU to
|
|
execute all po-earlier instructions before the store
|
|
associated with the fence (e.g., the store part of an
|
|
smp_store_release()).
|
|
|
|
Second, some types of fence affect the way the memory subsystem
|
|
propagates stores. When a fence instruction is executed on CPU C:
|
|
|
|
For each other CPU C', smb_wmb() forces all po-earlier stores
|
|
on C to propagate to C' before any po-later stores do.
|
|
|
|
For each other CPU C', any store which propagates to C before
|
|
a release fence is executed (including all po-earlier
|
|
stores executed on C) is forced to propagate to C' before the
|
|
store associated with the release fence does.
|
|
|
|
Any store which propagates to C before a strong fence is
|
|
executed (including all po-earlier stores on C) is forced to
|
|
propagate to all other CPUs before any instructions po-after
|
|
the strong fence are executed on C.
|
|
|
|
The propagation ordering enforced by release fences and strong fences
|
|
affects stores from other CPUs that propagate to CPU C before the
|
|
fence is executed, as well as stores that are executed on C before the
|
|
fence. We describe this property by saying that release fences and
|
|
strong fences are A-cumulative. By contrast, smp_wmb() fences are not
|
|
A-cumulative; they only affect the propagation of stores that are
|
|
executed on C before the fence (i.e., those which precede the fence in
|
|
program order).
|
|
|
|
rcu_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
|
|
other properties which we discuss later.
|
|
|
|
|
|
PROPAGATION ORDER RELATION: cumul-fence
|
|
---------------------------------------
|
|
|
|
The fences which affect propagation order (i.e., strong, release, and
|
|
smp_wmb() fences) are collectively referred to as cumul-fences, even
|
|
though smp_wmb() isn't A-cumulative. The cumul-fence relation is
|
|
defined to link memory access events E and F whenever:
|
|
|
|
E and F are both stores on the same CPU and an smp_wmb() fence
|
|
event occurs between them in program order; or
|
|
|
|
F is a release fence and some X comes before F in program order,
|
|
where either X = E or else E ->rf X; or
|
|
|
|
A strong fence event occurs between some X and F in program
|
|
order, where either X = E or else E ->rf X.
|
|
|
|
The operational model requires that whenever W and W' are both stores
|
|
and W ->cumul-fence W', then W must propagate to any given CPU
|
|
before W' does. However, for different CPUs C and C', it does not
|
|
require W to propagate to C before W' propagates to C'.
|
|
|
|
|
|
DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL
|
|
-------------------------------------------------
|
|
|
|
The LKMM is derived from the restrictions imposed by the design
|
|
outlined above. These restrictions involve the necessity of
|
|
maintaining cache coherence and the fact that a CPU can't operate on a
|
|
value before it knows what that value is, among other things.
|
|
|
|
The formal version of the LKMM is defined by five requirements, or
|
|
axioms:
|
|
|
|
Sequential consistency per variable: This requires that the
|
|
system obey the four coherency rules.
|
|
|
|
Atomicity: This requires that atomic read-modify-write
|
|
operations really are atomic, that is, no other stores can
|
|
sneak into the middle of such an update.
|
|
|
|
Happens-before: This requires that certain instructions are
|
|
executed in a specific order.
|
|
|
|
Propagation: This requires that certain stores propagate to
|
|
CPUs and to RAM in a specific order.
|
|
|
|
Rcu: This requires that RCU read-side critical sections and
|
|
grace periods obey the rules of RCU, in particular, the
|
|
Grace-Period Guarantee.
|
|
|
|
The first and second are quite common; they can be found in many
|
|
memory models (such as those for C11/C++11). The "happens-before" and
|
|
"propagation" axioms have analogs in other memory models as well. The
|
|
"rcu" axiom is specific to the LKMM.
|
|
|
|
Each of these axioms is discussed below.
|
|
|
|
|
|
SEQUENTIAL CONSISTENCY PER VARIABLE
|
|
-----------------------------------
|
|
|
|
According to the principle of cache coherence, the stores to any fixed
|
|
shared location in memory form a global ordering. We can imagine
|
|
inserting the loads from that location into this ordering, by placing
|
|
each load between the store that it reads from and the following
|
|
store. This leaves the relative positions of loads that read from the
|
|
same store unspecified; let's say they are inserted in program order,
|
|
first for CPU 0, then CPU 1, etc.
|
|
|
|
You can check that the four coherency rules imply that the rf, co, fr,
|
|
and po-loc relations agree with this global ordering; in other words,
|
|
whenever we have X ->rf Y or X ->co Y or X ->fr Y or X ->po-loc Y, the
|
|
X event comes before the Y event in the global ordering. The LKMM's
|
|
"coherence" axiom expresses this by requiring the union of these
|
|
relations not to have any cycles. This means it must not be possible
|
|
to find events
|
|
|
|
X0 -> X1 -> X2 -> ... -> Xn -> X0,
|
|
|
|
where each of the links is either rf, co, fr, or po-loc. This has to
|
|
hold if the accesses to the fixed memory location can be ordered as
|
|
cache coherence demands.
|
|
|
|
Although it is not obvious, it can be shown that the converse is also
|
|
true: This LKMM axiom implies that the four coherency rules are
|
|
obeyed.
|
|
|
|
|
|
ATOMIC UPDATES: rmw
|
|
-------------------
|
|
|
|
What does it mean to say that a read-modify-write (rmw) update, such
|
|
as atomic_inc(&x), is atomic? It means that the memory location (x in
|
|
this case) does not get altered between the read and the write events
|
|
making up the atomic operation. In particular, if two CPUs perform
|
|
atomic_inc(&x) concurrently, it must be guaranteed that the final
|
|
value of x will be the initial value plus two. We should never have
|
|
the following sequence of events:
|
|
|
|
CPU 0 loads x obtaining 13;
|
|
CPU 1 loads x obtaining 13;
|
|
CPU 0 stores 14 to x;
|
|
CPU 1 stores 14 to x;
|
|
|
|
where the final value of x is wrong (14 rather than 15).
|
|
|
|
In this example, CPU 0's increment effectively gets lost because it
|
|
occurs in between CPU 1's load and store. To put it another way, the
|
|
problem is that the position of CPU 0's store in x's coherence order
|
|
is between the store that CPU 1 reads from and the store that CPU 1
|
|
performs.
|
|
|
|
The same analysis applies to all atomic update operations. Therefore,
|
|
to enforce atomicity the LKMM requires that atomic updates follow this
|
|
rule: Whenever R and W are the read and write events composing an
|
|
atomic read-modify-write and W' is the write event which R reads from,
|
|
there must not be any stores coming between W' and W in the coherence
|
|
order. Equivalently,
|
|
|
|
(R ->rmw W) implies (there is no X with R ->fr X and X ->co W),
|
|
|
|
where the rmw relation links the read and write events making up each
|
|
atomic update. This is what the LKMM's "atomic" axiom says.
|
|
|
|
|
|
THE PRESERVED PROGRAM ORDER RELATION: ppo
|
|
-----------------------------------------
|
|
|
|
There are many situations where a CPU is obligated to execute two
|
|
instructions in program order. We amalgamate them into the ppo (for
|
|
"preserved program order") relation, which links the po-earlier
|
|
instruction to the po-later instruction and is thus a sub-relation of
|
|
po.
|
|
|
|
The operational model already includes a description of one such
|
|
situation: Fences are a source of ppo links. Suppose X and Y are
|
|
memory accesses with X ->po Y; then the CPU must execute X before Y if
|
|
any of the following hold:
|
|
|
|
A strong (smp_mb() or synchronize_rcu()) fence occurs between
|
|
X and Y;
|
|
|
|
X and Y are both stores and an smp_wmb() fence occurs between
|
|
them;
|
|
|
|
X and Y are both loads and an smp_rmb() fence occurs between
|
|
them;
|
|
|
|
X is also an acquire fence, such as smp_load_acquire();
|
|
|
|
Y is also a release fence, such as smp_store_release().
|
|
|
|
Another possibility, not mentioned earlier but discussed in the next
|
|
section, is:
|
|
|
|
X and Y are both loads, X ->addr Y (i.e., there is an address
|
|
dependency from X to Y), and X is a READ_ONCE() or an atomic
|
|
access.
|
|
|
|
Dependencies can also cause instructions to be executed in program
|
|
order. This is uncontroversial when the second instruction is a
|
|
store; either a data, address, or control dependency from a load R to
|
|
a store W will force the CPU to execute R before W. This is very
|
|
simply because the CPU cannot tell the memory subsystem about W's
|
|
store before it knows what value should be stored (in the case of a
|
|
data dependency), what location it should be stored into (in the case
|
|
of an address dependency), or whether the store should actually take
|
|
place (in the case of a control dependency).
|
|
|
|
Dependencies to load instructions are more problematic. To begin with,
|
|
there is no such thing as a data dependency to a load. Next, a CPU
|
|
has no reason to respect a control dependency to a load, because it
|
|
can always satisfy the second load speculatively before the first, and
|
|
then ignore the result if it turns out that the second load shouldn't
|
|
be executed after all. And lastly, the real difficulties begin when
|
|
we consider address dependencies to loads.
|
|
|
|
To be fair about it, all Linux-supported architectures do execute
|
|
loads in program order if there is an address dependency between them.
|
|
After all, a CPU cannot ask the memory subsystem to load a value from
|
|
a particular location before it knows what that location is. However,
|
|
the split-cache design used by Alpha can cause it to behave in a way
|
|
that looks as if the loads were executed out of order (see the next
|
|
section for more details). The kernel includes a workaround for this
|
|
problem when the loads come from READ_ONCE(), and therefore the LKMM
|
|
includes address dependencies to loads in the ppo relation.
|
|
|
|
On the other hand, dependencies can indirectly affect the ordering of
|
|
two loads. This happens when there is a dependency from a load to a
|
|
store and a second, po-later load reads from that store:
|
|
|
|
R ->dep W ->rfi R',
|
|
|
|
where the dep link can be either an address or a data dependency. In
|
|
this situation we know it is possible for the CPU to execute R' before
|
|
W, because it can forward the value that W will store to R'. But it
|
|
cannot execute R' before R, because it cannot forward the value before
|
|
it knows what that value is, or that W and R' do access the same
|
|
location. However, if there is merely a control dependency between R
|
|
and W then the CPU can speculatively forward W to R' before executing
|
|
R; if the speculation turns out to be wrong then the CPU merely has to
|
|
restart or abandon R'.
|
|
|
|
(In theory, a CPU might forward a store to a load when it runs across
|
|
an address dependency like this:
|
|
|
|
r1 = READ_ONCE(ptr);
|
|
WRITE_ONCE(*r1, 17);
|
|
r2 = READ_ONCE(*r1);
|
|
|
|
because it could tell that the store and the second load access the
|
|
same location even before it knows what the location's address is.
|
|
However, none of the architectures supported by the Linux kernel do
|
|
this.)
|
|
|
|
Two memory accesses of the same location must always be executed in
|
|
program order if the second access is a store. Thus, if we have
|
|
|
|
R ->po-loc W
|
|
|
|
(the po-loc link says that R comes before W in program order and they
|
|
access the same location), the CPU is obliged to execute W after R.
|
|
If it executed W first then the memory subsystem would respond to R's
|
|
read request with the value stored by W (or an even later store), in
|
|
violation of the read-write coherence rule. Similarly, if we had
|
|
|
|
W ->po-loc W'
|
|
|
|
and the CPU executed W' before W, then the memory subsystem would put
|
|
W' before W in the coherence order. It would effectively cause W to
|
|
overwrite W', in violation of the write-write coherence rule.
|
|
(Interestingly, an early ARMv8 memory model, now obsolete, proposed
|
|
allowing out-of-order writes like this to occur. The model avoided
|
|
violating the write-write coherence rule by requiring the CPU not to
|
|
send the W write to the memory subsystem at all!)
|
|
|
|
There is one last example of preserved program order in the LKMM: when
|
|
a load-acquire reads from an earlier store-release. For example:
|
|
|
|
smp_store_release(&x, 123);
|
|
r1 = smp_load_acquire(&x);
|
|
|
|
If the smp_load_acquire() ends up obtaining the 123 value that was
|
|
stored by the smp_store_release(), the LKMM says that the load must be
|
|
executed after the store; the store cannot be forwarded to the load.
|
|
This requirement does not arise from the operational model, but it
|
|
yields correct predictions on all architectures supported by the Linux
|
|
kernel, although for differing reasons.
|
|
|
|
On some architectures, including x86 and ARMv8, it is true that the
|
|
store cannot be forwarded to the load. On others, including PowerPC
|
|
and ARMv7, smp_store_release() generates object code that starts with
|
|
a fence and smp_load_acquire() generates object code that ends with a
|
|
fence. The upshot is that even though the store may be forwarded to
|
|
the load, it is still true that any instruction preceding the store
|
|
will be executed before the load or any following instructions, and
|
|
the store will be executed before any instruction following the load.
|
|
|
|
|
|
AND THEN THERE WAS ALPHA
|
|
------------------------
|
|
|
|
As mentioned above, the Alpha architecture is unique in that it does
|
|
not appear to respect address dependencies to loads. This means that
|
|
code such as the following:
|
|
|
|
int x = 0;
|
|
int y = -1;
|
|
int *ptr = &y;
|
|
|
|
P0()
|
|
{
|
|
WRITE_ONCE(x, 1);
|
|
smp_wmb();
|
|
WRITE_ONCE(ptr, &x);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int *r1;
|
|
int r2;
|
|
|
|
r1 = ptr;
|
|
r2 = READ_ONCE(*r1);
|
|
}
|
|
|
|
can malfunction on Alpha systems (notice that P1 uses an ordinary load
|
|
to read ptr instead of READ_ONCE()). It is quite possible that r1 = &x
|
|
and r2 = 0 at the end, in spite of the address dependency.
|
|
|
|
At first glance this doesn't seem to make sense. We know that the
|
|
smp_wmb() forces P0's store to x to propagate to P1 before the store
|
|
to ptr does. And since P1 can't execute its second load
|
|
until it knows what location to load from, i.e., after executing its
|
|
first load, the value x = 1 must have propagated to P1 before the
|
|
second load executed. So why doesn't r2 end up equal to 1?
|
|
|
|
The answer lies in the Alpha's split local caches. Although the two
|
|
stores do reach P1's local cache in the proper order, it can happen
|
|
that the first store is processed by a busy part of the cache while
|
|
the second store is processed by an idle part. As a result, the x = 1
|
|
value may not become available for P1's CPU to read until after the
|
|
ptr = &x value does, leading to the undesirable result above. The
|
|
final effect is that even though the two loads really are executed in
|
|
program order, it appears that they aren't.
|
|
|
|
This could not have happened if the local cache had processed the
|
|
incoming stores in FIFO order. By contrast, other architectures
|
|
maintain at least the appearance of FIFO order.
|
|
|
|
In practice, this difficulty is solved by inserting a special fence
|
|
between P1's two loads when the kernel is compiled for the Alpha
|
|
architecture. In fact, as of version 4.15, the kernel automatically
|
|
adds this fence (called smp_read_barrier_depends() and defined as
|
|
nothing at all on non-Alpha builds) after every READ_ONCE() and atomic
|
|
load. The effect of the fence is to cause the CPU not to execute any
|
|
po-later instructions until after the local cache has finished
|
|
processing all the stores it has already received. Thus, if the code
|
|
was changed to:
|
|
|
|
P1()
|
|
{
|
|
int *r1;
|
|
int r2;
|
|
|
|
r1 = READ_ONCE(ptr);
|
|
r2 = READ_ONCE(*r1);
|
|
}
|
|
|
|
then we would never get r1 = &x and r2 = 0. By the time P1 executed
|
|
its second load, the x = 1 store would already be fully processed by
|
|
the local cache and available for satisfying the read request. Thus
|
|
we have yet another reason why shared data should always be read with
|
|
READ_ONCE() or another synchronization primitive rather than accessed
|
|
directly.
|
|
|
|
The LKMM requires that smp_rmb(), acquire fences, and strong fences
|
|
share this property with smp_read_barrier_depends(): They do not allow
|
|
the CPU to execute any po-later instructions (or po-later loads in the
|
|
case of smp_rmb()) until all outstanding stores have been processed by
|
|
the local cache. In the case of a strong fence, the CPU first has to
|
|
wait for all of its po-earlier stores to propagate to every other CPU
|
|
in the system; then it has to wait for the local cache to process all
|
|
the stores received as of that time -- not just the stores received
|
|
when the strong fence began.
|
|
|
|
And of course, none of this matters for any architecture other than
|
|
Alpha.
|
|
|
|
|
|
THE HAPPENS-BEFORE RELATION: hb
|
|
-------------------------------
|
|
|
|
The happens-before relation (hb) links memory accesses that have to
|
|
execute in a certain order. hb includes the ppo relation and two
|
|
others, one of which is rfe.
|
|
|
|
W ->rfe R implies that W and R are on different CPUs. It also means
|
|
that W's store must have propagated to R's CPU before R executed;
|
|
otherwise R could not have read the value stored by W. Therefore W
|
|
must have executed before R, and so we have W ->hb R.
|
|
|
|
The equivalent fact need not hold if W ->rfi R (i.e., W and R are on
|
|
the same CPU). As we have already seen, the operational model allows
|
|
W's value to be forwarded to R in such cases, meaning that R may well
|
|
execute before W does.
|
|
|
|
It's important to understand that neither coe nor fre is included in
|
|
hb, despite their similarities to rfe. For example, suppose we have
|
|
W ->coe W'. This means that W and W' are stores to the same location,
|
|
they execute on different CPUs, and W comes before W' in the coherence
|
|
order (i.e., W' overwrites W). Nevertheless, it is possible for W' to
|
|
execute before W, because the decision as to which store overwrites
|
|
the other is made later by the memory subsystem. When the stores are
|
|
nearly simultaneous, either one can come out on top. Similarly,
|
|
R ->fre W means that W overwrites the value which R reads, but it
|
|
doesn't mean that W has to execute after R. All that's necessary is
|
|
for the memory subsystem not to propagate W to R's CPU until after R
|
|
has executed, which is possible if W executes shortly before R.
|
|
|
|
The third relation included in hb is like ppo, in that it only links
|
|
events that are on the same CPU. However it is more difficult to
|
|
explain, because it arises only indirectly from the requirement of
|
|
cache coherence. The relation is called prop, and it links two events
|
|
on CPU C in situations where a store from some other CPU comes after
|
|
the first event in the coherence order and propagates to C before the
|
|
second event executes.
|
|
|
|
This is best explained with some examples. The simplest case looks
|
|
like this:
|
|
|
|
int x;
|
|
|
|
P0()
|
|
{
|
|
int r1;
|
|
|
|
WRITE_ONCE(x, 1);
|
|
r1 = READ_ONCE(x);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
WRITE_ONCE(x, 8);
|
|
}
|
|
|
|
If r1 = 8 at the end then P0's accesses must have executed in program
|
|
order. We can deduce this from the operational model; if P0's load
|
|
had executed before its store then the value of the store would have
|
|
been forwarded to the load, so r1 would have ended up equal to 1, not
|
|
8. In this case there is a prop link from P0's write event to its read
|
|
event, because P1's store came after P0's store in x's coherence
|
|
order, and P1's store propagated to P0 before P0's load executed.
|
|
|
|
An equally simple case involves two loads of the same location that
|
|
read from different stores:
|
|
|
|
int x = 0;
|
|
|
|
P0()
|
|
{
|
|
int r1, r2;
|
|
|
|
r1 = READ_ONCE(x);
|
|
r2 = READ_ONCE(x);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
WRITE_ONCE(x, 9);
|
|
}
|
|
|
|
If r1 = 0 and r2 = 9 at the end then P0's accesses must have executed
|
|
in program order. If the second load had executed before the first
|
|
then the x = 9 store must have been propagated to P0 before the first
|
|
load executed, and so r1 would have been 9 rather than 0. In this
|
|
case there is a prop link from P0's first read event to its second,
|
|
because P1's store overwrote the value read by P0's first load, and
|
|
P1's store propagated to P0 before P0's second load executed.
|
|
|
|
Less trivial examples of prop all involve fences. Unlike the simple
|
|
examples above, they can require that some instructions are executed
|
|
out of program order. This next one should look familiar:
|
|
|
|
int buf = 0, flag = 0;
|
|
|
|
P0()
|
|
{
|
|
WRITE_ONCE(buf, 1);
|
|
smp_wmb();
|
|
WRITE_ONCE(flag, 1);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1;
|
|
int r2;
|
|
|
|
r1 = READ_ONCE(flag);
|
|
r2 = READ_ONCE(buf);
|
|
}
|
|
|
|
This is the MP pattern again, with an smp_wmb() fence between the two
|
|
stores. If r1 = 1 and r2 = 0 at the end then there is a prop link
|
|
from P1's second load to its first (backwards!). The reason is
|
|
similar to the previous examples: The value P1 loads from buf gets
|
|
overwritten by P0's store to buf, the fence guarantees that the store
|
|
to buf will propagate to P1 before the store to flag does, and the
|
|
store to flag propagates to P1 before P1 reads flag.
|
|
|
|
The prop link says that in order to obtain the r1 = 1, r2 = 0 result,
|
|
P1 must execute its second load before the first. Indeed, if the load
|
|
from flag were executed first, then the buf = 1 store would already
|
|
have propagated to P1 by the time P1's load from buf executed, so r2
|
|
would have been 1 at the end, not 0. (The reasoning holds even for
|
|
Alpha, although the details are more complicated and we will not go
|
|
into them.)
|
|
|
|
But what if we put an smp_rmb() fence between P1's loads? The fence
|
|
would force the two loads to be executed in program order, and it
|
|
would generate a cycle in the hb relation: The fence would create a ppo
|
|
link (hence an hb link) from the first load to the second, and the
|
|
prop relation would give an hb link from the second load to the first.
|
|
Since an instruction can't execute before itself, we are forced to
|
|
conclude that if an smp_rmb() fence is added, the r1 = 1, r2 = 0
|
|
outcome is impossible -- as it should be.
|
|
|
|
The formal definition of the prop relation involves a coe or fre link,
|
|
followed by an arbitrary number of cumul-fence links, ending with an
|
|
rfe link. You can concoct more exotic examples, containing more than
|
|
one fence, although this quickly leads to diminishing returns in terms
|
|
of complexity. For instance, here's an example containing a coe link
|
|
followed by two fences and an rfe link, utilizing the fact that
|
|
release fences are A-cumulative:
|
|
|
|
int x, y, z;
|
|
|
|
P0()
|
|
{
|
|
int r0;
|
|
|
|
WRITE_ONCE(x, 1);
|
|
r0 = READ_ONCE(z);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
WRITE_ONCE(x, 2);
|
|
smp_wmb();
|
|
WRITE_ONCE(y, 1);
|
|
}
|
|
|
|
P2()
|
|
{
|
|
int r2;
|
|
|
|
r2 = READ_ONCE(y);
|
|
smp_store_release(&z, 1);
|
|
}
|
|
|
|
If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
|
|
link from P0's store to its load. This is because P0's store gets
|
|
overwritten by P1's store since x = 2 at the end (a coe link), the
|
|
smp_wmb() ensures that P1's store to x propagates to P2 before the
|
|
store to y does (the first fence), the store to y propagates to P2
|
|
before P2's load and store execute, P2's smp_store_release()
|
|
guarantees that the stores to x and y both propagate to P0 before the
|
|
store to z does (the second fence), and P0's load executes after the
|
|
store to z has propagated to P0 (an rfe link).
|
|
|
|
In summary, the fact that the hb relation links memory access events
|
|
in the order they execute means that it must not have cycles. This
|
|
requirement is the content of the LKMM's "happens-before" axiom.
|
|
|
|
The LKMM defines yet another relation connected to times of
|
|
instruction execution, but it is not included in hb. It relies on the
|
|
particular properties of strong fences, which we cover in the next
|
|
section.
|
|
|
|
|
|
THE PROPAGATES-BEFORE RELATION: pb
|
|
----------------------------------
|
|
|
|
The propagates-before (pb) relation capitalizes on the special
|
|
features of strong fences. It links two events E and F whenever some
|
|
store is coherence-later than E and propagates to every CPU and to RAM
|
|
before F executes. The formal definition requires that E be linked to
|
|
F via a coe or fre link, an arbitrary number of cumul-fences, an
|
|
optional rfe link, a strong fence, and an arbitrary number of hb
|
|
links. Let's see how this definition works out.
|
|
|
|
Consider first the case where E is a store (implying that the sequence
|
|
of links begins with coe). Then there are events W, X, Y, and Z such
|
|
that:
|
|
|
|
E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F,
|
|
|
|
where the * suffix indicates an arbitrary number of links of the
|
|
specified type, and the ? suffix indicates the link is optional (Y may
|
|
be equal to X). Because of the cumul-fence links, we know that W will
|
|
propagate to Y's CPU before X does, hence before Y executes and hence
|
|
before the strong fence executes. Because this fence is strong, we
|
|
know that W will propagate to every CPU and to RAM before Z executes.
|
|
And because of the hb links, we know that Z will execute before F.
|
|
Thus W, which comes later than E in the coherence order, will
|
|
propagate to every CPU and to RAM before F executes.
|
|
|
|
The case where E is a load is exactly the same, except that the first
|
|
link in the sequence is fre instead of coe.
|
|
|
|
The existence of a pb link from E to F implies that E must execute
|
|
before F. To see why, suppose that F executed first. Then W would
|
|
have propagated to E's CPU before E executed. If E was a store, the
|
|
memory subsystem would then be forced to make E come after W in the
|
|
coherence order, contradicting the fact that E ->coe W. If E was a
|
|
load, the memory subsystem would then be forced to satisfy E's read
|
|
request with the value stored by W or an even later store,
|
|
contradicting the fact that E ->fre W.
|
|
|
|
A good example illustrating how pb works is the SB pattern with strong
|
|
fences:
|
|
|
|
int x = 0, y = 0;
|
|
|
|
P0()
|
|
{
|
|
int r0;
|
|
|
|
WRITE_ONCE(x, 1);
|
|
smp_mb();
|
|
r0 = READ_ONCE(y);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1;
|
|
|
|
WRITE_ONCE(y, 1);
|
|
smp_mb();
|
|
r1 = READ_ONCE(x);
|
|
}
|
|
|
|
If r0 = 0 at the end then there is a pb link from P0's load to P1's
|
|
load: an fre link from P0's load to P1's store (which overwrites the
|
|
value read by P0), and a strong fence between P1's store and its load.
|
|
In this example, the sequences of cumul-fence and hb links are empty.
|
|
Note that this pb link is not included in hb as an instance of prop,
|
|
because it does not start and end on the same CPU.
|
|
|
|
Similarly, if r1 = 0 at the end then there is a pb link from P1's load
|
|
to P0's. This means that if both r1 and r2 were 0 there would be a
|
|
cycle in pb, which is not possible since an instruction cannot execute
|
|
before itself. Thus, adding smp_mb() fences to the SB pattern
|
|
prevents the r0 = 0, r1 = 0 outcome.
|
|
|
|
In summary, the fact that the pb relation links events in the order
|
|
they execute means that it cannot have cycles. This requirement is
|
|
the content of the LKMM's "propagation" axiom.
|
|
|
|
|
|
RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
|
|
----------------------------------------------------
|
|
|
|
RCU (Read-Copy-Update) is a powerful synchronization mechanism. It
|
|
rests on two concepts: grace periods and read-side critical sections.
|
|
|
|
A grace period is the span of time occupied by a call to
|
|
synchronize_rcu(). A read-side critical section (or just critical
|
|
section, for short) is a region of code delimited by rcu_read_lock()
|
|
at the start and rcu_read_unlock() at the end. Critical sections can
|
|
be nested, although we won't make use of this fact.
|
|
|
|
As far as memory models are concerned, RCU's main feature is its
|
|
Grace-Period Guarantee, which states that a critical section can never
|
|
span a full grace period. In more detail, the Guarantee says:
|
|
|
|
If a critical section starts before a grace period then it
|
|
must end before the grace period does. In addition, every
|
|
store that propagates to the critical section's CPU before the
|
|
end of the critical section must propagate to every CPU before
|
|
the end of the grace period.
|
|
|
|
If a critical section ends after a grace period ends then it
|
|
must start after the grace period does. In addition, every
|
|
store that propagates to the grace period's CPU before the
|
|
start of the grace period must propagate to every CPU before
|
|
the start of the critical section.
|
|
|
|
Here is a simple example of RCU in action:
|
|
|
|
int x, y;
|
|
|
|
P0()
|
|
{
|
|
rcu_read_lock();
|
|
WRITE_ONCE(x, 1);
|
|
WRITE_ONCE(y, 1);
|
|
rcu_read_unlock();
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1, r2;
|
|
|
|
r1 = READ_ONCE(x);
|
|
synchronize_rcu();
|
|
r2 = READ_ONCE(y);
|
|
}
|
|
|
|
The Grace Period Guarantee tells us that when this code runs, it will
|
|
never end with r1 = 1 and r2 = 0. The reasoning is as follows. r1 = 1
|
|
means that P0's store to x propagated to P1 before P1 called
|
|
synchronize_rcu(), so P0's critical section must have started before
|
|
P1's grace period. On the other hand, r2 = 0 means that P0's store to
|
|
y, which occurs before the end of the critical section, did not
|
|
propagate to P1 before the end of the grace period, violating the
|
|
Guarantee.
|
|
|
|
In the kernel's implementations of RCU, the requirements for stores
|
|
to propagate to every CPU are fulfilled by placing strong fences at
|
|
suitable places in the RCU-related code. Thus, if a critical section
|
|
starts before a grace period does then the critical section's CPU will
|
|
execute an smp_mb() fence after the end of the critical section and
|
|
some time before the grace period's synchronize_rcu() call returns.
|
|
And if a critical section ends after a grace period does then the
|
|
synchronize_rcu() routine will execute an smp_mb() fence at its start
|
|
and some time before the critical section's opening rcu_read_lock()
|
|
executes.
|
|
|
|
What exactly do we mean by saying that a critical section "starts
|
|
before" or "ends after" a grace period? Some aspects of the meaning
|
|
are pretty obvious, as in the example above, but the details aren't
|
|
entirely clear. The LKMM formalizes this notion by means of the
|
|
rcu-link relation. rcu-link encompasses a very general notion of
|
|
"before": Among other things, X ->rcu-link Z includes cases where X
|
|
happens-before or is equal to some event Y which is equal to or comes
|
|
before Z in the coherence order. When Y = Z this says that X ->rfe Z
|
|
implies X ->rcu-link Z. In addition, when Y = X it says that X ->fr Z
|
|
and X ->co Z each imply X ->rcu-link Z.
|
|
|
|
The formal definition of the rcu-link relation is more than a little
|
|
obscure, and we won't give it here. It is closely related to the pb
|
|
relation, and the details don't matter unless you want to comb through
|
|
a somewhat lengthy formal proof. Pretty much all you need to know
|
|
about rcu-link is the information in the preceding paragraph.
|
|
|
|
The LKMM also defines the gp and rscs relations. They bring grace
|
|
periods and read-side critical sections into the picture, in the
|
|
following way:
|
|
|
|
E ->gp F means there is a synchronize_rcu() fence event S such
|
|
that E ->po S and either S ->po F or S = F. In simple terms,
|
|
there is a grace period po-between E and F.
|
|
|
|
E ->rscs F means there is a critical section delimited by an
|
|
rcu_read_lock() fence L and an rcu_read_unlock() fence U, such
|
|
that E ->po U and either L ->po F or L = F. You can think of
|
|
this as saying that E and F are in the same critical section
|
|
(in fact, it also allows E to be po-before the start of the
|
|
critical section and F to be po-after the end).
|
|
|
|
If we think of the rcu-link relation as standing for an extended
|
|
"before", then X ->gp Y ->rcu-link Z says that X executes before a
|
|
grace period which ends before Z executes. (In fact it covers more
|
|
than this, because it also includes cases where X executes before a
|
|
grace period and some store propagates to Z's CPU before Z executes
|
|
but doesn't propagate to some other CPU until after the grace period
|
|
ends.) Similarly, X ->rscs Y ->rcu-link Z says that X is part of (or
|
|
before the start of) a critical section which starts before Z
|
|
executes.
|
|
|
|
The LKMM goes on to define the rcu-fence relation as a sequence of gp
|
|
and rscs links separated by rcu-link links, in which the number of gp
|
|
links is >= the number of rscs links. For example:
|
|
|
|
X ->gp Y ->rcu-link Z ->rscs T ->rcu-link U ->gp V
|
|
|
|
would imply that X ->rcu-fence V, because this sequence contains two
|
|
gp links and only one rscs link. (It also implies that X ->rcu-fence T
|
|
and Z ->rcu-fence V.) On the other hand:
|
|
|
|
X ->rscs Y ->rcu-link Z ->rscs T ->rcu-link U ->gp V
|
|
|
|
does not imply X ->rcu-fence V, because the sequence contains only
|
|
one gp link but two rscs links.
|
|
|
|
The rcu-fence relation is important because the Grace Period Guarantee
|
|
means that rcu-fence acts kind of like a strong fence. In particular,
|
|
if W is a write and we have W ->rcu-fence Z, the Guarantee says that W
|
|
will propagate to every CPU before Z executes.
|
|
|
|
To prove this in full generality requires some intellectual effort.
|
|
We'll consider just a very simple case:
|
|
|
|
W ->gp X ->rcu-link Y ->rscs Z.
|
|
|
|
This formula means that there is a grace period G and a critical
|
|
section C such that:
|
|
|
|
1. W is po-before G;
|
|
|
|
2. X is equal to or po-after G;
|
|
|
|
3. X comes "before" Y in some sense;
|
|
|
|
4. Y is po-before the end of C;
|
|
|
|
5. Z is equal to or po-after the start of C.
|
|
|
|
From 2 - 4 we deduce that the grace period G ends before the critical
|
|
section C. Then the second part of the Grace Period Guarantee says
|
|
not only that G starts before C does, but also that W (which executes
|
|
on G's CPU before G starts) must propagate to every CPU before C
|
|
starts. In particular, W propagates to every CPU before Z executes
|
|
(or finishes executing, in the case where Z is equal to the
|
|
rcu_read_lock() fence event which starts C.) This sort of reasoning
|
|
can be expanded to handle all the situations covered by rcu-fence.
|
|
|
|
Finally, the LKMM defines the RCU-before (rb) relation in terms of
|
|
rcu-fence. This is done in essentially the same way as the pb
|
|
relation was defined in terms of strong-fence. We will omit the
|
|
details; the end result is that E ->rb F implies E must execute before
|
|
F, just as E ->pb F does (and for much the same reasons).
|
|
|
|
Putting this all together, the LKMM expresses the Grace Period
|
|
Guarantee by requiring that the rb relation does not contain a cycle.
|
|
Equivalently, this "rcu" axiom requires that there are no events E and
|
|
F with E ->rcu-link F ->rcu-fence E. Or to put it a third way, the
|
|
axiom requires that there are no cycles consisting of gp and rscs
|
|
alternating with rcu-link, where the number of gp links is >= the
|
|
number of rscs links.
|
|
|
|
Justifying the axiom isn't easy, but it is in fact a valid
|
|
formalization of the Grace Period Guarantee. We won't attempt to go
|
|
through the detailed argument, but the following analysis gives a
|
|
taste of what is involved. Suppose we have a violation of the first
|
|
part of the Guarantee: A critical section starts before a grace
|
|
period, and some store propagates to the critical section's CPU before
|
|
the end of the critical section but doesn't propagate to some other
|
|
CPU until after the end of the grace period.
|
|
|
|
Putting symbols to these ideas, let L and U be the rcu_read_lock() and
|
|
rcu_read_unlock() fence events delimiting the critical section in
|
|
question, and let S be the synchronize_rcu() fence event for the grace
|
|
period. Saying that the critical section starts before S means there
|
|
are events E and F where E is po-after L (which marks the start of the
|
|
critical section), E is "before" F in the sense of the rcu-link
|
|
relation, and F is po-before the grace period S:
|
|
|
|
L ->po E ->rcu-link F ->po S.
|
|
|
|
Let W be the store mentioned above, let Z come before the end of the
|
|
critical section and witness that W propagates to the critical
|
|
section's CPU by reading from W, and let Y on some arbitrary CPU be a
|
|
witness that W has not propagated to that CPU, where Y happens after
|
|
some event X which is po-after S. Symbolically, this amounts to:
|
|
|
|
S ->po X ->hb* Y ->fr W ->rf Z ->po U.
|
|
|
|
The fr link from Y to W indicates that W has not propagated to Y's CPU
|
|
at the time that Y executes. From this, it can be shown (see the
|
|
discussion of the rcu-link relation earlier) that X and Z are related
|
|
by rcu-link, yielding:
|
|
|
|
S ->po X ->rcu-link Z ->po U.
|
|
|
|
The formulas say that S is po-between F and X, hence F ->gp X. They
|
|
also say that Z comes before the end of the critical section and E
|
|
comes after its start, hence Z ->rscs E. From all this we obtain:
|
|
|
|
F ->gp X ->rcu-link Z ->rscs E ->rcu-link F,
|
|
|
|
a forbidden cycle. Thus the "rcu" axiom rules out this violation of
|
|
the Grace Period Guarantee.
|
|
|
|
For something a little more down-to-earth, let's see how the axiom
|
|
works out in practice. Consider the RCU code example from above, this
|
|
time with statement labels added to the memory access instructions:
|
|
|
|
int x, y;
|
|
|
|
P0()
|
|
{
|
|
rcu_read_lock();
|
|
W: WRITE_ONCE(x, 1);
|
|
X: WRITE_ONCE(y, 1);
|
|
rcu_read_unlock();
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1, r2;
|
|
|
|
Y: r1 = READ_ONCE(x);
|
|
synchronize_rcu();
|
|
Z: r2 = READ_ONCE(y);
|
|
}
|
|
|
|
|
|
If r2 = 0 at the end then P0's store at X overwrites the value that
|
|
P1's load at Z reads from, so we have Z ->fre X and thus Z ->rcu-link X.
|
|
In addition, there is a synchronize_rcu() between Y and Z, so therefore
|
|
we have Y ->gp Z.
|
|
|
|
If r1 = 1 at the end then P1's load at Y reads from P0's store at W,
|
|
so we have W ->rcu-link Y. In addition, W and X are in the same critical
|
|
section, so therefore we have X ->rscs W.
|
|
|
|
Then X ->rscs W ->rcu-link Y ->gp Z ->rcu-link X is a forbidden cycle,
|
|
violating the "rcu" axiom. Hence the outcome is not allowed by the
|
|
LKMM, as we would expect.
|
|
|
|
For contrast, let's see what can happen in a more complicated example:
|
|
|
|
int x, y, z;
|
|
|
|
P0()
|
|
{
|
|
int r0;
|
|
|
|
rcu_read_lock();
|
|
W: r0 = READ_ONCE(x);
|
|
X: WRITE_ONCE(y, 1);
|
|
rcu_read_unlock();
|
|
}
|
|
|
|
P1()
|
|
{
|
|
int r1;
|
|
|
|
Y: r1 = READ_ONCE(y);
|
|
synchronize_rcu();
|
|
Z: WRITE_ONCE(z, 1);
|
|
}
|
|
|
|
P2()
|
|
{
|
|
int r2;
|
|
|
|
rcu_read_lock();
|
|
U: r2 = READ_ONCE(z);
|
|
V: WRITE_ONCE(x, 1);
|
|
rcu_read_unlock();
|
|
}
|
|
|
|
If r0 = r1 = r2 = 1 at the end, then similar reasoning to before shows
|
|
that W ->rscs X ->rcu-link Y ->gp Z ->rcu-link U ->rscs V ->rcu-link W.
|
|
However this cycle is not forbidden, because the sequence of relations
|
|
contains fewer instances of gp (one) than of rscs (two). Consequently
|
|
the outcome is allowed by the LKMM. The following instruction timing
|
|
diagram shows how it might actually occur:
|
|
|
|
P0 P1 P2
|
|
-------------------- -------------------- --------------------
|
|
rcu_read_lock()
|
|
X: WRITE_ONCE(y, 1)
|
|
Y: r1 = READ_ONCE(y)
|
|
synchronize_rcu() starts
|
|
. rcu_read_lock()
|
|
. V: WRITE_ONCE(x, 1)
|
|
W: r0 = READ_ONCE(x) .
|
|
rcu_read_unlock() .
|
|
synchronize_rcu() ends
|
|
Z: WRITE_ONCE(z, 1)
|
|
U: r2 = READ_ONCE(z)
|
|
rcu_read_unlock()
|
|
|
|
This requires P0 and P2 to execute their loads and stores out of
|
|
program order, but of course they are allowed to do so. And as you
|
|
can see, the Grace Period Guarantee is not violated: The critical
|
|
section in P0 both starts before P1's grace period does and ends
|
|
before it does, and the critical section in P2 both starts after P1's
|
|
grace period does and ends after it does.
|
|
|
|
|
|
ODDS AND ENDS
|
|
-------------
|
|
|
|
This section covers material that didn't quite fit anywhere in the
|
|
earlier sections.
|
|
|
|
The descriptions in this document don't always match the formal
|
|
version of the LKMM exactly. For example, the actual formal
|
|
definition of the prop relation makes the initial coe or fre part
|
|
optional, and it doesn't require the events linked by the relation to
|
|
be on the same CPU. These differences are very unimportant; indeed,
|
|
instances where the coe/fre part of prop is missing are of no interest
|
|
because all the other parts (fences and rfe) are already included in
|
|
hb anyway, and where the formal model adds prop into hb, it includes
|
|
an explicit requirement that the events being linked are on the same
|
|
CPU.
|
|
|
|
Another minor difference has to do with events that are both memory
|
|
accesses and fences, such as those corresponding to smp_load_acquire()
|
|
calls. In the formal model, these events aren't actually both reads
|
|
and fences; rather, they are read events with an annotation marking
|
|
them as acquires. (Or write events annotated as releases, in the case
|
|
smp_store_release().) The final effect is the same.
|
|
|
|
Although we didn't mention it above, the instruction execution
|
|
ordering provided by the smp_rmb() fence doesn't apply to read events
|
|
that are part of a non-value-returning atomic update. For instance,
|
|
given:
|
|
|
|
atomic_inc(&x);
|
|
smp_rmb();
|
|
r1 = READ_ONCE(y);
|
|
|
|
it is not guaranteed that the load from y will execute after the
|
|
update to x. This is because the ARMv8 architecture allows
|
|
non-value-returning atomic operations effectively to be executed off
|
|
the CPU. Basically, the CPU tells the memory subsystem to increment
|
|
x, and then the increment is carried out by the memory hardware with
|
|
no further involvement from the CPU. Since the CPU doesn't ever read
|
|
the value of x, there is nothing for the smp_rmb() fence to act on.
|
|
|
|
The LKMM defines a few extra synchronization operations in terms of
|
|
things we have already covered. In particular, rcu_dereference() is
|
|
treated as READ_ONCE() and rcu_assign_pointer() is treated as
|
|
smp_store_release() -- which is basically how the Linux kernel treats
|
|
them.
|
|
|
|
There are a few oddball fences which need special treatment:
|
|
smp_mb__before_atomic(), smp_mb__after_atomic(), and
|
|
smp_mb__after_spinlock(). The LKMM uses fence events with special
|
|
annotations for them; they act as strong fences just like smp_mb()
|
|
except for the sets of events that they order. Instead of ordering
|
|
all po-earlier events against all po-later events, as smp_mb() does,
|
|
they behave as follows:
|
|
|
|
smp_mb__before_atomic() orders all po-earlier events against
|
|
po-later atomic updates and the events following them;
|
|
|
|
smp_mb__after_atomic() orders po-earlier atomic updates and
|
|
the events preceding them against all po-later events;
|
|
|
|
smp_mb_after_spinlock() orders po-earlier lock acquisition
|
|
events and the events preceding them against all po-later
|
|
events.
|
|
|
|
The LKMM includes locking. In fact, there is special code for locking
|
|
in the formal model, added in order to make tools run faster.
|
|
However, this special code is intended to be exactly equivalent to
|
|
concepts we have already covered. A spinlock_t variable is treated
|
|
the same as an int, and spin_lock(&s) is treated the same as:
|
|
|
|
while (cmpxchg_acquire(&s, 0, 1) != 0)
|
|
cpu_relax();
|
|
|
|
which waits until s is equal to 0 and then atomically sets it to 1,
|
|
and where the read part of the atomic update is also an acquire fence.
|
|
An alternate way to express the same thing would be:
|
|
|
|
r = xchg_acquire(&s, 1);
|
|
|
|
along with a requirement that at the end, r = 0. spin_unlock(&s) is
|
|
treated the same as:
|
|
|
|
smp_store_release(&s, 0);
|
|
|
|
Interestingly, RCU and locking each introduce the possibility of
|
|
deadlock. When faced with code sequences such as:
|
|
|
|
spin_lock(&s);
|
|
spin_lock(&s);
|
|
spin_unlock(&s);
|
|
spin_unlock(&s);
|
|
|
|
or:
|
|
|
|
rcu_read_lock();
|
|
synchronize_rcu();
|
|
rcu_read_unlock();
|
|
|
|
what does the LKMM have to say? Answer: It says there are no allowed
|
|
executions at all, which makes sense. But this can also lead to
|
|
misleading results, because if a piece of code has multiple possible
|
|
executions, some of which deadlock, the model will report only on the
|
|
non-deadlocking executions. For example:
|
|
|
|
int x, y;
|
|
|
|
P0()
|
|
{
|
|
int r0;
|
|
|
|
WRITE_ONCE(x, 1);
|
|
r0 = READ_ONCE(y);
|
|
}
|
|
|
|
P1()
|
|
{
|
|
rcu_read_lock();
|
|
if (READ_ONCE(x) > 0) {
|
|
WRITE_ONCE(y, 36);
|
|
synchronize_rcu();
|
|
}
|
|
rcu_read_unlock();
|
|
}
|
|
|
|
Is it possible to end up with r0 = 36 at the end? The LKMM will tell
|
|
you it is not, but the model won't mention that this is because P1
|
|
will self-deadlock in the executions where it stores 36 in y.
|