doc/notes/fence.txt

   1 -------------------------------------------------------------------------------
   2  Fence support:
   3 -------------------------------------------------------------------------------
   4
   5 [refer to release sequence notes for some definitions and similar (but simpler)
   6 algorithm]
   7
   8 Fences provide a few new modification order constraints as well as an
   9 interesting extension to release sequences, detailed in 29.3 (p4-p7) and 29.8
  10 (p2-p4).
  11
  12 Section 29.3 details the modification order constraints established by
  13 sequentially-consistent fences.
  14
  15 Section 29.8 details the behavior of release and acquire fences (note that
  16 memory_order_seq_cst is both release and acquire).
  17
  18 The text of these rules are provided at the end of this document for reference.
  19
  20 *******************************
  21  Backtracking requirements
  22 *******************************
  23
  24 Because we maintain the seq-cst order as consistent with the execution order,
  25 seq-cst fences cannot commute with each other, with seq-cst loads, nor with
  26 seq-cst stores; we backtrack at all such pairs.
  27
  28 Fences extend release/acquire synchronization beyond just
  29 store-release/load-acquire. We must backtrack with potentially-synchronizing
  30 fences: that is, with any pair of store- or fence-release and load- or
  31 fence-acquire, where the release comes after the acquire in the execution order
  32 (the other ordering is OK, as we will explore both behaviors; where the pair
  33 synchronize and where they don't).
  34
  35 Note that, for instance, a fence-release may synchronize with a fence-acquire
  36 only in the presence of a appropriate load/store pair (29.8p2); but the
  37 synchronization still occurs between the fences, so the backtracking
  38 requirements are only placed on the release/acquire fences themselves.
  39
  40 *******************************
  41  Seq-cst MO constraints (29.3 p4-p7)
  42 *******************************
  43
  44 The statements given in the specification regarding sequentially consistent
  45 fences can be transformed into the following 4 modification order constraints.
  46
  47 29.3p4
  48
  49 If
  50     is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
  51     is_seqcst(X) && is_seqcst(Y) && A != X &&
  52     same_loc(X, A, B) &&
  53     A --rf-> B &&
  54     X --sc-> Y --sb-> B
  55 then
  56     X --mo-> A
  57
  58 Intuition/Implementation:
  59  * We may (but don't currently) limit our considertion of X to only the most
  60    recent (in the SC order) store to the same location as A and B prior to Y
  61    (note that all prior writes will be ordered prior to X in both SC and MO)
  62  * We should consider the "most recent" seq-cst fence Y that precedes B
  63  * This search can be combined with the r_modification_order search, since we
  64    already iterate through the necessary stores X
  65
  66 29.3p5
  67
  68 If
  69     is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
  70     is_seqcst(B) && is_seqcst(Y) &&
  71     same_loc(X, A, B) &&
  72     A != X &&
  73     A --rf-> B &&
  74     X --sb-> Y --sc-> B
  75 then
  76     X --mo-> A
  77
  78 Intuition/Implementation:
  79  * We only need to examine the "most recent" seq-cst fence Y from each thread
  80  * We only need to examine the "most recent" qualifying store X that precedes Y;
  81    all other X will provide a weaker MO constraint
  82  * This search can be combined with the r_modification_order search, since we
  83    already iterate through the necessary stores X
  84
  85 For atomic operations A and B on an atomic object M, where A modifies M and B
  86 takes its value, if there is a memory_order_seq_cst fence X such that A is
  87 sequenced before X and B follows X in S, then B observes either the effects of
  88 A or a later modification of M in its modification order.
  89
  90 29.3p6
  91
  92 If
  93     is_write(A) && is_read(B) && is_write(X) && is_fence(Y) && is_fence(Z) &&
  94     is_seqcst(Y) && is_seqcst(Z) &&
  95     same_loc(X, A, B) &&
  96     A != X &&
  97     A --rf-> B &&
  98     X --sb-> Y --sc-> Z --sb-> B
  99 then
 100     X --mo-> A
 101
 102 Intuition/Implementation:
 103  * We should consider only the "most recent" fence Z in the same thread as B
 104    (prior fences may only yield the same or weaker constraints)
 105  * We may then consider the "most recent" seq-cst fence Y prior to Z (in SC order)
 106    from each thread (prior fences may only yield the same or weaker constraints)
 107  * We should consider only the "most recent" store X (to the same location as A,
 108    B) in the same thread as Y (prior stores may only yield the same or weaker
 109    constraints)
 110  * This search can be combined with the r_modification_order search, since we
 111    already iterate through the necessary stores X
 112
 113 29.3p7
 114
 115 If
 116     is_write(A) && is_write(B) && is_fence(X) && is_fence(Y) &&
 117     is_seqcst(X) && is_seqcst(Y) &&
 118     same_loc(A, B) &&
 119     A --sb-> X --sc-> Y --sb-> B
 120 then
 121     A --mo-> B
 122
 123 Intuition/Implementation:
 124  * (Similar to 29.3p6 rules, except using A/B write/write) only search for the
 125    most recent fence Y in the same thread; search for the most recent (prior to
 126    Y) fence X from each thread; search for the most recent store A prior to X
 127  * This search can be combined with the w_modification_order search, since we
 128    already iterate through the necessary stores A
 129
 130 **********************************************************************
 131  Release/acquire synchronization: extended to fences (29.3 p4-p7)
 132 **********************************************************************
 133
 134 [INCOMPLETE]
 135
 136
 137 *******************************
 138  Miscellaneous Notes
 139 *******************************
 140
 141 fence(memory_order_consume) acts like memory_order_release, so if we ever
 142 support consume, we must alias consume -> release
 143
 144 fence(memory_order_relaxed) is a no-op
 145
 146 *******************************
 147  Approximate Algorithm [incomplete; just copied from the (out-of-date) release
 148  sequence notes
 149 *******************************
 150
 151 Check read-write chain...
 152
 153 Given:
 154 current action = curr
 155 read from = rf
 156 Cases:
 157 * rf is NULL: return uncertain
 158 * rf is RMW:
 159         - if rf is release:
 160                 add rf to release heads
 161         - if rf is rel_acq:
 162                 return certain [note: we don't need to extend release sequence
 163                 further because this acquire will have synchronized already]
 164           else
 165                 return (recursively) "get release sequence head of rf"
 166 * if rf is release:
 167         add rf to release heads
 168         return certain
 169 * else, rf is relaxed write (NOT RMW)
 170   - check same thread
 171
 172 **************************************
 173  From the C++11 specification (N3337)
 174 **************************************
 175
 176 -------------
 177 Section 29.3
 178 -------------
 179
 180 29.3p4
 181
 182 For an atomic operation B that reads the value of an atomic object M, if there
 183 is a memory_order_seq_cst fence X sequenced before B, then B observes either
 184 the last memory_order_seq_cst modification of M preceding X in the total order
 185 S or a later modification of M in its modification order.
 186
 187 29.3p5
 188
 189 For atomic operations A and B on an atomic object M, where A modifies M and B
 190 takes its value, if there is a memory_order_seq_cst fence X such that A is
 191 sequenced before X and B follows X in S, then B observes either the effects of
 192 A or a later modification of M in its modification order.
 193
 194 29.3p6
 195
 196 For atomic operations A and B on an atomic object M, where A modifies M and B
 197 takes its value, if there are memory_order_seq_cst fences X and Y such that A
 198 is sequenced before X, Y is sequenced before B, and X precedes Y in S, then B
 199 observes either the effects of A or a later modification of M in its
 200 modification order.
 201
 202 29.3p7
 203
 204 For atomic operations A and B on an atomic object M, if there are
 205 memory_order_seq_cst fences X and Y such that A is sequenced before X, Y is
 206 sequenced before B, and X precedes Y in S, then B occurs later than A in the
 207 modification order of M.
 208
 209 -------------
 210 Section 29.8
 211 -------------
 212
 213 29.8p2
 214
 215 A release fence A synchronizes with an acquire fence B if there exist atomic
 216 operations X and Y, both operating on some atomic object M, such that A is
 217 sequenced before X, X modifies M, Y is sequenced before B, and Y reads the value
 218 written by X or a value written by any side effect in the hypothetical release
 219 sequence X would head if it were a release operation.
 220
 221 29.8p3
 222
 223 A release fence A synchronizes with an atomic operation B that performs an
 224 acquire operation on an atomic object M if there exists an atomic operation X
 225 such that A is sequenced before X, X modifies M, and B reads the value written
 226 by X or a value written by any side effect in the hypothetical release sequence
 227 X would head if it were a release operation.
 228
 229 29.8p4
 230
 231 An atomic operation A that is a release operation on an atomic object M
 232 synchronizes with an acquire fence B if there exists some atomic operation X on
 233 M such that X is sequenced before B and reads the value written by A or a value
 234 written by any side effect in the release sequence headed by A.