1 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
3 cat .input.define >> pan.ltl
5 spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl
6 cp urcu_free_no_rmb.define .input.define
7 cat .input.define > .input.spin
8 cat DEFINES >> .input.spin
9 cat urcu.spin >> .input.spin
10 rm -f .input.spin.trail
11 spin -a -X -N pan.ltl .input.spin
13 gcc -O2 -w -DHASH64 -o pan pan.c
14 ./pan -a -v -c1 -X -m10000000 -w20
15 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
16 (never claims generated from LTL formulae are stutter-invariant)
17 depth 0: Claim reached state 5 (line 1258)
18 Depth= 7365 States= 1e+06 Transitions= 1.38e+08 Memory= 550.432 t= 168 R= 6e+03
19 Depth= 7365 States= 2e+06 Transitions= 4.31e+08 Memory= 634.318 t= 540 R= 4e+03
20 pan: claim violated! (at depth 1624)
21 pan: wrote .input.spin.trail
23 (Spin Version 5.1.7 -- 23 December 2008)
24 Warning: Search not completed
25 + Partial Order Reduction
27 Full statespace search for:
29 assertion violations + (if within scope of claim)
30 acceptance cycles + (fairness disabled)
31 invalid end states - (disabled by never claim)
33 State-vector 88 byte, depth reached 7365, errors: 1
34 2266036 states, stored
35 5.03936e+08 states, matched
36 5.0620203e+08 transitions (= stored+matched)
37 2.8832147e+09 atomic steps
38 hash conflicts: 3.6698737e+08 (resolved)
40 Stats on memory usage (in Megabytes):
41 250.683 equivalent memory usage for states (stored*(State-vector + overhead))
42 191.039 actual memory usage for states (compression: 76.21%)
43 state-vector as stored = 60 byte + 28 byte overhead
44 8.000 memory used for hash table (-w20)
45 457.764 memory used for DFS stack (-m10000000)
46 656.682 total actual memory usage
48 unreached in proctype urcu_reader
49 line 250, "pan.___", state 30, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
50 line 258, "pan.___", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
51 line 262, "pan.___", state 61, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
52 line 227, "pan.___", state 77, "(1)"
53 line 231, "pan.___", state 85, "(1)"
54 line 235, "pan.___", state 97, "(1)"
55 line 239, "pan.___", state 105, "(1)"
56 line 395, "pan.___", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
57 line 404, "pan.___", state 163, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
58 line 408, "pan.___", state 177, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
59 line 412, "pan.___", state 196, "(1)"
60 line 421, "pan.___", state 226, "(1)"
61 line 425, "pan.___", state 239, "(1)"
62 line 670, "pan.___", state 260, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
63 line 395, "pan.___", state 267, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
64 line 404, "pan.___", state 299, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
65 line 408, "pan.___", state 313, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
66 line 412, "pan.___", state 332, "(1)"
67 line 421, "pan.___", state 362, "(1)"
68 line 425, "pan.___", state 375, "(1)"
69 line 395, "pan.___", state 396, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
70 line 404, "pan.___", state 428, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
71 line 408, "pan.___", state 442, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
72 line 412, "pan.___", state 461, "(1)"
73 line 421, "pan.___", state 491, "(1)"
74 line 425, "pan.___", state 504, "(1)"
75 line 395, "pan.___", state 527, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
76 line 395, "pan.___", state 529, "(1)"
77 line 395, "pan.___", state 530, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
78 line 395, "pan.___", state 530, "else"
79 line 395, "pan.___", state 533, "(1)"
80 line 399, "pan.___", state 541, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
81 line 399, "pan.___", state 543, "(1)"
82 line 399, "pan.___", state 544, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
83 line 399, "pan.___", state 544, "else"
84 line 399, "pan.___", state 547, "(1)"
85 line 399, "pan.___", state 548, "(1)"
86 line 399, "pan.___", state 548, "(1)"
87 line 397, "pan.___", state 553, "((i<1))"
88 line 397, "pan.___", state 553, "((i>=1))"
89 line 404, "pan.___", state 559, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
90 line 404, "pan.___", state 561, "(1)"
91 line 404, "pan.___", state 562, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
92 line 404, "pan.___", state 562, "else"
93 line 404, "pan.___", state 565, "(1)"
94 line 404, "pan.___", state 566, "(1)"
95 line 404, "pan.___", state 566, "(1)"
96 line 408, "pan.___", state 573, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
97 line 408, "pan.___", state 575, "(1)"
98 line 408, "pan.___", state 576, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
99 line 408, "pan.___", state 576, "else"
100 line 408, "pan.___", state 579, "(1)"
101 line 408, "pan.___", state 580, "(1)"
102 line 408, "pan.___", state 580, "(1)"
103 line 406, "pan.___", state 585, "((i<2))"
104 line 406, "pan.___", state 585, "((i>=2))"
105 line 412, "pan.___", state 592, "(1)"
106 line 412, "pan.___", state 593, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
107 line 412, "pan.___", state 593, "else"
108 line 412, "pan.___", state 596, "(1)"
109 line 412, "pan.___", state 597, "(1)"
110 line 412, "pan.___", state 597, "(1)"
111 line 416, "pan.___", state 605, "(1)"
112 line 416, "pan.___", state 606, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
113 line 416, "pan.___", state 606, "else"
114 line 416, "pan.___", state 609, "(1)"
115 line 416, "pan.___", state 610, "(1)"
116 line 416, "pan.___", state 610, "(1)"
117 line 414, "pan.___", state 615, "((i<1))"
118 line 414, "pan.___", state 615, "((i>=1))"
119 line 421, "pan.___", state 622, "(1)"
120 line 421, "pan.___", state 623, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
121 line 421, "pan.___", state 623, "else"
122 line 421, "pan.___", state 626, "(1)"
123 line 421, "pan.___", state 627, "(1)"
124 line 421, "pan.___", state 627, "(1)"
125 line 425, "pan.___", state 635, "(1)"
126 line 425, "pan.___", state 636, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
127 line 425, "pan.___", state 636, "else"
128 line 425, "pan.___", state 639, "(1)"
129 line 425, "pan.___", state 640, "(1)"
130 line 425, "pan.___", state 640, "(1)"
131 line 423, "pan.___", state 645, "((i<2))"
132 line 423, "pan.___", state 645, "((i>=2))"
133 line 430, "pan.___", state 649, "(1)"
134 line 430, "pan.___", state 649, "(1)"
135 line 670, "pan.___", state 652, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
136 line 670, "pan.___", state 653, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
137 line 670, "pan.___", state 654, "(1)"
138 line 395, "pan.___", state 661, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
139 line 404, "pan.___", state 693, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
140 line 408, "pan.___", state 707, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
141 line 412, "pan.___", state 726, "(1)"
142 line 421, "pan.___", state 756, "(1)"
143 line 425, "pan.___", state 769, "(1)"
144 line 395, "pan.___", state 797, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
145 line 395, "pan.___", state 799, "(1)"
146 line 395, "pan.___", state 800, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
147 line 395, "pan.___", state 800, "else"
148 line 395, "pan.___", state 803, "(1)"
149 line 399, "pan.___", state 811, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
150 line 399, "pan.___", state 813, "(1)"
151 line 399, "pan.___", state 814, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
152 line 399, "pan.___", state 814, "else"
153 line 399, "pan.___", state 817, "(1)"
154 line 399, "pan.___", state 818, "(1)"
155 line 399, "pan.___", state 818, "(1)"
156 line 397, "pan.___", state 823, "((i<1))"
157 line 397, "pan.___", state 823, "((i>=1))"
158 line 404, "pan.___", state 829, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
159 line 404, "pan.___", state 831, "(1)"
160 line 404, "pan.___", state 832, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
161 line 404, "pan.___", state 832, "else"
162 line 404, "pan.___", state 835, "(1)"
163 line 404, "pan.___", state 836, "(1)"
164 line 404, "pan.___", state 836, "(1)"
165 line 408, "pan.___", state 843, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
166 line 408, "pan.___", state 845, "(1)"
167 line 408, "pan.___", state 846, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
168 line 408, "pan.___", state 846, "else"
169 line 408, "pan.___", state 849, "(1)"
170 line 408, "pan.___", state 850, "(1)"
171 line 408, "pan.___", state 850, "(1)"
172 line 406, "pan.___", state 855, "((i<2))"
173 line 406, "pan.___", state 855, "((i>=2))"
174 line 412, "pan.___", state 862, "(1)"
175 line 412, "pan.___", state 863, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
176 line 412, "pan.___", state 863, "else"
177 line 412, "pan.___", state 866, "(1)"
178 line 412, "pan.___", state 867, "(1)"
179 line 412, "pan.___", state 867, "(1)"
180 line 416, "pan.___", state 875, "(1)"
181 line 416, "pan.___", state 876, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
182 line 416, "pan.___", state 876, "else"
183 line 416, "pan.___", state 879, "(1)"
184 line 416, "pan.___", state 880, "(1)"
185 line 416, "pan.___", state 880, "(1)"
186 line 414, "pan.___", state 885, "((i<1))"
187 line 414, "pan.___", state 885, "((i>=1))"
188 line 421, "pan.___", state 892, "(1)"
189 line 421, "pan.___", state 893, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
190 line 421, "pan.___", state 893, "else"
191 line 421, "pan.___", state 896, "(1)"
192 line 421, "pan.___", state 897, "(1)"
193 line 421, "pan.___", state 897, "(1)"
194 line 425, "pan.___", state 905, "(1)"
195 line 425, "pan.___", state 906, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
196 line 425, "pan.___", state 906, "else"
197 line 425, "pan.___", state 909, "(1)"
198 line 425, "pan.___", state 910, "(1)"
199 line 425, "pan.___", state 910, "(1)"
200 line 430, "pan.___", state 919, "(1)"
201 line 430, "pan.___", state 919, "(1)"
202 line 395, "pan.___", state 926, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
203 line 395, "pan.___", state 928, "(1)"
204 line 395, "pan.___", state 929, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
205 line 395, "pan.___", state 929, "else"
206 line 395, "pan.___", state 932, "(1)"
207 line 399, "pan.___", state 940, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
208 line 399, "pan.___", state 942, "(1)"
209 line 399, "pan.___", state 943, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
210 line 399, "pan.___", state 943, "else"
211 line 399, "pan.___", state 946, "(1)"
212 line 399, "pan.___", state 947, "(1)"
213 line 399, "pan.___", state 947, "(1)"
214 line 397, "pan.___", state 952, "((i<1))"
215 line 397, "pan.___", state 952, "((i>=1))"
216 line 404, "pan.___", state 958, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
217 line 404, "pan.___", state 960, "(1)"
218 line 404, "pan.___", state 961, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
219 line 404, "pan.___", state 961, "else"
220 line 404, "pan.___", state 964, "(1)"
221 line 404, "pan.___", state 965, "(1)"
222 line 404, "pan.___", state 965, "(1)"
223 line 408, "pan.___", state 972, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
224 line 408, "pan.___", state 974, "(1)"
225 line 408, "pan.___", state 975, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
226 line 408, "pan.___", state 975, "else"
227 line 408, "pan.___", state 978, "(1)"
228 line 408, "pan.___", state 979, "(1)"
229 line 408, "pan.___", state 979, "(1)"
230 line 406, "pan.___", state 984, "((i<2))"
231 line 406, "pan.___", state 984, "((i>=2))"
232 line 412, "pan.___", state 991, "(1)"
233 line 412, "pan.___", state 992, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
234 line 412, "pan.___", state 992, "else"
235 line 412, "pan.___", state 995, "(1)"
236 line 412, "pan.___", state 996, "(1)"
237 line 412, "pan.___", state 996, "(1)"
238 line 416, "pan.___", state 1004, "(1)"
239 line 416, "pan.___", state 1005, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
240 line 416, "pan.___", state 1005, "else"
241 line 416, "pan.___", state 1008, "(1)"
242 line 416, "pan.___", state 1009, "(1)"
243 line 416, "pan.___", state 1009, "(1)"
244 line 414, "pan.___", state 1014, "((i<1))"
245 line 414, "pan.___", state 1014, "((i>=1))"
246 line 421, "pan.___", state 1021, "(1)"
247 line 421, "pan.___", state 1022, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
248 line 421, "pan.___", state 1022, "else"
249 line 421, "pan.___", state 1025, "(1)"
250 line 421, "pan.___", state 1026, "(1)"
251 line 421, "pan.___", state 1026, "(1)"
252 line 425, "pan.___", state 1034, "(1)"
253 line 425, "pan.___", state 1035, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
254 line 425, "pan.___", state 1035, "else"
255 line 425, "pan.___", state 1038, "(1)"
256 line 425, "pan.___", state 1039, "(1)"
257 line 425, "pan.___", state 1039, "(1)"
258 line 423, "pan.___", state 1044, "((i<2))"
259 line 423, "pan.___", state 1044, "((i>=2))"
260 line 430, "pan.___", state 1048, "(1)"
261 line 430, "pan.___", state 1048, "(1)"
262 line 678, "pan.___", state 1052, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
263 line 395, "pan.___", state 1057, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
264 line 404, "pan.___", state 1089, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
265 line 408, "pan.___", state 1103, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
266 line 412, "pan.___", state 1122, "(1)"
267 line 421, "pan.___", state 1152, "(1)"
268 line 425, "pan.___", state 1165, "(1)"
269 line 395, "pan.___", state 1189, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
270 line 404, "pan.___", state 1221, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
271 line 408, "pan.___", state 1235, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
272 line 412, "pan.___", state 1254, "(1)"
273 line 421, "pan.___", state 1284, "(1)"
274 line 425, "pan.___", state 1297, "(1)"
275 line 395, "pan.___", state 1322, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
276 line 404, "pan.___", state 1354, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
277 line 408, "pan.___", state 1368, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
278 line 412, "pan.___", state 1387, "(1)"
279 line 421, "pan.___", state 1417, "(1)"
280 line 425, "pan.___", state 1430, "(1)"
281 line 395, "pan.___", state 1451, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
282 line 404, "pan.___", state 1483, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
283 line 408, "pan.___", state 1497, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
284 line 412, "pan.___", state 1516, "(1)"
285 line 421, "pan.___", state 1546, "(1)"
286 line 425, "pan.___", state 1559, "(1)"
287 line 395, "pan.___", state 1585, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
288 line 404, "pan.___", state 1617, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
289 line 408, "pan.___", state 1631, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
290 line 412, "pan.___", state 1650, "(1)"
291 line 421, "pan.___", state 1680, "(1)"
292 line 425, "pan.___", state 1693, "(1)"
293 line 395, "pan.___", state 1714, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
294 line 404, "pan.___", state 1746, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
295 line 408, "pan.___", state 1760, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
296 line 412, "pan.___", state 1779, "(1)"
297 line 421, "pan.___", state 1809, "(1)"
298 line 425, "pan.___", state 1822, "(1)"
299 line 395, "pan.___", state 1846, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
300 line 404, "pan.___", state 1878, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
301 line 408, "pan.___", state 1892, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
302 line 412, "pan.___", state 1911, "(1)"
303 line 421, "pan.___", state 1941, "(1)"
304 line 425, "pan.___", state 1954, "(1)"
305 line 717, "pan.___", state 1975, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
306 line 395, "pan.___", state 1982, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
307 line 404, "pan.___", state 2014, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
308 line 408, "pan.___", state 2028, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
309 line 412, "pan.___", state 2047, "(1)"
310 line 421, "pan.___", state 2077, "(1)"
311 line 425, "pan.___", state 2090, "(1)"
312 line 395, "pan.___", state 2111, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
313 line 404, "pan.___", state 2143, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
314 line 408, "pan.___", state 2157, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
315 line 412, "pan.___", state 2176, "(1)"
316 line 421, "pan.___", state 2206, "(1)"
317 line 425, "pan.___", state 2219, "(1)"
318 line 395, "pan.___", state 2242, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
319 line 395, "pan.___", state 2244, "(1)"
320 line 395, "pan.___", state 2245, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
321 line 395, "pan.___", state 2245, "else"
322 line 395, "pan.___", state 2248, "(1)"
323 line 399, "pan.___", state 2256, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
324 line 399, "pan.___", state 2258, "(1)"
325 line 399, "pan.___", state 2259, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
326 line 399, "pan.___", state 2259, "else"
327 line 399, "pan.___", state 2262, "(1)"
328 line 399, "pan.___", state 2263, "(1)"
329 line 399, "pan.___", state 2263, "(1)"
330 line 397, "pan.___", state 2268, "((i<1))"
331 line 397, "pan.___", state 2268, "((i>=1))"
332 line 404, "pan.___", state 2274, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
333 line 404, "pan.___", state 2276, "(1)"
334 line 404, "pan.___", state 2277, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
335 line 404, "pan.___", state 2277, "else"
336 line 404, "pan.___", state 2280, "(1)"
337 line 404, "pan.___", state 2281, "(1)"
338 line 404, "pan.___", state 2281, "(1)"
339 line 408, "pan.___", state 2288, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
340 line 408, "pan.___", state 2290, "(1)"
341 line 408, "pan.___", state 2291, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
342 line 408, "pan.___", state 2291, "else"
343 line 408, "pan.___", state 2294, "(1)"
344 line 408, "pan.___", state 2295, "(1)"
345 line 408, "pan.___", state 2295, "(1)"
346 line 406, "pan.___", state 2300, "((i<2))"
347 line 406, "pan.___", state 2300, "((i>=2))"
348 line 412, "pan.___", state 2307, "(1)"
349 line 412, "pan.___", state 2308, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
350 line 412, "pan.___", state 2308, "else"
351 line 412, "pan.___", state 2311, "(1)"
352 line 412, "pan.___", state 2312, "(1)"
353 line 412, "pan.___", state 2312, "(1)"
354 line 416, "pan.___", state 2320, "(1)"
355 line 416, "pan.___", state 2321, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
356 line 416, "pan.___", state 2321, "else"
357 line 416, "pan.___", state 2324, "(1)"
358 line 416, "pan.___", state 2325, "(1)"
359 line 416, "pan.___", state 2325, "(1)"
360 line 414, "pan.___", state 2330, "((i<1))"
361 line 414, "pan.___", state 2330, "((i>=1))"
362 line 421, "pan.___", state 2337, "(1)"
363 line 421, "pan.___", state 2338, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
364 line 421, "pan.___", state 2338, "else"
365 line 421, "pan.___", state 2341, "(1)"
366 line 421, "pan.___", state 2342, "(1)"
367 line 421, "pan.___", state 2342, "(1)"
368 line 425, "pan.___", state 2350, "(1)"
369 line 425, "pan.___", state 2351, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
370 line 425, "pan.___", state 2351, "else"
371 line 425, "pan.___", state 2354, "(1)"
372 line 425, "pan.___", state 2355, "(1)"
373 line 425, "pan.___", state 2355, "(1)"
374 line 423, "pan.___", state 2360, "((i<2))"
375 line 423, "pan.___", state 2360, "((i>=2))"
376 line 430, "pan.___", state 2364, "(1)"
377 line 430, "pan.___", state 2364, "(1)"
378 line 717, "pan.___", state 2367, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
379 line 717, "pan.___", state 2368, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
380 line 717, "pan.___", state 2369, "(1)"
381 line 395, "pan.___", state 2376, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
382 line 404, "pan.___", state 2408, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
383 line 408, "pan.___", state 2422, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
384 line 412, "pan.___", state 2441, "(1)"
385 line 421, "pan.___", state 2471, "(1)"
386 line 425, "pan.___", state 2484, "(1)"
387 line 395, "pan.___", state 2511, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
388 line 404, "pan.___", state 2543, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
389 line 408, "pan.___", state 2557, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
390 line 412, "pan.___", state 2576, "(1)"
391 line 421, "pan.___", state 2606, "(1)"
392 line 425, "pan.___", state 2619, "(1)"
393 line 395, "pan.___", state 2640, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
394 line 404, "pan.___", state 2672, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
395 line 408, "pan.___", state 2686, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
396 line 412, "pan.___", state 2705, "(1)"
397 line 421, "pan.___", state 2735, "(1)"
398 line 425, "pan.___", state 2748, "(1)"
399 line 395, "pan.___", state 2781, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
400 line 404, "pan.___", state 2813, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
401 line 408, "pan.___", state 2827, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
402 line 412, "pan.___", state 2846, "(1)"
403 line 421, "pan.___", state 2876, "(1)"
404 line 425, "pan.___", state 2889, "(1)"
405 line 395, "pan.___", state 2908, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
406 line 404, "pan.___", state 2940, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
407 line 408, "pan.___", state 2954, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
408 line 412, "pan.___", state 2973, "(1)"
409 line 421, "pan.___", state 3003, "(1)"
410 line 425, "pan.___", state 3016, "(1)"
411 line 877, "pan.___", state 3037, "-end-"
413 unreached in proctype urcu_writer
414 line 395, "pan.___", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
415 line 395, "pan.___", state 24, "(1)"
416 line 399, "pan.___", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
417 line 399, "pan.___", state 38, "(1)"
418 line 399, "pan.___", state 39, "(1)"
419 line 399, "pan.___", state 39, "(1)"
420 line 397, "pan.___", state 44, "((i<1))"
421 line 397, "pan.___", state 44, "((i>=1))"
422 line 404, "pan.___", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
423 line 404, "pan.___", state 56, "(1)"
424 line 404, "pan.___", state 57, "(1)"
425 line 404, "pan.___", state 57, "(1)"
426 line 408, "pan.___", state 70, "(1)"
427 line 408, "pan.___", state 71, "(1)"
428 line 408, "pan.___", state 71, "(1)"
429 line 406, "pan.___", state 76, "((i<2))"
430 line 406, "pan.___", state 76, "((i>=2))"
431 line 412, "pan.___", state 83, "(1)"
432 line 412, "pan.___", state 84, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
433 line 412, "pan.___", state 84, "else"
434 line 412, "pan.___", state 87, "(1)"
435 line 412, "pan.___", state 88, "(1)"
436 line 412, "pan.___", state 88, "(1)"
437 line 416, "pan.___", state 96, "(1)"
438 line 416, "pan.___", state 97, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
439 line 416, "pan.___", state 97, "else"
440 line 416, "pan.___", state 100, "(1)"
441 line 416, "pan.___", state 101, "(1)"
442 line 416, "pan.___", state 101, "(1)"
443 line 414, "pan.___", state 106, "((i<1))"
444 line 414, "pan.___", state 106, "((i>=1))"
445 line 421, "pan.___", state 113, "(1)"
446 line 421, "pan.___", state 114, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
447 line 421, "pan.___", state 114, "else"
448 line 421, "pan.___", state 117, "(1)"
449 line 421, "pan.___", state 118, "(1)"
450 line 421, "pan.___", state 118, "(1)"
451 line 425, "pan.___", state 126, "(1)"
452 line 425, "pan.___", state 127, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
453 line 425, "pan.___", state 127, "else"
454 line 425, "pan.___", state 130, "(1)"
455 line 425, "pan.___", state 131, "(1)"
456 line 425, "pan.___", state 131, "(1)"
457 line 423, "pan.___", state 136, "((i<2))"
458 line 423, "pan.___", state 136, "((i>=2))"
459 line 430, "pan.___", state 140, "(1)"
460 line 430, "pan.___", state 140, "(1)"
461 line 250, "pan.___", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
462 line 254, "pan.___", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
463 line 258, "pan.___", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
464 line 395, "pan.___", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
465 line 399, "pan.___", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
466 line 404, "pan.___", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
467 line 408, "pan.___", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
468 line 412, "pan.___", state 276, "(1)"
469 line 416, "pan.___", state 289, "(1)"
470 line 421, "pan.___", state 306, "(1)"
471 line 425, "pan.___", state 319, "(1)"
472 line 399, "pan.___", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
473 line 404, "pan.___", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
474 line 408, "pan.___", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
475 line 416, "pan.___", state 420, "(1)"
476 line 421, "pan.___", state 437, "(1)"
477 line 425, "pan.___", state 450, "(1)"
478 line 399, "pan.___", state 494, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
479 line 404, "pan.___", state 512, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
480 line 408, "pan.___", state 526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
481 line 416, "pan.___", state 558, "(1)"
482 line 421, "pan.___", state 575, "(1)"
483 line 425, "pan.___", state 588, "(1)"
484 line 399, "pan.___", state 623, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
485 line 404, "pan.___", state 641, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
486 line 408, "pan.___", state 655, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
487 line 416, "pan.___", state 687, "(1)"
488 line 421, "pan.___", state 704, "(1)"
489 line 425, "pan.___", state 717, "(1)"
490 line 399, "pan.___", state 754, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
491 line 404, "pan.___", state 772, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
492 line 408, "pan.___", state 786, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
493 line 416, "pan.___", state 818, "(1)"
494 line 421, "pan.___", state 835, "(1)"
495 line 425, "pan.___", state 848, "(1)"
496 line 250, "pan.___", state 903, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
497 line 254, "pan.___", state 912, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
498 line 258, "pan.___", state 927, "(1)"
499 line 262, "pan.___", state 934, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
500 line 227, "pan.___", state 950, "(1)"
501 line 231, "pan.___", state 958, "(1)"
502 line 235, "pan.___", state 970, "(1)"
503 line 239, "pan.___", state 978, "(1)"
504 line 250, "pan.___", state 1009, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
505 line 254, "pan.___", state 1018, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
506 line 258, "pan.___", state 1031, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
507 line 262, "pan.___", state 1040, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
508 line 227, "pan.___", state 1056, "(1)"
509 line 231, "pan.___", state 1064, "(1)"
510 line 235, "pan.___", state 1076, "(1)"
511 line 239, "pan.___", state 1084, "(1)"
512 line 254, "pan.___", state 1110, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
513 line 258, "pan.___", state 1123, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
514 line 262, "pan.___", state 1132, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
515 line 227, "pan.___", state 1148, "(1)"
516 line 231, "pan.___", state 1156, "(1)"
517 line 235, "pan.___", state 1168, "(1)"
518 line 239, "pan.___", state 1176, "(1)"
519 line 250, "pan.___", state 1207, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
520 line 254, "pan.___", state 1216, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
521 line 258, "pan.___", state 1229, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
522 line 262, "pan.___", state 1238, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
523 line 227, "pan.___", state 1254, "(1)"
524 line 231, "pan.___", state 1262, "(1)"
525 line 235, "pan.___", state 1274, "(1)"
526 line 239, "pan.___", state 1282, "(1)"
527 line 254, "pan.___", state 1308, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
528 line 258, "pan.___", state 1321, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
529 line 262, "pan.___", state 1330, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
530 line 227, "pan.___", state 1346, "(1)"
531 line 231, "pan.___", state 1354, "(1)"
532 line 235, "pan.___", state 1366, "(1)"
533 line 239, "pan.___", state 1374, "(1)"
534 line 250, "pan.___", state 1405, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
535 line 254, "pan.___", state 1414, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
536 line 258, "pan.___", state 1427, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
537 line 262, "pan.___", state 1436, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
538 line 227, "pan.___", state 1452, "(1)"
539 line 231, "pan.___", state 1460, "(1)"
540 line 235, "pan.___", state 1472, "(1)"
541 line 239, "pan.___", state 1480, "(1)"
542 line 254, "pan.___", state 1506, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
543 line 258, "pan.___", state 1519, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
544 line 262, "pan.___", state 1528, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
545 line 227, "pan.___", state 1544, "(1)"
546 line 231, "pan.___", state 1552, "(1)"
547 line 235, "pan.___", state 1564, "(1)"
548 line 239, "pan.___", state 1572, "(1)"
549 line 250, "pan.___", state 1603, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
550 line 254, "pan.___", state 1612, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
551 line 258, "pan.___", state 1625, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
552 line 262, "pan.___", state 1634, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
553 line 227, "pan.___", state 1650, "(1)"
554 line 231, "pan.___", state 1658, "(1)"
555 line 235, "pan.___", state 1670, "(1)"
556 line 239, "pan.___", state 1678, "(1)"
557 line 1204, "pan.___", state 1694, "-end-"
559 unreached in proctype :init:
560 line 1215, "pan.___", state 9, "((j<2))"
561 line 1215, "pan.___", state 9, "((j>=2))"
562 line 1216, "pan.___", state 20, "((j<2))"
563 line 1216, "pan.___", state 20, "((j>=2))"
564 line 1221, "pan.___", state 33, "((j<2))"
565 line 1221, "pan.___", state 33, "((j>=2))"
566 line 1219, "pan.___", state 43, "((i<1))"
567 line 1219, "pan.___", state 43, "((i>=1))"
568 line 1229, "pan.___", state 54, "((j<2))"
569 line 1229, "pan.___", state 54, "((j>=2))"
570 line 1233, "pan.___", state 67, "((j<2))"
571 line 1233, "pan.___", state 67, "((j>=2))"
573 unreached in proctype :never:
574 line 1263, "pan.___", state 8, "-end-"
577 pan: elapsed time 638 seconds
578 pan: rate 3551.057 states/second
579 pan: avg transition delay 1.2606e-06 usec
580 cp .input.spin urcu_free_no_rmb.spin.input
581 cp .input.spin.trail urcu_free_no_rmb.spin.input.trail
projects / urcu.git / blob