projects / urcu.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Update formal model from local copy
[urcu.git] / formal-model / urcu-nosched-model / result-standard-execution-nest / urcu_progress_writer_error.log
CommitLineData
06e8b2a8
MD		 1make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
2rm -f pan* trail.out .input.spin* *.spin.trail .input.define
3touch .input.define
4cat .input.define > pan.ltl
5cat DEFINES >> pan.ltl
6spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
7cp urcu_progress_writer_error.define .input.define
8cat .input.define > .input.spin
9cat DEFINES >> .input.spin
10cat urcu.spin >> .input.spin
11rm -f .input.spin.trail
12spin -a -X -N pan.ltl .input.spin
13Exit-Status 0
14gcc -O2 -w -DHASH64 -o pan pan.c
15./pan -a -f -v -c1 -X -m10000000 -w20
16warning: for p.o. reduction to be valid the never claim must be stutter-invariant
17(never claims generated from LTL formulae are stutter-invariant)
18depth 0: Claim reached state 5 (line 745)
19depth 15: Claim reached state 9 (line 750)
20depth 291: Claim reached state 9 (line 749)
21pan: acceptance cycle (at depth 4308)
22pan: wrote .input.spin.trail
23
24(Spin Version 5.1.7 -- 23 December 2008)
25Warning: Search not completed
26 + Partial Order Reduction
27
28Full statespace search for:
29 never claim +
30 assertion violations + (if within scope of claim)
31 acceptance cycles + (fairness enabled)
32 invalid end states - (disabled by never claim)
33
34State-vector 56 byte, depth reached 4820, errors: 1
35 62091 states, stored (169917 visited)
36 2179326 states, matched
37 2349243 transitions (= visited+matched)
38 8805349 atomic steps
39hash conflicts: 50953 (resolved)
40
41Stats on memory usage (in Megabytes):
42 4.974 equivalent memory usage for states (stored*(State-vector + overhead))
43 4.145 actual memory usage for states (compression: 83.33%)
44 state-vector as stored = 42 byte + 28 byte overhead
45 8.000 memory used for hash table (-w20)
46 457.764 memory used for DFS stack (-m10000000)
47 469.865 total actual memory usage
48
49unreached in proctype urcu_reader
50 line 400, "pan.___", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
51 line 409, "pan.___", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
52 line 410, "pan.___", state 61, "(1)"
53 line 419, "pan.___", state 91, "(1)"
54 line 400, "pan.___", state 106, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
55 line 409, "pan.___", state 138, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
56 line 410, "pan.___", state 151, "(1)"
57 line 419, "pan.___", state 181, "(1)"
58 line 400, "pan.___", state 197, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
59 line 409, "pan.___", state 229, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
60 line 410, "pan.___", state 242, "(1)"
61 line 419, "pan.___", state 272, "(1)"
62 line 400, "pan.___", state 315, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
63 line 409, "pan.___", state 347, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
64 line 410, "pan.___", state 360, "(1)"
65 line 419, "pan.___", state 390, "(1)"
66 line 541, "pan.___", state 414, "-end-"
67 (17 of 414 states)
68unreached in proctype urcu_writer
69 line 400, "pan.___", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
70 line 400, "pan.___", state 20, "(1)"
71 line 404, "pan.___", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
72 line 404, "pan.___", state 34, "(1)"
73 line 404, "pan.___", state 35, "(1)"
74 line 404, "pan.___", state 35, "(1)"
75 line 402, "pan.___", state 40, "((i<1))"
76 line 402, "pan.___", state 40, "((i>=1))"
77 line 409, "pan.___", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
78 line 410, "pan.___", state 59, "(1)"
79 line 410, "pan.___", state 60, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
80 line 410, "pan.___", state 60, "else"
81 line 410, "pan.___", state 63, "(1)"
82 line 410, "pan.___", state 64, "(1)"
83 line 410, "pan.___", state 64, "(1)"
84 line 414, "pan.___", state 72, "(1)"
85 line 414, "pan.___", state 73, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
86 line 414, "pan.___", state 73, "else"
87 line 414, "pan.___", state 76, "(1)"
88 line 414, "pan.___", state 77, "(1)"
89 line 414, "pan.___", state 77, "(1)"
90 line 412, "pan.___", state 82, "((i<1))"
91 line 412, "pan.___", state 82, "((i>=1))"
92 line 419, "pan.___", state 89, "(1)"
93 line 419, "pan.___", state 90, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
94 line 419, "pan.___", state 90, "else"
95 line 419, "pan.___", state 93, "(1)"
96 line 419, "pan.___", state 94, "(1)"
97 line 419, "pan.___", state 94, "(1)"
98 line 370, "pan.___", state 99, "(1)"
99 line 640, "pan.___", state 103, "cached_generation_ptr.val[_pid] = (old_gen+1)"
100 line 638, "pan.___", state 104, "old_gen = cached_generation_ptr.val[_pid]"
101 line 400, "pan.___", state 108, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
102 line 400, "pan.___", state 114, "(1)"
103 line 404, "pan.___", state 122, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
104 line 404, "pan.___", state 128, "(1)"
105 line 404, "pan.___", state 129, "(1)"
106 line 404, "pan.___", state 129, "(1)"
107 line 402, "pan.___", state 134, "((i<1))"
108 line 402, "pan.___", state 134, "((i>=1))"
109 line 410, "pan.___", state 153, "(1)"
110 line 410, "pan.___", state 154, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
111 line 410, "pan.___", state 154, "else"
112 line 410, "pan.___", state 157, "(1)"
113 line 410, "pan.___", state 158, "(1)"
114 line 410, "pan.___", state 158, "(1)"
115 line 414, "pan.___", state 166, "(1)"
116 line 414, "pan.___", state 167, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
117 line 414, "pan.___", state 167, "else"
118 line 414, "pan.___", state 170, "(1)"
119 line 414, "pan.___", state 171, "(1)"
120 line 414, "pan.___", state 171, "(1)"
121 line 412, "pan.___", state 176, "((i<1))"
122 line 412, "pan.___", state 176, "((i>=1))"
123 line 419, "pan.___", state 183, "(1)"
124 line 419, "pan.___", state 184, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
125 line 419, "pan.___", state 184, "else"
126 line 419, "pan.___", state 187, "(1)"
127 line 419, "pan.___", state 188, "(1)"
128 line 419, "pan.___", state 188, "(1)"
129 line 421, "pan.___", state 191, "(1)"
130 line 421, "pan.___", state 191, "(1)"
131 line 370, "pan.___", state 193, "(1)"
132 line 653, "pan.___", state 199, "(1)"
133 line 647, "pan.___", state 202, "((write_lock==0))"
134 line 647, "pan.___", state 202, "else"
135 line 645, "pan.___", state 203, "(1)"
136 line 176, "pan.___", state 208, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
137 line 180, "pan.___", state 217, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
138 line 178, "pan.___", state 225, "((j<1))"
139 line 178, "pan.___", state 225, "((j>=1))"
140 line 184, "pan.___", state 230, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
141 line 161, "pan.___", state 240, "(1)"
142 line 165, "pan.___", state 248, "(1)"
143 line 165, "pan.___", state 249, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
144 line 165, "pan.___", state 249, "else"
145 line 163, "pan.___", state 254, "((j<1))"
146 line 163, "pan.___", state 254, "((j>=1))"
147 line 169, "pan.___", state 260, "(1)"
148 line 169, "pan.___", state 261, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
149 line 169, "pan.___", state 261, "else"
150 line 171, "pan.___", state 264, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
151 line 171, "pan.___", state 264, "else"
152 line 176, "pan.___", state 271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
153 line 180, "pan.___", state 280, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
154 line 178, "pan.___", state 288, "((j<1))"
155 line 178, "pan.___", state 288, "((j>=1))"
156 line 184, "pan.___", state 293, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
157 line 161, "pan.___", state 303, "(1)"
158 line 165, "pan.___", state 311, "(1)"
159 line 165, "pan.___", state 312, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
160 line 165, "pan.___", state 312, "else"
161 line 163, "pan.___", state 317, "((j<1))"
162 line 163, "pan.___", state 317, "((j>=1))"
163 line 169, "pan.___", state 323, "(1)"
164 line 169, "pan.___", state 324, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
165 line 169, "pan.___", state 324, "else"
166 line 171, "pan.___", state 327, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
167 line 171, "pan.___", state 327, "else"
168 line 215, "pan.___", state 333, "((i<1))"
169 line 215, "pan.___", state 333, "((i>=1))"
170 line 176, "pan.___", state 338, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
171 line 180, "pan.___", state 347, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
172 line 178, "pan.___", state 355, "((j<1))"
173 line 178, "pan.___", state 355, "((j>=1))"
174 line 184, "pan.___", state 360, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
175 line 161, "pan.___", state 370, "(1)"
176 line 165, "pan.___", state 378, "(1)"
177 line 165, "pan.___", state 379, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
178 line 165, "pan.___", state 379, "else"
179 line 163, "pan.___", state 384, "((j<1))"
180 line 163, "pan.___", state 384, "((j>=1))"
181 line 169, "pan.___", state 390, "(1)"
182 line 169, "pan.___", state 391, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
183 line 169, "pan.___", state 391, "else"
184 line 171, "pan.___", state 394, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
185 line 171, "pan.___", state 394, "else"
186 line 400, "pan.___", state 404, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
187 line 400, "pan.___", state 410, "(1)"
188 line 404, "pan.___", state 418, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
189 line 404, "pan.___", state 424, "(1)"
190 line 404, "pan.___", state 425, "(1)"
191 line 404, "pan.___", state 425, "(1)"
192 line 402, "pan.___", state 430, "((i<1))"
193 line 402, "pan.___", state 430, "((i>=1))"
194 line 409, "pan.___", state 436, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
195 line 410, "pan.___", state 449, "(1)"
196 line 410, "pan.___", state 450, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
197 line 410, "pan.___", state 450, "else"
198 line 410, "pan.___", state 453, "(1)"
199 line 410, "pan.___", state 454, "(1)"
200 line 410, "pan.___", state 454, "(1)"
201 line 414, "pan.___", state 462, "(1)"
202 line 414, "pan.___", state 463, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
203 line 414, "pan.___", state 463, "else"
204 line 414, "pan.___", state 466, "(1)"
205 line 414, "pan.___", state 467, "(1)"
206 line 414, "pan.___", state 467, "(1)"
207 line 412, "pan.___", state 472, "((i<1))"
208 line 412, "pan.___", state 472, "((i>=1))"
209 line 419, "pan.___", state 479, "(1)"
210 line 419, "pan.___", state 480, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
211 line 419, "pan.___", state 480, "else"
212 line 419, "pan.___", state 483, "(1)"
213 line 419, "pan.___", state 484, "(1)"
214 line 419, "pan.___", state 484, "(1)"
215 line 421, "pan.___", state 487, "(1)"
216 line 421, "pan.___", state 487, "(1)"
217 line 370, "pan.___", state 489, "(1)"
218 line 662, "pan.___", state 492, "cached_urcu_gp_ctr.val[_pid] = (tmp^(1<<7))"
219 line 400, "pan.___", state 498, "(1)"
220 line 400, "pan.___", state 499, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
221 line 400, "pan.___", state 499, "else"
222 line 400, "pan.___", state 502, "(1)"
223 line 404, "pan.___", state 510, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
224 line 404, "pan.___", state 516, "(1)"
225 line 404, "pan.___", state 517, "(1)"
226 line 404, "pan.___", state 517, "(1)"
227 line 402, "pan.___", state 522, "((i<1))"
228 line 402, "pan.___", state 522, "((i>=1))"
229 line 409, "pan.___", state 528, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
230 line 410, "pan.___", state 541, "(1)"
231 line 410, "pan.___", state 542, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
232 line 410, "pan.___", state 542, "else"
233 line 410, "pan.___", state 545, "(1)"
234 line 410, "pan.___", state 546, "(1)"
235 line 410, "pan.___", state 546, "(1)"
236 line 414, "pan.___", state 554, "(1)"
237 line 414, "pan.___", state 555, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
238 line 414, "pan.___", state 555, "else"
239 line 414, "pan.___", state 558, "(1)"
240 line 414, "pan.___", state 559, "(1)"
241 line 414, "pan.___", state 559, "(1)"
242 line 412, "pan.___", state 564, "((i<1))"
243 line 412, "pan.___", state 564, "((i>=1))"
244 line 419, "pan.___", state 571, "(1)"
245 line 419, "pan.___", state 572, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
246 line 419, "pan.___", state 572, "else"
247 line 419, "pan.___", state 575, "(1)"
248 line 419, "pan.___", state 576, "(1)"
249 line 419, "pan.___", state 576, "(1)"
250 line 421, "pan.___", state 579, "(1)"
251 line 421, "pan.___", state 579, "(1)"
252 line 370, "pan.___", state 581, "(1)"
253 line 400, "pan.___", state 589, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
254 line 400, "pan.___", state 595, "(1)"
255 line 404, "pan.___", state 603, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
256 line 404, "pan.___", state 609, "(1)"
257 line 404, "pan.___", state 610, "(1)"
258 line 404, "pan.___", state 610, "(1)"
259 line 402, "pan.___", state 615, "((i<1))"
260 line 402, "pan.___", state 615, "((i>=1))"
261 line 409, "pan.___", state 621, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
262 line 410, "pan.___", state 634, "(1)"
263 line 410, "pan.___", state 635, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
264 line 410, "pan.___", state 635, "else"
265 line 410, "pan.___", state 638, "(1)"
266 line 410, "pan.___", state 639, "(1)"
267 line 410, "pan.___", state 639, "(1)"
268 line 414, "pan.___", state 647, "(1)"
269 line 414, "pan.___", state 648, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
270 line 414, "pan.___", state 648, "else"
271 line 414, "pan.___", state 651, "(1)"
272 line 414, "pan.___", state 652, "(1)"
273 line 414, "pan.___", state 652, "(1)"
274 line 412, "pan.___", state 657, "((i<1))"
275 line 412, "pan.___", state 657, "((i>=1))"
276 line 419, "pan.___", state 664, "(1)"
277 line 419, "pan.___", state 665, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
278 line 419, "pan.___", state 665, "else"
279 line 419, "pan.___", state 668, "(1)"
280 line 419, "pan.___", state 669, "(1)"
281 line 419, "pan.___", state 669, "(1)"
282 line 421, "pan.___", state 672, "(1)"
283 line 421, "pan.___", state 672, "(1)"
284 line 370, "pan.___", state 674, "(1)"
285 line 400, "pan.___", state 679, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
286 line 400, "pan.___", state 681, "(1)"
287 line 400, "pan.___", state 682, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
288 line 400, "pan.___", state 682, "else"
289 line 400, "pan.___", state 685, "(1)"
290 line 404, "pan.___", state 693, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
291 line 404, "pan.___", state 695, "(1)"
292 line 404, "pan.___", state 696, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
293 line 404, "pan.___", state 696, "else"
294 line 404, "pan.___", state 699, "(1)"
295 line 404, "pan.___", state 700, "(1)"
296 line 404, "pan.___", state 700, "(1)"
297 line 402, "pan.___", state 705, "((i<1))"
298 line 402, "pan.___", state 705, "((i>=1))"
299 line 409, "pan.___", state 711, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
300 line 410, "pan.___", state 724, "(1)"
301 line 410, "pan.___", state 725, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
302 line 410, "pan.___", state 725, "else"
303 line 410, "pan.___", state 728, "(1)"
304 line 410, "pan.___", state 729, "(1)"
305 line 410, "pan.___", state 729, "(1)"
306 line 414, "pan.___", state 737, "(1)"
307 line 414, "pan.___", state 738, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
308 line 414, "pan.___", state 738, "else"
309 line 414, "pan.___", state 741, "(1)"
310 line 414, "pan.___", state 742, "(1)"
311 line 414, "pan.___", state 742, "(1)"
312 line 412, "pan.___", state 747, "((i<1))"
313 line 412, "pan.___", state 747, "((i>=1))"
314 line 419, "pan.___", state 754, "(1)"
315 line 419, "pan.___", state 755, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
316 line 419, "pan.___", state 755, "else"
317 line 419, "pan.___", state 758, "(1)"
318 line 419, "pan.___", state 759, "(1)"
319 line 419, "pan.___", state 759, "(1)"
320 line 421, "pan.___", state 762, "(1)"
321 line 421, "pan.___", state 762, "(1)"
322 line 370, "pan.___", state 764, "(1)"
323 line 430, "pan.___", state 767, "(((tmp2&((1<<7)-1))&&((tmp2^cached_urcu_gp_ctr.val[_pid])&(1<<7))))"
324 line 430, "pan.___", state 767, "else"
325 line 400, "pan.___", state 777, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
326 line 400, "pan.___", state 779, "(1)"
327 line 400, "pan.___", state 780, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
328 line 400, "pan.___", state 780, "else"
329 line 400, "pan.___", state 783, "(1)"
330 line 404, "pan.___", state 791, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
331 line 404, "pan.___", state 793, "(1)"
332 line 404, "pan.___", state 794, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
333 line 404, "pan.___", state 794, "else"
334 line 404, "pan.___", state 797, "(1)"
335 line 404, "pan.___", state 798, "(1)"
336 line 404, "pan.___", state 798, "(1)"
337 line 402, "pan.___", state 803, "((i<1))"
338 line 402, "pan.___", state 803, "((i>=1))"
339 line 409, "pan.___", state 809, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
340 line 410, "pan.___", state 822, "(1)"
341 line 410, "pan.___", state 823, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
342 line 410, "pan.___", state 823, "else"
343 line 410, "pan.___", state 826, "(1)"
344 line 410, "pan.___", state 827, "(1)"
345 line 410, "pan.___", state 827, "(1)"
346 line 414, "pan.___", state 835, "(1)"
347 line 414, "pan.___", state 836, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
348 line 414, "pan.___", state 836, "else"
349 line 414, "pan.___", state 839, "(1)"
350 line 414, "pan.___", state 840, "(1)"
351 line 414, "pan.___", state 840, "(1)"
352 line 412, "pan.___", state 845, "((i<1))"
353 line 412, "pan.___", state 845, "((i>=1))"
354 line 419, "pan.___", state 852, "(1)"
355 line 419, "pan.___", state 853, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
356 line 419, "pan.___", state 853, "else"
357 line 419, "pan.___", state 856, "(1)"
358 line 419, "pan.___", state 857, "(1)"
359 line 419, "pan.___", state 857, "(1)"
360 line 421, "pan.___", state 860, "(1)"
361 line 421, "pan.___", state 860, "(1)"
362 line 370, "pan.___", state 862, "(1)"
363 line 449, "pan.___", state 870, "((tmp<1))"
364 line 449, "pan.___", state 870, "((tmp>=1))"
365 line 462, "pan.___", state 873, "tmp = 0"
366 line 400, "pan.___", state 877, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
367 line 400, "pan.___", state 883, "(1)"
368 line 404, "pan.___", state 891, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
369 line 404, "pan.___", state 897, "(1)"
370 line 404, "pan.___", state 898, "(1)"
371 line 404, "pan.___", state 898, "(1)"
372 line 402, "pan.___", state 903, "((i<1))"
373 line 402, "pan.___", state 903, "((i>=1))"
374 line 409, "pan.___", state 909, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
375 line 410, "pan.___", state 922, "(1)"
376 line 410, "pan.___", state 923, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
377 line 410, "pan.___", state 923, "else"
378 line 410, "pan.___", state 926, "(1)"
379 line 410, "pan.___", state 927, "(1)"
380 line 410, "pan.___", state 927, "(1)"
381 line 414, "pan.___", state 935, "(1)"
382 line 414, "pan.___", state 936, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
383 line 414, "pan.___", state 936, "else"
384 line 414, "pan.___", state 939, "(1)"
385 line 414, "pan.___", state 940, "(1)"
386 line 414, "pan.___", state 940, "(1)"
387 line 412, "pan.___", state 945, "((i<1))"
388 line 412, "pan.___", state 945, "((i>=1))"
389 line 419, "pan.___", state 952, "(1)"
390 line 419, "pan.___", state 953, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
391 line 419, "pan.___", state 953, "else"
392 line 419, "pan.___", state 956, "(1)"
393 line 419, "pan.___", state 957, "(1)"
394 line 419, "pan.___", state 957, "(1)"
395 line 421, "pan.___", state 960, "(1)"
396 line 421, "pan.___", state 960, "(1)"
397 line 370, "pan.___", state 962, "(1)"
398 line 671, "pan.___", state 963, "tmp = cached_urcu_gp_ctr.val[_pid]"
399 line 400, "pan.___", state 967, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
400 line 400, "pan.___", state 973, "(1)"
401 line 404, "pan.___", state 981, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
402 line 404, "pan.___", state 987, "(1)"
403 line 404, "pan.___", state 988, "(1)"
404 line 404, "pan.___", state 988, "(1)"
405 line 402, "pan.___", state 993, "((i<1))"
406 line 402, "pan.___", state 993, "((i>=1))"
407 line 409, "pan.___", state 999, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
408 line 410, "pan.___", state 1012, "(1)"
409 line 410, "pan.___", state 1013, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
410 line 410, "pan.___", state 1013, "else"
411 line 410, "pan.___", state 1016, "(1)"
412 line 410, "pan.___", state 1017, "(1)"
413 line 410, "pan.___", state 1017, "(1)"
414 line 414, "pan.___", state 1025, "(1)"
415 line 414, "pan.___", state 1026, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
416 line 414, "pan.___", state 1026, "else"
417 line 414, "pan.___", state 1029, "(1)"
418 line 414, "pan.___", state 1030, "(1)"
419 line 414, "pan.___", state 1030, "(1)"
420 line 412, "pan.___", state 1035, "((i<1))"
421 line 412, "pan.___", state 1035, "((i>=1))"
422 line 419, "pan.___", state 1042, "(1)"
423 line 419, "pan.___", state 1043, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
424 line 419, "pan.___", state 1043, "else"
425 line 419, "pan.___", state 1046, "(1)"
426 line 419, "pan.___", state 1047, "(1)"
427 line 419, "pan.___", state 1047, "(1)"
428 line 421, "pan.___", state 1050, "(1)"
429 line 421, "pan.___", state 1050, "(1)"
430 line 370, "pan.___", state 1052, "(1)"
431 line 400, "pan.___", state 1061, "(1)"
432 line 404, "pan.___", state 1073, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
433 line 409, "pan.___", state 1091, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
434 line 414, "pan.___", state 1117, "(1)"
435 line 419, "pan.___", state 1134, "(1)"
436 line 404, "pan.___", state 1166, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
437 line 409, "pan.___", state 1184, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
438 line 414, "pan.___", state 1210, "(1)"
439 line 419, "pan.___", state 1227, "(1)"
440 line 400, "pan.___", state 1242, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
441 line 404, "pan.___", state 1256, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
442 line 409, "pan.___", state 1274, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
443 line 410, "pan.___", state 1287, "(1)"
444 line 414, "pan.___", state 1300, "(1)"
445 line 419, "pan.___", state 1317, "(1)"
446 line 400, "pan.___", state 1340, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
447 line 400, "pan.___", state 1342, "(1)"
448 line 400, "pan.___", state 1343, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
449 line 400, "pan.___", state 1343, "else"
450 line 400, "pan.___", state 1346, "(1)"
451 line 404, "pan.___", state 1354, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
452 line 404, "pan.___", state 1356, "(1)"
453 line 404, "pan.___", state 1357, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
454 line 404, "pan.___", state 1357, "else"
455 line 404, "pan.___", state 1360, "(1)"
456 line 404, "pan.___", state 1361, "(1)"
457 line 404, "pan.___", state 1361, "(1)"
458 line 402, "pan.___", state 1366, "((i<1))"
459 line 402, "pan.___", state 1366, "((i>=1))"
460 line 409, "pan.___", state 1372, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
461 line 410, "pan.___", state 1385, "(1)"
462 line 410, "pan.___", state 1386, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
463 line 410, "pan.___", state 1386, "else"
464 line 410, "pan.___", state 1389, "(1)"
465 line 410, "pan.___", state 1390, "(1)"
466 line 410, "pan.___", state 1390, "(1)"
467 line 414, "pan.___", state 1398, "(1)"
468 line 414, "pan.___", state 1399, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
469 line 414, "pan.___", state 1399, "else"
470 line 414, "pan.___", state 1402, "(1)"
471 line 414, "pan.___", state 1403, "(1)"
472 line 414, "pan.___", state 1403, "(1)"
473 line 412, "pan.___", state 1408, "((i<1))"
474 line 412, "pan.___", state 1408, "((i>=1))"
475 line 419, "pan.___", state 1415, "(1)"
476 line 419, "pan.___", state 1416, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
477 line 419, "pan.___", state 1416, "else"
478 line 419, "pan.___", state 1419, "(1)"
479 line 419, "pan.___", state 1420, "(1)"
480 line 419, "pan.___", state 1420, "(1)"
481 line 421, "pan.___", state 1423, "(1)"
482 line 421, "pan.___", state 1423, "(1)"
483 line 180, "pan.___", state 1448, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
484 line 184, "pan.___", state 1461, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
485 line 161, "pan.___", state 1471, "(1)"
486 line 165, "pan.___", state 1479, "(1)"
487 line 169, "pan.___", state 1491, "(1)"
488 line 176, "pan.___", state 1502, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
489 line 184, "pan.___", state 1524, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
490 line 161, "pan.___", state 1534, "(1)"
491 line 165, "pan.___", state 1542, "(1)"
492 line 169, "pan.___", state 1554, "(1)"
493 line 176, "pan.___", state 1569, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
494 line 180, "pan.___", state 1578, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
495 line 184, "pan.___", state 1591, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
496 line 161, "pan.___", state 1601, "(1)"
497 line 165, "pan.___", state 1609, "(1)"
498 line 169, "pan.___", state 1621, "(1)"
499 line 370, "pan.___", state 1642, "(1)"
500 line 696, "pan.___", state 1643, "(1)"
501 line 703, "pan.___", state 1646, "-end-"
502 (308 of 1646 states)
503unreached in proctype :init:
504 (0 of 46 states)
505unreached in proctype :never:
506 line 752, "pan.___", state 11, "-end-"
507 (1 of 11 states)
508
509pan: elapsed time 2.02 seconds
510pan: rate 84117.327 states/second
511pan: avg transition delay 8.5985e-07 usec
512cp .input.spin urcu_progress_writer_error.spin.input
513cp .input.spin.trail urcu_progress_writer_error.spin.input.trail
514make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
Userspace RCU (urcu) for Linux
This page took 0.043235 seconds and 4 git commands to generate.