projects / urcu.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Add phase 3 : scalability run
[urcu.git] / formal-model / results / urcu-controldataflow-no-ipi / result-ipi-urcu_free / urcu_progress_writer.log
CommitLineData
dbf69285
MD		 1make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
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.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 1245)
19depth 23: Claim reached state 9 (line 1250)
20depth 51: Claim reached state 9 (line 1249)
21pan: acceptance cycle (at depth 573)
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 88 byte, depth reached 3997, errors: 1
35 24768 states, stored (55970 visited)
36 10426084 states, matched
37 10482054 transitions (= visited+matched)
38 56520057 atomic steps
39hash conflicts: 68749 (resolved)
40
41Stats on memory usage (in Megabytes):
42 2.740 equivalent memory usage for states (stored*(State-vector + overhead))
43 2.770 actual memory usage for states (unsuccessful compression: 101.10%)
44 state-vector as stored = 89 byte + 28 byte overhead
45 8.000 memory used for hash table (-w20)
46 457.764 memory used for DFS stack (-m10000000)
47 468.498 total actual memory usage
48
49unreached in proctype urcu_reader
50 line 647, "pan.___", state 20, "(1)"
51 line 250, "pan.___", state 32, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
52 line 258, "pan.___", state 54, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
53 line 262, "pan.___", state 63, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
54 line 227, "pan.___", state 79, "(1)"
55 line 231, "pan.___", state 87, "(1)"
56 line 235, "pan.___", state 99, "(1)"
57 line 239, "pan.___", state 107, "(1)"
58 line 387, "pan.___", state 133, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
59 line 396, "pan.___", state 165, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
60 line 400, "pan.___", state 179, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
61 line 404, "pan.___", state 198, "(1)"
62 line 413, "pan.___", state 228, "(1)"
63 line 417, "pan.___", state 241, "(1)"
64 line 663, "pan.___", state 262, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
65 line 387, "pan.___", state 269, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
66 line 396, "pan.___", state 301, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
67 line 400, "pan.___", state 315, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
68 line 404, "pan.___", state 334, "(1)"
69 line 413, "pan.___", state 364, "(1)"
70 line 417, "pan.___", state 377, "(1)"
71 line 387, "pan.___", state 398, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
72 line 396, "pan.___", state 430, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
73 line 400, "pan.___", state 444, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
74 line 404, "pan.___", state 463, "(1)"
75 line 413, "pan.___", state 493, "(1)"
76 line 417, "pan.___", state 506, "(1)"
77 line 387, "pan.___", state 529, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
78 line 387, "pan.___", state 531, "(1)"
79 line 387, "pan.___", state 532, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
80 line 387, "pan.___", state 532, "else"
81 line 387, "pan.___", state 535, "(1)"
82 line 391, "pan.___", state 543, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
83 line 391, "pan.___", state 545, "(1)"
84 line 391, "pan.___", state 546, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
85 line 391, "pan.___", state 546, "else"
86 line 391, "pan.___", state 549, "(1)"
87 line 391, "pan.___", state 550, "(1)"
88 line 391, "pan.___", state 550, "(1)"
89 line 389, "pan.___", state 555, "((i<1))"
90 line 389, "pan.___", state 555, "((i>=1))"
91 line 396, "pan.___", state 561, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
92 line 396, "pan.___", state 563, "(1)"
93 line 396, "pan.___", state 564, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
94 line 396, "pan.___", state 564, "else"
95 line 396, "pan.___", state 567, "(1)"
96 line 396, "pan.___", state 568, "(1)"
97 line 396, "pan.___", state 568, "(1)"
98 line 400, "pan.___", state 575, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
99 line 400, "pan.___", state 577, "(1)"
100 line 400, "pan.___", state 578, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
101 line 400, "pan.___", state 578, "else"
102 line 400, "pan.___", state 581, "(1)"
103 line 400, "pan.___", state 582, "(1)"
104 line 400, "pan.___", state 582, "(1)"
105 line 398, "pan.___", state 587, "((i<2))"
106 line 398, "pan.___", state 587, "((i>=2))"
107 line 404, "pan.___", state 594, "(1)"
108 line 404, "pan.___", state 595, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
109 line 404, "pan.___", state 595, "else"
110 line 404, "pan.___", state 598, "(1)"
111 line 404, "pan.___", state 599, "(1)"
112 line 404, "pan.___", state 599, "(1)"
113 line 408, "pan.___", state 607, "(1)"
114 line 408, "pan.___", state 608, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
115 line 408, "pan.___", state 608, "else"
116 line 408, "pan.___", state 611, "(1)"
117 line 408, "pan.___", state 612, "(1)"
118 line 408, "pan.___", state 612, "(1)"
119 line 406, "pan.___", state 617, "((i<1))"
120 line 406, "pan.___", state 617, "((i>=1))"
121 line 413, "pan.___", state 624, "(1)"
122 line 413, "pan.___", state 625, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
123 line 413, "pan.___", state 625, "else"
124 line 413, "pan.___", state 628, "(1)"
125 line 413, "pan.___", state 629, "(1)"
126 line 413, "pan.___", state 629, "(1)"
127 line 417, "pan.___", state 637, "(1)"
128 line 417, "pan.___", state 638, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
129 line 417, "pan.___", state 638, "else"
130 line 417, "pan.___", state 641, "(1)"
131 line 417, "pan.___", state 642, "(1)"
132 line 417, "pan.___", state 642, "(1)"
133 line 415, "pan.___", state 647, "((i<2))"
134 line 415, "pan.___", state 647, "((i>=2))"
135 line 422, "pan.___", state 651, "(1)"
136 line 422, "pan.___", state 651, "(1)"
137 line 663, "pan.___", state 654, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
138 line 663, "pan.___", state 655, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
139 line 663, "pan.___", state 656, "(1)"
140 line 387, "pan.___", state 663, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
141 line 396, "pan.___", state 695, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
142 line 400, "pan.___", state 709, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
143 line 404, "pan.___", state 728, "(1)"
144 line 413, "pan.___", state 758, "(1)"
145 line 417, "pan.___", state 771, "(1)"
146 line 387, "pan.___", state 799, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
147 line 387, "pan.___", state 801, "(1)"
148 line 387, "pan.___", state 802, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
149 line 387, "pan.___", state 802, "else"
150 line 387, "pan.___", state 805, "(1)"
151 line 391, "pan.___", state 813, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
152 line 391, "pan.___", state 815, "(1)"
153 line 391, "pan.___", state 816, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
154 line 391, "pan.___", state 816, "else"
155 line 391, "pan.___", state 819, "(1)"
156 line 391, "pan.___", state 820, "(1)"
157 line 391, "pan.___", state 820, "(1)"
158 line 389, "pan.___", state 825, "((i<1))"
159 line 389, "pan.___", state 825, "((i>=1))"
160 line 396, "pan.___", state 831, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
161 line 396, "pan.___", state 833, "(1)"
162 line 396, "pan.___", state 834, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
163 line 396, "pan.___", state 834, "else"
164 line 396, "pan.___", state 837, "(1)"
165 line 396, "pan.___", state 838, "(1)"
166 line 396, "pan.___", state 838, "(1)"
167 line 400, "pan.___", state 845, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
168 line 400, "pan.___", state 847, "(1)"
169 line 400, "pan.___", state 848, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
170 line 400, "pan.___", state 848, "else"
171 line 400, "pan.___", state 851, "(1)"
172 line 400, "pan.___", state 852, "(1)"
173 line 400, "pan.___", state 852, "(1)"
174 line 398, "pan.___", state 857, "((i<2))"
175 line 398, "pan.___", state 857, "((i>=2))"
176 line 404, "pan.___", state 864, "(1)"
177 line 404, "pan.___", state 865, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
178 line 404, "pan.___", state 865, "else"
179 line 404, "pan.___", state 868, "(1)"
180 line 404, "pan.___", state 869, "(1)"
181 line 404, "pan.___", state 869, "(1)"
182 line 408, "pan.___", state 877, "(1)"
183 line 408, "pan.___", state 878, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
184 line 408, "pan.___", state 878, "else"
185 line 408, "pan.___", state 881, "(1)"
186 line 408, "pan.___", state 882, "(1)"
187 line 408, "pan.___", state 882, "(1)"
188 line 406, "pan.___", state 887, "((i<1))"
189 line 406, "pan.___", state 887, "((i>=1))"
190 line 413, "pan.___", state 894, "(1)"
191 line 413, "pan.___", state 895, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
192 line 413, "pan.___", state 895, "else"
193 line 413, "pan.___", state 898, "(1)"
194 line 413, "pan.___", state 899, "(1)"
195 line 413, "pan.___", state 899, "(1)"
196 line 417, "pan.___", state 907, "(1)"
197 line 417, "pan.___", state 908, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
198 line 417, "pan.___", state 908, "else"
199 line 417, "pan.___", state 911, "(1)"
200 line 417, "pan.___", state 912, "(1)"
201 line 417, "pan.___", state 912, "(1)"
202 line 422, "pan.___", state 921, "(1)"
203 line 422, "pan.___", state 921, "(1)"
204 line 387, "pan.___", state 928, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
205 line 387, "pan.___", state 930, "(1)"
206 line 387, "pan.___", state 931, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
207 line 387, "pan.___", state 931, "else"
208 line 387, "pan.___", state 934, "(1)"
209 line 391, "pan.___", state 942, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
210 line 391, "pan.___", state 944, "(1)"
211 line 391, "pan.___", state 945, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
212 line 391, "pan.___", state 945, "else"
213 line 391, "pan.___", state 948, "(1)"
214 line 391, "pan.___", state 949, "(1)"
215 line 391, "pan.___", state 949, "(1)"
216 line 389, "pan.___", state 954, "((i<1))"
217 line 389, "pan.___", state 954, "((i>=1))"
218 line 396, "pan.___", state 960, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
219 line 396, "pan.___", state 962, "(1)"
220 line 396, "pan.___", state 963, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
221 line 396, "pan.___", state 963, "else"
222 line 396, "pan.___", state 966, "(1)"
223 line 396, "pan.___", state 967, "(1)"
224 line 396, "pan.___", state 967, "(1)"
225 line 400, "pan.___", state 974, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
226 line 400, "pan.___", state 976, "(1)"
227 line 400, "pan.___", state 977, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
228 line 400, "pan.___", state 977, "else"
229 line 400, "pan.___", state 980, "(1)"
230 line 400, "pan.___", state 981, "(1)"
231 line 400, "pan.___", state 981, "(1)"
232 line 398, "pan.___", state 986, "((i<2))"
233 line 398, "pan.___", state 986, "((i>=2))"
234 line 404, "pan.___", state 993, "(1)"
235 line 404, "pan.___", state 994, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
236 line 404, "pan.___", state 994, "else"
237 line 404, "pan.___", state 997, "(1)"
238 line 404, "pan.___", state 998, "(1)"
239 line 404, "pan.___", state 998, "(1)"
240 line 408, "pan.___", state 1006, "(1)"
241 line 408, "pan.___", state 1007, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
242 line 408, "pan.___", state 1007, "else"
243 line 408, "pan.___", state 1010, "(1)"
244 line 408, "pan.___", state 1011, "(1)"
245 line 408, "pan.___", state 1011, "(1)"
246 line 406, "pan.___", state 1016, "((i<1))"
247 line 406, "pan.___", state 1016, "((i>=1))"
248 line 413, "pan.___", state 1023, "(1)"
249 line 413, "pan.___", state 1024, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
250 line 413, "pan.___", state 1024, "else"
251 line 413, "pan.___", state 1027, "(1)"
252 line 413, "pan.___", state 1028, "(1)"
253 line 413, "pan.___", state 1028, "(1)"
254 line 417, "pan.___", state 1036, "(1)"
255 line 417, "pan.___", state 1037, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
256 line 417, "pan.___", state 1037, "else"
257 line 417, "pan.___", state 1040, "(1)"
258 line 417, "pan.___", state 1041, "(1)"
259 line 417, "pan.___", state 1041, "(1)"
260 line 415, "pan.___", state 1046, "((i<2))"
261 line 415, "pan.___", state 1046, "((i>=2))"
262 line 422, "pan.___", state 1050, "(1)"
263 line 422, "pan.___", state 1050, "(1)"
264 line 671, "pan.___", state 1054, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
265 line 387, "pan.___", state 1059, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
266 line 396, "pan.___", state 1091, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
267 line 400, "pan.___", state 1105, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
268 line 404, "pan.___", state 1124, "(1)"
269 line 413, "pan.___", state 1154, "(1)"
270 line 417, "pan.___", state 1167, "(1)"
271 line 387, "pan.___", state 1191, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
272 line 396, "pan.___", state 1223, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
273 line 400, "pan.___", state 1237, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
274 line 404, "pan.___", state 1256, "(1)"
275 line 413, "pan.___", state 1286, "(1)"
276 line 417, "pan.___", state 1299, "(1)"
277 line 387, "pan.___", state 1324, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
278 line 396, "pan.___", state 1356, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
279 line 400, "pan.___", state 1370, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
280 line 404, "pan.___", state 1389, "(1)"
281 line 413, "pan.___", state 1419, "(1)"
282 line 417, "pan.___", state 1432, "(1)"
283 line 387, "pan.___", state 1453, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
284 line 396, "pan.___", state 1485, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
285 line 400, "pan.___", state 1499, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
286 line 404, "pan.___", state 1518, "(1)"
287 line 413, "pan.___", state 1548, "(1)"
288 line 417, "pan.___", state 1561, "(1)"
289 line 387, "pan.___", state 1587, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
290 line 396, "pan.___", state 1619, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
291 line 400, "pan.___", state 1633, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
292 line 404, "pan.___", state 1652, "(1)"
293 line 413, "pan.___", state 1682, "(1)"
294 line 417, "pan.___", state 1695, "(1)"
295 line 387, "pan.___", state 1716, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
296 line 396, "pan.___", state 1748, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
297 line 400, "pan.___", state 1762, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
298 line 404, "pan.___", state 1781, "(1)"
299 line 413, "pan.___", state 1811, "(1)"
300 line 417, "pan.___", state 1824, "(1)"
301 line 387, "pan.___", state 1848, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
302 line 396, "pan.___", state 1880, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
303 line 400, "pan.___", state 1894, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
304 line 404, "pan.___", state 1913, "(1)"
305 line 413, "pan.___", state 1943, "(1)"
306 line 417, "pan.___", state 1956, "(1)"
307 line 710, "pan.___", state 1977, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
308 line 387, "pan.___", state 1984, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
309 line 396, "pan.___", state 2016, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
310 line 400, "pan.___", state 2030, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
311 line 404, "pan.___", state 2049, "(1)"
312 line 413, "pan.___", state 2079, "(1)"
313 line 417, "pan.___", state 2092, "(1)"
314 line 387, "pan.___", state 2113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
315 line 396, "pan.___", state 2145, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
316 line 400, "pan.___", state 2159, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
317 line 404, "pan.___", state 2178, "(1)"
318 line 413, "pan.___", state 2208, "(1)"
319 line 417, "pan.___", state 2221, "(1)"
320 line 387, "pan.___", state 2244, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
321 line 387, "pan.___", state 2246, "(1)"
322 line 387, "pan.___", state 2247, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
323 line 387, "pan.___", state 2247, "else"
324 line 387, "pan.___", state 2250, "(1)"
325 line 391, "pan.___", state 2258, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
326 line 391, "pan.___", state 2260, "(1)"
327 line 391, "pan.___", state 2261, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
328 line 391, "pan.___", state 2261, "else"
329 line 391, "pan.___", state 2264, "(1)"
330 line 391, "pan.___", state 2265, "(1)"
331 line 391, "pan.___", state 2265, "(1)"
332 line 389, "pan.___", state 2270, "((i<1))"
333 line 389, "pan.___", state 2270, "((i>=1))"
334 line 396, "pan.___", state 2276, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
335 line 396, "pan.___", state 2278, "(1)"
336 line 396, "pan.___", state 2279, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
337 line 396, "pan.___", state 2279, "else"
338 line 396, "pan.___", state 2282, "(1)"
339 line 396, "pan.___", state 2283, "(1)"
340 line 396, "pan.___", state 2283, "(1)"
341 line 400, "pan.___", state 2290, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
342 line 400, "pan.___", state 2292, "(1)"
343 line 400, "pan.___", state 2293, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
344 line 400, "pan.___", state 2293, "else"
345 line 400, "pan.___", state 2296, "(1)"
346 line 400, "pan.___", state 2297, "(1)"
347 line 400, "pan.___", state 2297, "(1)"
348 line 398, "pan.___", state 2302, "((i<2))"
349 line 398, "pan.___", state 2302, "((i>=2))"
350 line 404, "pan.___", state 2309, "(1)"
351 line 404, "pan.___", state 2310, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
352 line 404, "pan.___", state 2310, "else"
353 line 404, "pan.___", state 2313, "(1)"
354 line 404, "pan.___", state 2314, "(1)"
355 line 404, "pan.___", state 2314, "(1)"
356 line 408, "pan.___", state 2322, "(1)"
357 line 408, "pan.___", state 2323, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
358 line 408, "pan.___", state 2323, "else"
359 line 408, "pan.___", state 2326, "(1)"
360 line 408, "pan.___", state 2327, "(1)"
361 line 408, "pan.___", state 2327, "(1)"
362 line 406, "pan.___", state 2332, "((i<1))"
363 line 406, "pan.___", state 2332, "((i>=1))"
364 line 413, "pan.___", state 2339, "(1)"
365 line 413, "pan.___", state 2340, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
366 line 413, "pan.___", state 2340, "else"
367 line 413, "pan.___", state 2343, "(1)"
368 line 413, "pan.___", state 2344, "(1)"
369 line 413, "pan.___", state 2344, "(1)"
370 line 417, "pan.___", state 2352, "(1)"
371 line 417, "pan.___", state 2353, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
372 line 417, "pan.___", state 2353, "else"
373 line 417, "pan.___", state 2356, "(1)"
374 line 417, "pan.___", state 2357, "(1)"
375 line 417, "pan.___", state 2357, "(1)"
376 line 415, "pan.___", state 2362, "((i<2))"
377 line 415, "pan.___", state 2362, "((i>=2))"
378 line 422, "pan.___", state 2366, "(1)"
379 line 422, "pan.___", state 2366, "(1)"
380 line 710, "pan.___", state 2369, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
381 line 710, "pan.___", state 2370, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
382 line 710, "pan.___", state 2371, "(1)"
383 line 387, "pan.___", state 2378, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
384 line 396, "pan.___", state 2410, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
385 line 400, "pan.___", state 2424, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
386 line 404, "pan.___", state 2443, "(1)"
387 line 413, "pan.___", state 2473, "(1)"
388 line 417, "pan.___", state 2486, "(1)"
389 line 387, "pan.___", state 2513, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
390 line 396, "pan.___", state 2545, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
391 line 400, "pan.___", state 2559, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
392 line 404, "pan.___", state 2578, "(1)"
393 line 413, "pan.___", state 2608, "(1)"
394 line 417, "pan.___", state 2621, "(1)"
395 line 387, "pan.___", state 2642, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
396 line 396, "pan.___", state 2674, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
397 line 400, "pan.___", state 2688, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
398 line 404, "pan.___", state 2707, "(1)"
399 line 413, "pan.___", state 2737, "(1)"
400 line 417, "pan.___", state 2750, "(1)"
401 line 227, "pan.___", state 2783, "(1)"
402 line 235, "pan.___", state 2803, "(1)"
403 line 239, "pan.___", state 2811, "(1)"
404 line 227, "pan.___", state 2826, "(1)"
405 line 235, "pan.___", state 2846, "(1)"
406 line 239, "pan.___", state 2854, "(1)"
407 line 870, "pan.___", state 2871, "-end-"
408 (279 of 2871 states)
409unreached in proctype urcu_writer
410 line 387, "pan.___", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
411 line 387, "pan.___", state 24, "(1)"
412 line 391, "pan.___", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
413 line 391, "pan.___", state 38, "(1)"
414 line 391, "pan.___", state 39, "(1)"
415 line 391, "pan.___", state 39, "(1)"
416 line 389, "pan.___", state 44, "((i<1))"
417 line 389, "pan.___", state 44, "((i>=1))"
418 line 396, "pan.___", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
419 line 396, "pan.___", state 56, "(1)"
420 line 396, "pan.___", state 57, "(1)"
421 line 396, "pan.___", state 57, "(1)"
422 line 400, "pan.___", state 64, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
423 line 400, "pan.___", state 70, "(1)"
424 line 400, "pan.___", state 71, "(1)"
425 line 400, "pan.___", state 71, "(1)"
426 line 398, "pan.___", state 76, "((i<2))"
427 line 398, "pan.___", state 76, "((i>=2))"
428 line 404, "pan.___", state 83, "(1)"
429 line 404, "pan.___", state 84, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
430 line 404, "pan.___", state 84, "else"
431 line 404, "pan.___", state 87, "(1)"
432 line 404, "pan.___", state 88, "(1)"
433 line 404, "pan.___", state 88, "(1)"
434 line 408, "pan.___", state 96, "(1)"
435 line 408, "pan.___", state 97, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
436 line 408, "pan.___", state 97, "else"
437 line 408, "pan.___", state 100, "(1)"
438 line 408, "pan.___", state 101, "(1)"
439 line 408, "pan.___", state 101, "(1)"
440 line 406, "pan.___", state 106, "((i<1))"
441 line 406, "pan.___", state 106, "((i>=1))"
442 line 413, "pan.___", state 113, "(1)"
443 line 413, "pan.___", state 114, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
444 line 413, "pan.___", state 114, "else"
445 line 413, "pan.___", state 117, "(1)"
446 line 413, "pan.___", state 118, "(1)"
447 line 413, "pan.___", state 118, "(1)"
448 line 417, "pan.___", state 126, "(1)"
449 line 417, "pan.___", state 127, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
450 line 417, "pan.___", state 127, "else"
451 line 417, "pan.___", state 130, "(1)"
452 line 417, "pan.___", state 131, "(1)"
453 line 417, "pan.___", state 131, "(1)"
454 line 415, "pan.___", state 136, "((i<2))"
455 line 415, "pan.___", state 136, "((i>=2))"
456 line 422, "pan.___", state 140, "(1)"
457 line 422, "pan.___", state 140, "(1)"
458 line 250, "pan.___", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
459 line 254, "pan.___", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
460 line 252, "pan.___", state 166, "((i<1))"
461 line 252, "pan.___", state 166, "((i>=1))"
462 line 258, "pan.___", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
463 line 993, "pan.___", state 199, "old_data = cached_rcu_ptr.val[_pid]"
464 line 387, "pan.___", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
465 line 391, "pan.___", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
466 line 396, "pan.___", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
467 line 400, "pan.___", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
468 line 404, "pan.___", state 276, "(1)"
469 line 408, "pan.___", state 289, "(1)"
470 line 413, "pan.___", state 306, "(1)"
471 line 417, "pan.___", state 319, "(1)"
472 line 391, "pan.___", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
473 line 396, "pan.___", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
474 line 400, "pan.___", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
475 line 408, "pan.___", state 420, "(1)"
476 line 413, "pan.___", state 437, "(1)"
477 line 417, "pan.___", state 450, "(1)"
478 line 391, "pan.___", state 494, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
479 line 396, "pan.___", state 512, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
480 line 400, "pan.___", state 526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
481 line 408, "pan.___", state 558, "(1)"
482 line 413, "pan.___", state 575, "(1)"
483 line 417, "pan.___", state 588, "(1)"
484 line 391, "pan.___", state 623, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
485 line 396, "pan.___", state 641, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
486 line 400, "pan.___", state 655, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
487 line 408, "pan.___", state 687, "(1)"
488 line 413, "pan.___", state 704, "(1)"
489 line 417, "pan.___", state 717, "(1)"
490 line 391, "pan.___", state 754, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
491 line 396, "pan.___", state 772, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
492 line 400, "pan.___", state 786, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
493 line 408, "pan.___", state 818, "(1)"
494 line 413, "pan.___", state 835, "(1)"
495 line 417, "pan.___", state 848, "(1)"
496 line 1113, "pan.___", state 872, "_proc_urcu_writer = (_proc_urcu_writer&~(((1<<12)|(1<<11))))"
497 line 250, "pan.___", state 903, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
498 line 254, "pan.___", state 912, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
499 line 252, "pan.___", state 920, "((i<1))"
500 line 252, "pan.___", state 920, "((i>=1))"
501 line 258, "pan.___", state 927, "(1)"
502 line 258, "pan.___", state 928, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
503 line 258, "pan.___", state 928, "else"
504 line 262, "pan.___", state 934, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
505 line 260, "pan.___", state 942, "((i<2))"
506 line 260, "pan.___", state 942, "((i>=2))"
507 line 227, "pan.___", state 950, "(1)"
508 line 231, "pan.___", state 958, "(1)"
509 line 231, "pan.___", state 959, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
510 line 231, "pan.___", state 959, "else"
511 line 229, "pan.___", state 964, "((i<1))"
512 line 229, "pan.___", state 964, "((i>=1))"
513 line 235, "pan.___", state 970, "(1)"
514 line 235, "pan.___", state 971, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
515 line 235, "pan.___", state 971, "else"
516 line 239, "pan.___", state 978, "(1)"
517 line 239, "pan.___", state 979, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
518 line 239, "pan.___", state 979, "else"
519 line 244, "pan.___", state 988, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
520 line 244, "pan.___", state 988, "else"
521 line 250, "pan.___", state 1009, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
522 line 254, "pan.___", state 1018, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
523 line 258, "pan.___", state 1031, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
524 line 262, "pan.___", state 1040, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
525 line 227, "pan.___", state 1056, "(1)"
526 line 231, "pan.___", state 1064, "(1)"
527 line 235, "pan.___", state 1076, "(1)"
528 line 239, "pan.___", state 1084, "(1)"
529 line 250, "pan.___", state 1101, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
530 line 254, "pan.___", state 1110, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
531 line 252, "pan.___", state 1118, "((i<1))"
532 line 252, "pan.___", state 1118, "((i>=1))"
533 line 258, "pan.___", state 1123, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
534 line 262, "pan.___", state 1132, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
535 line 260, "pan.___", state 1140, "((i<2))"
536 line 260, "pan.___", state 1140, "((i>=2))"
537 line 227, "pan.___", state 1148, "(1)"
538 line 231, "pan.___", state 1156, "(1)"
539 line 231, "pan.___", state 1157, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
540 line 231, "pan.___", state 1157, "else"
541 line 229, "pan.___", state 1162, "((i<1))"
542 line 229, "pan.___", state 1162, "((i>=1))"
543 line 235, "pan.___", state 1168, "(1)"
544 line 235, "pan.___", state 1169, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
545 line 235, "pan.___", state 1169, "else"
546 line 239, "pan.___", state 1176, "(1)"
547 line 239, "pan.___", state 1177, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
548 line 239, "pan.___", state 1177, "else"
549 line 244, "pan.___", state 1186, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
550 line 244, "pan.___", state 1186, "else"
551 line 1180, "pan.___", state 1189, "i = 0"
552 line 1180, "pan.___", state 1191, "reader_barrier = 1"
553 line 1180, "pan.___", state 1202, "((i<1))"
554 line 1180, "pan.___", state 1202, "((i>=1))"
555 line 250, "pan.___", state 1207, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
556 line 254, "pan.___", state 1216, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
557 line 252, "pan.___", state 1224, "((i<1))"
558 line 252, "pan.___", state 1224, "((i>=1))"
559 line 258, "pan.___", state 1229, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
560 line 262, "pan.___", state 1238, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
561 line 260, "pan.___", state 1246, "((i<2))"
562 line 260, "pan.___", state 1246, "((i>=2))"
563 line 227, "pan.___", state 1254, "(1)"
564 line 231, "pan.___", state 1262, "(1)"
565 line 231, "pan.___", state 1263, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
566 line 231, "pan.___", state 1263, "else"
567 line 229, "pan.___", state 1268, "((i<1))"
568 line 229, "pan.___", state 1268, "((i>=1))"
569 line 235, "pan.___", state 1274, "(1)"
570 line 235, "pan.___", state 1275, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
571 line 235, "pan.___", state 1275, "else"
572 line 239, "pan.___", state 1282, "(1)"
573 line 239, "pan.___", state 1283, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
574 line 239, "pan.___", state 1283, "else"
575 line 244, "pan.___", state 1292, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
576 line 244, "pan.___", state 1292, "else"
577 line 250, "pan.___", state 1299, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
578 line 250, "pan.___", state 1301, "(1)"
579 line 254, "pan.___", state 1308, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
580 line 254, "pan.___", state 1310, "(1)"
581 line 254, "pan.___", state 1311, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
582 line 254, "pan.___", state 1311, "else"
583 line 252, "pan.___", state 1316, "((i<1))"
584 line 252, "pan.___", state 1316, "((i>=1))"
585 line 258, "pan.___", state 1321, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
586 line 258, "pan.___", state 1323, "(1)"
587 line 258, "pan.___", state 1324, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
588 line 258, "pan.___", state 1324, "else"
589 line 262, "pan.___", state 1330, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
590 line 262, "pan.___", state 1332, "(1)"
591 line 262, "pan.___", state 1333, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
592 line 262, "pan.___", state 1333, "else"
593 line 260, "pan.___", state 1338, "((i<2))"
594 line 260, "pan.___", state 1338, "((i>=2))"
595 line 227, "pan.___", state 1346, "(1)"
596 line 231, "pan.___", state 1354, "(1)"
597 line 231, "pan.___", state 1355, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
598 line 231, "pan.___", state 1355, "else"
599 line 229, "pan.___", state 1360, "((i<1))"
600 line 229, "pan.___", state 1360, "((i>=1))"
601 line 235, "pan.___", state 1366, "(1)"
602 line 235, "pan.___", state 1367, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
603 line 235, "pan.___", state 1367, "else"
604 line 239, "pan.___", state 1374, "(1)"
605 line 239, "pan.___", state 1375, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
606 line 239, "pan.___", state 1375, "else"
607 line 244, "pan.___", state 1384, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
608 line 244, "pan.___", state 1384, "else"
609 line 1183, "pan.___", state 1387, "i = 0"
610 line 1183, "pan.___", state 1389, "reader_barrier = 1"
611 line 1183, "pan.___", state 1400, "((i<1))"
612 line 1183, "pan.___", state 1400, "((i>=1))"
613 line 250, "pan.___", state 1405, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
614 line 250, "pan.___", state 1407, "(1)"
615 line 254, "pan.___", state 1414, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
616 line 254, "pan.___", state 1416, "(1)"
617 line 254, "pan.___", state 1417, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
618 line 254, "pan.___", state 1417, "else"
619 line 252, "pan.___", state 1422, "((i<1))"
620 line 252, "pan.___", state 1422, "((i>=1))"
621 line 258, "pan.___", state 1427, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
622 line 258, "pan.___", state 1429, "(1)"
623 line 258, "pan.___", state 1430, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
624 line 258, "pan.___", state 1430, "else"
625 line 262, "pan.___", state 1436, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
626 line 262, "pan.___", state 1438, "(1)"
627 line 262, "pan.___", state 1439, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
628 line 262, "pan.___", state 1439, "else"
629 line 260, "pan.___", state 1444, "((i<2))"
630 line 260, "pan.___", state 1444, "((i>=2))"
631 line 227, "pan.___", state 1452, "(1)"
632 line 231, "pan.___", state 1460, "(1)"
633 line 231, "pan.___", state 1461, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
634 line 231, "pan.___", state 1461, "else"
635 line 229, "pan.___", state 1466, "((i<1))"
636 line 229, "pan.___", state 1466, "((i>=1))"
637 line 235, "pan.___", state 1472, "(1)"
638 line 235, "pan.___", state 1473, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
639 line 235, "pan.___", state 1473, "else"
640 line 239, "pan.___", state 1480, "(1)"
641 line 239, "pan.___", state 1481, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
642 line 239, "pan.___", state 1481, "else"
643 line 244, "pan.___", state 1490, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
644 line 244, "pan.___", state 1490, "else"
645 line 277, "pan.___", state 1492, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
646 line 277, "pan.___", state 1492, "else"
647 line 1183, "pan.___", state 1493, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
648 line 1183, "pan.___", state 1493, "else"
649 line 254, "pan.___", state 1506, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
650 line 258, "pan.___", state 1519, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
651 line 262, "pan.___", state 1528, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
652 line 227, "pan.___", state 1544, "(1)"
653 line 231, "pan.___", state 1552, "(1)"
654 line 235, "pan.___", state 1564, "(1)"
655 line 239, "pan.___", state 1572, "(1)"
656 line 250, "pan.___", state 1603, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
657 line 254, "pan.___", state 1612, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
658 line 258, "pan.___", state 1625, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
659 line 262, "pan.___", state 1634, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
660 line 227, "pan.___", state 1650, "(1)"
661 line 231, "pan.___", state 1658, "(1)"
662 line 235, "pan.___", state 1670, "(1)"
663 line 239, "pan.___", state 1678, "(1)"
664 line 1191, "pan.___", state 1694, "-end-"
665 (192 of 1694 states)
666unreached in proctype :init:
667 (0 of 78 states)
668unreached in proctype :never:
669 line 1252, "pan.___", state 11, "-end-"
670 (1 of 11 states)
671
672pan: elapsed time 13.7 seconds
673pan: rate 4094.3672 states/second
674pan: avg transition delay 1.3041e-06 usec
675cp .input.spin urcu_progress_writer.spin.input
676cp .input.spin.trail urcu_progress_writer.spin.input.trail
677make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
Userspace RCU (urcu) for Linux
This page took 0.048861 seconds and 4 git commands to generate.