From b11f506f3f54562662bb0d790bcd5afd898d48ac Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 6 Dec 2012 12:13:25 -0800 Subject: [PATCH] notes: fence: replace variables to match 29.8 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 | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/doc/notes/fence.txt b/doc/notes/fence.txt index acc3e20b..8256735d 100644 --- a/doc/notes/fence.txt +++ b/doc/notes/fence.txt @@ -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: -- 2.34.1