1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-intel-ipi'
2 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
4 cat .input.define >> pan.ltl
6 spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl
7 cp urcu_free_no_mb.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 -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 1295)
19 Depth= 8619 States= 1e+06 Transitions= 8e+06 Memory= 550.432 t= 20.2 R= 5e+04
20 Depth= 8619 States= 2e+06 Transitions= 1.8e+07 Memory= 634.318 t= 46.3 R= 4e+04
21 Depth= 8619 States= 3e+06 Transitions= 2.53e+07 Memory= 718.303 t= 64.9 R= 5e+04
22 pan: resizing hashtable to -w22.. done
23 Depth= 8619 States= 4e+06 Transitions= 3.53e+07 Memory= 833.311 t= 91.4 R= 4e+04
24 Depth= 8619 States= 5e+06 Transitions= 5.71e+07 Memory= 917.295 t= 152 R= 3e+04
25 Depth= 8619 States= 6e+06 Transitions= 6.81e+07 Memory= 1001.279 t= 181 R= 3e+04
26 Depth= 8619 States= 7e+06 Transitions= 8.02e+07 Memory= 1085.264 t= 214 R= 3e+04
27 Depth= 8619 States= 8e+06 Transitions= 8.9e+07 Memory= 1169.151 t= 238 R= 3e+04
28 pan: claim violated! (at depth 1359)
29 pan: wrote .input.spin.trail
31 (Spin Version 5.1.7 -- 23 December 2008)
32 Warning: Search not completed
33 + Partial Order Reduction
35 Full statespace search for:
37 assertion violations + (if within scope of claim)
38 acceptance cycles + (fairness disabled)
39 invalid end states - (disabled by never claim)
41 State-vector 88 byte, depth reached 8619, errors: 1
42 8162162 states, stored
43 81941434 states, matched
44 90103596 transitions (= stored+matched)
45 1.3256628e+09 atomic steps
46 hash conflicts: 60101961 (resolved)
48 Stats on memory usage (in Megabytes):
49 902.949 equivalent memory usage for states (stored*(State-vector + overhead))
50 693.526 actual memory usage for states (compression: 76.81%)
51 state-vector as stored = 61 byte + 28 byte overhead
52 32.000 memory used for hash table (-w22)
53 457.764 memory used for DFS stack (-m10000000)
54 1182.822 total actual memory usage
56 unreached in proctype urcu_reader
57 line 272, "pan.___", state 34, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
58 line 280, "pan.___", state 56, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
59 line 284, "pan.___", state 65, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
60 line 249, "pan.___", state 81, "(1)"
61 line 253, "pan.___", state 89, "(1)"
62 line 257, "pan.___", state 101, "(1)"
63 line 261, "pan.___", state 109, "(1)"
64 line 411, "pan.___", state 135, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
65 line 420, "pan.___", state 167, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
66 line 424, "pan.___", state 181, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
67 line 249, "pan.___", state 199, "(1)"
68 line 257, "pan.___", state 219, "(1)"
69 line 261, "pan.___", state 227, "(1)"
70 line 700, "pan.___", state 246, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
71 line 411, "pan.___", state 253, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
72 line 420, "pan.___", state 285, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
73 line 424, "pan.___", state 299, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
74 line 249, "pan.___", state 317, "(1)"
75 line 257, "pan.___", state 337, "(1)"
76 line 261, "pan.___", state 345, "(1)"
77 line 411, "pan.___", state 364, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
78 line 420, "pan.___", state 396, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
79 line 424, "pan.___", state 410, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
80 line 249, "pan.___", state 428, "(1)"
81 line 257, "pan.___", state 448, "(1)"
82 line 261, "pan.___", state 456, "(1)"
83 line 411, "pan.___", state 477, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
84 line 411, "pan.___", state 479, "(1)"
85 line 411, "pan.___", state 480, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
86 line 411, "pan.___", state 480, "else"
87 line 411, "pan.___", state 483, "(1)"
88 line 415, "pan.___", state 491, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
89 line 415, "pan.___", state 493, "(1)"
90 line 415, "pan.___", state 494, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
91 line 415, "pan.___", state 494, "else"
92 line 415, "pan.___", state 497, "(1)"
93 line 415, "pan.___", state 498, "(1)"
94 line 415, "pan.___", state 498, "(1)"
95 line 413, "pan.___", state 503, "((i<1))"
96 line 413, "pan.___", state 503, "((i>=1))"
97 line 420, "pan.___", state 509, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
98 line 420, "pan.___", state 511, "(1)"
99 line 420, "pan.___", state 512, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
100 line 420, "pan.___", state 512, "else"
101 line 420, "pan.___", state 515, "(1)"
102 line 420, "pan.___", state 516, "(1)"
103 line 420, "pan.___", state 516, "(1)"
104 line 424, "pan.___", state 523, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
105 line 424, "pan.___", state 525, "(1)"
106 line 424, "pan.___", state 526, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
107 line 424, "pan.___", state 526, "else"
108 line 424, "pan.___", state 529, "(1)"
109 line 424, "pan.___", state 530, "(1)"
110 line 424, "pan.___", state 530, "(1)"
111 line 422, "pan.___", state 535, "((i<2))"
112 line 422, "pan.___", state 535, "((i>=2))"
113 line 249, "pan.___", state 541, "(1)"
114 line 253, "pan.___", state 549, "(1)"
115 line 253, "pan.___", state 550, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
116 line 253, "pan.___", state 550, "else"
117 line 251, "pan.___", state 555, "((i<1))"
118 line 251, "pan.___", state 555, "((i>=1))"
119 line 257, "pan.___", state 561, "(1)"
120 line 257, "pan.___", state 562, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
121 line 257, "pan.___", state 562, "else"
122 line 261, "pan.___", state 569, "(1)"
123 line 261, "pan.___", state 570, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
124 line 261, "pan.___", state 570, "else"
125 line 259, "pan.___", state 575, "((i<2))"
126 line 259, "pan.___", state 575, "((i>=2))"
127 line 266, "pan.___", state 579, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
128 line 266, "pan.___", state 579, "else"
129 line 431, "pan.___", state 581, "(1)"
130 line 431, "pan.___", state 581, "(1)"
131 line 700, "pan.___", state 584, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
132 line 700, "pan.___", state 585, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
133 line 700, "pan.___", state 586, "(1)"
134 line 411, "pan.___", state 593, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
135 line 420, "pan.___", state 625, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
136 line 424, "pan.___", state 639, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
137 line 249, "pan.___", state 657, "(1)"
138 line 257, "pan.___", state 677, "(1)"
139 line 261, "pan.___", state 685, "(1)"
140 line 411, "pan.___", state 711, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
141 line 420, "pan.___", state 743, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
142 line 424, "pan.___", state 757, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
143 line 249, "pan.___", state 775, "(1)"
144 line 257, "pan.___", state 795, "(1)"
145 line 261, "pan.___", state 803, "(1)"
146 line 411, "pan.___", state 822, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
147 line 411, "pan.___", state 824, "(1)"
148 line 411, "pan.___", state 825, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
149 line 411, "pan.___", state 825, "else"
150 line 411, "pan.___", state 828, "(1)"
151 line 415, "pan.___", state 836, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
152 line 415, "pan.___", state 838, "(1)"
153 line 415, "pan.___", state 839, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
154 line 415, "pan.___", state 839, "else"
155 line 415, "pan.___", state 842, "(1)"
156 line 415, "pan.___", state 843, "(1)"
157 line 415, "pan.___", state 843, "(1)"
158 line 413, "pan.___", state 848, "((i<1))"
159 line 413, "pan.___", state 848, "((i>=1))"
160 line 420, "pan.___", state 854, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
161 line 420, "pan.___", state 856, "(1)"
162 line 420, "pan.___", state 857, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
163 line 420, "pan.___", state 857, "else"
164 line 420, "pan.___", state 860, "(1)"
165 line 420, "pan.___", state 861, "(1)"
166 line 420, "pan.___", state 861, "(1)"
167 line 424, "pan.___", state 868, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
168 line 424, "pan.___", state 870, "(1)"
169 line 424, "pan.___", state 871, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
170 line 424, "pan.___", state 871, "else"
171 line 424, "pan.___", state 874, "(1)"
172 line 424, "pan.___", state 875, "(1)"
173 line 424, "pan.___", state 875, "(1)"
174 line 422, "pan.___", state 880, "((i<2))"
175 line 422, "pan.___", state 880, "((i>=2))"
176 line 249, "pan.___", state 886, "(1)"
177 line 253, "pan.___", state 894, "(1)"
178 line 253, "pan.___", state 895, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
179 line 253, "pan.___", state 895, "else"
180 line 251, "pan.___", state 900, "((i<1))"
181 line 251, "pan.___", state 900, "((i>=1))"
182 line 257, "pan.___", state 906, "(1)"
183 line 257, "pan.___", state 907, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
184 line 257, "pan.___", state 907, "else"
185 line 261, "pan.___", state 914, "(1)"
186 line 261, "pan.___", state 915, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
187 line 261, "pan.___", state 915, "else"
188 line 259, "pan.___", state 920, "((i<2))"
189 line 259, "pan.___", state 920, "((i>=2))"
190 line 266, "pan.___", state 924, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
191 line 266, "pan.___", state 924, "else"
192 line 431, "pan.___", state 926, "(1)"
193 line 431, "pan.___", state 926, "(1)"
194 line 708, "pan.___", state 930, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
195 line 411, "pan.___", state 935, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
196 line 420, "pan.___", state 967, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
197 line 424, "pan.___", state 981, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
198 line 249, "pan.___", state 999, "(1)"
199 line 257, "pan.___", state 1019, "(1)"
200 line 261, "pan.___", state 1027, "(1)"
201 line 411, "pan.___", state 1049, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
202 line 420, "pan.___", state 1081, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
203 line 424, "pan.___", state 1095, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
204 line 249, "pan.___", state 1113, "(1)"
205 line 257, "pan.___", state 1133, "(1)"
206 line 261, "pan.___", state 1141, "(1)"
207 line 411, "pan.___", state 1164, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
208 line 420, "pan.___", state 1196, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
209 line 424, "pan.___", state 1210, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
210 line 249, "pan.___", state 1228, "(1)"
211 line 257, "pan.___", state 1248, "(1)"
212 line 261, "pan.___", state 1256, "(1)"
213 line 411, "pan.___", state 1275, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
214 line 420, "pan.___", state 1307, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
215 line 424, "pan.___", state 1321, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
216 line 249, "pan.___", state 1339, "(1)"
217 line 257, "pan.___", state 1359, "(1)"
218 line 261, "pan.___", state 1367, "(1)"
219 line 411, "pan.___", state 1391, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
220 line 420, "pan.___", state 1423, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
221 line 424, "pan.___", state 1437, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
222 line 249, "pan.___", state 1455, "(1)"
223 line 257, "pan.___", state 1475, "(1)"
224 line 261, "pan.___", state 1483, "(1)"
225 line 411, "pan.___", state 1502, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
226 line 420, "pan.___", state 1534, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
227 line 424, "pan.___", state 1548, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
228 line 249, "pan.___", state 1566, "(1)"
229 line 257, "pan.___", state 1586, "(1)"
230 line 261, "pan.___", state 1594, "(1)"
231 line 411, "pan.___", state 1616, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
232 line 420, "pan.___", state 1648, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
233 line 424, "pan.___", state 1662, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
234 line 249, "pan.___", state 1680, "(1)"
235 line 257, "pan.___", state 1700, "(1)"
236 line 261, "pan.___", state 1708, "(1)"
237 line 747, "pan.___", state 1727, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
238 line 411, "pan.___", state 1734, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
239 line 420, "pan.___", state 1766, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
240 line 424, "pan.___", state 1780, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
241 line 249, "pan.___", state 1798, "(1)"
242 line 257, "pan.___", state 1818, "(1)"
243 line 261, "pan.___", state 1826, "(1)"
244 line 411, "pan.___", state 1845, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
245 line 420, "pan.___", state 1877, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
246 line 424, "pan.___", state 1891, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
247 line 249, "pan.___", state 1909, "(1)"
248 line 257, "pan.___", state 1929, "(1)"
249 line 261, "pan.___", state 1937, "(1)"
250 line 411, "pan.___", state 1958, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
251 line 411, "pan.___", state 1960, "(1)"
252 line 411, "pan.___", state 1961, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
253 line 411, "pan.___", state 1961, "else"
254 line 411, "pan.___", state 1964, "(1)"
255 line 415, "pan.___", state 1972, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
256 line 415, "pan.___", state 1974, "(1)"
257 line 415, "pan.___", state 1975, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
258 line 415, "pan.___", state 1975, "else"
259 line 415, "pan.___", state 1978, "(1)"
260 line 415, "pan.___", state 1979, "(1)"
261 line 415, "pan.___", state 1979, "(1)"
262 line 413, "pan.___", state 1984, "((i<1))"
263 line 413, "pan.___", state 1984, "((i>=1))"
264 line 420, "pan.___", state 1990, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
265 line 420, "pan.___", state 1992, "(1)"
266 line 420, "pan.___", state 1993, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
267 line 420, "pan.___", state 1993, "else"
268 line 420, "pan.___", state 1996, "(1)"
269 line 420, "pan.___", state 1997, "(1)"
270 line 420, "pan.___", state 1997, "(1)"
271 line 424, "pan.___", state 2004, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
272 line 424, "pan.___", state 2006, "(1)"
273 line 424, "pan.___", state 2007, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
274 line 424, "pan.___", state 2007, "else"
275 line 424, "pan.___", state 2010, "(1)"
276 line 424, "pan.___", state 2011, "(1)"
277 line 424, "pan.___", state 2011, "(1)"
278 line 422, "pan.___", state 2016, "((i<2))"
279 line 422, "pan.___", state 2016, "((i>=2))"
280 line 249, "pan.___", state 2022, "(1)"
281 line 253, "pan.___", state 2030, "(1)"
282 line 253, "pan.___", state 2031, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
283 line 253, "pan.___", state 2031, "else"
284 line 251, "pan.___", state 2036, "((i<1))"
285 line 251, "pan.___", state 2036, "((i>=1))"
286 line 257, "pan.___", state 2042, "(1)"
287 line 257, "pan.___", state 2043, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
288 line 257, "pan.___", state 2043, "else"
289 line 261, "pan.___", state 2050, "(1)"
290 line 261, "pan.___", state 2051, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
291 line 261, "pan.___", state 2051, "else"
292 line 259, "pan.___", state 2056, "((i<2))"
293 line 259, "pan.___", state 2056, "((i>=2))"
294 line 266, "pan.___", state 2060, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
295 line 266, "pan.___", state 2060, "else"
296 line 431, "pan.___", state 2062, "(1)"
297 line 431, "pan.___", state 2062, "(1)"
298 line 747, "pan.___", state 2065, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
299 line 747, "pan.___", state 2066, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
300 line 747, "pan.___", state 2067, "(1)"
301 line 411, "pan.___", state 2074, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
302 line 420, "pan.___", state 2106, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
303 line 424, "pan.___", state 2120, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
304 line 249, "pan.___", state 2138, "(1)"
305 line 257, "pan.___", state 2158, "(1)"
306 line 261, "pan.___", state 2166, "(1)"
307 line 411, "pan.___", state 2191, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
308 line 420, "pan.___", state 2223, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
309 line 424, "pan.___", state 2237, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
310 line 249, "pan.___", state 2255, "(1)"
311 line 257, "pan.___", state 2275, "(1)"
312 line 261, "pan.___", state 2283, "(1)"
313 line 411, "pan.___", state 2302, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
314 line 420, "pan.___", state 2334, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
315 line 424, "pan.___", state 2348, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
316 line 249, "pan.___", state 2366, "(1)"
317 line 257, "pan.___", state 2386, "(1)"
318 line 261, "pan.___", state 2394, "(1)"
319 line 249, "pan.___", state 2425, "(1)"
320 line 257, "pan.___", state 2445, "(1)"
321 line 261, "pan.___", state 2453, "(1)"
322 line 249, "pan.___", state 2468, "(1)"
323 line 257, "pan.___", state 2488, "(1)"
324 line 261, "pan.___", state 2496, "(1)"
325 line 898, "pan.___", state 2513, "-end-"
327 unreached in proctype urcu_writer
328 line 411, "pan.___", state 20, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
329 line 411, "pan.___", state 26, "(1)"
330 line 415, "pan.___", state 34, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
331 line 415, "pan.___", state 40, "(1)"
332 line 415, "pan.___", state 41, "(1)"
333 line 415, "pan.___", state 41, "(1)"
334 line 413, "pan.___", state 46, "((i<1))"
335 line 413, "pan.___", state 46, "((i>=1))"
336 line 420, "pan.___", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
337 line 420, "pan.___", state 58, "(1)"
338 line 420, "pan.___", state 59, "(1)"
339 line 420, "pan.___", state 59, "(1)"
340 line 424, "pan.___", state 72, "(1)"
341 line 424, "pan.___", state 73, "(1)"
342 line 424, "pan.___", state 73, "(1)"
343 line 422, "pan.___", state 78, "((i<2))"
344 line 422, "pan.___", state 78, "((i>=2))"
345 line 249, "pan.___", state 84, "(1)"
346 line 253, "pan.___", state 92, "(1)"
347 line 253, "pan.___", state 93, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
348 line 253, "pan.___", state 93, "else"
349 line 251, "pan.___", state 98, "((i<1))"
350 line 251, "pan.___", state 98, "((i>=1))"
351 line 257, "pan.___", state 104, "(1)"
352 line 257, "pan.___", state 105, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
353 line 257, "pan.___", state 105, "else"
354 line 261, "pan.___", state 112, "(1)"
355 line 261, "pan.___", state 113, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
356 line 261, "pan.___", state 113, "else"
357 line 259, "pan.___", state 118, "((i<2))"
358 line 259, "pan.___", state 118, "((i>=2))"
359 line 266, "pan.___", state 122, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
360 line 266, "pan.___", state 122, "else"
361 line 431, "pan.___", state 124, "(1)"
362 line 431, "pan.___", state 124, "(1)"
363 line 272, "pan.___", state 133, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
364 line 276, "pan.___", state 142, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
365 line 274, "pan.___", state 150, "((i<1))"
366 line 274, "pan.___", state 150, "((i>=1))"
367 line 280, "pan.___", state 155, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
368 line 1021, "pan.___", state 183, "old_data = cached_rcu_ptr.val[_pid]"
369 line 1032, "pan.___", state 187, "_proc_urcu_writer = (_proc_urcu_writer|(1<<4))"
370 line 411, "pan.___", state 195, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
371 line 411, "pan.___", state 201, "(1)"
372 line 415, "pan.___", state 209, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
373 line 415, "pan.___", state 215, "(1)"
374 line 415, "pan.___", state 216, "(1)"
375 line 415, "pan.___", state 216, "(1)"
376 line 420, "pan.___", state 229, "(1)"
377 line 424, "pan.___", state 241, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
378 line 249, "pan.___", state 259, "(1)"
379 line 253, "pan.___", state 267, "(1)"
380 line 261, "pan.___", state 287, "(1)"
381 line 431, "pan.___", state 299, "(1)"
382 line 431, "pan.___", state 299, "(1)"
383 line 415, "pan.___", state 322, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
384 line 424, "pan.___", state 354, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
385 line 253, "pan.___", state 380, "(1)"
386 line 261, "pan.___", state 400, "(1)"
387 line 415, "pan.___", state 443, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
388 line 253, "pan.___", state 501, "(1)"
389 line 415, "pan.___", state 554, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
390 line 253, "pan.___", state 612, "(1)"
391 line 415, "pan.___", state 667, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
392 line 424, "pan.___", state 699, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
393 line 253, "pan.___", state 725, "(1)"
394 line 261, "pan.___", state 745, "(1)"
395 line 1168, "pan.___", state 770, "_proc_urcu_writer = (_proc_urcu_writer|(1<<13))"
396 line 272, "pan.___", state 798, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
397 line 272, "pan.___", state 800, "(1)"
398 line 276, "pan.___", state 807, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
399 line 276, "pan.___", state 809, "(1)"
400 line 276, "pan.___", state 810, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
401 line 276, "pan.___", state 810, "else"
402 line 274, "pan.___", state 815, "((i<1))"
403 line 274, "pan.___", state 815, "((i>=1))"
404 line 280, "pan.___", state 820, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
405 line 280, "pan.___", state 822, "(1)"
406 line 280, "pan.___", state 823, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
407 line 280, "pan.___", state 823, "else"
408 line 284, "pan.___", state 829, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
409 line 284, "pan.___", state 831, "(1)"
410 line 284, "pan.___", state 832, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
411 line 284, "pan.___", state 832, "else"
412 line 282, "pan.___", state 837, "((i<2))"
413 line 282, "pan.___", state 837, "((i>=2))"
414 line 249, "pan.___", state 845, "(1)"
415 line 253, "pan.___", state 853, "(1)"
416 line 253, "pan.___", state 854, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
417 line 253, "pan.___", state 854, "else"
418 line 251, "pan.___", state 859, "((i<1))"
419 line 251, "pan.___", state 859, "((i>=1))"
420 line 257, "pan.___", state 865, "(1)"
421 line 257, "pan.___", state 866, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
422 line 257, "pan.___", state 866, "else"
423 line 261, "pan.___", state 873, "(1)"
424 line 261, "pan.___", state 874, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
425 line 261, "pan.___", state 874, "else"
426 line 266, "pan.___", state 883, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
427 line 266, "pan.___", state 883, "else"
428 line 1222, "pan.___", state 899, "((i<1))"
429 line 1222, "pan.___", state 899, "((i>=1))"
430 line 272, "pan.___", state 904, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
431 line 272, "pan.___", state 906, "(1)"
432 line 276, "pan.___", state 913, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
433 line 276, "pan.___", state 915, "(1)"
434 line 276, "pan.___", state 916, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
435 line 276, "pan.___", state 916, "else"
436 line 274, "pan.___", state 921, "((i<1))"
437 line 274, "pan.___", state 921, "((i>=1))"
438 line 280, "pan.___", state 926, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
439 line 280, "pan.___", state 928, "(1)"
440 line 280, "pan.___", state 929, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
441 line 280, "pan.___", state 929, "else"
442 line 284, "pan.___", state 935, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
443 line 284, "pan.___", state 937, "(1)"
444 line 284, "pan.___", state 938, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
445 line 284, "pan.___", state 938, "else"
446 line 282, "pan.___", state 943, "((i<2))"
447 line 282, "pan.___", state 943, "((i>=2))"
448 line 249, "pan.___", state 951, "(1)"
449 line 253, "pan.___", state 959, "(1)"
450 line 253, "pan.___", state 960, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
451 line 253, "pan.___", state 960, "else"
452 line 251, "pan.___", state 965, "((i<1))"
453 line 251, "pan.___", state 965, "((i>=1))"
454 line 257, "pan.___", state 971, "(1)"
455 line 257, "pan.___", state 972, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
456 line 257, "pan.___", state 972, "else"
457 line 261, "pan.___", state 979, "(1)"
458 line 261, "pan.___", state 980, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
459 line 261, "pan.___", state 980, "else"
460 line 266, "pan.___", state 989, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
461 line 266, "pan.___", state 989, "else"
462 line 299, "pan.___", state 991, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
463 line 299, "pan.___", state 991, "else"
464 line 1222, "pan.___", state 992, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
465 line 1222, "pan.___", state 992, "else"
466 line 276, "pan.___", state 1005, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
467 line 280, "pan.___", state 1018, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
468 line 284, "pan.___", state 1027, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
469 line 249, "pan.___", state 1043, "(1)"
470 line 253, "pan.___", state 1051, "(1)"
471 line 257, "pan.___", state 1063, "(1)"
472 line 261, "pan.___", state 1071, "(1)"
473 line 272, "pan.___", state 1102, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
474 line 276, "pan.___", state 1111, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
475 line 280, "pan.___", state 1124, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
476 line 284, "pan.___", state 1133, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
477 line 249, "pan.___", state 1149, "(1)"
478 line 253, "pan.___", state 1157, "(1)"
479 line 257, "pan.___", state 1169, "(1)"
480 line 261, "pan.___", state 1177, "(1)"
481 line 276, "pan.___", state 1203, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
482 line 284, "pan.___", state 1225, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
483 line 249, "pan.___", state 1241, "(1)"
484 line 253, "pan.___", state 1249, "(1)"
485 line 257, "pan.___", state 1261, "(1)"
486 line 261, "pan.___", state 1269, "(1)"
487 line 272, "pan.___", state 1300, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
488 line 276, "pan.___", state 1309, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
489 line 280, "pan.___", state 1322, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
490 line 284, "pan.___", state 1331, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
491 line 249, "pan.___", state 1347, "(1)"
492 line 253, "pan.___", state 1355, "(1)"
493 line 257, "pan.___", state 1367, "(1)"
494 line 261, "pan.___", state 1375, "(1)"
495 line 272, "pan.___", state 1392, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
496 line 272, "pan.___", state 1394, "(1)"
497 line 276, "pan.___", state 1401, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
498 line 276, "pan.___", state 1403, "(1)"
499 line 276, "pan.___", state 1404, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
500 line 276, "pan.___", state 1404, "else"
501 line 274, "pan.___", state 1409, "((i<1))"
502 line 274, "pan.___", state 1409, "((i>=1))"
503 line 280, "pan.___", state 1414, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
504 line 280, "pan.___", state 1416, "(1)"
505 line 280, "pan.___", state 1417, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
506 line 280, "pan.___", state 1417, "else"
507 line 284, "pan.___", state 1423, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
508 line 284, "pan.___", state 1425, "(1)"
509 line 284, "pan.___", state 1426, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
510 line 284, "pan.___", state 1426, "else"
511 line 282, "pan.___", state 1431, "((i<2))"
512 line 282, "pan.___", state 1431, "((i>=2))"
513 line 249, "pan.___", state 1439, "(1)"
514 line 253, "pan.___", state 1447, "(1)"
515 line 253, "pan.___", state 1448, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
516 line 253, "pan.___", state 1448, "else"
517 line 251, "pan.___", state 1453, "((i<1))"
518 line 251, "pan.___", state 1453, "((i>=1))"
519 line 257, "pan.___", state 1459, "(1)"
520 line 257, "pan.___", state 1460, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
521 line 257, "pan.___", state 1460, "else"
522 line 261, "pan.___", state 1467, "(1)"
523 line 261, "pan.___", state 1468, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
524 line 261, "pan.___", state 1468, "else"
525 line 266, "pan.___", state 1477, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
526 line 266, "pan.___", state 1477, "else"
527 line 1233, "pan.___", state 1480, "i = 0"
528 line 1233, "pan.___", state 1482, "reader_barrier = 1"
529 line 1233, "pan.___", state 1493, "((i<1))"
530 line 1233, "pan.___", state 1493, "((i>=1))"
531 line 272, "pan.___", state 1498, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
532 line 272, "pan.___", state 1500, "(1)"
533 line 276, "pan.___", state 1507, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
534 line 276, "pan.___", state 1509, "(1)"
535 line 276, "pan.___", state 1510, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
536 line 276, "pan.___", state 1510, "else"
537 line 274, "pan.___", state 1515, "((i<1))"
538 line 274, "pan.___", state 1515, "((i>=1))"
539 line 280, "pan.___", state 1520, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
540 line 280, "pan.___", state 1522, "(1)"
541 line 280, "pan.___", state 1523, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
542 line 280, "pan.___", state 1523, "else"
543 line 284, "pan.___", state 1529, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
544 line 284, "pan.___", state 1531, "(1)"
545 line 284, "pan.___", state 1532, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
546 line 284, "pan.___", state 1532, "else"
547 line 282, "pan.___", state 1537, "((i<2))"
548 line 282, "pan.___", state 1537, "((i>=2))"
549 line 249, "pan.___", state 1545, "(1)"
550 line 253, "pan.___", state 1553, "(1)"
551 line 253, "pan.___", state 1554, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
552 line 253, "pan.___", state 1554, "else"
553 line 251, "pan.___", state 1559, "((i<1))"
554 line 251, "pan.___", state 1559, "((i>=1))"
555 line 257, "pan.___", state 1565, "(1)"
556 line 257, "pan.___", state 1566, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
557 line 257, "pan.___", state 1566, "else"
558 line 261, "pan.___", state 1573, "(1)"
559 line 261, "pan.___", state 1574, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
560 line 261, "pan.___", state 1574, "else"
561 line 266, "pan.___", state 1583, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
562 line 266, "pan.___", state 1583, "else"
563 line 299, "pan.___", state 1585, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
564 line 299, "pan.___", state 1585, "else"
565 line 1233, "pan.___", state 1586, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
566 line 1233, "pan.___", state 1586, "else"
567 line 1237, "pan.___", state 1589, "-end-"
569 unreached in proctype :init:
570 line 1248, "pan.___", state 9, "((j<2))"
571 line 1248, "pan.___", state 9, "((j>=2))"
572 line 1249, "pan.___", state 20, "((j<2))"
573 line 1249, "pan.___", state 20, "((j>=2))"
574 line 1254, "pan.___", state 33, "((j<2))"
575 line 1254, "pan.___", state 33, "((j>=2))"
576 line 1252, "pan.___", state 43, "((i<1))"
577 line 1252, "pan.___", state 43, "((i>=1))"
578 line 1262, "pan.___", state 54, "((j<2))"
579 line 1262, "pan.___", state 54, "((j>=2))"
580 line 1266, "pan.___", state 67, "((j<2))"
581 line 1266, "pan.___", state 67, "((j>=2))"
583 unreached in proctype :never:
584 line 1300, "pan.___", state 8, "-end-"
587 pan: elapsed time 241 seconds
588 pan: rate 33888.985 states/second
589 pan: avg transition delay 2.673e-06 usec
590 cp .input.spin urcu_free_no_mb.spin.input
591 cp .input.spin.trail urcu_free_no_mb.spin.input.trail
592 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-intel-ipi'
projects / urcu.git / blob