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