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