1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
2 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
4 cat .input.define > pan.ltl
6 spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
7 cp urcu_progress_writer_error.define .input.define
8 cat .input.define > .input.spin
9 cat DEFINES >> .input.spin
10 cat urcu.spin >> .input.spin
11 rm -f .input.spin.trail
12 spin -a -X -N pan.ltl .input.spin
14 gcc -O2 -w -DHASH64 -o pan pan.c
15 ./pan -a -f -v -c1 -X -m10000000 -w20
16 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
17 (never claims generated from LTL formulae are stutter-invariant)
18 depth 0: Claim reached state 5 (line 1246)
19 depth 23: Claim reached state 9 (line 1251)
20 depth 51: Claim reached state 9 (line 1250)
21 pan: acceptance cycle (at depth 1200)
22 pan: wrote .input.spin.trail
24 (Spin Version 5.1.7 -- 23 December 2008)
25 Warning: Search not completed
26 + Partial Order Reduction
28 Full statespace search for:
30 assertion violations + (if within scope of claim)
31 acceptance cycles + (fairness enabled)
32 invalid end states - (disabled by never claim)
34 State-vector 88 byte, depth reached 3997, errors: 1
35 26291 states, stored (59381 visited)
36 11000989 states, matched
37 11060370 transitions (= visited+matched)
39 hash conflicts: 84608 (resolved)
41 Stats on memory usage (in Megabytes):
42 2.908 equivalent memory usage for states (stored*(State-vector + overhead))
43 2.889 actual memory usage for states (compression: 99.33%)
44 state-vector as stored = 87 byte + 28 byte overhead
45 8.000 memory used for hash table (-w20)
46 457.764 memory used for DFS stack (-m10000000)
47 468.596 total actual memory usage
49 unreached in proctype urcu_reader
50 line 648, "pan.___", state 20, "(1)"
51 line 251, "pan.___", state 32, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
52 line 259, "pan.___", state 54, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
53 line 263, "pan.___", state 63, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
54 line 228, "pan.___", state 79, "(1)"
55 line 232, "pan.___", state 87, "(1)"
56 line 236, "pan.___", state 99, "(1)"
57 line 240, "pan.___", state 107, "(1)"
58 line 388, "pan.___", state 133, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
59 line 397, "pan.___", state 165, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
60 line 401, "pan.___", state 179, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
61 line 405, "pan.___", state 198, "(1)"
62 line 414, "pan.___", state 228, "(1)"
63 line 418, "pan.___", state 241, "(1)"
64 line 664, "pan.___", state 262, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
65 line 388, "pan.___", state 269, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
66 line 397, "pan.___", state 301, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
67 line 401, "pan.___", state 315, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
68 line 405, "pan.___", state 334, "(1)"
69 line 414, "pan.___", state 364, "(1)"
70 line 418, "pan.___", state 377, "(1)"
71 line 388, "pan.___", state 398, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
72 line 397, "pan.___", state 430, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
73 line 401, "pan.___", state 444, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
74 line 405, "pan.___", state 463, "(1)"
75 line 414, "pan.___", state 493, "(1)"
76 line 418, "pan.___", state 506, "(1)"
77 line 388, "pan.___", state 529, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
78 line 388, "pan.___", state 531, "(1)"
79 line 388, "pan.___", state 532, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
80 line 388, "pan.___", state 532, "else"
81 line 388, "pan.___", state 535, "(1)"
82 line 392, "pan.___", state 543, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
83 line 392, "pan.___", state 545, "(1)"
84 line 392, "pan.___", state 546, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
85 line 392, "pan.___", state 546, "else"
86 line 392, "pan.___", state 549, "(1)"
87 line 392, "pan.___", state 550, "(1)"
88 line 392, "pan.___", state 550, "(1)"
89 line 390, "pan.___", state 555, "((i<1))"
90 line 390, "pan.___", state 555, "((i>=1))"
91 line 397, "pan.___", state 561, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
92 line 397, "pan.___", state 563, "(1)"
93 line 397, "pan.___", state 564, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
94 line 397, "pan.___", state 564, "else"
95 line 397, "pan.___", state 567, "(1)"
96 line 397, "pan.___", state 568, "(1)"
97 line 397, "pan.___", state 568, "(1)"
98 line 401, "pan.___", state 575, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
99 line 401, "pan.___", state 577, "(1)"
100 line 401, "pan.___", state 578, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
101 line 401, "pan.___", state 578, "else"
102 line 401, "pan.___", state 581, "(1)"
103 line 401, "pan.___", state 582, "(1)"
104 line 401, "pan.___", state 582, "(1)"
105 line 399, "pan.___", state 587, "((i<2))"
106 line 399, "pan.___", state 587, "((i>=2))"
107 line 405, "pan.___", state 594, "(1)"
108 line 405, "pan.___", state 595, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
109 line 405, "pan.___", state 595, "else"
110 line 405, "pan.___", state 598, "(1)"
111 line 405, "pan.___", state 599, "(1)"
112 line 405, "pan.___", state 599, "(1)"
113 line 409, "pan.___", state 607, "(1)"
114 line 409, "pan.___", state 608, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
115 line 409, "pan.___", state 608, "else"
116 line 409, "pan.___", state 611, "(1)"
117 line 409, "pan.___", state 612, "(1)"
118 line 409, "pan.___", state 612, "(1)"
119 line 407, "pan.___", state 617, "((i<1))"
120 line 407, "pan.___", state 617, "((i>=1))"
121 line 414, "pan.___", state 624, "(1)"
122 line 414, "pan.___", state 625, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
123 line 414, "pan.___", state 625, "else"
124 line 414, "pan.___", state 628, "(1)"
125 line 414, "pan.___", state 629, "(1)"
126 line 414, "pan.___", state 629, "(1)"
127 line 418, "pan.___", state 637, "(1)"
128 line 418, "pan.___", state 638, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
129 line 418, "pan.___", state 638, "else"
130 line 418, "pan.___", state 641, "(1)"
131 line 418, "pan.___", state 642, "(1)"
132 line 418, "pan.___", state 642, "(1)"
133 line 416, "pan.___", state 647, "((i<2))"
134 line 416, "pan.___", state 647, "((i>=2))"
135 line 423, "pan.___", state 651, "(1)"
136 line 423, "pan.___", state 651, "(1)"
137 line 664, "pan.___", state 654, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
138 line 664, "pan.___", state 655, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
139 line 664, "pan.___", state 656, "(1)"
140 line 388, "pan.___", state 663, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
141 line 397, "pan.___", state 695, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
142 line 401, "pan.___", state 709, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
143 line 405, "pan.___", state 728, "(1)"
144 line 414, "pan.___", state 758, "(1)"
145 line 418, "pan.___", state 771, "(1)"
146 line 388, "pan.___", state 799, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
147 line 388, "pan.___", state 801, "(1)"
148 line 388, "pan.___", state 802, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
149 line 388, "pan.___", state 802, "else"
150 line 388, "pan.___", state 805, "(1)"
151 line 392, "pan.___", state 813, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
152 line 392, "pan.___", state 815, "(1)"
153 line 392, "pan.___", state 816, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
154 line 392, "pan.___", state 816, "else"
155 line 392, "pan.___", state 819, "(1)"
156 line 392, "pan.___", state 820, "(1)"
157 line 392, "pan.___", state 820, "(1)"
158 line 390, "pan.___", state 825, "((i<1))"
159 line 390, "pan.___", state 825, "((i>=1))"
160 line 397, "pan.___", state 831, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
161 line 397, "pan.___", state 833, "(1)"
162 line 397, "pan.___", state 834, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
163 line 397, "pan.___", state 834, "else"
164 line 397, "pan.___", state 837, "(1)"
165 line 397, "pan.___", state 838, "(1)"
166 line 397, "pan.___", state 838, "(1)"
167 line 401, "pan.___", state 845, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
168 line 401, "pan.___", state 847, "(1)"
169 line 401, "pan.___", state 848, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
170 line 401, "pan.___", state 848, "else"
171 line 401, "pan.___", state 851, "(1)"
172 line 401, "pan.___", state 852, "(1)"
173 line 401, "pan.___", state 852, "(1)"
174 line 399, "pan.___", state 857, "((i<2))"
175 line 399, "pan.___", state 857, "((i>=2))"
176 line 405, "pan.___", state 864, "(1)"
177 line 405, "pan.___", state 865, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
178 line 405, "pan.___", state 865, "else"
179 line 405, "pan.___", state 868, "(1)"
180 line 405, "pan.___", state 869, "(1)"
181 line 405, "pan.___", state 869, "(1)"
182 line 409, "pan.___", state 877, "(1)"
183 line 409, "pan.___", state 878, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
184 line 409, "pan.___", state 878, "else"
185 line 409, "pan.___", state 881, "(1)"
186 line 409, "pan.___", state 882, "(1)"
187 line 409, "pan.___", state 882, "(1)"
188 line 407, "pan.___", state 887, "((i<1))"
189 line 407, "pan.___", state 887, "((i>=1))"
190 line 414, "pan.___", state 894, "(1)"
191 line 414, "pan.___", state 895, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
192 line 414, "pan.___", state 895, "else"
193 line 414, "pan.___", state 898, "(1)"
194 line 414, "pan.___", state 899, "(1)"
195 line 414, "pan.___", state 899, "(1)"
196 line 418, "pan.___", state 907, "(1)"
197 line 418, "pan.___", state 908, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
198 line 418, "pan.___", state 908, "else"
199 line 418, "pan.___", state 911, "(1)"
200 line 418, "pan.___", state 912, "(1)"
201 line 418, "pan.___", state 912, "(1)"
202 line 423, "pan.___", state 921, "(1)"
203 line 423, "pan.___", state 921, "(1)"
204 line 388, "pan.___", state 928, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
205 line 388, "pan.___", state 930, "(1)"
206 line 388, "pan.___", state 931, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
207 line 388, "pan.___", state 931, "else"
208 line 388, "pan.___", state 934, "(1)"
209 line 392, "pan.___", state 942, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
210 line 392, "pan.___", state 944, "(1)"
211 line 392, "pan.___", state 945, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
212 line 392, "pan.___", state 945, "else"
213 line 392, "pan.___", state 948, "(1)"
214 line 392, "pan.___", state 949, "(1)"
215 line 392, "pan.___", state 949, "(1)"
216 line 390, "pan.___", state 954, "((i<1))"
217 line 390, "pan.___", state 954, "((i>=1))"
218 line 397, "pan.___", state 960, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
219 line 397, "pan.___", state 962, "(1)"
220 line 397, "pan.___", state 963, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
221 line 397, "pan.___", state 963, "else"
222 line 397, "pan.___", state 966, "(1)"
223 line 397, "pan.___", state 967, "(1)"
224 line 397, "pan.___", state 967, "(1)"
225 line 401, "pan.___", state 974, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
226 line 401, "pan.___", state 976, "(1)"
227 line 401, "pan.___", state 977, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
228 line 401, "pan.___", state 977, "else"
229 line 401, "pan.___", state 980, "(1)"
230 line 401, "pan.___", state 981, "(1)"
231 line 401, "pan.___", state 981, "(1)"
232 line 399, "pan.___", state 986, "((i<2))"
233 line 399, "pan.___", state 986, "((i>=2))"
234 line 405, "pan.___", state 993, "(1)"
235 line 405, "pan.___", state 994, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
236 line 405, "pan.___", state 994, "else"
237 line 405, "pan.___", state 997, "(1)"
238 line 405, "pan.___", state 998, "(1)"
239 line 405, "pan.___", state 998, "(1)"
240 line 409, "pan.___", state 1006, "(1)"
241 line 409, "pan.___", state 1007, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
242 line 409, "pan.___", state 1007, "else"
243 line 409, "pan.___", state 1010, "(1)"
244 line 409, "pan.___", state 1011, "(1)"
245 line 409, "pan.___", state 1011, "(1)"
246 line 407, "pan.___", state 1016, "((i<1))"
247 line 407, "pan.___", state 1016, "((i>=1))"
248 line 414, "pan.___", state 1023, "(1)"
249 line 414, "pan.___", state 1024, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
250 line 414, "pan.___", state 1024, "else"
251 line 414, "pan.___", state 1027, "(1)"
252 line 414, "pan.___", state 1028, "(1)"
253 line 414, "pan.___", state 1028, "(1)"
254 line 418, "pan.___", state 1036, "(1)"
255 line 418, "pan.___", state 1037, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
256 line 418, "pan.___", state 1037, "else"
257 line 418, "pan.___", state 1040, "(1)"
258 line 418, "pan.___", state 1041, "(1)"
259 line 418, "pan.___", state 1041, "(1)"
260 line 416, "pan.___", state 1046, "((i<2))"
261 line 416, "pan.___", state 1046, "((i>=2))"
262 line 423, "pan.___", state 1050, "(1)"
263 line 423, "pan.___", state 1050, "(1)"
264 line 672, "pan.___", state 1054, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
265 line 388, "pan.___", state 1059, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
266 line 397, "pan.___", state 1091, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
267 line 401, "pan.___", state 1105, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
268 line 405, "pan.___", state 1124, "(1)"
269 line 414, "pan.___", state 1154, "(1)"
270 line 418, "pan.___", state 1167, "(1)"
271 line 388, "pan.___", state 1191, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
272 line 397, "pan.___", state 1223, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
273 line 401, "pan.___", state 1237, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
274 line 405, "pan.___", state 1256, "(1)"
275 line 414, "pan.___", state 1286, "(1)"
276 line 418, "pan.___", state 1299, "(1)"
277 line 388, "pan.___", state 1324, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
278 line 397, "pan.___", state 1356, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
279 line 401, "pan.___", state 1370, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
280 line 405, "pan.___", state 1389, "(1)"
281 line 414, "pan.___", state 1419, "(1)"
282 line 418, "pan.___", state 1432, "(1)"
283 line 388, "pan.___", state 1453, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
284 line 397, "pan.___", state 1485, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
285 line 401, "pan.___", state 1499, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
286 line 405, "pan.___", state 1518, "(1)"
287 line 414, "pan.___", state 1548, "(1)"
288 line 418, "pan.___", state 1561, "(1)"
289 line 388, "pan.___", state 1587, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
290 line 397, "pan.___", state 1619, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
291 line 401, "pan.___", state 1633, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
292 line 405, "pan.___", state 1652, "(1)"
293 line 414, "pan.___", state 1682, "(1)"
294 line 418, "pan.___", state 1695, "(1)"
295 line 388, "pan.___", state 1716, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
296 line 397, "pan.___", state 1748, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
297 line 401, "pan.___", state 1762, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
298 line 405, "pan.___", state 1781, "(1)"
299 line 414, "pan.___", state 1811, "(1)"
300 line 418, "pan.___", state 1824, "(1)"
301 line 388, "pan.___", state 1848, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
302 line 397, "pan.___", state 1880, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
303 line 401, "pan.___", state 1894, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
304 line 405, "pan.___", state 1913, "(1)"
305 line 414, "pan.___", state 1943, "(1)"
306 line 418, "pan.___", state 1956, "(1)"
307 line 711, "pan.___", state 1977, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
308 line 388, "pan.___", state 1984, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
309 line 397, "pan.___", state 2016, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
310 line 401, "pan.___", state 2030, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
311 line 405, "pan.___", state 2049, "(1)"
312 line 414, "pan.___", state 2079, "(1)"
313 line 418, "pan.___", state 2092, "(1)"
314 line 388, "pan.___", state 2113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
315 line 397, "pan.___", state 2145, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
316 line 401, "pan.___", state 2159, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
317 line 405, "pan.___", state 2178, "(1)"
318 line 414, "pan.___", state 2208, "(1)"
319 line 418, "pan.___", state 2221, "(1)"
320 line 388, "pan.___", state 2244, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
321 line 388, "pan.___", state 2246, "(1)"
322 line 388, "pan.___", state 2247, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
323 line 388, "pan.___", state 2247, "else"
324 line 388, "pan.___", state 2250, "(1)"
325 line 392, "pan.___", state 2258, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
326 line 392, "pan.___", state 2260, "(1)"
327 line 392, "pan.___", state 2261, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
328 line 392, "pan.___", state 2261, "else"
329 line 392, "pan.___", state 2264, "(1)"
330 line 392, "pan.___", state 2265, "(1)"
331 line 392, "pan.___", state 2265, "(1)"
332 line 390, "pan.___", state 2270, "((i<1))"
333 line 390, "pan.___", state 2270, "((i>=1))"
334 line 397, "pan.___", state 2276, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
335 line 397, "pan.___", state 2278, "(1)"
336 line 397, "pan.___", state 2279, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
337 line 397, "pan.___", state 2279, "else"
338 line 397, "pan.___", state 2282, "(1)"
339 line 397, "pan.___", state 2283, "(1)"
340 line 397, "pan.___", state 2283, "(1)"
341 line 401, "pan.___", state 2290, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
342 line 401, "pan.___", state 2292, "(1)"
343 line 401, "pan.___", state 2293, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
344 line 401, "pan.___", state 2293, "else"
345 line 401, "pan.___", state 2296, "(1)"
346 line 401, "pan.___", state 2297, "(1)"
347 line 401, "pan.___", state 2297, "(1)"
348 line 399, "pan.___", state 2302, "((i<2))"
349 line 399, "pan.___", state 2302, "((i>=2))"
350 line 405, "pan.___", state 2309, "(1)"
351 line 405, "pan.___", state 2310, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
352 line 405, "pan.___", state 2310, "else"
353 line 405, "pan.___", state 2313, "(1)"
354 line 405, "pan.___", state 2314, "(1)"
355 line 405, "pan.___", state 2314, "(1)"
356 line 409, "pan.___", state 2322, "(1)"
357 line 409, "pan.___", state 2323, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
358 line 409, "pan.___", state 2323, "else"
359 line 409, "pan.___", state 2326, "(1)"
360 line 409, "pan.___", state 2327, "(1)"
361 line 409, "pan.___", state 2327, "(1)"
362 line 407, "pan.___", state 2332, "((i<1))"
363 line 407, "pan.___", state 2332, "((i>=1))"
364 line 414, "pan.___", state 2339, "(1)"
365 line 414, "pan.___", state 2340, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
366 line 414, "pan.___", state 2340, "else"
367 line 414, "pan.___", state 2343, "(1)"
368 line 414, "pan.___", state 2344, "(1)"
369 line 414, "pan.___", state 2344, "(1)"
370 line 418, "pan.___", state 2352, "(1)"
371 line 418, "pan.___", state 2353, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
372 line 418, "pan.___", state 2353, "else"
373 line 418, "pan.___", state 2356, "(1)"
374 line 418, "pan.___", state 2357, "(1)"
375 line 418, "pan.___", state 2357, "(1)"
376 line 416, "pan.___", state 2362, "((i<2))"
377 line 416, "pan.___", state 2362, "((i>=2))"
378 line 423, "pan.___", state 2366, "(1)"
379 line 423, "pan.___", state 2366, "(1)"
380 line 711, "pan.___", state 2369, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
381 line 711, "pan.___", state 2370, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
382 line 711, "pan.___", state 2371, "(1)"
383 line 388, "pan.___", state 2378, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
384 line 397, "pan.___", state 2410, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
385 line 401, "pan.___", state 2424, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
386 line 405, "pan.___", state 2443, "(1)"
387 line 414, "pan.___", state 2473, "(1)"
388 line 418, "pan.___", state 2486, "(1)"
389 line 388, "pan.___", state 2513, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
390 line 397, "pan.___", state 2545, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
391 line 401, "pan.___", state 2559, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
392 line 405, "pan.___", state 2578, "(1)"
393 line 414, "pan.___", state 2608, "(1)"
394 line 418, "pan.___", state 2621, "(1)"
395 line 388, "pan.___", state 2642, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
396 line 397, "pan.___", state 2674, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
397 line 401, "pan.___", state 2688, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
398 line 405, "pan.___", state 2707, "(1)"
399 line 414, "pan.___", state 2737, "(1)"
400 line 418, "pan.___", state 2750, "(1)"
401 line 228, "pan.___", state 2783, "(1)"
402 line 236, "pan.___", state 2803, "(1)"
403 line 240, "pan.___", state 2811, "(1)"
404 line 228, "pan.___", state 2826, "(1)"
405 line 236, "pan.___", state 2846, "(1)"
406 line 240, "pan.___", state 2854, "(1)"
407 line 871, "pan.___", state 2871, "-end-"
409 unreached in proctype urcu_writer
410 line 388, "pan.___", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
411 line 388, "pan.___", state 24, "(1)"
412 line 392, "pan.___", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
413 line 392, "pan.___", state 38, "(1)"
414 line 392, "pan.___", state 39, "(1)"
415 line 392, "pan.___", state 39, "(1)"
416 line 390, "pan.___", state 44, "((i<1))"
417 line 390, "pan.___", state 44, "((i>=1))"
418 line 397, "pan.___", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
419 line 397, "pan.___", state 56, "(1)"
420 line 397, "pan.___", state 57, "(1)"
421 line 397, "pan.___", state 57, "(1)"
422 line 401, "pan.___", state 64, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
423 line 401, "pan.___", state 70, "(1)"
424 line 401, "pan.___", state 71, "(1)"
425 line 401, "pan.___", state 71, "(1)"
426 line 399, "pan.___", state 76, "((i<2))"
427 line 399, "pan.___", state 76, "((i>=2))"
428 line 405, "pan.___", state 83, "(1)"
429 line 405, "pan.___", state 84, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
430 line 405, "pan.___", state 84, "else"
431 line 405, "pan.___", state 87, "(1)"
432 line 405, "pan.___", state 88, "(1)"
433 line 405, "pan.___", state 88, "(1)"
434 line 409, "pan.___", state 96, "(1)"
435 line 409, "pan.___", state 97, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
436 line 409, "pan.___", state 97, "else"
437 line 409, "pan.___", state 100, "(1)"
438 line 409, "pan.___", state 101, "(1)"
439 line 409, "pan.___", state 101, "(1)"
440 line 407, "pan.___", state 106, "((i<1))"
441 line 407, "pan.___", state 106, "((i>=1))"
442 line 414, "pan.___", state 113, "(1)"
443 line 414, "pan.___", state 114, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
444 line 414, "pan.___", state 114, "else"
445 line 414, "pan.___", state 117, "(1)"
446 line 414, "pan.___", state 118, "(1)"
447 line 414, "pan.___", state 118, "(1)"
448 line 418, "pan.___", state 126, "(1)"
449 line 418, "pan.___", state 127, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
450 line 418, "pan.___", state 127, "else"
451 line 418, "pan.___", state 130, "(1)"
452 line 418, "pan.___", state 131, "(1)"
453 line 418, "pan.___", state 131, "(1)"
454 line 416, "pan.___", state 136, "((i<2))"
455 line 416, "pan.___", state 136, "((i>=2))"
456 line 423, "pan.___", state 140, "(1)"
457 line 423, "pan.___", state 140, "(1)"
458 line 251, "pan.___", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
459 line 255, "pan.___", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
460 line 253, "pan.___", state 166, "((i<1))"
461 line 253, "pan.___", state 166, "((i>=1))"
462 line 259, "pan.___", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
463 line 994, "pan.___", state 199, "old_data = cached_rcu_ptr.val[_pid]"
464 line 388, "pan.___", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
465 line 392, "pan.___", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
466 line 397, "pan.___", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
467 line 401, "pan.___", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
468 line 405, "pan.___", state 276, "(1)"
469 line 409, "pan.___", state 289, "(1)"
470 line 414, "pan.___", state 306, "(1)"
471 line 418, "pan.___", state 319, "(1)"
472 line 392, "pan.___", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
473 line 397, "pan.___", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
474 line 401, "pan.___", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
475 line 409, "pan.___", state 420, "(1)"
476 line 414, "pan.___", state 437, "(1)"
477 line 418, "pan.___", state 450, "(1)"
478 line 392, "pan.___", state 491, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
479 line 397, "pan.___", state 509, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
480 line 401, "pan.___", state 523, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
481 line 409, "pan.___", state 555, "(1)"
482 line 414, "pan.___", state 572, "(1)"
483 line 418, "pan.___", state 585, "(1)"
484 line 392, "pan.___", state 619, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
485 line 397, "pan.___", state 637, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
486 line 401, "pan.___", state 651, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
487 line 409, "pan.___", state 683, "(1)"
488 line 414, "pan.___", state 700, "(1)"
489 line 418, "pan.___", state 713, "(1)"
490 line 392, "pan.___", state 748, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
491 line 397, "pan.___", state 766, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
492 line 401, "pan.___", state 780, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
493 line 409, "pan.___", state 812, "(1)"
494 line 414, "pan.___", state 829, "(1)"
495 line 418, "pan.___", state 842, "(1)"
496 line 392, "pan.___", state 879, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
497 line 397, "pan.___", state 897, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
498 line 401, "pan.___", state 911, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
499 line 409, "pan.___", state 943, "(1)"
500 line 414, "pan.___", state 960, "(1)"
501 line 418, "pan.___", state 973, "(1)"
502 line 388, "pan.___", state 999, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
503 line 388, "pan.___", state 1001, "(1)"
504 line 388, "pan.___", state 1002, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
505 line 388, "pan.___", state 1002, "else"
506 line 388, "pan.___", state 1005, "(1)"
507 line 392, "pan.___", state 1013, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
508 line 392, "pan.___", state 1015, "(1)"
509 line 392, "pan.___", state 1016, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
510 line 392, "pan.___", state 1016, "else"
511 line 392, "pan.___", state 1019, "(1)"
512 line 392, "pan.___", state 1020, "(1)"
513 line 392, "pan.___", state 1020, "(1)"
514 line 390, "pan.___", state 1025, "((i<1))"
515 line 390, "pan.___", state 1025, "((i>=1))"
516 line 397, "pan.___", state 1031, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
517 line 397, "pan.___", state 1033, "(1)"
518 line 397, "pan.___", state 1034, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
519 line 397, "pan.___", state 1034, "else"
520 line 397, "pan.___", state 1037, "(1)"
521 line 397, "pan.___", state 1038, "(1)"
522 line 397, "pan.___", state 1038, "(1)"
523 line 401, "pan.___", state 1045, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
524 line 401, "pan.___", state 1047, "(1)"
525 line 401, "pan.___", state 1048, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
526 line 401, "pan.___", state 1048, "else"
527 line 401, "pan.___", state 1051, "(1)"
528 line 401, "pan.___", state 1052, "(1)"
529 line 401, "pan.___", state 1052, "(1)"
530 line 399, "pan.___", state 1057, "((i<2))"
531 line 399, "pan.___", state 1057, "((i>=2))"
532 line 405, "pan.___", state 1064, "(1)"
533 line 405, "pan.___", state 1065, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
534 line 405, "pan.___", state 1065, "else"
535 line 405, "pan.___", state 1068, "(1)"
536 line 405, "pan.___", state 1069, "(1)"
537 line 405, "pan.___", state 1069, "(1)"
538 line 409, "pan.___", state 1077, "(1)"
539 line 409, "pan.___", state 1078, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
540 line 409, "pan.___", state 1078, "else"
541 line 409, "pan.___", state 1081, "(1)"
542 line 409, "pan.___", state 1082, "(1)"
543 line 409, "pan.___", state 1082, "(1)"
544 line 407, "pan.___", state 1087, "((i<1))"
545 line 407, "pan.___", state 1087, "((i>=1))"
546 line 414, "pan.___", state 1094, "(1)"
547 line 414, "pan.___", state 1095, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
548 line 414, "pan.___", state 1095, "else"
549 line 414, "pan.___", state 1098, "(1)"
550 line 414, "pan.___", state 1099, "(1)"
551 line 414, "pan.___", state 1099, "(1)"
552 line 418, "pan.___", state 1107, "(1)"
553 line 418, "pan.___", state 1108, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
554 line 418, "pan.___", state 1108, "else"
555 line 418, "pan.___", state 1111, "(1)"
556 line 418, "pan.___", state 1112, "(1)"
557 line 418, "pan.___", state 1112, "(1)"
558 line 423, "pan.___", state 1121, "(1)"
559 line 423, "pan.___", state 1121, "(1)"
560 line 251, "pan.___", state 1153, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
561 line 255, "pan.___", state 1162, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
562 line 253, "pan.___", state 1170, "((i<1))"
563 line 253, "pan.___", state 1170, "((i>=1))"
564 line 259, "pan.___", state 1177, "(1)"
565 line 259, "pan.___", state 1178, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
566 line 259, "pan.___", state 1178, "else"
567 line 263, "pan.___", state 1184, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
568 line 261, "pan.___", state 1192, "((i<2))"
569 line 261, "pan.___", state 1192, "((i>=2))"
570 line 228, "pan.___", state 1200, "(1)"
571 line 232, "pan.___", state 1208, "(1)"
572 line 232, "pan.___", state 1209, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
573 line 232, "pan.___", state 1209, "else"
574 line 230, "pan.___", state 1214, "((i<1))"
575 line 230, "pan.___", state 1214, "((i>=1))"
576 line 236, "pan.___", state 1220, "(1)"
577 line 236, "pan.___", state 1221, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
578 line 236, "pan.___", state 1221, "else"
579 line 240, "pan.___", state 1228, "(1)"
580 line 240, "pan.___", state 1229, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
581 line 240, "pan.___", state 1229, "else"
582 line 245, "pan.___", state 1238, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
583 line 245, "pan.___", state 1238, "else"
584 line 251, "pan.___", state 1259, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
585 line 255, "pan.___", state 1268, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
586 line 259, "pan.___", state 1281, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
587 line 263, "pan.___", state 1290, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
588 line 228, "pan.___", state 1306, "(1)"
589 line 232, "pan.___", state 1314, "(1)"
590 line 236, "pan.___", state 1326, "(1)"
591 line 240, "pan.___", state 1334, "(1)"
592 line 255, "pan.___", state 1360, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
593 line 259, "pan.___", state 1373, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
594 line 263, "pan.___", state 1382, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
595 line 228, "pan.___", state 1398, "(1)"
596 line 232, "pan.___", state 1406, "(1)"
597 line 236, "pan.___", state 1418, "(1)"
598 line 240, "pan.___", state 1426, "(1)"
599 line 251, "pan.___", state 1457, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
600 line 255, "pan.___", state 1466, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
601 line 259, "pan.___", state 1479, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
602 line 263, "pan.___", state 1488, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
603 line 228, "pan.___", state 1504, "(1)"
604 line 232, "pan.___", state 1512, "(1)"
605 line 236, "pan.___", state 1524, "(1)"
606 line 240, "pan.___", state 1532, "(1)"
607 line 1192, "pan.___", state 1548, "-end-"
609 unreached in proctype :init:
611 unreached in proctype :never:
612 line 1253, "pan.___", state 11, "-end-"
615 pan: elapsed time 14 seconds
616 pan: rate 4238.4725 states/second
617 pan: avg transition delay 1.2667e-06 usec
618 cp .input.spin urcu_progress_writer_error.spin.input
619 cp .input.spin.trail urcu_progress_writer_error.spin.input.trail
620 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
projects / urcu.git / blob