diff --git a/src/atomics/acquire-release.md b/src/atomics/acquire-release.md index 9a7e24e..074fa9d 100644 --- a/src/atomics/acquire-release.md +++ b/src/atomics/acquire-release.md @@ -195,16 +195,16 @@ Thread 1 a Thread 2 ┃ Thread 1 a Thread 2 ``` These arrows are a new kind of arrow we -haven’t seen yet; they are known as _happens before_ (or happens after) +haven’t 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 1’s `store` (and everything sequenced before that) _happens -before_ Thread 2’s load (and everything sequenced after that). +execution, Thread 1’s `store` (and everything sequenced before that) +_happens-before_ Thread 2’s 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 2’s 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 2’s 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 diff --git a/src/atomics/seqcst.md b/src/atomics/seqcst.md index 6be9593..7c3dd6a 100644 --- a/src/atomics/seqcst.md +++ b/src/atomics/seqcst.md @@ -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 I’ve been alluding to for a while, I wasn’t 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 let’s 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, let’s 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 doesn’t happen before it (to avoid coherence getting in the +C and A) but C also doesn’t 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 can’t 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).