doc/notes/fence.txt

   1 -------------------------------------------------------------------------------
   2  Fence support:
   3 -------------------------------------------------------------------------------
   4
   5 Fences provide a few new modification order constraints as well as an
   6 interesting extension to release sequences, detailed in 29.3 (p4-p7) and 29.8
   7 (p2-p4). The specifications are pasted here in Appendix A and are applied to our
   8 model-checker in these notes.
   9
  10 Section 29.3 details the modification order constraints established by
  11 sequentially-consistent fences.
  12
  13 Section 29.8 details the behavior of release and acquire fences (note that
  14 memory_order_seq_cst is both release and acquire).
  15
  16 The text of these rules are provided at the end of this document for reference.
  17
  18 *******************************
  19  Backtracking requirements
  20 *******************************
  21
  22 Because we maintain the seq-cst order as consistent with the execution order,
  23 seq-cst fences cannot commute with each other, with seq-cst loads, nor with
  24 seq-cst stores; we backtrack at all such pairs.
  25
  26 Fences extend release/acquire synchronization beyond just
  27 store-release/load-acquire. We must backtrack with potentially-synchronizing
  28 fences: that is, with any pair of store- or fence-release and load- or
  29 fence-acquire, where the release comes after the acquire in the execution order
  30 (the other ordering is OK, as we will explore both behaviors; where the pair
  31 synchronize and where they don't).
  32
  33 Note that, for instance, a fence-release may synchronize with a fence-acquire
  34 only in the presence of a appropriate load/store pair (29.8p2); but the
  35 synchronization still occurs between the fences, so the backtracking
  36 requirements are only placed on the release/acquire fences themselves.
  37
  38 *******************************
  39  Seq-cst MO constraints (29.3 p4-p7)
  40 *******************************
  41
  42 The statements given in the specification regarding sequentially consistent
  43 fences can be transformed into the following 4 modification order constraints.
  44
  45 29.3p4
  46
  47 If
  48     is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
  49     is_seqcst(X) && is_seqcst(Y) && A != X &&
  50     same_loc(X, A, B) &&
  51     A --rf-> B &&
  52     X --sc-> Y --sb-> B
  53 then
  54     X --mo-> A
  55
  56 Intuition/Implementation:
  57  * We may (but don't currently) limit our considertion of X to only the most
  58    recent (in the SC order) store to the same location as A and B prior to Y
  59    (note that all prior writes will be ordered prior to X in both SC and MO)
  60  * We should consider the "most recent" seq-cst fence Y that precedes B
  61  * This search can be combined with the r_modification_order search, since we
  62    already iterate through the necessary stores X
  63
  64 29.3p5
  65
  66 If
  67     is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
  68     is_seqcst(B) && is_seqcst(Y) &&
  69     same_loc(X, A, B) &&
  70     A != X &&
  71     A --rf-> B &&
  72     X --sb-> Y --sc-> B
  73 then
  74     X --mo-> A
  75
  76 Intuition/Implementation:
  77  * We only need to examine the "most recent" seq-cst fence Y from each thread
  78  * We only need to examine the "most recent" qualifying store X that precedes Y;
  79    all other X will provide a weaker MO constraint
  80  * This search can be combined with the r_modification_order search, since we
  81    already iterate through the necessary stores X
  82
  83 For atomic operations A and B on an atomic object M, where A modifies M and B
  84 takes its value, if there is a memory_order_seq_cst fence X such that A is
  85 sequenced before X and B follows X in S, then B observes either the effects of
  86 A or a later modification of M in its modification order.
  87
  88 29.3p6
  89
  90 If
  91     is_write(A) && is_read(B) && is_write(X) && is_fence(Y) && is_fence(Z) &&
  92     is_seqcst(Y) && is_seqcst(Z) &&
  93     same_loc(X, A, B) &&
  94     A != X &&
  95     A --rf-> B &&
  96     X --sb-> Y --sc-> Z --sb-> B
  97 then
  98     X --mo-> A
  99
 100 Intuition/Implementation:
 101  * We should consider only the "most recent" fence Z in the same thread as B
 102    (prior fences may only yield the same or weaker constraints)
 103  * We may then consider the "most recent" seq-cst fence Y prior to Z (in SC order)
 104    from each thread (prior fences may only yield the same or weaker constraints)
 105  * We should consider only the "most recent" store X (to the same location as A,
 106    B) in the same thread as Y (prior stores may only yield the same or weaker
 107    constraints)
 108  * This search can be combined with the r_modification_order search, since we
 109    already iterate through the necessary stores X
 110
 111 29.3p7
 112
 113 If
 114     is_write(A) && is_write(B) && is_fence(X) && is_fence(Y) &&
 115     is_seqcst(X) && is_seqcst(Y) &&
 116     same_loc(A, B) &&
 117     A --sb-> X --sc-> Y --sb-> B
 118 then
 119     A --mo-> B
 120
 121 Intuition/Implementation:
 122  * (Similar to 29.3p6 rules, except using A/B write/write) only search for the
 123    most recent fence Y in the same thread; search for the most recent (prior to
 124    Y) fence X from each thread; search for the most recent store A prior to X
 125  * This search can be combined with the w_modification_order search, since we
 126    already iterate through the necessary stores A
 127
 128 **********************************************************************
 129  Release/acquire synchronization: extended to fences (29.3 p4-p7)
 130 **********************************************************************
 131
 132 The C++ specification statements regarding release and acquire fences make
 133 extensions to release sequences, using what they call "hypothetical release
 134 sequences." These hypothetical release sequences are the same as normal release
 135 sequences, except that the "head" doesn't have to be a release: it can have any
 136 memory order (e.g., relaxed). This change actually simplifies our release
 137 sequences (for the fence case), as we don't actually have to establish a
 138 contiguous modification order all the way to a release operation; we just need
 139 to reach the same thread (via a RMW chain, for instance).
 140
 141 The statements given in the specification regarding release and acquire fences
 142 do not result in totally separable conditions, so I will write down my
 143 semi-formal notation here along with some simple notes then present my
 144 implementation notes at the end.
 145
 146 Note that we will use A --rs-> B to denote that B is in the release sequence
 147 headed by A (we allow A = B, unless otherwise stated). The hypothetical release
 148 sequence will be similarly denoted A --hrs-> B.
 149
 150 29.8p2
 151
 152 If
 153     is_fence(A) && is_write(X) && is_write(Y) && is_read(Z) && is_fence(B) &&
 154     is_release(A) && is_acquire(B) &&
 155     A --sb-> X --hrs-> Y --rf-> Z --sb-> B
 156 then
 157     A --sw-> B
 158
 159 Notes:
 160  * The fence-release A does not result in any action on its own (i.e., when it
 161    is first explored); it only affects later release operations, at which point
 162    we may need to associate store X with A. Thus, for every store X, we eagerly
 163    record the most recent fence-release, then this record can be utilized during
 164    later (hypothetical) release sequence checks.
 165  * The fence-acquire B is more troublesome, since there may be many qualifying
 166    loads Z (loads from different locations; loads which read from different
 167    threads; etc.). Each Z may read from different hypothetical release
 168    sequences, ending in a different release A with which B should synchronize.
 169    It is difficult (but not impossible) to find good stopping conditions at
 170    which we should terminate our search for Z. However, we at least know we only
 171    need to consder Z such that:
 172        W --sb-> Z --sb-> B
 173    where W is a previous fence-acquire.
 174
 175 29.8p3
 176
 177 If
 178     is_fence(A) && is_write(X) && is_write(Y) && is_read(B) &&
 179     is_release(A) && is_acquire(B) &&
 180     A --sb-> X --hrs-> Y --rf-> B
 181 then
 182     A --sw-> B
 183
 184 Notes:
 185  * See the note for fence-release A in 29.8p2
 186
 187 29.8p4
 188
 189 If
 190     is_write(A) && is_write(X) && is_read(Y) && is_fence(B) &&
 191     is_release(A) && is_acquire(B) &&
 192     A --rs-> X --rf-> Y --sb-> B
 193 then
 194     A --sw-> B
 195
 196 Notes:
 197  * See the note for fence-acquire B in 29.8p2. The A, Z, and B in 29.8p2
 198    correspond to A, Y, and B in this rule (29.8p4).
 199
 200 Summary notes:
 201
 202 Now, noting the overlap in implementation notes between 29.8p2,3,4 and the
 203 similarity between release sequences and hypothetical release sequences, I can
 204 extend our release sequence support to provide easy facilities for
 205 release/acquire fence support.
 206
 207 I extend release sequence support to include fences first by distinguishing the
 208 'acquire' from the 'load'; previously, release sequence searches were always
 209 triggered by a load-acquire operation. Now, we may have a *fence*-acquire which
 210 finds a previous load-*relaxed*, then follows any chain to a release sequence
 211 (29.8p4). Any release heads found by our existing release sequence support must
 212 synchronize with the fence-acquire. Any uncertain release sequences can be
 213 stashed (along with both the fence-acquire and the load-relaxed) as "pending" in
 214 the existing lists.
 215
 216 Next I extend the release sequence support to include hypothetical release
 217 sequences. Note that any search for a release sequence can also search for a
 218 hypothetical release sequence with little additional effort (and even saving
 219 effort in cases where a fence-release hides a prior store-release, whose release
 220 sequence may be harder to establish eagerly). Because the "most recent"
 221 fence-release is stashed in each ModelAction (see the fence-release note in
 222 29.8p2), release sequence searches can easily add the most recent fence-release
 223 to the release_heads vector as it explores a RMW chain. Then, once it reaches a
 224 thread in which it looks for a store-release, it can perform this interesting
 225 optimization: if the most recent store-release is sequenced before the most
 226 recent fence-release, then we can ignore the store-release and simply
 227 synchronize with the fence-release. This avoids a "contiguous MO" computation.
 228
 229 So, with hypothetical release sequences seamlessly integrated into the release
 230 sequence code, we easily cover 29.8p3 (fence-release --sw-> load-acquire). Then,
 231 it's a simple extension to see how 29.8p2 is just a combination of the rules
 232 described for 29.8p3 and 29.8p4: a fence-acquire triggers a search for loads in
 233 its same thread; these loads then launch a series of release sequence
 234 searches--hypothetical (29.8p2) or real (29.8p4)--and synchronizes with all the
 235 release heads.
 236
 237 The best part about all of the preceding explanations: the lazy fixups, etc.,
 238 can simply be re-used from existing release sequence code, with slight
 239 adjustments for dealing the presence of a fence-acquire preceded by a
 240 load-relaxed.
 241
 242 *******************************
 243  Miscellaneous Notes
 244 *******************************
 245
 246 fence(memory_order_consume) acts like memory_order_release, so if we ever
 247 support consume, we must alias consume -> release
 248
 249 fence(memory_order_relaxed) is a no-op
 250
 251 **************************************************
 252  Appendix A: From the C++11 specification (N3337)
 253 **************************************************
 254
 255 -------------
 256 Section 29.3
 257 -------------
 258
 259 29.3p4
 260
 261 For an atomic operation B that reads the value of an atomic object M, if there
 262 is a memory_order_seq_cst fence X sequenced before B, then B observes either
 263 the last memory_order_seq_cst modification of M preceding X in the total order
 264 S or a later modification of M in its modification order.
 265
 266 29.3p5
 267
 268 For atomic operations A and B on an atomic object M, where A modifies M and B
 269 takes its value, if there is a memory_order_seq_cst fence X such that A is
 270 sequenced before X and B follows X in S, then B observes either the effects of
 271 A or a later modification of M in its modification order.
 272
 273 29.3p6
 274
 275 For atomic operations A and B on an atomic object M, where A modifies M and B
 276 takes its value, if there are memory_order_seq_cst fences X and Y such that A
 277 is sequenced before X, Y is sequenced before B, and X precedes Y in S, then B
 278 observes either the effects of A or a later modification of M in its
 279 modification order.
 280
 281 29.3p7
 282
 283 For atomic operations A and B on an atomic object M, if there are
 284 memory_order_seq_cst fences X and Y such that A is sequenced before X, Y is
 285 sequenced before B, and X precedes Y in S, then B occurs later than A in the
 286 modification order of M.
 287
 288 -------------
 289 Section 29.8
 290 -------------
 291
 292 29.8p2
 293
 294 A release fence A synchronizes with an acquire fence B if there exist atomic
 295 operations X and Y, both operating on some atomic object M, such that A is
 296 sequenced before X, X modifies M, Y is sequenced before B, and Y reads the value
 297 written by X or a value written by any side effect in the hypothetical release
 298 sequence X would head if it were a release operation.
 299
 300 29.8p3
 301
 302 A release fence A synchronizes with an atomic operation B that performs an
 303 acquire operation on an atomic object M if there exists an atomic operation X
 304 such that A is sequenced before X, X modifies M, and B reads the value written
 305 by X or a value written by any side effect in the hypothetical release sequence
 306 X would head if it were a release operation.
 307
 308 29.8p4
 309
 310 An atomic operation A that is a release operation on an atomic object M
 311 synchronizes with an acquire fence B if there exists some atomic operation X on
 312 M such that X is sequenced before B and reads the value written by A or a value
 313 written by any side effect in the release sequence headed by A.