1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
2 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
3 cat DEFINES > .input.spin
4 cat urcu.spin >> .input.spin
5 rm -f .input.spin.trail
8 gcc -O2 -w -DHASH64 -DSAFETY -o pan pan.c
9 ./pan -v -c1 -X -m10000000 -w20
10 Depth= 4926 States= 1e+06 Transitions= 9.03e+06 Memory= 527.287 t= 5.98 R= 2e+05
11 Depth= 7228 States= 2e+06 Transitions= 1.88e+07 Memory= 588.322 t= 12.9 R= 2e+05
12 Depth= 7228 States= 3e+06 Transitions= 3.14e+07 Memory= 649.358 t= 21.9 R= 1e+05
13 pan: resizing hashtable to -w22.. done
14 Depth= 7228 States= 4e+06 Transitions= 4.3e+07 Memory= 741.416 t= 30.3 R= 1e+05
15 Depth= 7228 States= 5e+06 Transitions= 5.65e+07 Memory= 802.451 t= 39.6 R= 1e+05
16 Depth= 7228 States= 6e+06 Transitions= 6.78e+07 Memory= 863.486 t= 47.5 R= 1e+05
17 Depth= 7228 States= 7e+06 Transitions= 8.05e+07 Memory= 924.522 t= 56.5 R= 1e+05
18 Depth= 7228 States= 8e+06 Transitions= 9.49e+07 Memory= 985.557 t= 66.8 R= 1e+05
19 Depth= 7228 States= 9e+06 Transitions= 1.06e+08 Memory= 1046.592 t= 74.7 R= 1e+05
20 pan: resizing hashtable to -w24.. done
21 Depth= 7228 States= 1e+07 Transitions= 1.18e+08 Memory= 1231.721 t= 84.9 R= 1e+05
22 Depth= 7228 States= 1.1e+07 Transitions= 1.29e+08 Memory= 1292.756 t= 92.8 R= 1e+05
23 Depth= 7228 States= 1.2e+07 Transitions= 1.4e+08 Memory= 1353.791 t= 100 R= 1e+05
24 Depth= 7228 States= 1.3e+07 Transitions= 1.53e+08 Memory= 1414.826 t= 109 R= 1e+05
25 Depth= 7228 States= 1.4e+07 Transitions= 1.65e+08 Memory= 1475.861 t= 117 R= 1e+05
26 Depth= 7228 States= 1.5e+07 Transitions= 1.77e+08 Memory= 1536.897 t= 126 R= 1e+05
27 Depth= 7228 States= 1.6e+07 Transitions= 1.89e+08 Memory= 1597.932 t= 134 R= 1e+05
28 Depth= 7228 States= 1.7e+07 Transitions= 2.02e+08 Memory= 1658.967 t= 143 R= 1e+05
29 Depth= 7228 States= 1.8e+07 Transitions= 2.16e+08 Memory= 1720.002 t= 153 R= 1e+05
30 Depth= 7228 States= 1.9e+07 Transitions= 2.27e+08 Memory= 1781.037 t= 160 R= 1e+05
31 Depth= 7228 States= 2e+07 Transitions= 2.39e+08 Memory= 1842.072 t= 169 R= 1e+05
32 Depth= 7228 States= 2.1e+07 Transitions= 2.51e+08 Memory= 1903.108 t= 177 R= 1e+05
33 Depth= 7228 States= 2.2e+07 Transitions= 2.62e+08 Memory= 1964.143 t= 185 R= 1e+05
34 Depth= 7228 States= 2.3e+07 Transitions= 2.74e+08 Memory= 2025.178 t= 194 R= 1e+05
35 Depth= 7228 States= 2.4e+07 Transitions= 2.86e+08 Memory= 2086.213 t= 203 R= 1e+05
36 Depth= 7228 States= 2.5e+07 Transitions= 2.99e+08 Memory= 2147.248 t= 212 R= 1e+05
37 Depth= 7228 States= 2.6e+07 Transitions= 3.1e+08 Memory= 2208.283 t= 220 R= 1e+05
38 Depth= 7228 States= 2.7e+07 Transitions= 3.24e+08 Memory= 2269.318 t= 230 R= 1e+05
39 Depth= 7228 States= 2.8e+07 Transitions= 3.37e+08 Memory= 2330.354 t= 239 R= 1e+05
40 Depth= 7228 States= 2.9e+07 Transitions= 3.49e+08 Memory= 2391.389 t= 248 R= 1e+05
41 Depth= 7228 States= 3e+07 Transitions= 3.6e+08 Memory= 2452.424 t= 256 R= 1e+05
42 Depth= 7228 States= 3.1e+07 Transitions= 3.72e+08 Memory= 2513.459 t= 265 R= 1e+05
43 Depth= 7228 States= 3.2e+07 Transitions= 3.83e+08 Memory= 2574.494 t= 273 R= 1e+05
44 Depth= 7228 States= 3.3e+07 Transitions= 3.95e+08 Memory= 2635.529 t= 282 R= 1e+05
45 Depth= 7228 States= 3.4e+07 Transitions= 4.07e+08 Memory= 2696.565 t= 291 R= 1e+05
46 pan: resizing hashtable to -w26.. done
47 Depth= 7228 States= 3.5e+07 Transitions= 4.2e+08 Memory= 3253.682 t= 308 R= 1e+05
48 Depth= 7228 States= 3.6e+07 Transitions= 4.32e+08 Memory= 3314.717 t= 316 R= 1e+05
49 Depth= 7228 States= 3.7e+07 Transitions= 4.45e+08 Memory= 3375.752 t= 325 R= 1e+05
50 Depth= 7228 States= 3.8e+07 Transitions= 4.58e+08 Memory= 3436.787 t= 334 R= 1e+05
51 Depth= 7228 States= 3.9e+07 Transitions= 4.71e+08 Memory= 3497.822 t= 343 R= 1e+05
52 Depth= 7228 States= 4e+07 Transitions= 4.82e+08 Memory= 3558.858 t= 350 R= 1e+05
53 Depth= 7228 States= 4.1e+07 Transitions= 4.94e+08 Memory= 3619.893 t= 359 R= 1e+05
54 Depth= 7228 States= 4.2e+07 Transitions= 5.04e+08 Memory= 3680.928 t= 366 R= 1e+05
55 Depth= 7228 States= 4.3e+07 Transitions= 5.16e+08 Memory= 3741.963 t= 374 R= 1e+05
56 Depth= 7228 States= 4.4e+07 Transitions= 5.29e+08 Memory= 3802.998 t= 383 R= 1e+05
58 (Spin Version 5.1.7 -- 23 December 2008)
59 + Partial Order Reduction
61 Full statespace search for:
62 never claim - (none specified)
63 assertion violations +
64 cycle checks - (disabled by -DSAFETY)
67 State-vector 56 byte, depth reached 7228, errors: 0
68 44157204 states, stored
69 4.8641845e+08 states, matched
70 5.3057565e+08 transitions (= stored+matched)
71 1.8453582e+09 atomic steps
72 hash conflicts: 2.8837553e+08 (resolved)
74 Stats on memory usage (in Megabytes):
75 3537.374 equivalent memory usage for states (stored*(State-vector + overhead))
76 2843.050 actual memory usage for states (compression: 80.37%)
77 state-vector as stored = 40 byte + 28 byte overhead
78 512.000 memory used for hash table (-w26)
79 457.764 memory used for DFS stack (-m10000000)
80 3812.568 total actual memory usage
82 unreached in proctype urcu_reader
83 line 398, ".input.spin", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
84 line 407, ".input.spin", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
85 line 408, ".input.spin", state 61, "(1)"
86 line 417, ".input.spin", state 91, "(1)"
87 line 398, ".input.spin", state 113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
88 line 407, ".input.spin", state 145, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
89 line 408, ".input.spin", state 158, "(1)"
90 line 417, ".input.spin", state 188, "(1)"
91 line 398, ".input.spin", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
92 line 407, ".input.spin", state 243, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
93 line 408, ".input.spin", state 256, "(1)"
94 line 417, ".input.spin", state 286, "(1)"
95 line 398, ".input.spin", state 350, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
96 line 407, ".input.spin", state 382, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
97 line 408, ".input.spin", state 395, "(1)"
98 line 417, ".input.spin", state 425, "(1)"
99 line 539, ".input.spin", state 456, "-end-"
101 unreached in proctype urcu_reader_sig
102 line 398, ".input.spin", state 25, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
103 line 407, ".input.spin", state 57, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
104 line 408, ".input.spin", state 70, "(1)"
105 line 417, ".input.spin", state 100, "(1)"
106 line 398, ".input.spin", state 113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
107 line 407, ".input.spin", state 145, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
108 line 408, ".input.spin", state 158, "(1)"
109 line 417, ".input.spin", state 188, "(1)"
110 line 398, ".input.spin", state 202, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
111 line 407, ".input.spin", state 234, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
112 line 408, ".input.spin", state 247, "(1)"
113 line 417, ".input.spin", state 277, "(1)"
114 line 398, ".input.spin", state 314, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
115 line 407, ".input.spin", state 346, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
116 line 408, ".input.spin", state 359, "(1)"
117 line 417, ".input.spin", state 389, "(1)"
118 line 613, ".input.spin", state 411, "-end-"
120 unreached in proctype urcu_writer
121 line 398, ".input.spin", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
122 line 402, ".input.spin", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
123 line 407, ".input.spin", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
124 line 408, ".input.spin", state 59, "(1)"
125 line 412, ".input.spin", state 72, "(1)"
126 line 417, ".input.spin", state 89, "(1)"
127 line 398, ".input.spin", state 108, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
128 line 402, ".input.spin", state 122, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
129 line 408, ".input.spin", state 153, "(1)"
130 line 412, ".input.spin", state 166, "(1)"
131 line 651, ".input.spin", state 199, "(1)"
132 line 174, ".input.spin", state 208, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
133 line 178, ".input.spin", state 217, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
134 line 159, ".input.spin", state 240, "(1)"
135 line 163, ".input.spin", state 248, "(1)"
136 line 167, ".input.spin", state 260, "(1)"
137 line 174, ".input.spin", state 271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
138 line 182, ".input.spin", state 293, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
139 line 159, ".input.spin", state 303, "(1)"
140 line 163, ".input.spin", state 311, "(1)"
141 line 167, ".input.spin", state 323, "(1)"
142 line 174, ".input.spin", state 338, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
143 line 178, ".input.spin", state 347, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
144 line 182, ".input.spin", state 360, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
145 line 159, ".input.spin", state 370, "(1)"
146 line 163, ".input.spin", state 378, "(1)"
147 line 167, ".input.spin", state 390, "(1)"
148 line 398, ".input.spin", state 404, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
149 line 402, ".input.spin", state 418, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
150 line 407, ".input.spin", state 436, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
151 line 408, ".input.spin", state 449, "(1)"
152 line 412, ".input.spin", state 462, "(1)"
153 line 417, ".input.spin", state 479, "(1)"
154 line 398, ".input.spin", state 498, "(1)"
155 line 402, ".input.spin", state 510, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
156 line 407, ".input.spin", state 528, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
157 line 412, ".input.spin", state 554, "(1)"
158 line 417, ".input.spin", state 571, "(1)"
159 line 402, ".input.spin", state 603, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
160 line 407, ".input.spin", state 621, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
161 line 412, ".input.spin", state 647, "(1)"
162 line 417, ".input.spin", state 664, "(1)"
163 line 178, ".input.spin", state 687, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
164 line 182, ".input.spin", state 700, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
165 line 159, ".input.spin", state 710, "(1)"
166 line 163, ".input.spin", state 718, "(1)"
167 line 167, ".input.spin", state 730, "(1)"
168 line 174, ".input.spin", state 741, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
169 line 182, ".input.spin", state 763, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
170 line 159, ".input.spin", state 773, "(1)"
171 line 163, ".input.spin", state 781, "(1)"
172 line 167, ".input.spin", state 793, "(1)"
173 line 174, ".input.spin", state 808, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
174 line 178, ".input.spin", state 817, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
175 line 182, ".input.spin", state 830, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
176 line 159, ".input.spin", state 840, "(1)"
177 line 163, ".input.spin", state 848, "(1)"
178 line 167, ".input.spin", state 860, "(1)"
179 line 398, ".input.spin", state 882, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
180 line 398, ".input.spin", state 884, "(1)"
181 line 398, ".input.spin", state 885, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
182 line 398, ".input.spin", state 885, "else"
183 line 398, ".input.spin", state 888, "(1)"
184 line 402, ".input.spin", state 896, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
185 line 402, ".input.spin", state 898, "(1)"
186 line 402, ".input.spin", state 899, "((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
187 line 402, ".input.spin", state 899, "else"
188 line 402, ".input.spin", state 902, "(1)"
189 line 402, ".input.spin", state 903, "(1)"
190 line 402, ".input.spin", state 903, "(1)"
191 line 400, ".input.spin", state 908, "((i<1))"
192 line 400, ".input.spin", state 908, "((i>=1))"
193 line 407, ".input.spin", state 914, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
194 line 408, ".input.spin", state 927, "(1)"
195 line 408, ".input.spin", state 928, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
196 line 408, ".input.spin", state 928, "else"
197 line 408, ".input.spin", state 931, "(1)"
198 line 408, ".input.spin", state 932, "(1)"
199 line 408, ".input.spin", state 932, "(1)"
200 line 412, ".input.spin", state 940, "(1)"
201 line 412, ".input.spin", state 941, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
202 line 412, ".input.spin", state 941, "else"
203 line 412, ".input.spin", state 944, "(1)"
204 line 412, ".input.spin", state 945, "(1)"
205 line 412, ".input.spin", state 945, "(1)"
206 line 410, ".input.spin", state 950, "((i<1))"
207 line 410, ".input.spin", state 950, "((i>=1))"
208 line 417, ".input.spin", state 957, "(1)"
209 line 417, ".input.spin", state 958, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
210 line 417, ".input.spin", state 958, "else"
211 line 417, ".input.spin", state 961, "(1)"
212 line 417, ".input.spin", state 962, "(1)"
213 line 417, ".input.spin", state 962, "(1)"
214 line 419, ".input.spin", state 965, "(1)"
215 line 419, ".input.spin", state 965, "(1)"
216 line 402, ".input.spin", state 996, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
217 line 407, ".input.spin", state 1014, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
218 line 412, ".input.spin", state 1040, "(1)"
219 line 417, ".input.spin", state 1057, "(1)"
220 line 402, ".input.spin", state 1086, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
221 line 407, ".input.spin", state 1104, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
222 line 412, ".input.spin", state 1130, "(1)"
223 line 417, ".input.spin", state 1147, "(1)"
224 line 398, ".input.spin", state 1166, "(1)"
225 line 402, ".input.spin", state 1178, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
226 line 407, ".input.spin", state 1196, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
227 line 412, ".input.spin", state 1222, "(1)"
228 line 417, ".input.spin", state 1239, "(1)"
229 line 402, ".input.spin", state 1271, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
230 line 407, ".input.spin", state 1289, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
231 line 412, ".input.spin", state 1315, "(1)"
232 line 417, ".input.spin", state 1332, "(1)"
233 line 178, ".input.spin", state 1355, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
234 line 182, ".input.spin", state 1368, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
235 line 159, ".input.spin", state 1378, "(1)"
236 line 163, ".input.spin", state 1386, "(1)"
237 line 167, ".input.spin", state 1398, "(1)"
238 line 174, ".input.spin", state 1409, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
239 line 182, ".input.spin", state 1431, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
240 line 159, ".input.spin", state 1441, "(1)"
241 line 163, ".input.spin", state 1449, "(1)"
242 line 167, ".input.spin", state 1461, "(1)"
243 line 174, ".input.spin", state 1476, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
244 line 178, ".input.spin", state 1485, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
245 line 182, ".input.spin", state 1498, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
246 line 159, ".input.spin", state 1508, "(1)"
247 line 163, ".input.spin", state 1516, "(1)"
248 line 167, ".input.spin", state 1528, "(1)"
249 line 398, ".input.spin", state 1550, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
250 line 398, ".input.spin", state 1552, "(1)"
251 line 398, ".input.spin", state 1553, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
252 line 398, ".input.spin", state 1553, "else"
253 line 398, ".input.spin", state 1556, "(1)"
254 line 402, ".input.spin", state 1564, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
255 line 402, ".input.spin", state 1566, "(1)"
256 line 402, ".input.spin", state 1567, "((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
257 line 402, ".input.spin", state 1567, "else"
258 line 402, ".input.spin", state 1570, "(1)"
259 line 402, ".input.spin", state 1571, "(1)"
260 line 402, ".input.spin", state 1571, "(1)"
261 line 400, ".input.spin", state 1576, "((i<1))"
262 line 400, ".input.spin", state 1576, "((i>=1))"
263 line 407, ".input.spin", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
264 line 408, ".input.spin", state 1595, "(1)"
265 line 408, ".input.spin", state 1596, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
266 line 408, ".input.spin", state 1596, "else"
267 line 408, ".input.spin", state 1599, "(1)"
268 line 408, ".input.spin", state 1600, "(1)"
269 line 408, ".input.spin", state 1600, "(1)"
270 line 412, ".input.spin", state 1608, "(1)"
271 line 412, ".input.spin", state 1609, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
272 line 412, ".input.spin", state 1609, "else"
273 line 412, ".input.spin", state 1612, "(1)"
274 line 412, ".input.spin", state 1613, "(1)"
275 line 412, ".input.spin", state 1613, "(1)"
276 line 410, ".input.spin", state 1618, "((i<1))"
277 line 410, ".input.spin", state 1618, "((i>=1))"
278 line 417, ".input.spin", state 1625, "(1)"
279 line 417, ".input.spin", state 1626, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
280 line 417, ".input.spin", state 1626, "else"
281 line 417, ".input.spin", state 1629, "(1)"
282 line 417, ".input.spin", state 1630, "(1)"
283 line 417, ".input.spin", state 1630, "(1)"
284 line 419, ".input.spin", state 1633, "(1)"
285 line 419, ".input.spin", state 1633, "(1)"
286 line 178, ".input.spin", state 1658, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
287 line 182, ".input.spin", state 1671, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
288 line 159, ".input.spin", state 1681, "(1)"
289 line 163, ".input.spin", state 1689, "(1)"
290 line 167, ".input.spin", state 1701, "(1)"
291 line 174, ".input.spin", state 1712, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
292 line 182, ".input.spin", state 1734, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
293 line 159, ".input.spin", state 1744, "(1)"
294 line 163, ".input.spin", state 1752, "(1)"
295 line 167, ".input.spin", state 1764, "(1)"
296 line 174, ".input.spin", state 1779, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
297 line 178, ".input.spin", state 1788, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
298 line 182, ".input.spin", state 1801, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
299 line 159, ".input.spin", state 1811, "(1)"
300 line 163, ".input.spin", state 1819, "(1)"
301 line 167, ".input.spin", state 1831, "(1)"
302 line 701, ".input.spin", state 1856, "-end-"
304 unreached in proctype :init:
307 pan: elapsed time 384 seconds
308 pan: rate 114968.77 states/second
309 pan: avg transition delay 7.2389e-07 usec
310 cp .input.spin asserts.spin.input
311 cp .input.spin.trail asserts.spin.input.trail
312 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
projects / urcu.git / blob