|
|
@ -2,21 +2,22 @@
|
|
|
|
|
|
|
|
|
|
|
|
Rust pretty blatantly just inherits C11's memory model for atomics. This is not
|
|
|
|
Rust pretty blatantly just inherits C11's memory model for atomics. This is not
|
|
|
|
due this model being particularly excellent or easy to understand. Indeed, this
|
|
|
|
due this model being particularly excellent or easy to understand. Indeed, this
|
|
|
|
model is quite complex and known to have [several flaws][C11-busted]. Rather,
|
|
|
|
model is quite complex and known to have [several flaws][C11-busted]. Rather, it
|
|
|
|
it is a pragmatic concession to the fact that *everyone* is pretty bad at modeling
|
|
|
|
is a pragmatic concession to the fact that *everyone* is pretty bad at modeling
|
|
|
|
atomics. At very least, we can benefit from existing tooling and research around
|
|
|
|
atomics. At very least, we can benefit from existing tooling and research around
|
|
|
|
C.
|
|
|
|
C.
|
|
|
|
|
|
|
|
|
|
|
|
Trying to fully explain the model in this book is fairly hopeless. It's defined
|
|
|
|
Trying to fully explain the model in this book is fairly hopeless. It's defined
|
|
|
|
in terms of madness-inducing causality graphs that require a full book to properly
|
|
|
|
in terms of madness-inducing causality graphs that require a full book to
|
|
|
|
understand in a practical way. If you want all the nitty-gritty details, you
|
|
|
|
properly understand in a practical way. If you want all the nitty-gritty
|
|
|
|
should check out [C's specification (Section 7.17)][C11-model]. Still, we'll try
|
|
|
|
details, you should check out [C's specification (Section 7.17)][C11-model].
|
|
|
|
to cover the basics and some of the problems Rust developers face.
|
|
|
|
Still, we'll try to cover the basics and some of the problems Rust developers
|
|
|
|
|
|
|
|
face.
|
|
|
|
|
|
|
|
|
|
|
|
The C11 memory model is fundamentally about trying to bridge the gap between
|
|
|
|
The C11 memory model is fundamentally about trying to bridge the gap between the
|
|
|
|
the semantics we want, the optimizations compilers want, and the inconsistent
|
|
|
|
semantics we want, the optimizations compilers want, and the inconsistent chaos
|
|
|
|
chaos our hardware wants. *We* would like to just write programs and have them
|
|
|
|
our hardware wants. *We* would like to just write programs and have them do
|
|
|
|
do exactly what we said but, you know, *fast*. Wouldn't that be great?
|
|
|
|
exactly what we said but, you know, *fast*. Wouldn't that be great?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -41,13 +42,14 @@ x = 2;
|
|
|
|
y = 3;
|
|
|
|
y = 3;
|
|
|
|
```
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
This has inverted the order of events *and* completely eliminated one event. From
|
|
|
|
This has inverted the order of events *and* completely eliminated one event.
|
|
|
|
a single-threaded perspective this is completely unobservable: after all the
|
|
|
|
From a single-threaded perspective this is completely unobservable: after all
|
|
|
|
statements have executed we are in exactly the same state. But if our program is
|
|
|
|
the statements have executed we are in exactly the same state. But if our
|
|
|
|
multi-threaded, we may have been relying on `x` to *actually* be assigned to 1 before
|
|
|
|
program is multi-threaded, we may have been relying on `x` to *actually* be
|
|
|
|
`y` was assigned. We would *really* like the compiler to be able to make these kinds
|
|
|
|
assigned to 1 before `y` was assigned. We would *really* like the compiler to be
|
|
|
|
of optimizations, because they can seriously improve performance. On the other hand,
|
|
|
|
able to make these kinds of optimizations, because they can seriously improve
|
|
|
|
we'd really like to be able to depend on our program *doing the thing we said*.
|
|
|
|
performance. On the other hand, we'd really like to be able to depend on our
|
|
|
|
|
|
|
|
program *doing the thing we said*.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -55,19 +57,20 @@ we'd really like to be able to depend on our program *doing the thing we said*.
|
|
|
|
# Hardware Reordering
|
|
|
|
# Hardware Reordering
|
|
|
|
|
|
|
|
|
|
|
|
On the other hand, even if the compiler totally understood what we wanted and
|
|
|
|
On the other hand, even if the compiler totally understood what we wanted and
|
|
|
|
respected our wishes, our *hardware* might instead get us in trouble. Trouble comes
|
|
|
|
respected our wishes, our *hardware* might instead get us in trouble. Trouble
|
|
|
|
from CPUs in the form of memory hierarchies. There is indeed a global shared memory
|
|
|
|
comes from CPUs in the form of memory hierarchies. There is indeed a global
|
|
|
|
space somewhere in your hardware, but from the perspective of each CPU core it is
|
|
|
|
shared memory space somewhere in your hardware, but from the perspective of each
|
|
|
|
*so very far away* and *so very slow*. Each CPU would rather work with its local
|
|
|
|
CPU core it is *so very far away* and *so very slow*. Each CPU would rather work
|
|
|
|
cache of the data and only go through all the *anguish* of talking to shared
|
|
|
|
with its local cache of the data and only go through all the *anguish* of
|
|
|
|
memory *only* when it doesn't actually have that memory in cache.
|
|
|
|
talking to shared memory *only* when it doesn't actually have that memory in
|
|
|
|
|
|
|
|
cache.
|
|
|
|
|
|
|
|
|
|
|
|
After all, that's the whole *point* of the cache, right? If every read from the
|
|
|
|
After all, that's the whole *point* of the cache, right? If every read from the
|
|
|
|
cache had to run back to shared memory to double check that it hadn't changed,
|
|
|
|
cache had to run back to shared memory to double check that it hadn't changed,
|
|
|
|
what would the point be? The end result is that the hardware doesn't guarantee
|
|
|
|
what would the point be? The end result is that the hardware doesn't guarantee
|
|
|
|
that events that occur in the same order on *one* thread, occur in the same order
|
|
|
|
that events that occur in the same order on *one* thread, occur in the same
|
|
|
|
on *another* thread. To guarantee this, we must issue special instructions to
|
|
|
|
order on *another* thread. To guarantee this, we must issue special instructions
|
|
|
|
the CPU telling it to be a bit less smart.
|
|
|
|
to the CPU telling it to be a bit less smart.
|
|
|
|
|
|
|
|
|
|
|
|
For instance, say we convince the compiler to emit this logic:
|
|
|
|
For instance, say we convince the compiler to emit this logic:
|
|
|
|
|
|
|
|
|
|
|
@ -82,27 +85,27 @@ x = 1; y *= 2;
|
|
|
|
|
|
|
|
|
|
|
|
Ideally this program has 2 possible final states:
|
|
|
|
Ideally this program has 2 possible final states:
|
|
|
|
|
|
|
|
|
|
|
|
* `y = 3`: (thread 2 did the check before thread 1 completed)
|
|
|
|
* `y = 3`: (thread 2 did the check before thread 1 completed) y = 6`: (thread 2
|
|
|
|
* `y = 6`: (thread 2 did the check after thread 1 completed)
|
|
|
|
* `did the check after thread 1 completed)
|
|
|
|
|
|
|
|
|
|
|
|
However there's a third potential state that the hardware enables:
|
|
|
|
However there's a third potential state that the hardware enables:
|
|
|
|
|
|
|
|
|
|
|
|
* `y = 2`: (thread 2 saw `x = 2`, but not `y = 3`, and then overwrote `y = 3`)
|
|
|
|
* `y = 2`: (thread 2 saw `x = 2`, but not `y = 3`, and then overwrote `y = 3`)
|
|
|
|
|
|
|
|
|
|
|
|
It's worth noting that different kinds of CPU provide different guarantees. It
|
|
|
|
It's worth noting that different kinds of CPU provide different guarantees. It
|
|
|
|
is common to seperate hardware into two categories: strongly-ordered and weakly-
|
|
|
|
is common to separate hardware into two categories: strongly-ordered and weakly-
|
|
|
|
ordered. Most notably x86/64 provides strong ordering guarantees, while ARM and
|
|
|
|
ordered. Most notably x86/64 provides strong ordering guarantees, while ARM
|
|
|
|
provides weak ordering guarantees. This has two consequences for
|
|
|
|
provides weak ordering guarantees. This has two consequences for concurrent
|
|
|
|
concurrent programming:
|
|
|
|
programming:
|
|
|
|
|
|
|
|
|
|
|
|
* Asking for stronger guarantees on strongly-ordered hardware may be cheap or
|
|
|
|
* Asking for stronger guarantees on strongly-ordered hardware may be cheap or
|
|
|
|
even *free* because they already provide strong guarantees unconditionally.
|
|
|
|
even *free* because they already provide strong guarantees unconditionally.
|
|
|
|
Weaker guarantees may only yield performance wins on weakly-ordered hardware.
|
|
|
|
Weaker guarantees may only yield performance wins on weakly-ordered hardware.
|
|
|
|
|
|
|
|
|
|
|
|
* Asking for guarantees that are *too* weak on strongly-ordered hardware
|
|
|
|
* Asking for guarantees that are *too* weak on strongly-ordered hardware is
|
|
|
|
is more likely to *happen* to work, even though your program is strictly
|
|
|
|
more likely to *happen* to work, even though your program is strictly
|
|
|
|
incorrect. If possible, concurrent algorithms should be tested on
|
|
|
|
incorrect. If possible, concurrent algorithms should be tested on weakly-
|
|
|
|
weakly-ordered hardware.
|
|
|
|
ordered hardware.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -110,58 +113,54 @@ concurrent programming:
|
|
|
|
|
|
|
|
|
|
|
|
# Data Accesses
|
|
|
|
# Data Accesses
|
|
|
|
|
|
|
|
|
|
|
|
The C11 memory model attempts to bridge the gap by allowing us to talk about
|
|
|
|
The C11 memory model attempts to bridge the gap by allowing us to talk about the
|
|
|
|
the *causality* of our program. Generally, this is by establishing a
|
|
|
|
*causality* of our program. Generally, this is by establishing a *happens
|
|
|
|
*happens before* relationships between parts of the program and the threads
|
|
|
|
before* relationships between parts of the program and the threads that are
|
|
|
|
that are running them. This gives the hardware and compiler room to optimize the
|
|
|
|
running them. This gives the hardware and compiler room to optimize the program
|
|
|
|
program more aggressively where a strict happens-before relationship isn't
|
|
|
|
more aggressively where a strict happens-before relationship isn't established,
|
|
|
|
established, but forces them to be more careful where one *is* established.
|
|
|
|
but forces them to be more careful where one *is* established. The way we
|
|
|
|
The way we communicate these relationships are through *data accesses* and
|
|
|
|
communicate these relationships are through *data accesses* and *atomic
|
|
|
|
*atomic accesses*.
|
|
|
|
accesses*.
|
|
|
|
|
|
|
|
|
|
|
|
Data accesses are the bread-and-butter of the programming world. They are
|
|
|
|
Data accesses are the bread-and-butter of the programming world. They are
|
|
|
|
fundamentally unsynchronized and compilers are free to aggressively optimize
|
|
|
|
fundamentally unsynchronized and compilers are free to aggressively optimize
|
|
|
|
them. In particular, data accesses are free to be reordered by the compiler
|
|
|
|
them. In particular, data accesses are free to be reordered by the compiler on
|
|
|
|
on the assumption that the program is single-threaded. The hardware is also free
|
|
|
|
the assumption that the program is single-threaded. The hardware is also free to
|
|
|
|
to propagate the changes made in data accesses to other threads
|
|
|
|
propagate the changes made in data accesses to other threads as lazily and
|
|
|
|
as lazily and inconsistently as it wants. Mostly critically, data accesses are
|
|
|
|
inconsistently as it wants. Mostly critically, data accesses are how data races
|
|
|
|
how data races happen. Data accesses are very friendly to the hardware and
|
|
|
|
happen. Data accesses are very friendly to the hardware and compiler, but as
|
|
|
|
compiler, but as we've seen they offer *awful* semantics to try to
|
|
|
|
we've seen they offer *awful* semantics to try to write synchronized code with.
|
|
|
|
write synchronized code with. Actually, that's too weak. *It is literally
|
|
|
|
Actually, that's too weak. *It is literally impossible to write correct
|
|
|
|
impossible to write correct synchronized code using only data accesses*.
|
|
|
|
synchronized code using only data accesses*.
|
|
|
|
|
|
|
|
|
|
|
|
Atomic accesses are how we tell the hardware and compiler that our program is
|
|
|
|
Atomic accesses are how we tell the hardware and compiler that our program is
|
|
|
|
multi-threaded. Each atomic access can be marked with
|
|
|
|
multi-threaded. Each atomic access can be marked with an *ordering* that
|
|
|
|
an *ordering* that specifies what kind of relationship it establishes with
|
|
|
|
specifies what kind of relationship it establishes with other accesses. In
|
|
|
|
other accesses. In practice, this boils down to telling the compiler and hardware
|
|
|
|
practice, this boils down to telling the compiler and hardware certain things
|
|
|
|
certain things they *can't* do. For the compiler, this largely revolves
|
|
|
|
they *can't* do. For the compiler, this largely revolves around re-ordering of
|
|
|
|
around re-ordering of instructions. For the hardware, this largely revolves
|
|
|
|
instructions. For the hardware, this largely revolves around how writes are
|
|
|
|
around how writes are propagated to other threads. The set of orderings Rust
|
|
|
|
propagated to other threads. The set of orderings Rust exposes are:
|
|
|
|
exposes are:
|
|
|
|
|
|
|
|
|
|
|
|
* Sequentially Consistent (SeqCst) Release Acquire Relaxed
|
|
|
|
* Sequentially Consistent (SeqCst)
|
|
|
|
|
|
|
|
* Release
|
|
|
|
|
|
|
|
* Acquire
|
|
|
|
|
|
|
|
* Relaxed
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(Note: We explicitly do not expose the C11 *consume* ordering)
|
|
|
|
(Note: We explicitly do not expose the C11 *consume* ordering)
|
|
|
|
|
|
|
|
|
|
|
|
TODO: negative reasoning vs positive reasoning?
|
|
|
|
TODO: negative reasoning vs positive reasoning? TODO: "can't forget to
|
|
|
|
TODO: "can't forget to synchronize"
|
|
|
|
synchronize"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
# Sequentially Consistent
|
|
|
|
# Sequentially Consistent
|
|
|
|
|
|
|
|
|
|
|
|
Sequentially Consistent is the most powerful of all, implying the restrictions
|
|
|
|
Sequentially Consistent is the most powerful of all, implying the restrictions
|
|
|
|
of all other orderings. Intuitively, a sequentially consistent operation *cannot*
|
|
|
|
of all other orderings. Intuitively, a sequentially consistent operation
|
|
|
|
be reordered: all accesses on one thread that happen before and after it *stay*
|
|
|
|
*cannot* be reordered: all accesses on one thread that happen before and after a
|
|
|
|
before and after it. A data-race-free program that uses only sequentially consistent
|
|
|
|
SeqCst access *stay* before and after it. A data-race-free program that uses
|
|
|
|
atomics and data accesses has the very nice property that there is a single global
|
|
|
|
only sequentially consistent atomics and data accesses has the very nice
|
|
|
|
execution of the program's instructions that all threads agree on. This execution
|
|
|
|
property that there is a single global execution of the program's instructions
|
|
|
|
is also particularly nice to reason about: it's just an interleaving of each thread's
|
|
|
|
that all threads agree on. This execution is also particularly nice to reason
|
|
|
|
individual executions. This *does not* hold if you start using the weaker atomic
|
|
|
|
about: it's just an interleaving of each thread's individual executions. This
|
|
|
|
orderings.
|
|
|
|
*does not* hold if you start using the weaker atomic orderings.
|
|
|
|
|
|
|
|
|
|
|
|
The relative developer-friendliness of sequential consistency doesn't come for
|
|
|
|
The relative developer-friendliness of sequential consistency doesn't come for
|
|
|
|
free. Even on strongly-ordered platforms sequential consistency involves
|
|
|
|
free. Even on strongly-ordered platforms sequential consistency involves
|
|
|
@ -173,26 +172,26 @@ confident about the other memory orders. Having your program run a bit slower
|
|
|
|
than it needs to is certainly better than it running incorrectly! It's also
|
|
|
|
than it needs to is certainly better than it running incorrectly! It's also
|
|
|
|
*mechanically* trivial to downgrade atomic operations to have a weaker
|
|
|
|
*mechanically* trivial to downgrade atomic operations to have a weaker
|
|
|
|
consistency later on. Just change `SeqCst` to e.g. `Relaxed` and you're done! Of
|
|
|
|
consistency later on. Just change `SeqCst` to e.g. `Relaxed` and you're done! Of
|
|
|
|
course, proving that this transformation is *correct* is whole other matter.
|
|
|
|
course, proving that this transformation is *correct* is a whole other matter.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
# Acquire-Release
|
|
|
|
# Acquire-Release
|
|
|
|
|
|
|
|
|
|
|
|
Acquire and Release are largely intended to be paired. Their names hint at
|
|
|
|
Acquire and Release are largely intended to be paired. Their names hint at their
|
|
|
|
their use case: they're perfectly suited for acquiring and releasing locks,
|
|
|
|
use case: they're perfectly suited for acquiring and releasing locks, and
|
|
|
|
and ensuring that critical sections don't overlap.
|
|
|
|
ensuring that critical sections don't overlap.
|
|
|
|
|
|
|
|
|
|
|
|
Intuitively, an acquire access ensures that every access after it *stays* after
|
|
|
|
Intuitively, an acquire access ensures that every access after it *stays* after
|
|
|
|
it. However operations that occur before an acquire are free to be reordered to
|
|
|
|
it. However operations that occur before an acquire are free to be reordered to
|
|
|
|
occur after it. Similarly, a release access ensures that every access before it
|
|
|
|
occur after it. Similarly, a release access ensures that every access before it
|
|
|
|
*stays* before it. However operations that occur after a release are free to
|
|
|
|
*stays* before it. However operations that occur after a release are free to be
|
|
|
|
be reordered to occur before it.
|
|
|
|
reordered to occur before it.
|
|
|
|
|
|
|
|
|
|
|
|
When thread A releases a location in memory and then thread B subsequently
|
|
|
|
When thread A releases a location in memory and then thread B subsequently
|
|
|
|
acquires *the same* location in memory, causality is established. Every write
|
|
|
|
acquires *the same* location in memory, causality is established. Every write
|
|
|
|
that happened *before* A's release will be observed by B *after* it's release.
|
|
|
|
that happened *before* A's release will be observed by B *after* its release.
|
|
|
|
However no causality is established with any other threads. Similarly, no
|
|
|
|
However no causality is established with any other threads. Similarly, no
|
|
|
|
causality is established if A and B access *different* locations in memory.
|
|
|
|
causality is established if A and B access *different* locations in memory.
|
|
|
|
|
|
|
|
|
|
|
|