“happens before” → “happens-before”

pull/378/head
SabrinaJewson 2 years ago
parent afe0ee2bf0
commit c1129e31c8
No known key found for this signature in database
GPG Key ID: 3D5438FFA5F05564

@ -195,16 +195,16 @@ Thread 1 a Thread 2 ┃ Thread 1 a Thread 2
```
These arrows are a new kind of arrow we
havent seen yet; they are known as _happens before_ (or happens after)
havent seen yet; they are known as _happens-before_ (or happens-after)
relations and are represented as thin arrows (→) on these diagrams. They are
weaker than the _sequenced before_ double-arrows (⇒) that occur inside a single
thread, but can still be used with the arrow rules to determine which values of
a memory location are valid to read. We can say that in the first possible
execution, Thread 1s `store` (and everything sequenced before that) _happens
before_ Thread 2s load (and everything sequenced after that).
execution, Thread 1s `store` (and everything sequenced before that)
_happens-before_ Thread 2s load (and everything sequenced after that).
There is one more rule required for these to be useful, and that is _release
sequences_: after a release store is performed on an atomic, happens before
sequences_: after a release store is performed on an atomic, happens-before
arrows will connect together each subsequent value of the atomic as long as the
new value is caused by an RMW and not just a plain store.
@ -233,9 +233,9 @@ Thread 1 locked data Thread 2
```
We now can trace back along the reverse direction of arrows from the `guard`
bubble to the `+= 1` bubble; we have established that Thread 2s load happens
after the `+= 1` side effect. This both avoids the data race and gives the
guarantee that `1` will be always read by Thread 2 (as long as locks after
bubble to the `+= 1` bubble; we have established that Thread 2s load
happens-after the `+= 1` side effect. This both avoids the data race and gives
the guarantee that `1` will be always read by Thread 2 (as long as locks after
Thread 1, of course).
However, that is not the only execution of the program possible. Even with this

@ -105,8 +105,8 @@ do). It is in contrast to modification orders, which are similarly total but
only scoped to a single atomic rather than the whole program.
Other than an edge case involving `SeqCst` mixed with weaker orderings (detailed
in the next section), _S_ is primarily controlled by the happens before
relations in a program: this means that if an action _A_ happens before an
in the next section), _S_ is primarily controlled by the happens-before
relations in a program: this means that if an action _A_ happens-before an
action _B_, it is also guaranteed to appear before _B_ in _S_. Other than that
restriction, _S_ is unspecified and will be chosen arbitrarily during execution.
@ -214,18 +214,18 @@ impossible.
## The mixed-`SeqCst` special case
As Ive been alluding to for a while, I wasnt being totally truthful when I
said that _S_ is consistent with happens before relations — in reality, it is
only consistent with _strongly happens before_ relations, which presents a
subtly-defined subset of happens before relations. In particular, it excludes
said that _S_ is consistent with happens-before relations — in reality, it is
only consistent with _strongly happens-before_ relations, which presents a
subtly-defined subset of happens-before relations. In particular, it excludes
two situations:
1. The `SeqCst` operation A synchronizes-with an `Acquire` or `AcqRel` operation
B which is sequenced before another `SeqCst` operation C. Here, despite the
fact that A happens before C, A does not _strongly_ happen before C and so is
fact that A happens-before C, A does not _strongly_ happen-before C and so is
there not guaranteed to precede C in _S_.
2. The `SeqCst` operation A is sequenced-before the `Release` or `AcqRel`
operation B, which synchronizes-with another `SeqCst` operation C. Similarly,
despite the fact that A happens before C, A might not precede C in _S_.
despite the fact that A happens-before C, A might not precede C in _S_.
The first situation is illustrated below, with `SeqCst` accesses repesented with
asterisks:
@ -240,12 +240,12 @@ asterisks:
╰─────╯
```
A happens before, but does not strongly happen before, C — and anything
A happens-before, but does not strongly happen-before, C — and anything
sequenced after C will have the same treatment (unless more synchronization is
used). This means that C is actually allowed to _precede_ A in _S_, despite
conceptually happening after it. However, anything sequenced before A, because
conceptually occuring after it. However, anything sequenced before A, because
there is at least one sequence on either side of the synchronization, will
strongly happen before C.
strongly happen-before C.
But this is all highly theoretical at the moment, so lets make an example to
show how that rule can actually affect the execution of code. So, if C were to
@ -272,12 +272,12 @@ _S_ after all.
So somehow, to observe this difference we need to have a _different_ `SeqCst`
operation, lets call it E, be the one that loads from `x`, where C is
guaranteed to precede it in _S_ (so we can observe the “weird” state in between
C and A) but C also doesnt happen before it (to avoid coherence getting in the
C and A) but C also doesnt happen-before it (to avoid coherence getting in the
way) — and to do that, all we have to do is have C appear before a `SeqCst`
operation D in the modification order of another atomic, but have D be a store
so as to avoid C synchronizing with it, and then our desired load E can simply
be sequenced after D (this will carry over the “precedes in _S_” guarantee, but
does not restore the happens after relation to C since that was already dropped
does not restore the happens-after relation to C since that was already dropped
by having D be a store).
In diagram form, that looks like this:
@ -321,7 +321,7 @@ assert_eq!(X.load(SeqCst), 0); // E
The second situation listed above has very similar consequences. Its abstract
form is the following execution in which A is not guaranteed to precede C in
_S_, despite A happening before C:
_S_, despite A happening-before C:
```text
t_1 x t_2
@ -335,7 +335,7 @@ _S_, despite A happening before C:
Similarly to before, we cant just have A access `x` to show why A not
necessarily preceding C in _S_ matters; instead, we have to introduce a second
atomic and third thread to break the happens before chain first. And finally, a
atomic and third thread to break the happens-before chain first. And finally, a
single relaxed load F at the end is added just to prove that the weird execution
actually happened (leaving `x` as 2 instead of 1).

Loading…
Cancel
Save