make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu' rm -f pan* trail.out .input.spin* *.spin.trail .input.define cat DEFINES > .input.spin cat urcu.spin >> .input.spin rm -f .input.spin.trail spin -a -X .input.spin Exit-Status 0 gcc -O2 -w -DHASH64 -DSAFETY -o pan pan.c ./pan -v -c1 -X -m10000000 -w20 Depth= 4926 States= 1e+06 Transitions= 9.03e+06 Memory= 527.287 t= 5.98 R= 2e+05 Depth= 7228 States= 2e+06 Transitions= 1.88e+07 Memory= 588.322 t= 12.9 R= 2e+05 Depth= 7228 States= 3e+06 Transitions= 3.14e+07 Memory= 649.358 t= 21.9 R= 1e+05 pan: resizing hashtable to -w22.. done Depth= 7228 States= 4e+06 Transitions= 4.3e+07 Memory= 741.416 t= 30.3 R= 1e+05 Depth= 7228 States= 5e+06 Transitions= 5.65e+07 Memory= 802.451 t= 39.6 R= 1e+05 Depth= 7228 States= 6e+06 Transitions= 6.78e+07 Memory= 863.486 t= 47.5 R= 1e+05 Depth= 7228 States= 7e+06 Transitions= 8.05e+07 Memory= 924.522 t= 56.5 R= 1e+05 Depth= 7228 States= 8e+06 Transitions= 9.49e+07 Memory= 985.557 t= 66.8 R= 1e+05 Depth= 7228 States= 9e+06 Transitions= 1.06e+08 Memory= 1046.592 t= 74.7 R= 1e+05 pan: resizing hashtable to -w24.. done Depth= 7228 States= 1e+07 Transitions= 1.18e+08 Memory= 1231.721 t= 84.9 R= 1e+05 Depth= 7228 States= 1.1e+07 Transitions= 1.29e+08 Memory= 1292.756 t= 92.8 R= 1e+05 Depth= 7228 States= 1.2e+07 Transitions= 1.4e+08 Memory= 1353.791 t= 100 R= 1e+05 Depth= 7228 States= 1.3e+07 Transitions= 1.53e+08 Memory= 1414.826 t= 109 R= 1e+05 Depth= 7228 States= 1.4e+07 Transitions= 1.65e+08 Memory= 1475.861 t= 117 R= 1e+05 Depth= 7228 States= 1.5e+07 Transitions= 1.77e+08 Memory= 1536.897 t= 126 R= 1e+05 Depth= 7228 States= 1.6e+07 Transitions= 1.89e+08 Memory= 1597.932 t= 134 R= 1e+05 Depth= 7228 States= 1.7e+07 Transitions= 2.02e+08 Memory= 1658.967 t= 143 R= 1e+05 Depth= 7228 States= 1.8e+07 Transitions= 2.16e+08 Memory= 1720.002 t= 153 R= 1e+05 Depth= 7228 States= 1.9e+07 Transitions= 2.27e+08 Memory= 1781.037 t= 160 R= 1e+05 Depth= 7228 States= 2e+07 Transitions= 2.39e+08 Memory= 1842.072 t= 169 R= 1e+05 Depth= 7228 States= 2.1e+07 Transitions= 2.51e+08 Memory= 1903.108 t= 177 R= 1e+05 Depth= 7228 States= 2.2e+07 Transitions= 2.62e+08 Memory= 1964.143 t= 185 R= 1e+05 Depth= 7228 States= 2.3e+07 Transitions= 2.74e+08 Memory= 2025.178 t= 194 R= 1e+05 Depth= 7228 States= 2.4e+07 Transitions= 2.86e+08 Memory= 2086.213 t= 203 R= 1e+05 Depth= 7228 States= 2.5e+07 Transitions= 2.99e+08 Memory= 2147.248 t= 212 R= 1e+05 Depth= 7228 States= 2.6e+07 Transitions= 3.1e+08 Memory= 2208.283 t= 220 R= 1e+05 Depth= 7228 States= 2.7e+07 Transitions= 3.24e+08 Memory= 2269.318 t= 230 R= 1e+05 Depth= 7228 States= 2.8e+07 Transitions= 3.37e+08 Memory= 2330.354 t= 239 R= 1e+05 Depth= 7228 States= 2.9e+07 Transitions= 3.49e+08 Memory= 2391.389 t= 248 R= 1e+05 Depth= 7228 States= 3e+07 Transitions= 3.6e+08 Memory= 2452.424 t= 256 R= 1e+05 Depth= 7228 States= 3.1e+07 Transitions= 3.72e+08 Memory= 2513.459 t= 265 R= 1e+05 Depth= 7228 States= 3.2e+07 Transitions= 3.83e+08 Memory= 2574.494 t= 273 R= 1e+05 Depth= 7228 States= 3.3e+07 Transitions= 3.95e+08 Memory= 2635.529 t= 282 R= 1e+05 Depth= 7228 States= 3.4e+07 Transitions= 4.07e+08 Memory= 2696.565 t= 291 R= 1e+05 pan: resizing hashtable to -w26.. done Depth= 7228 States= 3.5e+07 Transitions= 4.2e+08 Memory= 3253.682 t= 308 R= 1e+05 Depth= 7228 States= 3.6e+07 Transitions= 4.32e+08 Memory= 3314.717 t= 316 R= 1e+05 Depth= 7228 States= 3.7e+07 Transitions= 4.45e+08 Memory= 3375.752 t= 325 R= 1e+05 Depth= 7228 States= 3.8e+07 Transitions= 4.58e+08 Memory= 3436.787 t= 334 R= 1e+05 Depth= 7228 States= 3.9e+07 Transitions= 4.71e+08 Memory= 3497.822 t= 343 R= 1e+05 Depth= 7228 States= 4e+07 Transitions= 4.82e+08 Memory= 3558.858 t= 350 R= 1e+05 Depth= 7228 States= 4.1e+07 Transitions= 4.94e+08 Memory= 3619.893 t= 359 R= 1e+05 Depth= 7228 States= 4.2e+07 Transitions= 5.04e+08 Memory= 3680.928 t= 366 R= 1e+05 Depth= 7228 States= 4.3e+07 Transitions= 5.16e+08 Memory= 3741.963 t= 374 R= 1e+05 Depth= 7228 States= 4.4e+07 Transitions= 5.29e+08 Memory= 3802.998 t= 383 R= 1e+05 (Spin Version 5.1.7 -- 23 December 2008) + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 56 byte, depth reached 7228, errors: 0 44157204 states, stored 4.8641845e+08 states, matched 5.3057565e+08 transitions (= stored+matched) 1.8453582e+09 atomic steps hash conflicts: 2.8837553e+08 (resolved) Stats on memory usage (in Megabytes): 3537.374 equivalent memory usage for states (stored*(State-vector + overhead)) 2843.050 actual memory usage for states (compression: 80.37%) state-vector as stored = 40 byte + 28 byte overhead 512.000 memory used for hash table (-w26) 457.764 memory used for DFS stack (-m10000000) 3812.568 total actual memory usage unreached in proctype urcu_reader line 398, ".input.spin", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 61, "(1)" line 417, ".input.spin", state 91, "(1)" line 398, ".input.spin", state 113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 145, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 158, "(1)" line 417, ".input.spin", state 188, "(1)" line 398, ".input.spin", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 243, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 256, "(1)" line 417, ".input.spin", state 286, "(1)" line 398, ".input.spin", state 350, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 382, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 395, "(1)" line 417, ".input.spin", state 425, "(1)" line 539, ".input.spin", state 456, "-end-" (17 of 456 states) unreached in proctype urcu_reader_sig line 398, ".input.spin", state 25, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 57, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 70, "(1)" line 417, ".input.spin", state 100, "(1)" line 398, ".input.spin", state 113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 145, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 158, "(1)" line 417, ".input.spin", state 188, "(1)" line 398, ".input.spin", state 202, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 234, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 247, "(1)" line 417, ".input.spin", state 277, "(1)" line 398, ".input.spin", state 314, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 346, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 359, "(1)" line 417, ".input.spin", state 389, "(1)" line 613, ".input.spin", state 411, "-end-" (17 of 411 states) unreached in proctype urcu_writer line 398, ".input.spin", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 402, ".input.spin", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 59, "(1)" line 412, ".input.spin", state 72, "(1)" line 417, ".input.spin", state 89, "(1)" line 398, ".input.spin", state 108, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 402, ".input.spin", state 122, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 153, "(1)" line 412, ".input.spin", state 166, "(1)" line 651, ".input.spin", state 199, "(1)" line 174, ".input.spin", state 208, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 178, ".input.spin", state 217, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 159, ".input.spin", state 240, "(1)" line 163, ".input.spin", state 248, "(1)" line 167, ".input.spin", state 260, "(1)" line 174, ".input.spin", state 271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1< (0) : (1) ))))" line 178, ".input.spin", state 347, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 182, ".input.spin", state 360, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 159, ".input.spin", state 370, "(1)" line 163, ".input.spin", state 378, "(1)" line 167, ".input.spin", state 390, "(1)" line 398, ".input.spin", state 404, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 402, ".input.spin", state 418, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 436, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 449, "(1)" line 412, ".input.spin", state 462, "(1)" line 417, ".input.spin", state 479, "(1)" line 398, ".input.spin", state 498, "(1)" line 402, ".input.spin", state 510, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 528, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 412, ".input.spin", state 554, "(1)" line 417, ".input.spin", state 571, "(1)" line 402, ".input.spin", state 603, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 621, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 412, ".input.spin", state 647, "(1)" line 417, ".input.spin", state 664, "(1)" line 178, ".input.spin", state 687, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 182, ".input.spin", state 700, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 159, ".input.spin", state 710, "(1)" line 163, ".input.spin", state 718, "(1)" line 167, ".input.spin", state 730, "(1)" line 174, ".input.spin", state 741, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1< (0) : (1) ))))" line 178, ".input.spin", state 817, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 182, ".input.spin", state 830, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 159, ".input.spin", state 840, "(1)" line 163, ".input.spin", state 848, "(1)" line 167, ".input.spin", state 860, "(1)" line 398, ".input.spin", state 882, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 398, ".input.spin", state 884, "(1)" line 398, ".input.spin", state 885, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))" line 398, ".input.spin", state 885, "else" line 398, ".input.spin", state 888, "(1)" line 402, ".input.spin", state 896, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 402, ".input.spin", state 898, "(1)" line 402, ".input.spin", state 899, "((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))" line 402, ".input.spin", state 899, "else" line 402, ".input.spin", state 902, "(1)" line 402, ".input.spin", state 903, "(1)" line 402, ".input.spin", state 903, "(1)" line 400, ".input.spin", state 908, "((i<1))" line 400, ".input.spin", state 908, "((i>=1))" line 407, ".input.spin", state 914, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 927, "(1)" line 408, ".input.spin", state 928, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))" line 408, ".input.spin", state 928, "else" line 408, ".input.spin", state 931, "(1)" line 408, ".input.spin", state 932, "(1)" line 408, ".input.spin", state 932, "(1)" line 412, ".input.spin", state 940, "(1)" line 412, ".input.spin", state 941, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))" line 412, ".input.spin", state 941, "else" line 412, ".input.spin", state 944, "(1)" line 412, ".input.spin", state 945, "(1)" line 412, ".input.spin", state 945, "(1)" line 410, ".input.spin", state 950, "((i<1))" line 410, ".input.spin", state 950, "((i>=1))" line 417, ".input.spin", state 957, "(1)" line 417, ".input.spin", state 958, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))" line 417, ".input.spin", state 958, "else" line 417, ".input.spin", state 961, "(1)" line 417, ".input.spin", state 962, "(1)" line 417, ".input.spin", state 962, "(1)" line 419, ".input.spin", state 965, "(1)" line 419, ".input.spin", state 965, "(1)" line 402, ".input.spin", state 996, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 1014, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 412, ".input.spin", state 1040, "(1)" line 417, ".input.spin", state 1057, "(1)" line 402, ".input.spin", state 1086, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 1104, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 412, ".input.spin", state 1130, "(1)" line 417, ".input.spin", state 1147, "(1)" line 398, ".input.spin", state 1166, "(1)" line 402, ".input.spin", state 1178, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 1196, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 412, ".input.spin", state 1222, "(1)" line 417, ".input.spin", state 1239, "(1)" line 402, ".input.spin", state 1271, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 407, ".input.spin", state 1289, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 412, ".input.spin", state 1315, "(1)" line 417, ".input.spin", state 1332, "(1)" line 178, ".input.spin", state 1355, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 182, ".input.spin", state 1368, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 159, ".input.spin", state 1378, "(1)" line 163, ".input.spin", state 1386, "(1)" line 167, ".input.spin", state 1398, "(1)" line 174, ".input.spin", state 1409, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1< (0) : (1) ))))" line 178, ".input.spin", state 1485, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 182, ".input.spin", state 1498, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 159, ".input.spin", state 1508, "(1)" line 163, ".input.spin", state 1516, "(1)" line 167, ".input.spin", state 1528, "(1)" line 398, ".input.spin", state 1550, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 398, ".input.spin", state 1552, "(1)" line 398, ".input.spin", state 1553, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))" line 398, ".input.spin", state 1553, "else" line 398, ".input.spin", state 1556, "(1)" line 402, ".input.spin", state 1564, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 402, ".input.spin", state 1566, "(1)" line 402, ".input.spin", state 1567, "((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))" line 402, ".input.spin", state 1567, "else" line 402, ".input.spin", state 1570, "(1)" line 402, ".input.spin", state 1571, "(1)" line 402, ".input.spin", state 1571, "(1)" line 400, ".input.spin", state 1576, "((i<1))" line 400, ".input.spin", state 1576, "((i>=1))" line 407, ".input.spin", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 408, ".input.spin", state 1595, "(1)" line 408, ".input.spin", state 1596, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))" line 408, ".input.spin", state 1596, "else" line 408, ".input.spin", state 1599, "(1)" line 408, ".input.spin", state 1600, "(1)" line 408, ".input.spin", state 1600, "(1)" line 412, ".input.spin", state 1608, "(1)" line 412, ".input.spin", state 1609, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))" line 412, ".input.spin", state 1609, "else" line 412, ".input.spin", state 1612, "(1)" line 412, ".input.spin", state 1613, "(1)" line 412, ".input.spin", state 1613, "(1)" line 410, ".input.spin", state 1618, "((i<1))" line 410, ".input.spin", state 1618, "((i>=1))" line 417, ".input.spin", state 1625, "(1)" line 417, ".input.spin", state 1626, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))" line 417, ".input.spin", state 1626, "else" line 417, ".input.spin", state 1629, "(1)" line 417, ".input.spin", state 1630, "(1)" line 417, ".input.spin", state 1630, "(1)" line 419, ".input.spin", state 1633, "(1)" line 419, ".input.spin", state 1633, "(1)" line 178, ".input.spin", state 1658, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 182, ".input.spin", state 1671, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 159, ".input.spin", state 1681, "(1)" line 163, ".input.spin", state 1689, "(1)" line 167, ".input.spin", state 1701, "(1)" line 174, ".input.spin", state 1712, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1< (0) : (1) ))))" line 178, ".input.spin", state 1788, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 182, ".input.spin", state 1801, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))" line 159, ".input.spin", state 1811, "(1)" line 163, ".input.spin", state 1819, "(1)" line 167, ".input.spin", state 1831, "(1)" line 701, ".input.spin", state 1856, "-end-" (158 of 1856 states) unreached in proctype :init: (0 of 46 states) pan: elapsed time 384 seconds pan: rate 114968.77 states/second pan: avg transition delay 7.2389e-07 usec cp .input.spin asserts.spin.input cp .input.spin.trail asserts.spin.input.trail make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'