notes: fence: add release/acquire fence notes
authorBrian Norris <banorris@uci.edu>
Thu, 6 Dec 2012 00:41:17 +0000 (16:41 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 6 Dec 2012 00:41:17 +0000 (16:41 -0800)
I remove the copied-and-pasted algorithm pseudocode, since I didn't feel
like it was necessary to tweak the pseudocode to include fences. I might
change my mind later.

doc/notes/fence.txt

index c6c2d4b..50a252c 100644 (file)
@@ -129,8 +129,115 @@ Intuition/Implementation:
  Release/acquire synchronization: extended to fences (29.3 p4-p7)
 **********************************************************************
 
-[INCOMPLETE]
+The C++ specification statements regarding release and acquire fences make
+extensions to release sequences, using what they call "hypothetical release
+sequences." These hypothetical release sequences are the same as normal release
+sequences, except that the "head" doesn't have to be a release: it can have any
+memory order (e.g., relaxed). This change actually simplifies our release
+sequences (for the fence case), as we don't actually have to establish a
+contiguous modification order all the way to a release operation; we just need
+to reach the same thread (via a RMW chain, for instance).
+
+The statements given in the specification regarding release and acquire fences
+do not result in totally separable conditions, so I will write down my
+semi-formal notation here along with some simple notes then present my
+implementation notes at the end.
+
+Note that we will use A --rs-> B to denote that B is in the release sequence
+headed by A (we allow A = B, unless otherwise stated). The hypothetical release
+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_release(A) && is_acquire(B) &&
+    A --sb-> X --hrs-> Y --rf-> Z --sb-> B
+then
+    A --sw-> B
+
+Notes:
+ * The fence-release A does not result in any action on its own (i.e., when it
+   is first explored); it only affects later release operations, at which point
+   we may need to associate store X with A. Thus, for every store X, we eagerly
+   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
+   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.
+
+29.8p3
+
+If
+    is_fence(A) && is_write(X) && is_write(Y) && is_read(B) &&
+    is_release(A) && is_acquire(B) &&
+    A --sb-> X --hrs-> Y --rf-> B
+then
+    A --sw-> B
+
+Notes:
+ * See the note for fence-release A in 29.8p2
+
+29.8p4
+
+If
+    is_write(A) && is_write(X) && is_read(Y) && is_fence(B) &&
+    is_release(A) && is_acquire(B) &&
+    A --rs-> X --rf-> Y --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).
+
+Summary notes:
+
+Now, noting the overlap in implementation notes between 29.8p2,3,4 and the
+similarity between release sequences and hypothetical release sequences, I can
+extend our release sequence support to provide easy facilities for
+release/acquire fence support.
+
+I extend release sequence support to include fences first by distinguishing the
+'acquire' from the 'load'; previously, release sequence searches were always
+triggered by a load-acquire operation. Now, we may have a *fence*-acquire which
+finds a previous load-*relaxed*, then follows any chain to a release sequence
+(29.8p4). Any release heads found by our existing release sequence support must
+synchronize with the fence-acquire. Any uncertain release sequences can be
+stashed (along with both the fence-acquire and the load-relaxed) as "pending" in
+the existing lists.
+
+Next I extend the release sequence support to include hypothetical release
+sequences. Note that any search for a release sequence can also search for a
+hypothetical release sequence with little additional effort (and even saving
+effort in cases where a fence-release hides a prior store-release, whose release
+sequence may be harder to establish eagerly). Because the "most recent" 
+fence-release is stashed in each ModelAction (see the fence-release note in
+29.8p2), release sequence searches can easily add the most recent fence-release
+to the release_heads vector as it explores a RMW chain. Then, once it reaches a
+thread in which it looks for a store-release, it can perform this interesting
+optimization: if the most recent store-release is sequenced before the most
+recent fence-release, then we can ignore the store-release and simply
+synchronize with the fence-release. This avoids a "contiguous MO" computation.
+
+So, with hypothetical release sequences seamlessly integrated into the release
+sequence code, we easily cover 29.8p3 (fence-release --sw-> load-acquire). Then,
+it's a simple extension to see how 29.8p2 is just a combination of the rules
+described for 29.8p3 and 29.8p4: a fence-acquire triggers a search for loads in
+its same thread; these loads then launch a series of release sequence
+searches--hypothetical (29.8p2) or real (29.8p4)--and synchronizes with all the
+release heads.
+
+The best part about all of the preceding explanations: the lazy fixups, etc.,
+can simply be re-used from existing release sequence code, with slight
+adjustments for dealing the presence of a fence-acquire preceded by a
+load-relaxed.
 
 *******************************
  Miscellaneous Notes
@@ -141,32 +248,6 @@ support consume, we must alias consume -> release
 
 fence(memory_order_relaxed) is a no-op
 
-*******************************
- Approximate Algorithm [incomplete; just copied from the (out-of-date) release
- sequence notes
-*******************************
-
-Check read-write chain...
-
-Given:
-current action = curr
-read from = rf
-Cases:
-* rf is NULL: return uncertain
-* rf is RMW:
-       - if rf is release:
-               add rf to release heads
-       - if rf is rel_acq:
-               return certain [note: we don't need to extend release sequence
-               further because this acquire will have synchronized already]
-         else
-               return (recursively) "get release sequence head of rf"
-* if rf is release:
-       add rf to release heads
-       return certain
-* else, rf is relaxed write (NOT RMW)
-  - check same thread
-
 **************************************************
  Appendix A: From the C++11 specification (N3337)
 **************************************************