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 [INCOMPLETE]
 133
 134
 135 *******************************
 136  Miscellaneous Notes
 137 *******************************
 138
 139 fence(memory_order_consume) acts like memory_order_release, so if we ever
 140 support consume, we must alias consume -> release
 141
 142 fence(memory_order_relaxed) is a no-op
 143
 144 *******************************
 145  Approximate Algorithm [incomplete; just copied from the (out-of-date) release
 146  sequence notes
 147 *******************************
 148
 149 Check read-write chain...
 150
 151 Given:
 152 current action = curr
 153 read from = rf
 154 Cases:
 155 * rf is NULL: return uncertain
 156 * rf is RMW:
 157         - if rf is release:
 158                 add rf to release heads
 159         - if rf is rel_acq:
 160                 return certain [note: we don't need to extend release sequence
 161                 further because this acquire will have synchronized already]
 162           else
 163                 return (recursively) "get release sequence head of rf"
 164 * if rf is release:
 165         add rf to release heads
 166         return certain
 167 * else, rf is relaxed write (NOT RMW)
 168   - check same thread
 169
 170 **************************************************
 171  Appendix A: From the C++11 specification (N3337)
 172 **************************************************
 173
 174 -------------
 175 Section 29.3
 176 -------------
 177
 178 29.3p4
 179
 180 For an atomic operation B that reads the value of an atomic object M, if there
 181 is a memory_order_seq_cst fence X sequenced before B, then B observes either
 182 the last memory_order_seq_cst modification of M preceding X in the total order
 183 S or a later modification of M in its modification order.
 184
 185 29.3p5
 186
 187 For atomic operations A and B on an atomic object M, where A modifies M and B
 188 takes its value, if there is a memory_order_seq_cst fence X such that A is
 189 sequenced before X and B follows X in S, then B observes either the effects of
 190 A or a later modification of M in its modification order.
 191
 192 29.3p6
 193
 194 For atomic operations A and B on an atomic object M, where A modifies M and B
 195 takes its value, if there are memory_order_seq_cst fences X and Y such that A
 196 is sequenced before X, Y is sequenced before B, and X precedes Y in S, then B
 197 observes either the effects of A or a later modification of M in its
 198 modification order.
 199
 200 29.3p7
 201
 202 For atomic operations A and B on an atomic object M, if there are
 203 memory_order_seq_cst fences X and Y such that A is sequenced before X, Y is
 204 sequenced before B, and X precedes Y in S, then B occurs later than A in the
 205 modification order of M.
 206
 207 -------------
 208 Section 29.8
 209 -------------
 210
 211 29.8p2
 212
 213 A release fence A synchronizes with an acquire fence B if there exist atomic
 214 operations X and Y, both operating on some atomic object M, such that A is
 215 sequenced before X, X modifies M, Y is sequenced before B, and Y reads the value
 216 written by X or a value written by any side effect in the hypothetical release
 217 sequence X would head if it were a release operation.
 218
 219 29.8p3
 220
 221 A release fence A synchronizes with an atomic operation B that performs an
 222 acquire operation on an atomic object M if there exists an atomic operation X
 223 such that A is sequenced before X, X modifies M, and B reads the value written
 224 by X or a value written by any side effect in the hypothetical release sequence
 225 X would head if it were a release operation.
 226
 227 29.8p4
 228
 229 An atomic operation A that is a release operation on an atomic object M
 230 synchronizes with an acquire fence B if there exists some atomic operation X on
 231 M such that X is sequenced before B and reads the value written by A or a value
 232 written by any side effect in the release sequence headed by A.