notes: fence: replace variables to match 29.8

[c11tester.git] / doc / notes / fence.txt

diff --git a/doc/notes/fence.txt b/doc/notes/fence.txt
index 50a252ce42f3cd08f102e299dec8dec51ceedae8..8256735dc9834a1227e83d9e9ead0d4cefd042b9 100644 (file)
--- a/doc/notes/fence.txt
+++ b/doc/notes/fence.txt
@@ -45,68 +45,63 @@ fences can be transformed into the following 4 modification order constraints.
 29.3p4
 
 If
 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 &&
     A --rf-> B &&

-    X --sc-> Y --sb-> B
+    W --sc-> X --sb-> B

 then
 then

-    X --mo-> A
+    W --mo-> A

 
 Intuition/Implementation:
 
 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
  * 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
 
 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 &&
     A --rf-> B &&

-    X --sb-> Y --sc-> B
+    W --sb-> X --sc-> B

 then
 then

-    X --mo-> A
+    W --mo-> A

 
 Intuition/Implementation:
 
 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
  * 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
 
 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 &&
     A --rf-> B &&

-    X --sb-> Y --sc-> Z --sb-> B
+    W --sb-> X --sc-> Y --sb-> B

 then
 then

-    X --mo-> A
+    W --mo-> A

 
 Intuition/Implementation:
 
 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)
    (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)
    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
    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.3p7
 


@@ -150,9 +145,9 @@ sequence will be similarly denoted A --hrs-> B.
 29.8p2
 
 If
 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) &&
     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
 
 then
     A --sw-> B
 


@@ -163,21 +158,21 @@ Notes:
    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.

 
 29.8p3
 
 If
 
 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) &&
     is_release(A) && is_acquire(B) &&

-    A --sb-> X --hrs-> Y --rf-> B
+    A --sb-> X --hrs-> W --rf-> B

 then
     A --sw-> B
 
 then
     A --sw-> B
 


@@ -187,15 +182,15 @@ Notes:
 29.8p4
 
 If
 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) &&
     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:
 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:
 
 
 Summary notes: