29.3p4
If
- is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
- is_seqcst(X) && is_seqcst(Y) && A != X &&
- same_loc(X, A, B) &&
+ is_write(A) && is_read(B) && is_write(W) && is_fence(X) &&
+ is_seqcst(W) && is_seqcst(X) && A != W &&
+ same_loc(W, A, B) &&
A --rf-> B &&
- X --sc-> Y --sb-> B
+ W --sc-> X --sb-> B
then
- X --mo-> A
+ W --mo-> A
Intuition/Implementation:
- * We may (but don't currently) limit our considertion of X to only the most
- recent (in the SC order) store to the same location as A and B prior to Y
- (note that all prior writes will be ordered prior to X in both SC and MO)
- * We should consider the "most recent" seq-cst fence Y that precedes B
+ * We may (but don't currently) limit our considertion of W to only the most
+ recent (in the SC order) store to the same location as A and B prior to X
+ (note that all prior writes will be ordered prior to W in both SC and MO)
+ * We should consider the "most recent" seq-cst fence X that precedes B
* This search can be combined with the r_modification_order search, since we
- already iterate through the necessary stores X
+ already iterate through the necessary stores W
29.3p5
If
- is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
- is_seqcst(B) && is_seqcst(Y) &&
- same_loc(X, A, B) &&
- A != X &&
+ is_write(A) && is_read(B) && is_write(W) && is_fence(X) &&
+ is_seqcst(B) && is_seqcst(X) &&
+ same_loc(W, A, B) &&
+ A != W &&
A --rf-> B &&
- X --sb-> Y --sc-> B
+ W --sb-> X --sc-> B
then
- X --mo-> A
+ W --mo-> A
Intuition/Implementation:
- * We only need to examine the "most recent" seq-cst fence Y from each thread
- * We only need to examine the "most recent" qualifying store X that precedes Y;
- all other X will provide a weaker MO constraint
+ * We only need to examine the "most recent" seq-cst fence X from each thread
+ * We only need to examine the "most recent" qualifying store W that precedes X;
+ all other W will provide a weaker MO constraint
* This search can be combined with the r_modification_order search, since we
- already iterate through the necessary stores X
-
-For atomic operations A and B on an atomic object M, where A modifies M and B
-takes its value, if there is a memory_order_seq_cst fence X such that A is
-sequenced before X and B follows X in S, then B observes either the effects of
-A or a later modification of M in its modification order.
+ already iterate through the necessary stores W
29.3p6
If
- is_write(A) && is_read(B) && is_write(X) && is_fence(Y) && is_fence(Z) &&
- is_seqcst(Y) && is_seqcst(Z) &&
- same_loc(X, A, B) &&
- A != X &&
+ is_write(A) && is_read(B) && is_write(W) && is_fence(X) && is_fence(Y) &&
+ is_seqcst(X) && is_seqcst(Y) &&
+ same_loc(W, A, B) &&
+ A != W &&
A --rf-> B &&
- X --sb-> Y --sc-> Z --sb-> B
+ W --sb-> X --sc-> Y --sb-> B
then
- X --mo-> A
+ W --mo-> A
Intuition/Implementation:
- * We should consider only the "most recent" fence Z in the same thread as B
+ * We should consider only the "most recent" fence Y in the same thread as B
(prior fences may only yield the same or weaker constraints)
- * We may then consider the "most recent" seq-cst fence Y prior to Z (in SC order)
+ * We may then consider the "most recent" seq-cst fence X prior to Y (in SC order)
from each thread (prior fences may only yield the same or weaker constraints)
- * We should consider only the "most recent" store X (to the same location as A,
- B) in the same thread as Y (prior stores may only yield the same or weaker
+ * We should consider only the "most recent" store W (to the same location as A,
+ B) in the same thread as X (prior stores may only yield the same or weaker
constraints)
* This search can be combined with the r_modification_order search, since we
- already iterate through the necessary stores X
+ already iterate through the necessary stores W
29.3p7
29.8p2
If
- is_fence(A) && is_write(X) && is_write(Y) && is_read(Z) && is_fence(B) &&
+ is_fence(A) && is_write(X) && is_write(W) && is_read(Y) && is_fence(B) &&
is_release(A) && is_acquire(B) &&
- A --sb-> X --hrs-> Y --rf-> Z --sb-> B
+ A --sb-> X --hrs-> W --rf-> Y --sb-> B
then
A --sw-> B
record the most recent fence-release, then this record can be utilized during
later (hypothetical) release sequence checks.
* The fence-acquire B is more troublesome, since there may be many qualifying
- loads Z (loads from different locations; loads which read from different
- threads; etc.). Each Z may read from different hypothetical release
+ loads Y (loads from different locations; loads which read from different
+ threads; etc.). Each Y may read from different hypothetical release
sequences, ending in a different release A with which B should synchronize.
It is difficult (but not impossible) to find good stopping conditions at
- which we should terminate our search for Z. However, we at least know we only
- need to consder Z such that:
- W --sb-> Z --sb-> B
- where W is a previous fence-acquire.
+ which we should terminate our search for Y. However, we at least know we only
+ need to consder Y such that:
+ V --sb-> Y --sb-> B
+ where V is a previous fence-acquire.
29.8p3
If
- is_fence(A) && is_write(X) && is_write(Y) && is_read(B) &&
+ is_fence(A) && is_write(X) && is_write(W) && is_read(B) &&
is_release(A) && is_acquire(B) &&
- A --sb-> X --hrs-> Y --rf-> B
+ A --sb-> X --hrs-> W --rf-> B
then
A --sw-> B
29.8p4
If
- is_write(A) && is_write(X) && is_read(Y) && is_fence(B) &&
+ is_write(A) && is_write(W) && is_read(X) && is_fence(B) &&
is_release(A) && is_acquire(B) &&
- A --rs-> X --rf-> Y --sb-> B
+ A --rs-> W --rf-> X --sb-> B
then
A --sw-> B
Notes:
- * See the note for fence-acquire B in 29.8p2. The A, Z, and B in 29.8p2
- correspond to A, Y, and B in this rule (29.8p4).
+ * See the note for fence-acquire B in 29.8p2. The A, Y, and B in 29.8p2
+ correspond to A, X, and B in this rule (29.8p4).
Summary notes: