+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(W) && is_read(Y) && is_fence(B) &&
+ is_release(A) && is_acquire(B) &&
+ A --sb-> X --hrs-> W --rf-> Y --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 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 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(W) && is_read(B) &&
+ is_release(A) && is_acquire(B) &&
+ A --sb-> X --hrs-> W --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(W) && is_read(X) && is_fence(B) &&
+ is_release(A) && is_acquire(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, Y, and B in 29.8p2
+ correspond to A, X, 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.