Simplify SeqCst demonstration, and remove incorrect claim

pull/378/head
SabrinaJewson 8 months ago
parent 19b059a6eb
commit b139a3ce58
No known key found for this signature in database
GPG Key ID: 3D5438FFA5F05564

@ -230,25 +230,25 @@ Namely, the power of `SeqCst` fences can be summarized in three points:
The “motivating use-case” for `SeqCst` demonstrated in the `SeqCst` chapter can
also be rewritten to use exclusively `SeqCst` fences and `Relaxed` operations,
by inserting fences in between the loads in threads `c` and `d`:
by inserting fences in between the operations in the two threads:
```text
a static X c d static Y b
╭─────────╮ ┌───────┐ ╭─────────╮ ╭─────────╮ ┌───────┐ ╭─────────╮
│ store X ├─┐ │ false │ ┌─┤ load X │ │ load Y ├─┐ │ false │ ┌─┤ store Y │
╰─────────╯ │ └───────┘ │ ╰────╥────╯ ╰────╥────╯ │ └───────┘ │ ╰─────────╯
└─┬───────┐ │ ╭────⇓────╮ ╭────⇓────╮ │ ┌───────┬─┘
│ true ├─┘ │ *fence* │ │ *fence* │ └─┤ true
└───────┘ ╰────╥────╯ ╰────╥────╯ └───────┘
a static X static Y b
╭─────────╮ ┌───────┐ ┌───────┐ ╭─────────╮
│ store X ├─┐ │ false │ │ false │ ┌─┤ store Y │
╰────╥────╯ │ └───────┘ └───────┘ │ ╰────╥────╯
╭────⇓────╮ └─┬───────┐ ┌───────┬─┘ ╭────⇓────╮
*fence* │ │ true │ │ true │ │ *fence*
╰────╥────╯ └───────┘ └───────┘ ╰────╥────╯
╭────⇓────╮ ╭────⇓────╮
│ load Y ├─? ?─┤ load X │
╰─────────╯ ╰─────────╯
```
There are two executions to consider here, depending on which way round the
fences appear in _S_. Should `c`s fence appear first, the fencefence `SeqCst`
guarantee tells us that `c`s load of `X` is not coherence-ordered-after `d`s
load of `X`, which forbids `d`s load of `X` from seeing the value `false`. The
fences appear in _S_. Should `a`s fence appear first, the fencefence `SeqCst`
guarantee tells us that `b`s load of `X` is not coherence-ordered-after `a`s
store of `X`, which forbids `b`s load of `X` from seeing the value `false`. The
same logic can be applied should the fences appear the other way around, proving
that at least one thread must load `true` in the end.

@ -12,10 +12,8 @@ behind it are, and it gets really ugly really fast as soon as you try to mix it
with any other ordering.
To understand `SeqCst`, we first have to understand the problem it exists to
solve. The first complexity is that this problem can only be observed in the
presence of at least four different threads _and_ two separate atomic variables;
anything less and its not possible to notice a difference. The common example
used to show where weaker orderings produce counterintuitive results is this:
solve. A simple example used to show where weaker orderings produce
counterintuitive results is this:
```rust
# use std::sync::atomic::{self, AtomicBool};
@ -29,56 +27,48 @@ const ORDERING: atomic::Ordering = atomic::Ordering::Relaxed;
static X: AtomicBool = AtomicBool::new(false);
static Y: AtomicBool = AtomicBool::new(false);
let a = thread::spawn(|| { X.store(true, ORDERING) });
let b = thread::spawn(|| { Y.store(true, ORDERING) });
let c = thread::spawn(|| { while !X.load(ORDERING) {} Y.load(ORDERING) });
let d = thread::spawn(|| { while !Y.load(ORDERING) {} X.load(ORDERING) });
let a = thread::spawn(|| { X.store(true, ORDERING); Y.load(ORDERING) });
let b = thread::spawn(|| { Y.store(true, ORDERING); X.load(ORDERING) });
let a = a.join().unwrap();
let b = b.join().unwrap();
let c = c.join().unwrap();
let d = d.join().unwrap();
# return;
// This assert is allowed to fail.
assert!(c || d);
assert!(a || b);
```
The basic setup of this code, for all of its possible executions, looks like
this:
```text
a static X c d static Y b
╭─────────╮ ┌───────┐ ╭─────────╮ ╭─────────╮ ┌───────┐ ╭─────────╮
│ store X ├─┐ │ false │ ┌─┤ load X │ │ load Y ├─┐ │ false │ ┌─┤ store Y │
╰─────────╯ │ └───────┘ │ ╰────╥────╯ ╰────╥────╯ │ └───────┘ │ ╰─────────╯
└─┬───────┐ │ ╭────⇓────╮ ╭────⇓────╮ │ ┌───────┬─┘
│ true ├─┘ │ load Y ├─? ?─┤ load X │ └─┤ true
└───────┘ ╰─────────╯ ╰─────────╯ └───────┘
a static X static Y b
╭─────────╮ ┌───────┐ ┌───────┐ ╭─────────╮
│ store X ├─┐ │ false │ │ false │ ┌─┤ store Y │
╰────╥────╯ │ └───────┘ └───────┘ │ ╰────╥────╯
╭────⇓────╮ └─┬───────┐ ┌───────┬─┘ ╭────⇓────╮
│ load Y ├─? │ true │ │ true │ ?─┤ load X
╰─────────╯ └───────┘ └───────┘ ╰─────────╯
```
In other words, `a` and `b` are guaranteed to, at some point, store `true` into
`X` and `Y` respectively, and `c` and `d` are guaranteed to, at some point, load
those values of `true` from `X` and `Y` (there could also be an arbitrary number
of loads of `false` by `c` and `d`, but theyve been omitted since they dont
actually affect the execution at all). The question now is when `c` and `d` load
from `Y` and `X` respectively, is it possible for them _both_ to load `false`?
In other words, `a` and `b` are guaranteed to store `true` into `X` and `Y`
respectively, and then attempt to load from the other threads atomic. The
question now is: is it possible for them _both_ to load `false`?
And looking at this diagram, theres absolutely no reason why not. There isnt
even a single arrow connecting the left and right hand sides so far, so the load
has no coherence-based restrictions on which value it is allowed to pick — and
this goes for both sides equally, so we could end up with an execution like
this:
even a single arrow connecting the left and right hand sides so far, so the
loads have no coherence-based restrictions on which values they are allowed to
pick, and we could end up with an execution like this:
```text
a static X c d static Y b
╭─────────╮ ┌───────┐ ╭─────────╮ ╭─────────╮ ┌───────┐ ╭─────────╮
│ store X ├─┐ │ false ├┐ ┌┤ load X │ │ load Y ├┐ ┌┤ false │ ┌─┤ store Y │
╰─────────╯ │ └───────┘│ │╰────╥────╯ ╰────╥────╯│ │└───────┘ │ ╰─────────╯
└─┬───────┐└─│─────║──────┐┌─────║─────│─┘┌───────┬─┘
│ true ├──┘╭────⇓────╮┌─┘╭────⇓────╮└──┤ true │
└───────┘ │ load Y ├┘└─┤ load X │ └───────┘
╰─────────╯ ╰─────────╯
a static X static Y b
╭─────────╮ ┌───────┐ ┌───────┐ ╭─────────╮
│ store X ├┐ │ false ├─┐┌┤ false │ ┌┤ store Y │
╰────╥────╯│ └───────┘┌─┘└───────┘ │╰────╥────╯
║ │ ┌─────────┘└───────────┐│ ║
╭────⇓────╮└─│┬───────┐ ┌───────┬─│┘╭────⇓────╮
│ load Y ├──┘│ true │ │ true │ └─┤ load X │
╰─────────╯ └───────┘ └───────┘ ╰─────────╯
```
Which results in a failed assert. This execution is brought about because the
@ -178,16 +168,16 @@ make that execution invalid. As a refresher, heres the framework for every
possible execution of the program:
```text
a static X c d static Y b
╭─────────╮ ┌───────┐ ╭─────────╮ ╭─────────╮ ┌───────┐ ╭─────────╮
│ store X ├─┐ │ false │ ┌─┤ load X │ │ load Y ├─┐ │ false │ ┌─┤ store Y │
╰─────────╯ │ └───────┘ │ ╰────╥────╯ ╰────╥────╯ │ └───────┘ │ ╰─────────╯
└─┬───────┐ │ ╭────⇓────╮ ╭────⇓────╮ │ ┌───────┬─┘
│ true ├─┘ │ load Y ├─? ?─┤ load X │ └─┤ true
└───────┘ ╰─────────╯ ╰─────────╯ └───────┘
a static X static Y b
╭─────────╮ ┌───────┐ ┌───────┐ ╭─────────╮
│ store X ├─┐ │ false │ │ false │ ┌─┤ store Y │
╰────╥────╯ │ └───────┘ └───────┘ │ ╰────╥────╯
╭────⇓────╮ └─┬───────┐ ┌───────┬─┘ ╭────⇓────╮
│ load Y ├─? │ true │ │ true │ ?─┤ load X
╰─────────╯ └───────┘ └───────┘ ╰─────────╯
```
First of all, both the final loads (`c` and `d`s second operations) need to
First of all, both the final loads (`a` and `b`s second operations) need to
become `SeqCst`, because they need to be aware of the total ordering that
determines whether `X` or `Y` becomes `true` first. And secondly, we need to
establish that ordering in the first place, and that needs to be done by making
@ -195,77 +185,74 @@ sure that there is always one operation in _S_ that both sees one of the atomics
as `true` and precedes both final loads in _S_, so that the coherence ordering
guarantee will apply (the final loads themselves dont work for this since
although they “know” that their corresponding atomic is `true` they dont
interact with it directly so _S_ doesnt care).
There are two operations in the program that could fulfill the first condition,
should they be made `SeqCst`: the stores of `true` and the first loads. However,
the second condition ends up ruling out using the stores, since in order to make
sure that they precede the final loads in _S_ it would be necessary to have the
first loads be `SeqCst` anyway (due to the mixed-`SeqCst` special case detailed
later), so in the end we can just leave them as `Relaxed`.
interact with it directly so _S_ doesnt care) — for this, we must set both
stores to use the `SeqCst` ordering.
This leaves us with the correct version of the above program, which is
guaranteed to never panic:
```rust
# use std::sync::atomic::{AtomicBool, Ordering::{Relaxed, SeqCst}};
# use std::sync::atomic::{self, AtomicBool};
use std::thread;
const ORDERING: atomic::Ordering = atomic::Ordering::SeqCst;
static X: AtomicBool = AtomicBool::new(false);
static Y: AtomicBool = AtomicBool::new(false);
let a = thread::spawn(|| { X.store(true, Relaxed) });
let b = thread::spawn(|| { Y.store(true, Relaxed) });
let c = thread::spawn(|| { while !X.load(SeqCst) {} Y.load(SeqCst) });
let d = thread::spawn(|| { while !Y.load(SeqCst) {} X.load(SeqCst) });
let a = thread::spawn(|| { X.store(true, ORDERING); Y.load(ORDERING) });
let b = thread::spawn(|| { Y.store(true, ORDERING); X.load(ORDERING) });
let a = a.join().unwrap();
let b = b.join().unwrap();
let c = c.join().unwrap();
let d = d.join().unwrap();
# return;
// This assert is **not** allowed to fail.
assert!(c || d);
assert!(a || b);
```
As there are four `SeqCst` operations with a partial order between two pairs in
them (caused by the sequenced-before relation), there are six possible
executions of this program:
- All of `c`s loads precede `d`s loads:
1. `c` loads `X` (gives `true`)
1. `c` loads `Y` (gives either `false` or `true`)
1. `d` loads `Y` (gives `true`)
1. `d` loads `X` (required to be `true`)
- Both initial loads precede both final loads:
1. `c` loads `X` (gives `true`)
1. `d` loads `Y` (gives `true`)
1. `c` loads `Y` (required to be `true`)
1. `d` loads `X` (required to be `true`)
- As above, but the final loads occur in a different order:
1. `c` loads `X` (gives `true`)
1. `d` loads `Y` (gives `true`)
1. `d` loads `X` (required to be `true`)
1. `c` loads `Y` (required to be `true`)
- As before, but the initial loads occur in a different order:
1. `d` loads `Y` (gives `true`)
1. `c` loads `X` (gives `true`)
1. `c` loads `Y` (required to be `true`)
1. `d` loads `X` (required to be `true`)
- As above, but the final loads occur in a different order:
1. `d` loads `Y` (gives `true`)
1. `c` loads `X` (gives `true`)
1. `d` loads `X` (required to be `true`)
1. `c` loads `Y` (required to be `true`)
- All of `d`s loads precede `c`s loads:
1. `d` loads `Y` (gives `true`)
1. `d` loads `X` (gives either `false` or `true`)
1. `c` loads `X` (gives `true`)
1. `c` loads `Y` (required to be `true`)
- All of `a`s operations precede `b`s operations:
1. `a` stores `true` into `X`
1. `a` loads `Y` (gives `false`)
1. `b` stores `true` into `Y`
1. `b` loads `X` (required to give `true`)
- All of `b`s operations precede `a`s operations:
1. `b` stores `true` into `Y`
1. `b` loads `X` (gives `false`)
1. `a` stores `true` into `X`
1. `a` loads `Y` (required to give `true`)
- The stores precede the loads,
`a`s store precedes `b`s and `a`s load precedes `b`s:
1. `a` stores `true` to `X`
1. `b` stores `true` into `Y`
1. `a` loads `Y` (required to give `true`)
1. `b` loads `X` (required to give `true`)
- The stores precede the loads,
`a`s store precedes `b`s and `b`s load precedes `a`s:
1. `a` stores `true` to `X`
1. `b` stores `true` into `Y`
1. `b` loads `X` (required to give `true`)
1. `a` loads `Y` (required to give `true`)
- The stores precede the loads,
`b`s store precedes `a`s and `a`s load precedes `b`s:
1. `b` stores `true` into `Y`
1. `a` stores `true` to `X`
1. `a` loads `Y` (required to give `true`)
1. `b` loads `X` (required to give `true`)
- The stores precede the loads,
`b`s store precedes `a`s and `b`s load precedes `a`s:
1. `b` stores `true` into `Y`
1. `a` stores `true` to `X`
1. `b` loads `X` (required to give `true`)
1. `a` loads `Y` (required to give `true`)
All the places where the load was required to give `true` were caused by a
preceding load in _S_ of the same atomic which saw `true` — otherwise, the load
would be coherence-ordered-before a load which precedes it in _S_, and that is
preceding store in _S_ of the same atomic of `true` — otherwise, the load would
be coherence-ordered-before a store which precedes it in _S_, and that is
impossible.
## The mixed-`SeqCst` special case

Loading…
Cancel
Save