1 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
3 cat .input.define > pan.ltl
5 spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
6 cp urcu_progress_writer.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 -f -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 23: Claim reached state 9 (line 1263)
19 depth 51: Claim reached state 9 (line 1262)
20 Depth= 6084 States= 1e+06 Transitions= 2e+08 Memory= 516.838 t= 264 R= 4e+03
21 Depth= 7018 States= 2e+06 Transitions= 4.38e+08 Memory= 566.154 t= 585 R= 3e+03
22 Depth= 7018 States= 3e+06 Transitions= 6.49e+08 Memory= 616.545 t= 870 R= 3e+03
23 pan: resizing hashtable to -w22.. done
24 Depth= 7018 States= 4e+06 Transitions= 8.46e+08 Memory= 698.447 t= 1.13e+03 R= 4e+03
25 Depth= 7018 States= 5e+06 Transitions= 1.29e+09 Memory= 742.979 t= 1.73e+03 R= 3e+03
26 Depth= 7018 States= 6e+06 Transitions= 1.8e+09 Memory= 789.170 t= 2.44e+03 R= 2e+03
27 Depth= 7018 States= 7e+06 Transitions= 2.27e+09 Memory= 833.506 t= 3.09e+03 R= 2e+03
28 Depth= 7018 States= 8e+06 Transitions= 2.76e+09 Memory= 880.283 t= 3.76e+03 R= 2e+03
29 Depth= 7018 States= 9e+06 Transitions= 3.05e+09 Memory= 928.135 t= 4.16e+03 R= 2e+03
30 pan: resizing hashtable to -w24.. done
31 Depth= 7018 States= 1e+07 Transitions= 3.3e+09 Memory= 1102.815 t= 4.5e+03 R= 2e+03
32 Depth= 7018 States= 1.1e+07 Transitions= 3.74e+09 Memory= 1148.322 t= 5.08e+03 R= 2e+03
33 Depth= 7018 States= 1.2e+07 Transitions= 4.65e+09 Memory= 1195.783 t= 6.37e+03 R= 2e+03
34 Depth= 7018 States= 1.3e+07 Transitions= 5.63e+09 Memory= 1235.334 t= 7.72e+03 R= 2e+03
35 Depth= 7018 States= 1.4e+07 Transitions= 6.21e+09 Memory= 1277.912 t= 8.53e+03 R= 2e+03
36 Depth= 7018 States= 1.5e+07 Transitions= 6.77e+09 Memory= 1325.276 t= 9.3e+03 R= 2e+03
37 Depth= 7018 States= 1.6e+07 Transitions= 7.05e+09 Memory= 1372.248 t= 9.68e+03 R= 2e+03
38 Depth= 7018 States= 1.7e+07 Transitions= 7.66e+09 Memory= 1417.463 t= 1.05e+04 R= 2e+03
39 Depth= 7018 States= 1.8e+07 Transitions= 8.25e+09 Memory= 1463.264 t= 1.13e+04 R= 2e+03
40 Depth= 7018 States= 1.9e+07 Transitions= 8.65e+09 Memory= 1513.068 t= 1.19e+04 R= 2e+03
41 Depth= 7018 States= 2e+07 Transitions= 8.97e+09 Memory= 1561.408 t= 1.23e+04 R= 2e+03
42 Depth= 7018 States= 2.1e+07 Transitions= 9.29e+09 Memory= 1609.651 t= 1.28e+04 R= 2e+03
43 Depth= 7018 States= 2.2e+07 Transitions= 9.65e+09 Memory= 1659.065 t= 1.33e+04 R= 2e+03
44 Depth= 7018 States= 2.3e+07 Transitions= 9.91e+09 Memory= 1708.186 t= 1.36e+04 R= 2e+03
45 Depth= 7018 States= 2.4e+07 Transitions= 1.03e+10 Memory= 1757.307 t= 1.41e+04 R= 2e+03
46 Depth= 7018 States= 2.5e+07 Transitions= 1.05e+10 Memory= 1807.014 t= 1.45e+04 R= 2e+03
47 Depth= 7018 States= 2.6e+07 Transitions= 1.09e+10 Memory= 1856.623 t= 1.49e+04 R= 2e+03
48 Depth= 7018 States= 2.7e+07 Transitions= 1.12e+10 Memory= 1906.428 t= 1.54e+04 R= 2e+03
49 Depth= 7018 States= 2.8e+07 Transitions= 1.16e+10 Memory= 1951.838 t= 1.59e+04 R= 2e+03
50 Depth= 7018 States= 2.9e+07 Transitions= 1.2e+10 Memory= 1998.615 t= 1.65e+04 R= 2e+03
51 Depth= 7018 States= 3e+07 Transitions= 1.25e+10 Memory= 2044.026 t= 1.73e+04 R= 2e+03
52 Depth= 7018 States= 3.1e+07 Transitions= 1.31e+10 Memory= 2087.971 t= 1.8e+04 R= 2e+03
53 Depth= 7018 States= 3.2e+07 Transitions= 1.36e+10 Memory= 2134.455 t= 1.87e+04 R= 2e+03
54 Depth= 7018 States= 3.3e+07 Transitions= 1.39e+10 Memory= 2181.818 t= 1.92e+04 R= 2e+03
55 Depth= 7018 States= 3.4e+07 Transitions= 1.42e+10 Memory= 2232.795 t= 1.95e+04 R= 2e+03
56 pan: resizing hashtable to -w26.. done
57 Depth= 7018 States= 3.5e+07 Transitions= 1.45e+10 Memory= 2776.338 t= 1.99e+04 R= 2e+03
58 Depth= 7018 States= 3.6e+07 Transitions= 1.52e+10 Memory= 2822.041 t= 2.09e+04 R= 2e+03
59 Depth= 7018 States= 3.7e+07 Transitions= 1.62e+10 Memory= 2866.182 t= 2.23e+04 R= 2e+03
60 Depth= 7018 States= 3.8e+07 Transitions= 1.7e+10 Memory= 2904.365 t= 2.35e+04 R= 2e+03
61 Depth= 7018 States= 3.9e+07 Transitions= 1.76e+10 Memory= 2950.361 t= 2.43e+04 R= 2e+03
62 Depth= 7018 States= 4e+07 Transitions= 1.79e+10 Memory= 2998.701 t= 2.47e+04 R= 2e+03
63 Depth= 7018 States= 4.1e+07 Transitions= 1.84e+10 Memory= 3044.600 t= 2.53e+04 R= 2e+03
64 Depth= 7018 States= 4.2e+07 Transitions= 1.89e+10 Memory= 3090.498 t= 2.61e+04 R= 2e+03
65 Depth= 7018 States= 4.3e+07 Transitions= 1.95e+10 Memory= 3136.885 t= 2.68e+04 R= 2e+03
66 Depth= 7018 States= 4.4e+07 Transitions= 1.98e+10 Memory= 3186.299 t= 2.73e+04 R= 2e+03
67 Depth= 7018 States= 4.5e+07 Transitions= 2.01e+10 Memory= 3235.225 t= 2.77e+04 R= 2e+03
68 Depth= 7018 States= 4.6e+07 Transitions= 2.04e+10 Memory= 3284.541 t= 2.82e+04 R= 2e+03
69 Depth= 7018 States= 4.7e+07 Transitions= 2.08e+10 Memory= 3334.541 t= 2.87e+04 R= 2e+03
70 Depth= 7018 States= 4.8e+07 Transitions= 2.11e+10 Memory= 3383.565 t= 2.91e+04 R= 2e+03
71 Depth= 7018 States= 4.9e+07 Transitions= 2.14e+10 Memory= 3432.588 t= 2.95e+04 R= 2e+03
72 Depth= 7018 States= 5e+07 Transitions= 2.17e+10 Memory= 3483.369 t= 2.99e+04 R= 2e+03
73 Depth= 7018 States= 5.1e+07 Transitions= 2.21e+10 Memory= 3532.490 t= 3.04e+04 R= 2e+03
74 Depth= 7018 States= 5.2e+07 Transitions= 2.23e+10 Memory= 3580.147 t= 3.07e+04 R= 2e+03
75 Depth= 7018 States= 5.3e+07 Transitions= 2.27e+10 Memory= 3625.752 t= 3.13e+04 R= 2e+03
76 Depth= 7018 States= 5.4e+07 Transitions= 2.32e+10 Memory= 3671.943 t= 3.2e+04 R= 2e+03
77 Depth= 7018 States= 5.5e+07 Transitions= 2.38e+10 Memory= 3715.693 t= 3.27e+04 R= 2e+03
78 Depth= 7018 States= 5.6e+07 Transitions= 2.42e+10 Memory= 3762.276 t= 3.33e+04 R= 2e+03
79 Depth= 7018 States= 5.7e+07 Transitions= 2.48e+10 Memory= 3808.565 t= 3.41e+04 R= 2e+03
80 Depth= 7018 States= 5.8e+07 Transitions= 2.53e+10 Memory= 3855.440 t= 3.48e+04 R= 2e+03
82 (Spin Version 5.1.7 -- 23 December 2008)
83 + Partial Order Reduction
85 Full statespace search for:
87 assertion violations + (if within scope of claim)
88 acceptance cycles + (fairness enabled)
89 invalid end states - (disabled by never claim)
91 State-vector 88 byte, depth reached 7018, errors: 0
92 32735820 states, stored (5.82355e+07 visited)
93 2.5283515e+10 states, matched
94 2.534175e+10 transitions (= visited+matched)
95 1.4761827e+11 atomic steps
96 hash conflicts: 8.6523014e+09 (resolved)
98 Stats on memory usage (in Megabytes):
99 3621.440 equivalent memory usage for states (stored*(State-vector + overhead))
100 2898.114 actual memory usage for states (compression: 80.03%)
101 state-vector as stored = 65 byte + 28 byte overhead
102 512.000 memory used for hash table (-w26)
103 457.764 memory used for DFS stack (-m10000000)
104 1.598 memory lost to fragmentation
105 3866.279 total actual memory usage
107 unreached in proctype urcu_reader
108 line 250, "pan.___", state 30, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
109 line 258, "pan.___", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
110 line 262, "pan.___", state 61, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
111 line 227, "pan.___", state 77, "(1)"
112 line 231, "pan.___", state 85, "(1)"
113 line 235, "pan.___", state 97, "(1)"
114 line 239, "pan.___", state 105, "(1)"
115 line 395, "pan.___", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
116 line 404, "pan.___", state 163, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
117 line 408, "pan.___", state 177, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
118 line 412, "pan.___", state 196, "(1)"
119 line 421, "pan.___", state 226, "(1)"
120 line 425, "pan.___", state 239, "(1)"
121 line 670, "pan.___", state 260, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
122 line 395, "pan.___", state 267, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
123 line 404, "pan.___", state 299, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
124 line 408, "pan.___", state 313, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
125 line 412, "pan.___", state 332, "(1)"
126 line 421, "pan.___", state 362, "(1)"
127 line 425, "pan.___", state 375, "(1)"
128 line 395, "pan.___", state 396, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
129 line 404, "pan.___", state 428, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
130 line 408, "pan.___", state 442, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
131 line 412, "pan.___", state 461, "(1)"
132 line 421, "pan.___", state 491, "(1)"
133 line 425, "pan.___", state 504, "(1)"
134 line 395, "pan.___", state 527, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
135 line 395, "pan.___", state 529, "(1)"
136 line 395, "pan.___", state 530, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
137 line 395, "pan.___", state 530, "else"
138 line 395, "pan.___", state 533, "(1)"
139 line 399, "pan.___", state 541, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
140 line 399, "pan.___", state 543, "(1)"
141 line 399, "pan.___", state 544, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
142 line 399, "pan.___", state 544, "else"
143 line 399, "pan.___", state 547, "(1)"
144 line 399, "pan.___", state 548, "(1)"
145 line 399, "pan.___", state 548, "(1)"
146 line 397, "pan.___", state 553, "((i<1))"
147 line 397, "pan.___", state 553, "((i>=1))"
148 line 404, "pan.___", state 559, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
149 line 404, "pan.___", state 561, "(1)"
150 line 404, "pan.___", state 562, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
151 line 404, "pan.___", state 562, "else"
152 line 404, "pan.___", state 565, "(1)"
153 line 404, "pan.___", state 566, "(1)"
154 line 404, "pan.___", state 566, "(1)"
155 line 408, "pan.___", state 573, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
156 line 408, "pan.___", state 575, "(1)"
157 line 408, "pan.___", state 576, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
158 line 408, "pan.___", state 576, "else"
159 line 408, "pan.___", state 579, "(1)"
160 line 408, "pan.___", state 580, "(1)"
161 line 408, "pan.___", state 580, "(1)"
162 line 406, "pan.___", state 585, "((i<2))"
163 line 406, "pan.___", state 585, "((i>=2))"
164 line 412, "pan.___", state 592, "(1)"
165 line 412, "pan.___", state 593, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
166 line 412, "pan.___", state 593, "else"
167 line 412, "pan.___", state 596, "(1)"
168 line 412, "pan.___", state 597, "(1)"
169 line 412, "pan.___", state 597, "(1)"
170 line 416, "pan.___", state 605, "(1)"
171 line 416, "pan.___", state 606, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
172 line 416, "pan.___", state 606, "else"
173 line 416, "pan.___", state 609, "(1)"
174 line 416, "pan.___", state 610, "(1)"
175 line 416, "pan.___", state 610, "(1)"
176 line 414, "pan.___", state 615, "((i<1))"
177 line 414, "pan.___", state 615, "((i>=1))"
178 line 421, "pan.___", state 622, "(1)"
179 line 421, "pan.___", state 623, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
180 line 421, "pan.___", state 623, "else"
181 line 421, "pan.___", state 626, "(1)"
182 line 421, "pan.___", state 627, "(1)"
183 line 421, "pan.___", state 627, "(1)"
184 line 425, "pan.___", state 635, "(1)"
185 line 425, "pan.___", state 636, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
186 line 425, "pan.___", state 636, "else"
187 line 425, "pan.___", state 639, "(1)"
188 line 425, "pan.___", state 640, "(1)"
189 line 425, "pan.___", state 640, "(1)"
190 line 423, "pan.___", state 645, "((i<2))"
191 line 423, "pan.___", state 645, "((i>=2))"
192 line 430, "pan.___", state 649, "(1)"
193 line 430, "pan.___", state 649, "(1)"
194 line 670, "pan.___", state 652, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
195 line 670, "pan.___", state 653, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
196 line 670, "pan.___", state 654, "(1)"
197 line 395, "pan.___", state 661, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
198 line 404, "pan.___", state 693, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
199 line 408, "pan.___", state 707, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
200 line 412, "pan.___", state 726, "(1)"
201 line 421, "pan.___", state 756, "(1)"
202 line 425, "pan.___", state 769, "(1)"
203 line 395, "pan.___", state 797, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
204 line 395, "pan.___", state 799, "(1)"
205 line 395, "pan.___", state 800, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
206 line 395, "pan.___", state 800, "else"
207 line 395, "pan.___", state 803, "(1)"
208 line 399, "pan.___", state 811, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
209 line 399, "pan.___", state 813, "(1)"
210 line 399, "pan.___", state 814, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
211 line 399, "pan.___", state 814, "else"
212 line 399, "pan.___", state 817, "(1)"
213 line 399, "pan.___", state 818, "(1)"
214 line 399, "pan.___", state 818, "(1)"
215 line 397, "pan.___", state 823, "((i<1))"
216 line 397, "pan.___", state 823, "((i>=1))"
217 line 404, "pan.___", state 829, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
218 line 404, "pan.___", state 831, "(1)"
219 line 404, "pan.___", state 832, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
220 line 404, "pan.___", state 832, "else"
221 line 404, "pan.___", state 835, "(1)"
222 line 404, "pan.___", state 836, "(1)"
223 line 404, "pan.___", state 836, "(1)"
224 line 408, "pan.___", state 843, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
225 line 408, "pan.___", state 845, "(1)"
226 line 408, "pan.___", state 846, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
227 line 408, "pan.___", state 846, "else"
228 line 408, "pan.___", state 849, "(1)"
229 line 408, "pan.___", state 850, "(1)"
230 line 408, "pan.___", state 850, "(1)"
231 line 406, "pan.___", state 855, "((i<2))"
232 line 406, "pan.___", state 855, "((i>=2))"
233 line 412, "pan.___", state 862, "(1)"
234 line 412, "pan.___", state 863, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
235 line 412, "pan.___", state 863, "else"
236 line 412, "pan.___", state 866, "(1)"
237 line 412, "pan.___", state 867, "(1)"
238 line 412, "pan.___", state 867, "(1)"
239 line 416, "pan.___", state 875, "(1)"
240 line 416, "pan.___", state 876, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
241 line 416, "pan.___", state 876, "else"
242 line 416, "pan.___", state 879, "(1)"
243 line 416, "pan.___", state 880, "(1)"
244 line 416, "pan.___", state 880, "(1)"
245 line 414, "pan.___", state 885, "((i<1))"
246 line 414, "pan.___", state 885, "((i>=1))"
247 line 421, "pan.___", state 892, "(1)"
248 line 421, "pan.___", state 893, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
249 line 421, "pan.___", state 893, "else"
250 line 421, "pan.___", state 896, "(1)"
251 line 421, "pan.___", state 897, "(1)"
252 line 421, "pan.___", state 897, "(1)"
253 line 425, "pan.___", state 905, "(1)"
254 line 425, "pan.___", state 906, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
255 line 425, "pan.___", state 906, "else"
256 line 425, "pan.___", state 909, "(1)"
257 line 425, "pan.___", state 910, "(1)"
258 line 425, "pan.___", state 910, "(1)"
259 line 430, "pan.___", state 919, "(1)"
260 line 430, "pan.___", state 919, "(1)"
261 line 395, "pan.___", state 926, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
262 line 395, "pan.___", state 928, "(1)"
263 line 395, "pan.___", state 929, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
264 line 395, "pan.___", state 929, "else"
265 line 395, "pan.___", state 932, "(1)"
266 line 399, "pan.___", state 940, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
267 line 399, "pan.___", state 942, "(1)"
268 line 399, "pan.___", state 943, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
269 line 399, "pan.___", state 943, "else"
270 line 399, "pan.___", state 946, "(1)"
271 line 399, "pan.___", state 947, "(1)"
272 line 399, "pan.___", state 947, "(1)"
273 line 397, "pan.___", state 952, "((i<1))"
274 line 397, "pan.___", state 952, "((i>=1))"
275 line 404, "pan.___", state 958, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
276 line 404, "pan.___", state 960, "(1)"
277 line 404, "pan.___", state 961, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
278 line 404, "pan.___", state 961, "else"
279 line 404, "pan.___", state 964, "(1)"
280 line 404, "pan.___", state 965, "(1)"
281 line 404, "pan.___", state 965, "(1)"
282 line 408, "pan.___", state 972, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
283 line 408, "pan.___", state 974, "(1)"
284 line 408, "pan.___", state 975, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
285 line 408, "pan.___", state 975, "else"
286 line 408, "pan.___", state 978, "(1)"
287 line 408, "pan.___", state 979, "(1)"
288 line 408, "pan.___", state 979, "(1)"
289 line 406, "pan.___", state 984, "((i<2))"
290 line 406, "pan.___", state 984, "((i>=2))"
291 line 412, "pan.___", state 991, "(1)"
292 line 412, "pan.___", state 992, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
293 line 412, "pan.___", state 992, "else"
294 line 412, "pan.___", state 995, "(1)"
295 line 412, "pan.___", state 996, "(1)"
296 line 412, "pan.___", state 996, "(1)"
297 line 416, "pan.___", state 1004, "(1)"
298 line 416, "pan.___", state 1005, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
299 line 416, "pan.___", state 1005, "else"
300 line 416, "pan.___", state 1008, "(1)"
301 line 416, "pan.___", state 1009, "(1)"
302 line 416, "pan.___", state 1009, "(1)"
303 line 414, "pan.___", state 1014, "((i<1))"
304 line 414, "pan.___", state 1014, "((i>=1))"
305 line 421, "pan.___", state 1021, "(1)"
306 line 421, "pan.___", state 1022, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
307 line 421, "pan.___", state 1022, "else"
308 line 421, "pan.___", state 1025, "(1)"
309 line 421, "pan.___", state 1026, "(1)"
310 line 421, "pan.___", state 1026, "(1)"
311 line 425, "pan.___", state 1034, "(1)"
312 line 425, "pan.___", state 1035, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
313 line 425, "pan.___", state 1035, "else"
314 line 425, "pan.___", state 1038, "(1)"
315 line 425, "pan.___", state 1039, "(1)"
316 line 425, "pan.___", state 1039, "(1)"
317 line 423, "pan.___", state 1044, "((i<2))"
318 line 423, "pan.___", state 1044, "((i>=2))"
319 line 430, "pan.___", state 1048, "(1)"
320 line 430, "pan.___", state 1048, "(1)"
321 line 678, "pan.___", state 1052, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
322 line 395, "pan.___", state 1057, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
323 line 404, "pan.___", state 1089, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
324 line 408, "pan.___", state 1103, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
325 line 412, "pan.___", state 1122, "(1)"
326 line 421, "pan.___", state 1152, "(1)"
327 line 425, "pan.___", state 1165, "(1)"
328 line 395, "pan.___", state 1189, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
329 line 404, "pan.___", state 1221, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
330 line 408, "pan.___", state 1235, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
331 line 412, "pan.___", state 1254, "(1)"
332 line 421, "pan.___", state 1284, "(1)"
333 line 425, "pan.___", state 1297, "(1)"
334 line 395, "pan.___", state 1322, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
335 line 404, "pan.___", state 1354, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
336 line 408, "pan.___", state 1368, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
337 line 412, "pan.___", state 1387, "(1)"
338 line 421, "pan.___", state 1417, "(1)"
339 line 425, "pan.___", state 1430, "(1)"
340 line 395, "pan.___", state 1451, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
341 line 404, "pan.___", state 1483, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
342 line 408, "pan.___", state 1497, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
343 line 412, "pan.___", state 1516, "(1)"
344 line 421, "pan.___", state 1546, "(1)"
345 line 425, "pan.___", state 1559, "(1)"
346 line 395, "pan.___", state 1585, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
347 line 404, "pan.___", state 1617, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
348 line 408, "pan.___", state 1631, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
349 line 412, "pan.___", state 1650, "(1)"
350 line 421, "pan.___", state 1680, "(1)"
351 line 425, "pan.___", state 1693, "(1)"
352 line 395, "pan.___", state 1714, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
353 line 404, "pan.___", state 1746, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
354 line 408, "pan.___", state 1760, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
355 line 412, "pan.___", state 1779, "(1)"
356 line 421, "pan.___", state 1809, "(1)"
357 line 425, "pan.___", state 1822, "(1)"
358 line 395, "pan.___", state 1846, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
359 line 404, "pan.___", state 1878, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
360 line 408, "pan.___", state 1892, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
361 line 412, "pan.___", state 1911, "(1)"
362 line 421, "pan.___", state 1941, "(1)"
363 line 425, "pan.___", state 1954, "(1)"
364 line 717, "pan.___", state 1975, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
365 line 395, "pan.___", state 1982, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
366 line 404, "pan.___", state 2014, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
367 line 408, "pan.___", state 2028, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
368 line 412, "pan.___", state 2047, "(1)"
369 line 421, "pan.___", state 2077, "(1)"
370 line 425, "pan.___", state 2090, "(1)"
371 line 395, "pan.___", state 2111, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
372 line 404, "pan.___", state 2143, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
373 line 408, "pan.___", state 2157, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
374 line 412, "pan.___", state 2176, "(1)"
375 line 421, "pan.___", state 2206, "(1)"
376 line 425, "pan.___", state 2219, "(1)"
377 line 395, "pan.___", state 2242, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
378 line 395, "pan.___", state 2244, "(1)"
379 line 395, "pan.___", state 2245, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
380 line 395, "pan.___", state 2245, "else"
381 line 395, "pan.___", state 2248, "(1)"
382 line 399, "pan.___", state 2256, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
383 line 399, "pan.___", state 2258, "(1)"
384 line 399, "pan.___", state 2259, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
385 line 399, "pan.___", state 2259, "else"
386 line 399, "pan.___", state 2262, "(1)"
387 line 399, "pan.___", state 2263, "(1)"
388 line 399, "pan.___", state 2263, "(1)"
389 line 397, "pan.___", state 2268, "((i<1))"
390 line 397, "pan.___", state 2268, "((i>=1))"
391 line 404, "pan.___", state 2274, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
392 line 404, "pan.___", state 2276, "(1)"
393 line 404, "pan.___", state 2277, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
394 line 404, "pan.___", state 2277, "else"
395 line 404, "pan.___", state 2280, "(1)"
396 line 404, "pan.___", state 2281, "(1)"
397 line 404, "pan.___", state 2281, "(1)"
398 line 408, "pan.___", state 2288, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
399 line 408, "pan.___", state 2290, "(1)"
400 line 408, "pan.___", state 2291, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
401 line 408, "pan.___", state 2291, "else"
402 line 408, "pan.___", state 2294, "(1)"
403 line 408, "pan.___", state 2295, "(1)"
404 line 408, "pan.___", state 2295, "(1)"
405 line 406, "pan.___", state 2300, "((i<2))"
406 line 406, "pan.___", state 2300, "((i>=2))"
407 line 412, "pan.___", state 2307, "(1)"
408 line 412, "pan.___", state 2308, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
409 line 412, "pan.___", state 2308, "else"
410 line 412, "pan.___", state 2311, "(1)"
411 line 412, "pan.___", state 2312, "(1)"
412 line 412, "pan.___", state 2312, "(1)"
413 line 416, "pan.___", state 2320, "(1)"
414 line 416, "pan.___", state 2321, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
415 line 416, "pan.___", state 2321, "else"
416 line 416, "pan.___", state 2324, "(1)"
417 line 416, "pan.___", state 2325, "(1)"
418 line 416, "pan.___", state 2325, "(1)"
419 line 414, "pan.___", state 2330, "((i<1))"
420 line 414, "pan.___", state 2330, "((i>=1))"
421 line 421, "pan.___", state 2337, "(1)"
422 line 421, "pan.___", state 2338, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
423 line 421, "pan.___", state 2338, "else"
424 line 421, "pan.___", state 2341, "(1)"
425 line 421, "pan.___", state 2342, "(1)"
426 line 421, "pan.___", state 2342, "(1)"
427 line 425, "pan.___", state 2350, "(1)"
428 line 425, "pan.___", state 2351, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
429 line 425, "pan.___", state 2351, "else"
430 line 425, "pan.___", state 2354, "(1)"
431 line 425, "pan.___", state 2355, "(1)"
432 line 425, "pan.___", state 2355, "(1)"
433 line 423, "pan.___", state 2360, "((i<2))"
434 line 423, "pan.___", state 2360, "((i>=2))"
435 line 430, "pan.___", state 2364, "(1)"
436 line 430, "pan.___", state 2364, "(1)"
437 line 717, "pan.___", state 2367, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
438 line 717, "pan.___", state 2368, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
439 line 717, "pan.___", state 2369, "(1)"
440 line 395, "pan.___", state 2376, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
441 line 404, "pan.___", state 2408, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
442 line 408, "pan.___", state 2422, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
443 line 412, "pan.___", state 2441, "(1)"
444 line 421, "pan.___", state 2471, "(1)"
445 line 425, "pan.___", state 2484, "(1)"
446 line 395, "pan.___", state 2511, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
447 line 404, "pan.___", state 2543, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
448 line 408, "pan.___", state 2557, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
449 line 412, "pan.___", state 2576, "(1)"
450 line 421, "pan.___", state 2606, "(1)"
451 line 425, "pan.___", state 2619, "(1)"
452 line 395, "pan.___", state 2640, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
453 line 404, "pan.___", state 2672, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
454 line 408, "pan.___", state 2686, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
455 line 412, "pan.___", state 2705, "(1)"
456 line 421, "pan.___", state 2735, "(1)"
457 line 425, "pan.___", state 2748, "(1)"
458 line 227, "pan.___", state 2781, "(1)"
459 line 235, "pan.___", state 2801, "(1)"
460 line 239, "pan.___", state 2809, "(1)"
461 line 227, "pan.___", state 2824, "(1)"
462 line 235, "pan.___", state 2844, "(1)"
463 line 239, "pan.___", state 2852, "(1)"
464 line 877, "pan.___", state 2869, "-end-"
466 unreached in proctype urcu_writer
467 line 395, "pan.___", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
468 line 399, "pan.___", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
469 line 404, "pan.___", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
470 line 412, "pan.___", state 83, "(1)"
471 line 416, "pan.___", state 96, "(1)"
472 line 421, "pan.___", state 113, "(1)"
473 line 250, "pan.___", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
474 line 254, "pan.___", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
475 line 258, "pan.___", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
476 line 395, "pan.___", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
477 line 399, "pan.___", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
478 line 404, "pan.___", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
479 line 408, "pan.___", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
480 line 412, "pan.___", state 276, "(1)"
481 line 416, "pan.___", state 289, "(1)"
482 line 421, "pan.___", state 306, "(1)"
483 line 425, "pan.___", state 319, "(1)"
484 line 399, "pan.___", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
485 line 404, "pan.___", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
486 line 408, "pan.___", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
487 line 416, "pan.___", state 420, "(1)"
488 line 421, "pan.___", state 437, "(1)"
489 line 425, "pan.___", state 450, "(1)"
490 line 399, "pan.___", state 494, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
491 line 404, "pan.___", state 512, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
492 line 408, "pan.___", state 526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
493 line 416, "pan.___", state 558, "(1)"
494 line 421, "pan.___", state 575, "(1)"
495 line 425, "pan.___", state 588, "(1)"
496 line 399, "pan.___", state 623, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
497 line 404, "pan.___", state 641, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
498 line 408, "pan.___", state 655, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
499 line 416, "pan.___", state 687, "(1)"
500 line 421, "pan.___", state 704, "(1)"
501 line 425, "pan.___", state 717, "(1)"
502 line 399, "pan.___", state 754, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
503 line 404, "pan.___", state 772, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
504 line 408, "pan.___", state 786, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
505 line 416, "pan.___", state 818, "(1)"
506 line 421, "pan.___", state 835, "(1)"
507 line 425, "pan.___", state 848, "(1)"
508 line 250, "pan.___", state 903, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
509 line 254, "pan.___", state 912, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
510 line 258, "pan.___", state 927, "(1)"
511 line 262, "pan.___", state 934, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
512 line 227, "pan.___", state 950, "(1)"
513 line 231, "pan.___", state 958, "(1)"
514 line 235, "pan.___", state 970, "(1)"
515 line 239, "pan.___", state 978, "(1)"
516 line 250, "pan.___", state 1009, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
517 line 254, "pan.___", state 1018, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
518 line 258, "pan.___", state 1031, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
519 line 262, "pan.___", state 1040, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
520 line 227, "pan.___", state 1056, "(1)"
521 line 231, "pan.___", state 1064, "(1)"
522 line 235, "pan.___", state 1076, "(1)"
523 line 239, "pan.___", state 1084, "(1)"
524 line 254, "pan.___", state 1110, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
525 line 258, "pan.___", state 1123, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
526 line 262, "pan.___", state 1132, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
527 line 227, "pan.___", state 1148, "(1)"
528 line 231, "pan.___", state 1156, "(1)"
529 line 235, "pan.___", state 1168, "(1)"
530 line 239, "pan.___", state 1176, "(1)"
531 line 250, "pan.___", state 1207, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
532 line 254, "pan.___", state 1216, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
533 line 258, "pan.___", state 1229, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
534 line 262, "pan.___", state 1238, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
535 line 227, "pan.___", state 1254, "(1)"
536 line 231, "pan.___", state 1262, "(1)"
537 line 235, "pan.___", state 1274, "(1)"
538 line 239, "pan.___", state 1282, "(1)"
539 line 254, "pan.___", state 1308, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
540 line 258, "pan.___", state 1321, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
541 line 262, "pan.___", state 1330, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
542 line 227, "pan.___", state 1346, "(1)"
543 line 231, "pan.___", state 1354, "(1)"
544 line 235, "pan.___", state 1366, "(1)"
545 line 239, "pan.___", state 1374, "(1)"
546 line 250, "pan.___", state 1405, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
547 line 254, "pan.___", state 1414, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
548 line 258, "pan.___", state 1427, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
549 line 262, "pan.___", state 1436, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
550 line 227, "pan.___", state 1452, "(1)"
551 line 231, "pan.___", state 1460, "(1)"
552 line 235, "pan.___", state 1472, "(1)"
553 line 239, "pan.___", state 1480, "(1)"
554 line 254, "pan.___", state 1506, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
555 line 258, "pan.___", state 1519, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
556 line 262, "pan.___", state 1528, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
557 line 227, "pan.___", state 1544, "(1)"
558 line 231, "pan.___", state 1552, "(1)"
559 line 235, "pan.___", state 1564, "(1)"
560 line 239, "pan.___", state 1572, "(1)"
561 line 250, "pan.___", state 1603, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
562 line 254, "pan.___", state 1612, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
563 line 258, "pan.___", state 1625, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
564 line 262, "pan.___", state 1634, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
565 line 227, "pan.___", state 1650, "(1)"
566 line 231, "pan.___", state 1658, "(1)"
567 line 235, "pan.___", state 1670, "(1)"
568 line 239, "pan.___", state 1678, "(1)"
569 line 1204, "pan.___", state 1694, "-end-"
571 unreached in proctype :init:
573 unreached in proctype :never:
574 line 1265, "pan.___", state 11, "-end-"
577 pan: elapsed time 3.48e+04 seconds
578 pan: rate 1671.9756 states/second
579 pan: avg transition delay 1.3744e-06 usec
580 cp .input.spin urcu_progress_writer.spin.input
581 cp .input.spin.trail urcu_progress_writer.spin.input.trail
projects / urcu.git / blob