notes: fence: replace variables to match 29.8
authorBrian Norris <banorris@uci.edu>
Thu, 6 Dec 2012 20:13:25 +0000 (12:13 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 6 Dec 2012 20:13:25 +0000 (12:13 -0800)
I had some remaining edits to do for my notes 29.8, to match back with
the specification's variables (X, Y, A, B).

doc/notes/fence.txt

index acc3e20..8256735 100644 (file)
@@ -145,9 +145,9 @@ sequence will be similarly denoted A --hrs-> B.
 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
 
@@ -158,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
-   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
 
@@ -182,15 +182,15 @@ Notes:
 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: