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 / result-standard-execution-nest / asserts.log
CommitLineData
8baf2c95
MD		 1make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
2rm -f pan* trail.out .input.spin* *.spin.trail .input.define
3cat DEFINES > .input.spin
4cat urcu.spin >> .input.spin
5rm -f .input.spin.trail
6spin -a -X .input.spin
7Exit-Status 0
8gcc -O2 -w -DHASH64 -DSAFETY -o pan pan.c
9./pan -v -c1 -X -m10000000 -w20
10Depth= 3212 States= 1e+06 Transitions= 1.17e+07 Memory= 519.572 t= 7.66 R= 1e+05
11Depth= 3212 States= 2e+06 Transitions= 2.38e+07 Memory= 572.990 t= 16 R= 1e+05
12Depth= 3212 States= 3e+06 Transitions= 3.62e+07 Memory= 626.408 t= 24.9 R= 1e+05
13pan: resizing hashtable to -w22.. done
14
15(Spin Version 5.1.7 -- 23 December 2008)
16 + Partial Order Reduction
17
18Full statespace search for:
19 never claim - (none specified)
20 assertion violations +
21 cycle checks - (disabled by -DSAFETY)
22 invalid end states +
23
24State-vector 48 byte, depth reached 3212, errors: 0
25 3539988 states, stored
26 39085459 states, matched
27 42625447 transitions (= stored+matched)
281.5602888e+08 atomic steps
29hash conflicts: 28971442 (resolved)
30
31Stats on memory usage (in Megabytes):
32 256.576 equivalent memory usage for states (stored*(State-vector + overhead))
33 196.718 actual memory usage for states (compression: 76.67%)
34 state-vector as stored = 30 byte + 28 byte overhead
35 32.000 memory used for hash table (-w22)
36 457.764 memory used for DFS stack (-m10000000)
37 686.338 total actual memory usage
38
39unreached in proctype urcu_reader
40 line 398, ".input.spin", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
41 line 407, ".input.spin", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
42 line 408, ".input.spin", state 61, "(1)"
43 line 417, ".input.spin", state 91, "(1)"
44 line 398, ".input.spin", state 106, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
45 line 407, ".input.spin", state 138, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
46 line 408, ".input.spin", state 151, "(1)"
47 line 417, ".input.spin", state 181, "(1)"
48 line 398, ".input.spin", state 197, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
49 line 407, ".input.spin", state 229, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
50 line 408, ".input.spin", state 242, "(1)"
51 line 417, ".input.spin", state 272, "(1)"
52 line 398, ".input.spin", state 315, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
53 line 407, ".input.spin", state 347, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
54 line 408, ".input.spin", state 360, "(1)"
55 line 417, ".input.spin", state 390, "(1)"
56 line 539, ".input.spin", state 414, "-end-"
57 (17 of 414 states)
58unreached in proctype urcu_writer
59 line 398, ".input.spin", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
60 line 402, ".input.spin", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
61 line 407, ".input.spin", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
62 line 408, ".input.spin", state 59, "(1)"
63 line 412, ".input.spin", state 72, "(1)"
64 line 417, ".input.spin", state 89, "(1)"
65 line 398, ".input.spin", state 108, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
66 line 402, ".input.spin", state 122, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
67 line 408, ".input.spin", state 153, "(1)"
68 line 412, ".input.spin", state 166, "(1)"
69 line 651, ".input.spin", state 199, "(1)"
70 line 174, ".input.spin", state 208, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
71 line 178, ".input.spin", state 217, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
72 line 159, ".input.spin", state 240, "(1)"
73 line 163, ".input.spin", state 248, "(1)"
74 line 167, ".input.spin", state 260, "(1)"
75 line 174, ".input.spin", state 271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
76 line 182, ".input.spin", state 293, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
77 line 159, ".input.spin", state 303, "(1)"
78 line 163, ".input.spin", state 311, "(1)"
79 line 167, ".input.spin", state 323, "(1)"
80 line 174, ".input.spin", state 338, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
81 line 178, ".input.spin", state 347, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
82 line 182, ".input.spin", state 360, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
83 line 159, ".input.spin", state 370, "(1)"
84 line 163, ".input.spin", state 378, "(1)"
85 line 167, ".input.spin", state 390, "(1)"
86 line 398, ".input.spin", state 404, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
87 line 402, ".input.spin", state 418, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
88 line 407, ".input.spin", state 436, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
89 line 408, ".input.spin", state 449, "(1)"
90 line 412, ".input.spin", state 462, "(1)"
91 line 417, ".input.spin", state 479, "(1)"
92 line 398, ".input.spin", state 498, "(1)"
93 line 402, ".input.spin", state 510, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
94 line 407, ".input.spin", state 528, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
95 line 412, ".input.spin", state 554, "(1)"
96 line 417, ".input.spin", state 571, "(1)"
97 line 402, ".input.spin", state 603, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
98 line 407, ".input.spin", state 621, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
99 line 412, ".input.spin", state 647, "(1)"
100 line 417, ".input.spin", state 664, "(1)"
101 line 178, ".input.spin", state 687, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
102 line 182, ".input.spin", state 700, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
103 line 159, ".input.spin", state 710, "(1)"
104 line 163, ".input.spin", state 718, "(1)"
105 line 167, ".input.spin", state 730, "(1)"
106 line 174, ".input.spin", state 741, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
107 line 182, ".input.spin", state 763, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
108 line 159, ".input.spin", state 773, "(1)"
109 line 163, ".input.spin", state 781, "(1)"
110 line 167, ".input.spin", state 793, "(1)"
111 line 174, ".input.spin", state 808, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
112 line 178, ".input.spin", state 817, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
113 line 182, ".input.spin", state 830, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
114 line 159, ".input.spin", state 840, "(1)"
115 line 163, ".input.spin", state 848, "(1)"
116 line 167, ".input.spin", state 860, "(1)"
117 line 398, ".input.spin", state 882, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
118 line 398, ".input.spin", state 884, "(1)"
119 line 398, ".input.spin", state 885, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
120 line 398, ".input.spin", state 885, "else"
121 line 398, ".input.spin", state 888, "(1)"
122 line 402, ".input.spin", state 896, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
123 line 402, ".input.spin", state 898, "(1)"
124 line 402, ".input.spin", state 899, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
125 line 402, ".input.spin", state 899, "else"
126 line 402, ".input.spin", state 902, "(1)"
127 line 402, ".input.spin", state 903, "(1)"
128 line 402, ".input.spin", state 903, "(1)"
129 line 400, ".input.spin", state 908, "((i<1))"
130 line 400, ".input.spin", state 908, "((i>=1))"
131 line 407, ".input.spin", state 914, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
132 line 408, ".input.spin", state 927, "(1)"
133 line 408, ".input.spin", state 928, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
134 line 408, ".input.spin", state 928, "else"
135 line 408, ".input.spin", state 931, "(1)"
136 line 408, ".input.spin", state 932, "(1)"
137 line 408, ".input.spin", state 932, "(1)"
138 line 412, ".input.spin", state 940, "(1)"
139 line 412, ".input.spin", state 941, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
140 line 412, ".input.spin", state 941, "else"
141 line 412, ".input.spin", state 944, "(1)"
142 line 412, ".input.spin", state 945, "(1)"
143 line 412, ".input.spin", state 945, "(1)"
144 line 410, ".input.spin", state 950, "((i<1))"
145 line 410, ".input.spin", state 950, "((i>=1))"
146 line 417, ".input.spin", state 957, "(1)"
147 line 417, ".input.spin", state 958, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
148 line 417, ".input.spin", state 958, "else"
149 line 417, ".input.spin", state 961, "(1)"
150 line 417, ".input.spin", state 962, "(1)"
151 line 417, ".input.spin", state 962, "(1)"
152 line 419, ".input.spin", state 965, "(1)"
153 line 419, ".input.spin", state 965, "(1)"
154 line 402, ".input.spin", state 996, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
155 line 407, ".input.spin", state 1014, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
156 line 412, ".input.spin", state 1040, "(1)"
157 line 417, ".input.spin", state 1057, "(1)"
158 line 402, ".input.spin", state 1086, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
159 line 407, ".input.spin", state 1104, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
160 line 412, ".input.spin", state 1130, "(1)"
161 line 417, ".input.spin", state 1147, "(1)"
162 line 398, ".input.spin", state 1166, "(1)"
163 line 402, ".input.spin", state 1178, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
164 line 407, ".input.spin", state 1196, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
165 line 412, ".input.spin", state 1222, "(1)"
166 line 417, ".input.spin", state 1239, "(1)"
167 line 402, ".input.spin", state 1271, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
168 line 407, ".input.spin", state 1289, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
169 line 412, ".input.spin", state 1315, "(1)"
170 line 417, ".input.spin", state 1332, "(1)"
171 line 178, ".input.spin", state 1355, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
172 line 182, ".input.spin", state 1368, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
173 line 159, ".input.spin", state 1378, "(1)"
174 line 163, ".input.spin", state 1386, "(1)"
175 line 167, ".input.spin", state 1398, "(1)"
176 line 174, ".input.spin", state 1409, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
177 line 182, ".input.spin", state 1431, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
178 line 159, ".input.spin", state 1441, "(1)"
179 line 163, ".input.spin", state 1449, "(1)"
180 line 167, ".input.spin", state 1461, "(1)"
181 line 174, ".input.spin", state 1476, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
182 line 178, ".input.spin", state 1485, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
183 line 182, ".input.spin", state 1498, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
184 line 159, ".input.spin", state 1508, "(1)"
185 line 163, ".input.spin", state 1516, "(1)"
186 line 167, ".input.spin", state 1528, "(1)"
187 line 398, ".input.spin", state 1550, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
188 line 398, ".input.spin", state 1552, "(1)"
189 line 398, ".input.spin", state 1553, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
190 line 398, ".input.spin", state 1553, "else"
191 line 398, ".input.spin", state 1556, "(1)"
192 line 402, ".input.spin", state 1564, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
193 line 402, ".input.spin", state 1566, "(1)"
194 line 402, ".input.spin", state 1567, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
195 line 402, ".input.spin", state 1567, "else"
196 line 402, ".input.spin", state 1570, "(1)"
197 line 402, ".input.spin", state 1571, "(1)"
198 line 402, ".input.spin", state 1571, "(1)"
199 line 400, ".input.spin", state 1576, "((i<1))"
200 line 400, ".input.spin", state 1576, "((i>=1))"
201 line 407, ".input.spin", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
202 line 408, ".input.spin", state 1595, "(1)"
203 line 408, ".input.spin", state 1596, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
204 line 408, ".input.spin", state 1596, "else"
205 line 408, ".input.spin", state 1599, "(1)"
206 line 408, ".input.spin", state 1600, "(1)"
207 line 408, ".input.spin", state 1600, "(1)"
208 line 412, ".input.spin", state 1608, "(1)"
209 line 412, ".input.spin", state 1609, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
210 line 412, ".input.spin", state 1609, "else"
211 line 412, ".input.spin", state 1612, "(1)"
212 line 412, ".input.spin", state 1613, "(1)"
213 line 412, ".input.spin", state 1613, "(1)"
214 line 410, ".input.spin", state 1618, "((i<1))"
215 line 410, ".input.spin", state 1618, "((i>=1))"
216 line 417, ".input.spin", state 1625, "(1)"
217 line 417, ".input.spin", state 1626, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
218 line 417, ".input.spin", state 1626, "else"
219 line 417, ".input.spin", state 1629, "(1)"
220 line 417, ".input.spin", state 1630, "(1)"
221 line 417, ".input.spin", state 1630, "(1)"
222 line 419, ".input.spin", state 1633, "(1)"
223 line 419, ".input.spin", state 1633, "(1)"
224 line 178, ".input.spin", state 1658, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
225 line 182, ".input.spin", state 1671, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
226 line 159, ".input.spin", state 1681, "(1)"
227 line 163, ".input.spin", state 1689, "(1)"
228 line 167, ".input.spin", state 1701, "(1)"
229 line 174, ".input.spin", state 1712, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
230 line 182, ".input.spin", state 1734, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
231 line 159, ".input.spin", state 1744, "(1)"
232 line 163, ".input.spin", state 1752, "(1)"
233 line 167, ".input.spin", state 1764, "(1)"
234 line 174, ".input.spin", state 1779, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
235 line 178, ".input.spin", state 1788, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
236 line 182, ".input.spin", state 1801, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
237 line 159, ".input.spin", state 1811, "(1)"
238 line 163, ".input.spin", state 1819, "(1)"
239 line 167, ".input.spin", state 1831, "(1)"
240 line 701, ".input.spin", state 1856, "-end-"
241 (158 of 1856 states)
242unreached in proctype :init:
243 (0 of 46 states)
244
245pan: elapsed time 29.8 seconds
246pan: rate 118871.32 states/second
247pan: avg transition delay 6.9864e-07 usec
248cp .input.spin asserts.spin.input
249cp .input.spin.trail asserts.spin.input.trail
250make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
Userspace RCU (urcu) for Linux
This page took 0.032424 seconds and 4 git commands to generate.