1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu/testmerge'
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_nested.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 -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 566)
19 Depth= 4234 States= 1e+06 Transitions= 1.7e+07 Memory= 527.287 t= 31.2 R= 3e+04
20 Depth= 4234 States= 2e+06 Transitions= 3.44e+07 Memory= 588.322 t= 63.7 R= 3e+04
21 Depth= 4234 States= 3e+06 Transitions= 5.2e+07 Memory= 649.358 t= 96.8 R= 3e+04
22 pan: resizing hashtable to -w22.. done
23 Depth= 4234 States= 4e+06 Transitions= 6.97e+07 Memory= 741.416 t= 130 R= 3e+04
25 (Spin Version 5.1.7 -- 23 December 2008)
26 + Partial Order Reduction
28 Full statespace search for:
30 assertion violations + (if within scope of claim)
31 acceptance cycles + (fairness disabled)
32 invalid end states - (disabled by never claim)
34 State-vector 56 byte, depth reached 4234, errors: 0
35 4027146 states, stored
36 66145121 states, matched
37 70172267 transitions (= stored+matched)
38 2.6437688e+08 atomic steps
39 hash conflicts: 47318190 (resolved)
41 Stats on memory usage (in Megabytes):
42 322.609 equivalent memory usage for states (stored*(State-vector + overhead))
43 253.418 actual memory usage for states (compression: 78.55%)
44 state-vector as stored = 38 byte + 28 byte overhead
45 32.000 memory used for hash table (-w22)
46 457.764 memory used for DFS stack (-m10000000)
47 743.076 total actual memory usage
49 unreached in proctype urcu_reader
50 line 288, "pan.___", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
51 line 297, "pan.___", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
52 line 298, "pan.___", state 61, "(1)"
53 line 307, "pan.___", state 91, "(1)"
54 line 288, "pan.___", state 104, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
55 line 297, "pan.___", state 136, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
56 line 298, "pan.___", state 149, "(1)"
57 line 307, "pan.___", state 179, "(1)"
58 line 288, "pan.___", state 193, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
59 line 297, "pan.___", state 225, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
60 line 298, "pan.___", state 238, "(1)"
61 line 307, "pan.___", state 268, "(1)"
62 line 158, "pan.___", state 289, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
63 line 158, "pan.___", state 291, "(1)"
64 line 162, "pan.___", state 298, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
65 line 162, "pan.___", state 300, "(1)"
66 line 162, "pan.___", state 301, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
67 line 162, "pan.___", state 301, "else"
68 line 160, "pan.___", state 306, "((j<1))"
69 line 160, "pan.___", state 306, "((j>=1))"
70 line 166, "pan.___", state 311, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
71 line 143, "pan.___", state 321, "(1)"
72 line 147, "pan.___", state 329, "(1)"
73 line 147, "pan.___", state 330, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
74 line 147, "pan.___", state 330, "else"
75 line 145, "pan.___", state 335, "((j<1))"
76 line 145, "pan.___", state 335, "((j>=1))"
77 line 151, "pan.___", state 341, "(1)"
78 line 151, "pan.___", state 342, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
79 line 151, "pan.___", state 342, "else"
80 line 153, "pan.___", state 345, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
81 line 153, "pan.___", state 345, "else"
82 line 185, "pan.___", state 347, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
83 line 185, "pan.___", state 347, "else"
84 line 158, "pan.___", state 352, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
85 line 158, "pan.___", state 354, "(1)"
86 line 162, "pan.___", state 361, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
87 line 162, "pan.___", state 363, "(1)"
88 line 162, "pan.___", state 364, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
89 line 162, "pan.___", state 364, "else"
90 line 160, "pan.___", state 369, "((j<1))"
91 line 160, "pan.___", state 369, "((j>=1))"
92 line 166, "pan.___", state 374, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
93 line 143, "pan.___", state 384, "(1)"
94 line 147, "pan.___", state 392, "(1)"
95 line 147, "pan.___", state 393, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
96 line 147, "pan.___", state 393, "else"
97 line 145, "pan.___", state 398, "((j<1))"
98 line 145, "pan.___", state 398, "((j>=1))"
99 line 151, "pan.___", state 404, "(1)"
100 line 151, "pan.___", state 405, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
101 line 151, "pan.___", state 405, "else"
102 line 153, "pan.___", state 408, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
103 line 153, "pan.___", state 408, "else"
104 line 185, "pan.___", state 410, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
105 line 185, "pan.___", state 410, "else"
106 line 199, "pan.___", state 414, "((i<1))"
107 line 199, "pan.___", state 414, "((i>=1))"
108 line 158, "pan.___", state 419, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
109 line 158, "pan.___", state 421, "(1)"
110 line 162, "pan.___", state 428, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
111 line 162, "pan.___", state 430, "(1)"
112 line 162, "pan.___", state 431, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
113 line 162, "pan.___", state 431, "else"
114 line 160, "pan.___", state 436, "((j<1))"
115 line 160, "pan.___", state 436, "((j>=1))"
116 line 166, "pan.___", state 441, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
117 line 143, "pan.___", state 451, "(1)"
118 line 147, "pan.___", state 459, "(1)"
119 line 147, "pan.___", state 460, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
120 line 147, "pan.___", state 460, "else"
121 line 145, "pan.___", state 465, "((j<1))"
122 line 145, "pan.___", state 465, "((j>=1))"
123 line 151, "pan.___", state 471, "(1)"
124 line 151, "pan.___", state 472, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
125 line 151, "pan.___", state 472, "else"
126 line 153, "pan.___", state 475, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
127 line 153, "pan.___", state 475, "else"
128 line 185, "pan.___", state 477, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
129 line 185, "pan.___", state 477, "else"
130 line 288, "pan.___", state 492, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
131 line 297, "pan.___", state 524, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
132 line 298, "pan.___", state 537, "(1)"
133 line 307, "pan.___", state 567, "(1)"
134 line 288, "pan.___", state 580, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
135 line 297, "pan.___", state 612, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
136 line 298, "pan.___", state 625, "(1)"
137 line 307, "pan.___", state 655, "(1)"
138 line 288, "pan.___", state 668, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
139 line 297, "pan.___", state 700, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
140 line 298, "pan.___", state 713, "(1)"
141 line 307, "pan.___", state 743, "(1)"
142 line 158, "pan.___", state 758, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
143 line 158, "pan.___", state 760, "(1)"
144 line 162, "pan.___", state 767, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
145 line 162, "pan.___", state 769, "(1)"
146 line 162, "pan.___", state 770, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
147 line 162, "pan.___", state 770, "else"
148 line 160, "pan.___", state 775, "((j<1))"
149 line 160, "pan.___", state 775, "((j>=1))"
150 line 166, "pan.___", state 780, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
151 line 143, "pan.___", state 790, "(1)"
152 line 147, "pan.___", state 798, "(1)"
153 line 147, "pan.___", state 799, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
154 line 147, "pan.___", state 799, "else"
155 line 145, "pan.___", state 804, "((j<1))"
156 line 145, "pan.___", state 804, "((j>=1))"
157 line 151, "pan.___", state 810, "(1)"
158 line 151, "pan.___", state 811, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
159 line 151, "pan.___", state 811, "else"
160 line 153, "pan.___", state 814, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
161 line 153, "pan.___", state 814, "else"
162 line 185, "pan.___", state 816, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
163 line 185, "pan.___", state 816, "else"
164 line 158, "pan.___", state 821, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
165 line 158, "pan.___", state 823, "(1)"
166 line 162, "pan.___", state 830, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
167 line 162, "pan.___", state 832, "(1)"
168 line 162, "pan.___", state 833, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
169 line 162, "pan.___", state 833, "else"
170 line 160, "pan.___", state 838, "((j<1))"
171 line 160, "pan.___", state 838, "((j>=1))"
172 line 166, "pan.___", state 843, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
173 line 143, "pan.___", state 853, "(1)"
174 line 147, "pan.___", state 861, "(1)"
175 line 147, "pan.___", state 862, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
176 line 147, "pan.___", state 862, "else"
177 line 145, "pan.___", state 867, "((j<1))"
178 line 145, "pan.___", state 867, "((j>=1))"
179 line 151, "pan.___", state 873, "(1)"
180 line 151, "pan.___", state 874, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
181 line 151, "pan.___", state 874, "else"
182 line 153, "pan.___", state 877, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
183 line 153, "pan.___", state 877, "else"
184 line 185, "pan.___", state 879, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
185 line 185, "pan.___", state 879, "else"
186 line 199, "pan.___", state 883, "((i<1))"
187 line 199, "pan.___", state 883, "((i>=1))"
188 line 158, "pan.___", state 888, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
189 line 158, "pan.___", state 890, "(1)"
190 line 162, "pan.___", state 897, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
191 line 162, "pan.___", state 899, "(1)"
192 line 162, "pan.___", state 900, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
193 line 162, "pan.___", state 900, "else"
194 line 160, "pan.___", state 905, "((j<1))"
195 line 160, "pan.___", state 905, "((j>=1))"
196 line 166, "pan.___", state 910, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
197 line 143, "pan.___", state 920, "(1)"
198 line 147, "pan.___", state 928, "(1)"
199 line 147, "pan.___", state 929, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
200 line 147, "pan.___", state 929, "else"
201 line 145, "pan.___", state 934, "((j<1))"
202 line 145, "pan.___", state 934, "((j>=1))"
203 line 151, "pan.___", state 940, "(1)"
204 line 151, "pan.___", state 941, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
205 line 151, "pan.___", state 941, "else"
206 line 153, "pan.___", state 944, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
207 line 153, "pan.___", state 944, "else"
208 line 185, "pan.___", state 946, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
209 line 185, "pan.___", state 946, "else"
210 line 288, "pan.___", state 956, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
211 line 297, "pan.___", state 988, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
212 line 298, "pan.___", state 1001, "(1)"
213 line 307, "pan.___", state 1031, "(1)"
214 line 288, "pan.___", state 1052, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
215 line 297, "pan.___", state 1084, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
216 line 298, "pan.___", state 1097, "(1)"
217 line 307, "pan.___", state 1127, "(1)"
218 line 433, "pan.___", state 1140, "-end-"
220 unreached in proctype urcu_writer
221 line 288, "pan.___", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
222 line 292, "pan.___", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
223 line 297, "pan.___", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
224 line 298, "pan.___", state 59, "(1)"
225 line 302, "pan.___", state 72, "(1)"
226 line 307, "pan.___", state 89, "(1)"
227 line 288, "pan.___", state 106, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
228 line 292, "pan.___", state 120, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
229 line 298, "pan.___", state 151, "(1)"
230 line 302, "pan.___", state 164, "(1)"
231 line 467, "pan.___", state 195, "(1)"
232 line 158, "pan.___", state 205, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
233 line 162, "pan.___", state 214, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
234 line 143, "pan.___", state 237, "(1)"
235 line 147, "pan.___", state 245, "(1)"
236 line 151, "pan.___", state 257, "(1)"
237 line 158, "pan.___", state 268, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
238 line 166, "pan.___", state 290, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
239 line 143, "pan.___", state 300, "(1)"
240 line 147, "pan.___", state 308, "(1)"
241 line 151, "pan.___", state 320, "(1)"
242 line 158, "pan.___", state 335, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
243 line 162, "pan.___", state 344, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
244 line 166, "pan.___", state 357, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
245 line 143, "pan.___", state 367, "(1)"
246 line 147, "pan.___", state 375, "(1)"
247 line 151, "pan.___", state 387, "(1)"
248 line 288, "pan.___", state 403, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
249 line 292, "pan.___", state 417, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
250 line 297, "pan.___", state 435, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
251 line 298, "pan.___", state 448, "(1)"
252 line 302, "pan.___", state 461, "(1)"
253 line 307, "pan.___", state 478, "(1)"
254 line 288, "pan.___", state 495, "(1)"
255 line 292, "pan.___", state 507, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
256 line 297, "pan.___", state 525, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
257 line 302, "pan.___", state 551, "(1)"
258 line 307, "pan.___", state 568, "(1)"
259 line 292, "pan.___", state 598, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
260 line 297, "pan.___", state 616, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
261 line 302, "pan.___", state 642, "(1)"
262 line 307, "pan.___", state 659, "(1)"
263 line 162, "pan.___", state 681, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
264 line 166, "pan.___", state 694, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
265 line 143, "pan.___", state 704, "(1)"
266 line 147, "pan.___", state 712, "(1)"
267 line 151, "pan.___", state 724, "(1)"
268 line 158, "pan.___", state 735, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
269 line 166, "pan.___", state 757, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
270 line 143, "pan.___", state 767, "(1)"
271 line 147, "pan.___", state 775, "(1)"
272 line 151, "pan.___", state 787, "(1)"
273 line 158, "pan.___", state 802, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
274 line 162, "pan.___", state 811, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
275 line 166, "pan.___", state 824, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
276 line 143, "pan.___", state 834, "(1)"
277 line 147, "pan.___", state 842, "(1)"
278 line 151, "pan.___", state 854, "(1)"
279 line 288, "pan.___", state 878, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
280 line 288, "pan.___", state 880, "(1)"
281 line 288, "pan.___", state 881, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
282 line 288, "pan.___", state 881, "else"
283 line 288, "pan.___", state 884, "(1)"
284 line 292, "pan.___", state 892, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
285 line 292, "pan.___", state 894, "(1)"
286 line 292, "pan.___", state 895, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
287 line 292, "pan.___", state 895, "else"
288 line 292, "pan.___", state 898, "(1)"
289 line 292, "pan.___", state 899, "(1)"
290 line 292, "pan.___", state 899, "(1)"
291 line 290, "pan.___", state 904, "((i<1))"
292 line 290, "pan.___", state 904, "((i>=1))"
293 line 297, "pan.___", state 910, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
294 line 298, "pan.___", state 923, "(1)"
295 line 298, "pan.___", state 924, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
296 line 298, "pan.___", state 924, "else"
297 line 298, "pan.___", state 927, "(1)"
298 line 298, "pan.___", state 928, "(1)"
299 line 298, "pan.___", state 928, "(1)"
300 line 302, "pan.___", state 936, "(1)"
301 line 302, "pan.___", state 937, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
302 line 302, "pan.___", state 937, "else"
303 line 302, "pan.___", state 940, "(1)"
304 line 302, "pan.___", state 941, "(1)"
305 line 302, "pan.___", state 941, "(1)"
306 line 300, "pan.___", state 946, "((i<1))"
307 line 300, "pan.___", state 946, "((i>=1))"
308 line 307, "pan.___", state 953, "(1)"
309 line 307, "pan.___", state 954, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
310 line 307, "pan.___", state 954, "else"
311 line 307, "pan.___", state 957, "(1)"
312 line 307, "pan.___", state 958, "(1)"
313 line 307, "pan.___", state 958, "(1)"
314 line 309, "pan.___", state 961, "(1)"
315 line 309, "pan.___", state 961, "(1)"
316 line 292, "pan.___", state 990, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
317 line 297, "pan.___", state 1008, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
318 line 302, "pan.___", state 1034, "(1)"
319 line 307, "pan.___", state 1051, "(1)"
320 line 292, "pan.___", state 1078, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
321 line 297, "pan.___", state 1096, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
322 line 302, "pan.___", state 1122, "(1)"
323 line 307, "pan.___", state 1139, "(1)"
324 line 288, "pan.___", state 1156, "(1)"
325 line 292, "pan.___", state 1168, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
326 line 297, "pan.___", state 1186, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
327 line 302, "pan.___", state 1212, "(1)"
328 line 307, "pan.___", state 1229, "(1)"
329 line 292, "pan.___", state 1259, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
330 line 297, "pan.___", state 1277, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
331 line 302, "pan.___", state 1303, "(1)"
332 line 307, "pan.___", state 1320, "(1)"
333 line 162, "pan.___", state 1342, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
334 line 166, "pan.___", state 1355, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
335 line 143, "pan.___", state 1365, "(1)"
336 line 147, "pan.___", state 1373, "(1)"
337 line 151, "pan.___", state 1385, "(1)"
338 line 158, "pan.___", state 1396, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
339 line 166, "pan.___", state 1418, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
340 line 143, "pan.___", state 1428, "(1)"
341 line 147, "pan.___", state 1436, "(1)"
342 line 151, "pan.___", state 1448, "(1)"
343 line 158, "pan.___", state 1463, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
344 line 162, "pan.___", state 1472, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
345 line 166, "pan.___", state 1485, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
346 line 143, "pan.___", state 1495, "(1)"
347 line 147, "pan.___", state 1503, "(1)"
348 line 151, "pan.___", state 1515, "(1)"
349 line 288, "pan.___", state 1539, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
350 line 288, "pan.___", state 1541, "(1)"
351 line 288, "pan.___", state 1542, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
352 line 288, "pan.___", state 1542, "else"
353 line 288, "pan.___", state 1545, "(1)"
354 line 292, "pan.___", state 1553, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
355 line 292, "pan.___", state 1555, "(1)"
356 line 292, "pan.___", state 1556, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
357 line 292, "pan.___", state 1556, "else"
358 line 292, "pan.___", state 1559, "(1)"
359 line 292, "pan.___", state 1560, "(1)"
360 line 292, "pan.___", state 1560, "(1)"
361 line 290, "pan.___", state 1565, "((i<1))"
362 line 290, "pan.___", state 1565, "((i>=1))"
363 line 297, "pan.___", state 1571, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
364 line 298, "pan.___", state 1584, "(1)"
365 line 298, "pan.___", state 1585, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
366 line 298, "pan.___", state 1585, "else"
367 line 298, "pan.___", state 1588, "(1)"
368 line 298, "pan.___", state 1589, "(1)"
369 line 298, "pan.___", state 1589, "(1)"
370 line 302, "pan.___", state 1597, "(1)"
371 line 302, "pan.___", state 1598, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
372 line 302, "pan.___", state 1598, "else"
373 line 302, "pan.___", state 1601, "(1)"
374 line 302, "pan.___", state 1602, "(1)"
375 line 302, "pan.___", state 1602, "(1)"
376 line 300, "pan.___", state 1607, "((i<1))"
377 line 300, "pan.___", state 1607, "((i>=1))"
378 line 307, "pan.___", state 1614, "(1)"
379 line 307, "pan.___", state 1615, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
380 line 307, "pan.___", state 1615, "else"
381 line 307, "pan.___", state 1618, "(1)"
382 line 307, "pan.___", state 1619, "(1)"
383 line 307, "pan.___", state 1619, "(1)"
384 line 309, "pan.___", state 1622, "(1)"
385 line 309, "pan.___", state 1622, "(1)"
386 line 162, "pan.___", state 1646, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
387 line 166, "pan.___", state 1659, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
388 line 143, "pan.___", state 1669, "(1)"
389 line 147, "pan.___", state 1677, "(1)"
390 line 151, "pan.___", state 1689, "(1)"
391 line 158, "pan.___", state 1700, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
392 line 166, "pan.___", state 1722, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
393 line 143, "pan.___", state 1732, "(1)"
394 line 147, "pan.___", state 1740, "(1)"
395 line 151, "pan.___", state 1752, "(1)"
396 line 158, "pan.___", state 1767, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
397 line 162, "pan.___", state 1776, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
398 line 166, "pan.___", state 1789, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
399 line 143, "pan.___", state 1799, "(1)"
400 line 147, "pan.___", state 1807, "(1)"
401 line 151, "pan.___", state 1819, "(1)"
402 line 510, "pan.___", state 1845, "-end-"
404 unreached in proctype :init:
406 unreached in proctype :never:
407 line 571, "pan.___", state 8, "-end-"
410 pan: elapsed time 131 seconds
411 pan: rate 30755.659 states/second
412 pan: avg transition delay 1.866e-06 usec
413 cp .input.spin urcu_free_nested.spin.input
414 cp .input.spin.trail urcu_free_nested.spin.input.trail
415 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu/testmerge'
projects / urcu.git / blob