1 -------------------------------------------------------------------------------
3 -------------------------------------------------------------------------------
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.
10 Section 29.3 details the modification order constraints established by
11 sequentially-consistent fences.
13 Section 29.8 details the behavior of release and acquire fences (note that
14 memory_order_seq_cst is both release and acquire).
16 The text of these rules are provided at the end of this document for reference.
18 *******************************
19 Backtracking requirements
20 *******************************
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.
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).
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.
38 *******************************
39 Seq-cst MO constraints (29.3 p4-p7)
40 *******************************
42 The statements given in the specification regarding sequentially consistent
43 fences can be transformed into the following 4 modification order constraints.
48 is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
49 is_seqcst(X) && is_seqcst(Y) && A != X &&
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
67 is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
68 is_seqcst(B) && is_seqcst(Y) &&
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
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.
91 is_write(A) && is_read(B) && is_write(X) && is_fence(Y) && is_fence(Z) &&
92 is_seqcst(Y) && is_seqcst(Z) &&
96 X --sb-> Y --sc-> Z --sb-> B
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
108 * This search can be combined with the r_modification_order search, since we
109 already iterate through the necessary stores X
114 is_write(A) && is_write(B) && is_fence(X) && is_fence(Y) &&
115 is_seqcst(X) && is_seqcst(Y) &&
117 A --sb-> X --sc-> Y --sb-> B
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
128 **********************************************************************
129 Release/acquire synchronization: extended to fences (29.3 p4-p7)
130 **********************************************************************
135 *******************************
137 *******************************
139 fence(memory_order_consume) acts like memory_order_release, so if we ever
140 support consume, we must alias consume -> release
142 fence(memory_order_relaxed) is a no-op
144 *******************************
145 Approximate Algorithm [incomplete; just copied from the (out-of-date) release
147 *******************************
149 Check read-write chain...
152 current action = curr
155 * rf is NULL: return uncertain
158 add rf to release heads
160 return certain [note: we don't need to extend release sequence
161 further because this acquire will have synchronized already]
163 return (recursively) "get release sequence head of rf"
165 add rf to release heads
167 * else, rf is relaxed write (NOT RMW)
170 **************************************************
171 Appendix A: From the C++11 specification (N3337)
172 **************************************************
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.
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.
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
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.
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.
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.
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.