summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
e2f5717)
I had some remaining edits to do for my notes 29.8, to match back with
the specification's variables (X, Y, A, B).
- 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) &&
is_release(A) && is_acquire(B) &&
- A --sb-> X --hrs-> Y --rf-> Z --sb-> B
+ A --sb-> X --hrs-> W --rf-> Y --sb-> 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
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
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.
- 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) &&
is_release(A) && is_acquire(B) &&
- A --sb-> X --hrs-> Y --rf-> B
+ A --sb-> X --hrs-> W --rf-> B
- 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) &&
is_release(A) && is_acquire(B) &&
- A --rs-> X --rf-> Y --sb-> B
+ A --rs-> W --rf-> X --sb-> B
- * 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).