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, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb
  23. SRCU READ-SIDE CRITICAL SECTIONS
  24. LOCKING
  25. PLAIN ACCESSES AND DATA RACES
  26. 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, P0'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.  The use of READ_ONCE(), WRITE_ONCE(),
or one of the other atomic or synchronization primitives prevents 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.

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, the compiler won't reorder P0's write event to
buf and P0's write event to flag, and similarly for the other shared
memory accesses in the examples.

Since private variables are not shared between CPUs, they can be
accessed normally without READ_ONCE() or WRITE_ONCE().  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 function calls 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 X and a write event Y are linked by a control
dependency if Y syntactically lies within an arm of an if statement and
X affects the evaluation of the if condition via a data or address
dependency (or similarly for a switch statement).  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!

Here's a trick question: When is a dependency not a dependency?  Answer:
When it is purely syntactic rather than semantic.  We say a dependency
between two accesses is purely syntactic if the second access doesn't
actually depend on the result of the first.  Here is a trivial example:

	r1 = READ_ONCE(x);
	WRITE_ONCE(y, r1 * 0);

There appears to be a data dependency from the load of x to the store
of y, since the value to be stored is computed from the value that was
loaded.  But in fact, the value stored does not really depend on
anything since it will always be 0.  Thus the data dependency is only
syntactic (it appears to exist in the code) but not semantic (the
second access will always be the same, regardless of the value of the
first access).  Given code like this, a compiler could simply discard
the value returned by the load from x, which would certainly destroy
any dependency.  (The compiler is not permitted to eliminate entirely
the load generated for a READ_ONCE() -- that's one of the nice
properties of READ_ONCE() -- but it is allowed to ignore the load's
value.)

It's natural to object that no one in their right mind would write
code like the above.  However, macro expansions can easily give rise
to this sort of thing, in ways that often are not apparent to the
programmer.

Another mechanism that can lead to purely syntactic dependencies is
related to the notion of "undefined behavior".  Certain program
behaviors are called "undefined" in the C language specification,
which means that when they occur there are no guarantees at all about
the outcome.  Consider the following example:

	int a[1];
	int i;

	r1 = READ_ONCE(i);
	r2 = READ_ONCE(a[r1]);

Access beyond the end or before the beginning of an array is one kind
of undefined behavior.  Therefore the compiler doesn't have to worry
about what will happen if r1 is nonzero, and it can assume that r1
will always be zero regardless of the value actually loaded from i.
(If the assumption turns out to be wrong the resulting behavior will
be undefined anyway, so the compiler doesn't care!)  Thus the value
from the load can be discarded, breaking the address dependency.

The LKMM is unaware that purely syntactic dependencies are different
from semantic dependencies and therefore mistakenly predicts that the
accesses in the two examples above will be ordered.  This is another
example of how the compiler can undermine the memory model.  Be warned.


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 main 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 r