From 2384caab54d63060327d875b08a7821e463cd51c Mon Sep 17 00:00:00 2001 From: SabrinaJewson Date: Sun, 4 Sep 2022 17:52:16 +0100 Subject: [PATCH] =?UTF-8?q?Define=20=E2=80=9Cunsequenced=E2=80=9D=20early?= =?UTF-8?q?=20on?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit And be consistent with “sequenced before” versus “sequenced-before” to always use the hyphen. --- src/atomics/acquire-release.md | 6 +++--- src/atomics/multithread.md | 20 ++++++++++++-------- src/atomics/seqcst.md | 10 +++++----- 3 files changed, 20 insertions(+), 16 deletions(-) diff --git a/src/atomics/acquire-release.md b/src/atomics/acquire-release.md index ef630a3..6bad64a 100644 --- a/src/atomics/acquire-release.md +++ b/src/atomics/acquire-release.md @@ -196,7 +196,7 @@ 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) 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 1’s `store` synchronizes-with Thread 2’s `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: diff --git a/src/atomics/multithread.md b/src/atomics/multithread.md index de82113..6c1a287 100644 --- a/src/atomics/multithread.md +++ b/src/atomics/multithread.md @@ -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 program’s 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 program’s 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. That’s reads done, so we’ll look at the other kind of data access next: writes. We’ll also return to a single thread for now, just to keep things simple. diff --git a/src/atomics/seqcst.md b/src/atomics/seqcst.md index ee039e4..4f427ff 100644 --- a/src/atomics/seqcst.md +++ b/src/atomics/seqcst.md @@ -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 doesn’t 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).