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-signal-over-writer / testmerge / urcu_free_single_flip.log
CommitLineData
06e8b2a8
MD		 1make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu/testmerge'
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_free.ltl | grep -v ^//`)" >> pan.ltl
7cp urcu_free_single_flip.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 -w -DHASH64 -o pan pan.c
15./pan -a -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 567)
19pan: claim violated! (at depth 1353)
20pan: wrote .input.spin.trail
21
22(Spin Version 5.1.7 -- 23 December 2008)
23Warning: Search not completed
24 + Partial Order Reduction
25
26Full statespace search for:
27 never claim +
28 assertion violations + (if within scope of claim)
29 acceptance cycles + (fairness disabled)
30 invalid end states - (disabled by never claim)
31
32State-vector 56 byte, depth reached 3705, errors: 1
33 216253 states, stored
34 2924019 states, matched
35 3140272 transitions (= stored+matched)
36 11791015 atomic steps
37hash conflicts: 155585 (resolved)
38
39Stats on memory usage (in Megabytes):
40 17.324 equivalent memory usage for states (stored*(State-vector + overhead))
41 13.576 actual memory usage for states (compression: 78.37%)
42 state-vector as stored = 38 byte + 28 byte overhead
43 8.000 memory used for hash table (-w20)
44 457.764 memory used for DFS stack (-m10000000)
45 479.338 total actual memory usage
46
47unreached in proctype urcu_reader
48 line 289, "pan.___", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
49 line 298, "pan.___", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
50 line 299, "pan.___", state 61, "(1)"
51 line 308, "pan.___", state 91, "(1)"
52 line 289, "pan.___", state 104, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
53 line 298, "pan.___", state 136, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
54 line 299, "pan.___", state 149, "(1)"
55 line 308, "pan.___", state 179, "(1)"
56 line 289, "pan.___", state 193, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
57 line 298, "pan.___", state 225, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
58 line 299, "pan.___", state 238, "(1)"
59 line 308, "pan.___", state 268, "(1)"
60 line 159, "pan.___", state 289, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
61 line 159, "pan.___", state 291, "(1)"
62 line 163, "pan.___", state 298, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
63 line 163, "pan.___", state 300, "(1)"
64 line 163, "pan.___", state 301, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
65 line 163, "pan.___", state 301, "else"
66 line 161, "pan.___", state 306, "((j<1))"
67 line 161, "pan.___", state 306, "((j>=1))"
68 line 167, "pan.___", state 311, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
69 line 144, "pan.___", state 321, "(1)"
70 line 148, "pan.___", state 329, "(1)"
71 line 148, "pan.___", state 330, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
72 line 148, "pan.___", state 330, "else"
73 line 146, "pan.___", state 335, "((j<1))"
74 line 146, "pan.___", state 335, "((j>=1))"
75 line 152, "pan.___", state 341, "(1)"
76 line 152, "pan.___", state 342, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
77 line 152, "pan.___", state 342, "else"
78 line 154, "pan.___", state 345, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
79 line 154, "pan.___", state 345, "else"
80 line 186, "pan.___", state 347, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
81 line 186, "pan.___", state 347, "else"
82 line 159, "pan.___", state 352, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
83 line 159, "pan.___", state 354, "(1)"
84 line 163, "pan.___", state 361, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
85 line 163, "pan.___", state 363, "(1)"
86 line 163, "pan.___", state 364, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
87 line 163, "pan.___", state 364, "else"
88 line 161, "pan.___", state 369, "((j<1))"
89 line 161, "pan.___", state 369, "((j>=1))"
90 line 167, "pan.___", state 374, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
91 line 144, "pan.___", state 384, "(1)"
92 line 148, "pan.___", state 392, "(1)"
93 line 148, "pan.___", state 393, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
94 line 148, "pan.___", state 393, "else"
95 line 146, "pan.___", state 398, "((j<1))"
96 line 146, "pan.___", state 398, "((j>=1))"
97 line 152, "pan.___", state 404, "(1)"
98 line 152, "pan.___", state 405, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
99 line 152, "pan.___", state 405, "else"
100 line 154, "pan.___", state 408, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
101 line 154, "pan.___", state 408, "else"
102 line 186, "pan.___", state 410, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
103 line 186, "pan.___", state 410, "else"
104 line 200, "pan.___", state 414, "((i<1))"
105 line 200, "pan.___", state 414, "((i>=1))"
106 line 159, "pan.___", state 419, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
107 line 159, "pan.___", state 421, "(1)"
108 line 163, "pan.___", state 428, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
109 line 163, "pan.___", state 430, "(1)"
110 line 163, "pan.___", state 431, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
111 line 163, "pan.___", state 431, "else"
112 line 161, "pan.___", state 436, "((j<1))"
113 line 161, "pan.___", state 436, "((j>=1))"
114 line 167, "pan.___", state 441, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
115 line 144, "pan.___", state 451, "(1)"
116 line 148, "pan.___", state 459, "(1)"
117 line 148, "pan.___", state 460, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
118 line 148, "pan.___", state 460, "else"
119 line 146, "pan.___", state 465, "((j<1))"
120 line 146, "pan.___", state 465, "((j>=1))"
121 line 152, "pan.___", state 471, "(1)"
122 line 152, "pan.___", state 472, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
123 line 152, "pan.___", state 472, "else"
124 line 154, "pan.___", state 475, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
125 line 154, "pan.___", state 475, "else"
126 line 186, "pan.___", state 477, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
127 line 186, "pan.___", state 477, "else"
128 line 289, "pan.___", state 492, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
129 line 298, "pan.___", state 524, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
130 line 299, "pan.___", state 537, "(1)"
131 line 308, "pan.___", state 567, "(1)"
132 line 289, "pan.___", state 580, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
133 line 298, "pan.___", state 612, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
134 line 299, "pan.___", state 625, "(1)"
135 line 308, "pan.___", state 655, "(1)"
136 line 289, "pan.___", state 668, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
137 line 298, "pan.___", state 700, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
138 line 299, "pan.___", state 713, "(1)"
139 line 308, "pan.___", state 743, "(1)"
140 line 159, "pan.___", state 758, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
141 line 159, "pan.___", state 760, "(1)"
142 line 163, "pan.___", state 767, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
143 line 163, "pan.___", state 769, "(1)"
144 line 163, "pan.___", state 770, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
145 line 163, "pan.___", state 770, "else"
146 line 161, "pan.___", state 775, "((j<1))"
147 line 161, "pan.___", state 775, "((j>=1))"
148 line 167, "pan.___", state 780, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
149 line 144, "pan.___", state 790, "(1)"
150 line 148, "pan.___", state 798, "(1)"
151 line 148, "pan.___", state 799, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
152 line 148, "pan.___", state 799, "else"
153 line 146, "pan.___", state 804, "((j<1))"
154 line 146, "pan.___", state 804, "((j>=1))"
155 line 152, "pan.___", state 810, "(1)"
156 line 152, "pan.___", state 811, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
157 line 152, "pan.___", state 811, "else"
158 line 154, "pan.___", state 814, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
159 line 154, "pan.___", state 814, "else"
160 line 186, "pan.___", state 816, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
161 line 186, "pan.___", state 816, "else"
162 line 159, "pan.___", state 821, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
163 line 159, "pan.___", state 823, "(1)"
164 line 163, "pan.___", state 830, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
165 line 163, "pan.___", state 832, "(1)"
166 line 163, "pan.___", state 833, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
167 line 163, "pan.___", state 833, "else"
168 line 161, "pan.___", state 838, "((j<1))"
169 line 161, "pan.___", state 838, "((j>=1))"
170 line 167, "pan.___", state 843, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
171 line 144, "pan.___", state 853, "(1)"
172 line 148, "pan.___", state 861, "(1)"
173 line 148, "pan.___", state 862, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
174 line 148, "pan.___", state 862, "else"
175 line 146, "pan.___", state 867, "((j<1))"
176 line 146, "pan.___", state 867, "((j>=1))"
177 line 152, "pan.___", state 873, "(1)"
178 line 152, "pan.___", state 874, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
179 line 152, "pan.___", state 874, "else"
180 line 154, "pan.___", state 877, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
181 line 154, "pan.___", state 877, "else"
182 line 186, "pan.___", state 879, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
183 line 186, "pan.___", state 879, "else"
184 line 200, "pan.___", state 883, "((i<1))"
185 line 200, "pan.___", state 883, "((i>=1))"
186 line 159, "pan.___", state 888, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
187 line 159, "pan.___", state 890, "(1)"
188 line 163, "pan.___", state 897, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
189 line 163, "pan.___", state 899, "(1)"
190 line 163, "pan.___", state 900, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
191 line 163, "pan.___", state 900, "else"
192 line 161, "pan.___", state 905, "((j<1))"
193 line 161, "pan.___", state 905, "((j>=1))"
194 line 167, "pan.___", state 910, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
195 line 144, "pan.___", state 920, "(1)"
196 line 148, "pan.___", state 928, "(1)"
197 line 148, "pan.___", state 929, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
198 line 148, "pan.___", state 929, "else"
199 line 146, "pan.___", state 934, "((j<1))"
200 line 146, "pan.___", state 934, "((j>=1))"
201 line 152, "pan.___", state 940, "(1)"
202 line 152, "pan.___", state 941, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
203 line 152, "pan.___", state 941, "else"
204 line 154, "pan.___", state 944, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
205 line 154, "pan.___", state 944, "else"
206 line 186, "pan.___", state 946, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
207 line 186, "pan.___", state 946, "else"
208 line 289, "pan.___", state 956, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
209 line 298, "pan.___", state 988, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
210 line 299, "pan.___", state 1001, "(1)"
211 line 308, "pan.___", state 1031, "(1)"
212 line 289, "pan.___", state 1052, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
213 line 298, "pan.___", state 1084, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
214 line 299, "pan.___", state 1097, "(1)"
215 line 308, "pan.___", state 1127, "(1)"
216 line 434, "pan.___", state 1140, "-end-"
217 (125 of 1140 states)
218unreached in proctype urcu_writer
219 line 289, "pan.___", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
220 line 293, "pan.___", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
221 line 298, "pan.___", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
222 line 299, "pan.___", state 59, "(1)"
223 line 303, "pan.___", state 72, "(1)"
224 line 308, "pan.___", state 89, "(1)"
225 line 289, "pan.___", state 106, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
226 line 293, "pan.___", state 120, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
227 line 299, "pan.___", state 151, "(1)"
228 line 303, "pan.___", state 164, "(1)"
229 line 468, "pan.___", state 195, "(1)"
230 line 159, "pan.___", state 205, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
231 line 163, "pan.___", state 214, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
232 line 144, "pan.___", state 237, "(1)"
233 line 148, "pan.___", state 245, "(1)"
234 line 152, "pan.___", state 257, "(1)"
235 line 159, "pan.___", state 268, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
236 line 167, "pan.___", state 290, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
237 line 144, "pan.___", state 300, "(1)"
238 line 148, "pan.___", state 308, "(1)"
239 line 152, "pan.___", state 320, "(1)"
240 line 159, "pan.___", state 335, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
241 line 163, "pan.___", state 344, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
242 line 167, "pan.___", state 357, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
243 line 144, "pan.___", state 367, "(1)"
244 line 148, "pan.___", state 375, "(1)"
245 line 152, "pan.___", state 387, "(1)"
246 line 289, "pan.___", state 403, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
247 line 293, "pan.___", state 417, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
248 line 298, "pan.___", state 435, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
249 line 299, "pan.___", state 448, "(1)"
250 line 303, "pan.___", state 461, "(1)"
251 line 308, "pan.___", state 478, "(1)"
252 line 289, "pan.___", state 495, "(1)"
253 line 293, "pan.___", state 507, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
254 line 298, "pan.___", state 525, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
255 line 303, "pan.___", state 551, "(1)"
256 line 308, "pan.___", state 568, "(1)"
257 line 293, "pan.___", state 598, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
258 line 298, "pan.___", state 616, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
259 line 303, "pan.___", state 642, "(1)"
260 line 308, "pan.___", state 659, "(1)"
261 line 163, "pan.___", state 681, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
262 line 167, "pan.___", state 694, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
263 line 144, "pan.___", state 704, "(1)"
264 line 148, "pan.___", state 712, "(1)"
265 line 152, "pan.___", state 724, "(1)"
266 line 159, "pan.___", state 735, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
267 line 167, "pan.___", state 757, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
268 line 144, "pan.___", state 767, "(1)"
269 line 148, "pan.___", state 775, "(1)"
270 line 152, "pan.___", state 787, "(1)"
271 line 159, "pan.___", state 802, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
272 line 163, "pan.___", state 811, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
273 line 167, "pan.___", state 824, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
274 line 144, "pan.___", state 834, "(1)"
275 line 148, "pan.___", state 842, "(1)"
276 line 152, "pan.___", state 854, "(1)"
277 line 289, "pan.___", state 878, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
278 line 289, "pan.___", state 880, "(1)"
279 line 289, "pan.___", state 881, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
280 line 289, "pan.___", state 881, "else"
281 line 289, "pan.___", state 884, "(1)"
282 line 293, "pan.___", state 892, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
283 line 293, "pan.___", state 894, "(1)"
284 line 293, "pan.___", state 895, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
285 line 293, "pan.___", state 895, "else"
286 line 293, "pan.___", state 898, "(1)"
287 line 293, "pan.___", state 899, "(1)"
288 line 293, "pan.___", state 899, "(1)"
289 line 291, "pan.___", state 904, "((i<1))"
290 line 291, "pan.___", state 904, "((i>=1))"
291 line 298, "pan.___", state 910, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
292 line 299, "pan.___", state 923, "(1)"
293 line 299, "pan.___", state 924, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
294 line 299, "pan.___", state 924, "else"
295 line 299, "pan.___", state 927, "(1)"
296 line 299, "pan.___", state 928, "(1)"
297 line 299, "pan.___", state 928, "(1)"
298 line 303, "pan.___", state 936, "(1)"
299 line 303, "pan.___", state 937, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
300 line 303, "pan.___", state 937, "else"
301 line 303, "pan.___", state 940, "(1)"
302 line 303, "pan.___", state 941, "(1)"
303 line 303, "pan.___", state 941, "(1)"
304 line 301, "pan.___", state 946, "((i<1))"
305 line 301, "pan.___", state 946, "((i>=1))"
306 line 308, "pan.___", state 953, "(1)"
307 line 308, "pan.___", state 954, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
308 line 308, "pan.___", state 954, "else"
309 line 308, "pan.___", state 957, "(1)"
310 line 308, "pan.___", state 958, "(1)"
311 line 308, "pan.___", state 958, "(1)"
312 line 310, "pan.___", state 961, "(1)"
313 line 310, "pan.___", state 961, "(1)"
314 line 163, "pan.___", state 985, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
315 line 167, "pan.___", state 998, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
316 line 144, "pan.___", state 1008, "(1)"
317 line 148, "pan.___", state 1016, "(1)"
318 line 152, "pan.___", state 1028, "(1)"
319 line 159, "pan.___", state 1039, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
320 line 167, "pan.___", state 1061, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
321 line 144, "pan.___", state 1071, "(1)"
322 line 148, "pan.___", state 1079, "(1)"
323 line 152, "pan.___", state 1091, "(1)"
324 line 159, "pan.___", state 1106, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
325 line 163, "pan.___", state 1115, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
326 line 167, "pan.___", state 1128, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
327 line 144, "pan.___", state 1138, "(1)"
328 line 148, "pan.___", state 1146, "(1)"
329 line 152, "pan.___", state 1158, "(1)"
330 line 511, "pan.___", state 1184, "-end-"
331 (100 of 1184 states)
332unreached in proctype :init:
333 line 518, "pan.___", state 9, "((j<2))"
334 line 518, "pan.___", state 9, "((j>=2))"
335 line 519, "pan.___", state 20, "((j<2))"
336 line 519, "pan.___", state 20, "((j>=2))"
337 line 524, "pan.___", state 33, "((j<2))"
338 line 524, "pan.___", state 33, "((j>=2))"
339 (3 of 46 states)
340unreached in proctype :never:
341 line 572, "pan.___", state 8, "-end-"
342 (1 of 8 states)
343
344pan: elapsed time 5.58 seconds
345pan: rate 38755.018 states/second
346pan: avg transition delay 1.7769e-06 usec
347cp .input.spin urcu_free_single_flip.spin.input
348cp .input.spin.trail urcu_free_single_flip.spin.input.trail
349make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu/testmerge'
Userspace RCU (urcu) for Linux
This page took 0.036645 seconds and 4 git commands to generate.