190708ceaf3add5cf660077f5f0ead4ccf7694ed
[c11tester.git] / 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.