Define “unsequenced” early on

And be consistent with “sequenced before” versus “sequenced-before” to
always use the hyphen.
pull/378/head
SabrinaJewson 2 years ago
parent c19184a94a
commit 2384caab54
No known key found for this signature in database
GPG Key ID: 3D5438FFA5F05564

@ -196,7 +196,7 @@ 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) relations and are represented as thin arrows
(→) on these diagrams. They are weaker than the _sequenced before_
(→) 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 coherence rules to determine which values of a memory location are valid to
read.
@ -207,8 +207,8 @@ operation) we say that the release operation _synchronized-with_ the acquire
operation, which in doing so establishes that the release operation
_happens-before_ the acquire operation. Therefore, we can say that in the first
possible execution, Thread 1s `store` synchronizes-with Thread 2s `load`,
which causes that `store` and everything sequenced before it to happen-before
the `load` and everything sequenced after it.
which causes that `store` and everything sequenced-before it to happen-before
the `load` and everything sequenced-after it.
> More formally, we can say that A happens-before B if any of the following
> conditions are true:

@ -67,8 +67,8 @@ its sequence during one possible execution can be visualized like so:
```
That double arrow in between the two boxes (`⇒`) represents that the second
statement is _sequenced after_ the first (and similarly the first statement is
_sequenced before_ the second). This is the strongest kind of ordering guarantee
statement is _sequenced-after_ the first (and similarly the first statement is
_sequenced-before_ the second). This is the strongest kind of ordering guarantee
between any two operations, and only comes about when those two operations
happen one after the other and on the same thread.
@ -96,10 +96,14 @@ sequence:
╰───────────────╯ ╰─────────────────╯
```
Note that this is **not** a representation of multiple things that _could_
happen at runtime — instead, this diagram describes exactly what _did_ happen
when the program ran once. This distinction is key, because it highlights that
even the lowest-level representation of a programs execution does not have
We can say that the prints of `A` and `B` are _unsequenced_ with regard to the
prints of `01` and `02` that occur in the second thread, since they have no
sequenced-before arrows connecting the boxes together.
Note that these diagrams are **not** a representation of multiple things that
_could_ happen at runtime — instead, this diagram describes exactly what _did_
happen when the program ran once. This distinction is key, because it highlights
that even the lowest-level representation of a programs execution does not have
a global ordering between threads; those two disconnected chains are all there
is.
@ -128,8 +132,8 @@ Thread 1 data Thread 2
╰──────╯ └────┘ ╰──────╯
```
That is, both threads read the same value of `0` from `data`, with no relative
ordering between them.
That is, both threads read the same value of `0` from `data`, and the two
operations are unsequenced — they have no relative ordering between them.
Thats reads done, so well look at the other kind of data access next: writes.
Well also return to a single thread for now, just to keep things simple.

@ -229,7 +229,7 @@ assert!(c || d);
```
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
them (caused by the sequenced-before relation), there are six possible
executions of this program:
- All of `c`s loads precede `d`s loads:
@ -277,7 +277,7 @@ 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
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
there not guaranteed to precede C in _S_.
2. The `SeqCst` operation A is sequenced-before the `Release` or `AcqRel`
@ -298,9 +298,9 @@ asterisks:
```
A happens-before, but does not strongly happen-before, C — and anything
sequenced after C will have the same treatment (unless more synchronization is
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 occuring 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.
@ -333,7 +333,7 @@ C and A) but C also doesnt happen-before it (to avoid coherence getting in th
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
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
by having D be a store).

Loading…
Cancel
Save