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= 5832 States= 1e+06 Transitions= 1.25e+08 Memory= 542.717 t= 123 R= 8e+03 Depth= 5832 States= 2e+06 Transitions= 4.09e+08 Memory= 618.986 t= 417 R= 5e+03 Depth= 5832 States= 3e+06 Transitions= 6.64e+08 Memory= 695.256 t= 685 R= 4e+03 pan: resizing hashtable to -w22.. done Depth= 5832 States= 4e+06 Transitions= 1.15e+09 Memory= 802.647 t= 1.2e+03 R= 3e+03 Depth= 5832 States= 5e+06 Transitions= 1.46e+09 Memory= 878.916 t= 1.52e+03 R= 3e+03 Depth= 5832 States= 6e+06 Transitions= 1.66e+09 Memory= 955.186 t= 1.72e+03 R= 3e+03 Depth= 5832 States= 7e+06 Transitions= 1.86e+09 Memory= 1031.455 t= 1.93e+03 R= 4e+03 Depth= 5832 States= 8e+06 Transitions= 2.13e+09 Memory= 1107.822 t= 2.22e+03 R= 4e+03 Depth= 5832 States= 9e+06 Transitions= 2.38e+09 Memory= 1184.092 t= 2.49e+03 R= 4e+03 pan: resizing hashtable to -w24.. done Depth= 5832 States= 1e+07 Transitions= 2.87e+09 Memory= 1384.455 t= 3e+03 R= 3e+03 Depth= 5832 States= 1.1e+07 Transitions= 3.15e+09 Memory= 1460.725 t= 3.29e+03 R= 3e+03 Depth= 5832 States= 1.2e+07 Transitions= 3.42e+09 Memory= 1536.994 t= 3.57e+03 R= 3e+03 Depth= 5832 States= 1.3e+07 Transitions= 3.62e+09 Memory= 1613.361 t= 3.77e+03 R= 3e+03 Depth= 5832 States= 1.4e+07 Transitions= 3.84e+09 Memory= 1689.631 t= 3.99e+03 R= 4e+03 Depth= 5832 States= 1.5e+07 Transitions= 4.13e+09 Memory= 1765.901 t= 4.29e+03 R= 3e+03 (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 72 byte, depth reached 5832, errors: 0 15444143 states, stored 4.2527754e+09 states, matched 4.2682195e+09 transitions (= stored+matched) 2.483245e+10 atomic steps hash conflicts: 2.790927e+09 (resolved) Stats on memory usage (in Megabytes): 1472.868 equivalent memory usage for states (stored*(State-vector + overhead)) 1214.135 actual memory usage for states (compression: 82.43%) state-vector as stored = 54 byte + 28 byte overhead 128.000 memory used for hash table (-w24) 457.764 memory used for DFS stack (-m10000000) 1799.787 total actual memory usage unreached in proctype urcu_reader line 249, ".input.spin", state 30, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 261, ".input.spin", state 61, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 77, "(1)" line 230, ".input.spin", state 85, "(1)" line 234, ".input.spin", state 97, "(1)" line 238, ".input.spin", state 105, "(1)" line 394, ".input.spin", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 163, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 177, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 196, "(1)" line 420, ".input.spin", state 226, "(1)" line 424, ".input.spin", state 239, "(1)" line 669, ".input.spin", state 260, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))" line 394, ".input.spin", state 267, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 299, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 313, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 332, "(1)" line 420, ".input.spin", state 362, "(1)" line 424, ".input.spin", state 375, "(1)" line 394, ".input.spin", state 396, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 428, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 442, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 461, "(1)" line 420, ".input.spin", state 491, "(1)" line 424, ".input.spin", state 504, "(1)" line 394, ".input.spin", state 527, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 394, ".input.spin", state 529, "(1)" line 394, ".input.spin", state 530, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))" line 394, ".input.spin", state 530, "else" line 394, ".input.spin", state 533, "(1)" line 398, ".input.spin", state 541, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 398, ".input.spin", state 543, "(1)" line 398, ".input.spin", state 544, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))" line 398, ".input.spin", state 544, "else" line 398, ".input.spin", state 547, "(1)" line 398, ".input.spin", state 548, "(1)" line 398, ".input.spin", state 548, "(1)" line 396, ".input.spin", state 553, "((i<1))" line 396, ".input.spin", state 553, "((i>=1))" line 403, ".input.spin", state 559, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 561, "(1)" line 403, ".input.spin", state 562, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))" line 403, ".input.spin", state 562, "else" line 403, ".input.spin", state 565, "(1)" line 403, ".input.spin", state 566, "(1)" line 403, ".input.spin", state 566, "(1)" line 407, ".input.spin", state 573, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 407, ".input.spin", state 575, "(1)" line 407, ".input.spin", state 576, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))" line 407, ".input.spin", state 576, "else" line 407, ".input.spin", state 579, "(1)" line 407, ".input.spin", state 580, "(1)" line 407, ".input.spin", state 580, "(1)" line 405, ".input.spin", state 585, "((i<2))" line 405, ".input.spin", state 585, "((i>=2))" line 411, ".input.spin", state 592, "(1)" line 411, ".input.spin", state 593, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))" line 411, ".input.spin", state 593, "else" line 411, ".input.spin", state 596, "(1)" line 411, ".input.spin", state 597, "(1)" line 411, ".input.spin", state 597, "(1)" line 415, ".input.spin", state 605, "(1)" line 415, ".input.spin", state 606, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))" line 415, ".input.spin", state 606, "else" line 415, ".input.spin", state 609, "(1)" line 415, ".input.spin", state 610, "(1)" line 415, ".input.spin", state 610, "(1)" line 413, ".input.spin", state 615, "((i<1))" line 413, ".input.spin", state 615, "((i>=1))" line 420, ".input.spin", state 622, "(1)" line 420, ".input.spin", state 623, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))" line 420, ".input.spin", state 623, "else" line 420, ".input.spin", state 626, "(1)" line 420, ".input.spin", state 627, "(1)" line 420, ".input.spin", state 627, "(1)" line 424, ".input.spin", state 635, "(1)" line 424, ".input.spin", state 636, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))" line 424, ".input.spin", state 636, "else" line 424, ".input.spin", state 639, "(1)" line 424, ".input.spin", state 640, "(1)" line 424, ".input.spin", state 640, "(1)" line 422, ".input.spin", state 645, "((i<2))" line 422, ".input.spin", state 645, "((i>=2))" line 429, ".input.spin", state 649, "(1)" line 429, ".input.spin", state 649, "(1)" line 669, ".input.spin", state 652, "cached_urcu_active_readers.val[_pid] = (tmp+1)" line 669, ".input.spin", state 653, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))" line 669, ".input.spin", state 654, "(1)" line 394, ".input.spin", state 661, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 693, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 707, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 726, "(1)" line 420, ".input.spin", state 756, "(1)" line 424, ".input.spin", state 769, "(1)" line 394, ".input.spin", state 797, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 394, ".input.spin", state 799, "(1)" line 394, ".input.spin", state 800, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))" line 394, ".input.spin", state 800, "else" line 394, ".input.spin", state 803, "(1)" line 398, ".input.spin", state 811, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 398, ".input.spin", state 813, "(1)" line 398, ".input.spin", state 814, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))" line 398, ".input.spin", state 814, "else" line 398, ".input.spin", state 817, "(1)" line 398, ".input.spin", state 818, "(1)" line 398, ".input.spin", state 818, "(1)" line 396, ".input.spin", state 823, "((i<1))" line 396, ".input.spin", state 823, "((i>=1))" line 403, ".input.spin", state 829, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 831, "(1)" line 403, ".input.spin", state 832, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))" line 403, ".input.spin", state 832, "else" line 403, ".input.spin", state 835, "(1)" line 403, ".input.spin", state 836, "(1)" line 403, ".input.spin", state 836, "(1)" line 407, ".input.spin", state 843, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 407, ".input.spin", state 845, "(1)" line 407, ".input.spin", state 846, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))" line 407, ".input.spin", state 846, "else" line 407, ".input.spin", state 849, "(1)" line 407, ".input.spin", state 850, "(1)" line 407, ".input.spin", state 850, "(1)" line 405, ".input.spin", state 855, "((i<2))" line 405, ".input.spin", state 855, "((i>=2))" line 411, ".input.spin", state 862, "(1)" line 411, ".input.spin", state 863, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))" line 411, ".input.spin", state 863, "else" line 411, ".input.spin", state 866, "(1)" line 411, ".input.spin", state 867, "(1)" line 411, ".input.spin", state 867, "(1)" line 415, ".input.spin", state 875, "(1)" line 415, ".input.spin", state 876, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))" line 415, ".input.spin", state 876, "else" line 415, ".input.spin", state 879, "(1)" line 415, ".input.spin", state 880, "(1)" line 415, ".input.spin", state 880, "(1)" line 413, ".input.spin", state 885, "((i<1))" line 413, ".input.spin", state 885, "((i>=1))" line 420, ".input.spin", state 892, "(1)" line 420, ".input.spin", state 893, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))" line 420, ".input.spin", state 893, "else" line 420, ".input.spin", state 896, "(1)" line 420, ".input.spin", state 897, "(1)" line 420, ".input.spin", state 897, "(1)" line 424, ".input.spin", state 905, "(1)" line 424, ".input.spin", state 906, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))" line 424, ".input.spin", state 906, "else" line 424, ".input.spin", state 909, "(1)" line 424, ".input.spin", state 910, "(1)" line 424, ".input.spin", state 910, "(1)" line 429, ".input.spin", state 919, "(1)" line 429, ".input.spin", state 919, "(1)" line 394, ".input.spin", state 926, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 394, ".input.spin", state 928, "(1)" line 394, ".input.spin", state 929, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))" line 394, ".input.spin", state 929, "else" line 394, ".input.spin", state 932, "(1)" line 398, ".input.spin", state 940, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 398, ".input.spin", state 942, "(1)" line 398, ".input.spin", state 943, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))" line 398, ".input.spin", state 943, "else" line 398, ".input.spin", state 946, "(1)" line 398, ".input.spin", state 947, "(1)" line 398, ".input.spin", state 947, "(1)" line 396, ".input.spin", state 952, "((i<1))" line 396, ".input.spin", state 952, "((i>=1))" line 403, ".input.spin", state 958, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 960, "(1)" line 403, ".input.spin", state 961, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))" line 403, ".input.spin", state 961, "else" line 403, ".input.spin", state 964, "(1)" line 403, ".input.spin", state 965, "(1)" line 403, ".input.spin", state 965, "(1)" line 407, ".input.spin", state 972, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 407, ".input.spin", state 974, "(1)" line 407, ".input.spin", state 975, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))" line 407, ".input.spin", state 975, "else" line 407, ".input.spin", state 978, "(1)" line 407, ".input.spin", state 979, "(1)" line 407, ".input.spin", state 979, "(1)" line 405, ".input.spin", state 984, "((i<2))" line 405, ".input.spin", state 984, "((i>=2))" line 411, ".input.spin", state 991, "(1)" line 411, ".input.spin", state 992, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))" line 411, ".input.spin", state 992, "else" line 411, ".input.spin", state 995, "(1)" line 411, ".input.spin", state 996, "(1)" line 411, ".input.spin", state 996, "(1)" line 415, ".input.spin", state 1004, "(1)" line 415, ".input.spin", state 1005, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))" line 415, ".input.spin", state 1005, "else" line 415, ".input.spin", state 1008, "(1)" line 415, ".input.spin", state 1009, "(1)" line 415, ".input.spin", state 1009, "(1)" line 413, ".input.spin", state 1014, "((i<1))" line 413, ".input.spin", state 1014, "((i>=1))" line 420, ".input.spin", state 1021, "(1)" line 420, ".input.spin", state 1022, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))" line 420, ".input.spin", state 1022, "else" line 420, ".input.spin", state 1025, "(1)" line 420, ".input.spin", state 1026, "(1)" line 420, ".input.spin", state 1026, "(1)" line 424, ".input.spin", state 1034, "(1)" line 424, ".input.spin", state 1035, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))" line 424, ".input.spin", state 1035, "else" line 424, ".input.spin", state 1038, "(1)" line 424, ".input.spin", state 1039, "(1)" line 424, ".input.spin", state 1039, "(1)" line 422, ".input.spin", state 1044, "((i<2))" line 422, ".input.spin", state 1044, "((i>=2))" line 429, ".input.spin", state 1048, "(1)" line 429, ".input.spin", state 1048, "(1)" line 677, ".input.spin", state 1052, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))" line 394, ".input.spin", state 1057, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 1089, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 1103, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 1122, "(1)" line 420, ".input.spin", state 1152, "(1)" line 424, ".input.spin", state 1165, "(1)" line 394, ".input.spin", state 1189, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 1221, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 1235, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 1254, "(1)" line 420, ".input.spin", state 1284, "(1)" line 424, ".input.spin", state 1297, "(1)" line 394, ".input.spin", state 1322, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 1354, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 1368, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 1387, "(1)" line 420, ".input.spin", state 1417, "(1)" line 424, ".input.spin", state 1430, "(1)" line 394, ".input.spin", state 1451, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 1483, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 1497, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 1516, "(1)" line 420, ".input.spin", state 1546, "(1)" line 424, ".input.spin", state 1559, "(1)" line 394, ".input.spin", state 1585, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 1617, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 1631, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 1650, "(1)" line 420, ".input.spin", state 1680, "(1)" line 424, ".input.spin", state 1693, "(1)" line 394, ".input.spin", state 1714, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 1746, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 1760, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 1779, "(1)" line 420, ".input.spin", state 1809, "(1)" line 424, ".input.spin", state 1822, "(1)" line 394, ".input.spin", state 1846, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 1878, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 1892, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 1911, "(1)" line 420, ".input.spin", state 1941, "(1)" line 424, ".input.spin", state 1954, "(1)" line 716, ".input.spin", state 1975, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))" line 394, ".input.spin", state 1982, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 2014, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 2028, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 2047, "(1)" line 420, ".input.spin", state 2077, "(1)" line 424, ".input.spin", state 2090, "(1)" line 394, ".input.spin", state 2111, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 2143, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 2157, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 2176, "(1)" line 420, ".input.spin", state 2206, "(1)" line 424, ".input.spin", state 2219, "(1)" line 394, ".input.spin", state 2242, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 394, ".input.spin", state 2244, "(1)" line 394, ".input.spin", state 2245, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))" line 394, ".input.spin", state 2245, "else" line 394, ".input.spin", state 2248, "(1)" line 398, ".input.spin", state 2256, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 398, ".input.spin", state 2258, "(1)" line 398, ".input.spin", state 2259, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))" line 398, ".input.spin", state 2259, "else" line 398, ".input.spin", state 2262, "(1)" line 398, ".input.spin", state 2263, "(1)" line 398, ".input.spin", state 2263, "(1)" line 396, ".input.spin", state 2268, "((i<1))" line 396, ".input.spin", state 2268, "((i>=1))" line 403, ".input.spin", state 2274, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 2276, "(1)" line 403, ".input.spin", state 2277, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))" line 403, ".input.spin", state 2277, "else" line 403, ".input.spin", state 2280, "(1)" line 403, ".input.spin", state 2281, "(1)" line 403, ".input.spin", state 2281, "(1)" line 407, ".input.spin", state 2288, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 407, ".input.spin", state 2290, "(1)" line 407, ".input.spin", state 2291, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))" line 407, ".input.spin", state 2291, "else" line 407, ".input.spin", state 2294, "(1)" line 407, ".input.spin", state 2295, "(1)" line 407, ".input.spin", state 2295, "(1)" line 405, ".input.spin", state 2300, "((i<2))" line 405, ".input.spin", state 2300, "((i>=2))" line 411, ".input.spin", state 2307, "(1)" line 411, ".input.spin", state 2308, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))" line 411, ".input.spin", state 2308, "else" line 411, ".input.spin", state 2311, "(1)" line 411, ".input.spin", state 2312, "(1)" line 411, ".input.spin", state 2312, "(1)" line 415, ".input.spin", state 2320, "(1)" line 415, ".input.spin", state 2321, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))" line 415, ".input.spin", state 2321, "else" line 415, ".input.spin", state 2324, "(1)" line 415, ".input.spin", state 2325, "(1)" line 415, ".input.spin", state 2325, "(1)" line 413, ".input.spin", state 2330, "((i<1))" line 413, ".input.spin", state 2330, "((i>=1))" line 420, ".input.spin", state 2337, "(1)" line 420, ".input.spin", state 2338, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))" line 420, ".input.spin", state 2338, "else" line 420, ".input.spin", state 2341, "(1)" line 420, ".input.spin", state 2342, "(1)" line 420, ".input.spin", state 2342, "(1)" line 424, ".input.spin", state 2350, "(1)" line 424, ".input.spin", state 2351, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))" line 424, ".input.spin", state 2351, "else" line 424, ".input.spin", state 2354, "(1)" line 424, ".input.spin", state 2355, "(1)" line 424, ".input.spin", state 2355, "(1)" line 422, ".input.spin", state 2360, "((i<2))" line 422, ".input.spin", state 2360, "((i>=2))" line 429, ".input.spin", state 2364, "(1)" line 429, ".input.spin", state 2364, "(1)" line 716, ".input.spin", state 2367, "cached_urcu_active_readers.val[_pid] = (tmp+1)" line 716, ".input.spin", state 2368, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))" line 716, ".input.spin", state 2369, "(1)" line 394, ".input.spin", state 2376, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 2408, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 2422, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 2441, "(1)" line 420, ".input.spin", state 2471, "(1)" line 424, ".input.spin", state 2484, "(1)" line 394, ".input.spin", state 2511, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 2543, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 2557, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 2576, "(1)" line 420, ".input.spin", state 2606, "(1)" line 424, ".input.spin", state 2619, "(1)" line 394, ".input.spin", state 2640, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 2672, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 2686, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 2705, "(1)" line 420, ".input.spin", state 2735, "(1)" line 424, ".input.spin", state 2748, "(1)" line 226, ".input.spin", state 2781, "(1)" line 234, ".input.spin", state 2801, "(1)" line 238, ".input.spin", state 2809, "(1)" line 226, ".input.spin", state 2824, "(1)" line 234, ".input.spin", state 2844, "(1)" line 238, ".input.spin", state 2852, "(1)" line 876, ".input.spin", state 2869, "-end-" (278 of 2869 states) unreached in proctype urcu_writer line 394, ".input.spin", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 398, ".input.spin", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 411, ".input.spin", state 83, "(1)" line 415, ".input.spin", state 96, "(1)" line 420, ".input.spin", state 113, "(1)" line 249, ".input.spin", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 253, ".input.spin", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 394, ".input.spin", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 398, ".input.spin", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 411, ".input.spin", state 276, "(1)" line 415, ".input.spin", state 289, "(1)" line 420, ".input.spin", state 306, "(1)" line 424, ".input.spin", state 319, "(1)" line 398, ".input.spin", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 415, ".input.spin", state 420, "(1)" line 420, ".input.spin", state 437, "(1)" line 424, ".input.spin", state 450, "(1)" line 398, ".input.spin", state 494, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 512, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 415, ".input.spin", state 558, "(1)" line 420, ".input.spin", state 575, "(1)" line 424, ".input.spin", state 588, "(1)" line 398, ".input.spin", state 623, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 641, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 655, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 415, ".input.spin", state 687, "(1)" line 420, ".input.spin", state 704, "(1)" line 424, ".input.spin", state 717, "(1)" line 398, ".input.spin", state 754, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 403, ".input.spin", state 772, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 407, ".input.spin", state 786, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 415, ".input.spin", state 818, "(1)" line 420, ".input.spin", state 835, "(1)" line 424, ".input.spin", state 848, "(1)" line 249, ".input.spin", state 903, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 253, ".input.spin", state 912, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 927, "(1)" line 261, ".input.spin", state 934, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 950, "(1)" line 230, ".input.spin", state 958, "(1)" line 234, ".input.spin", state 970, "(1)" line 238, ".input.spin", state 978, "(1)" line 249, ".input.spin", state 1009, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 253, ".input.spin", state 1018, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 1031, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 261, ".input.spin", state 1040, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 1056, "(1)" line 230, ".input.spin", state 1064, "(1)" line 234, ".input.spin", state 1076, "(1)" line 238, ".input.spin", state 1084, "(1)" line 253, ".input.spin", state 1110, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 1123, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 261, ".input.spin", state 1132, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 1148, "(1)" line 230, ".input.spin", state 1156, "(1)" line 234, ".input.spin", state 1168, "(1)" line 238, ".input.spin", state 1176, "(1)" line 249, ".input.spin", state 1207, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 253, ".input.spin", state 1216, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 1229, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 261, ".input.spin", state 1238, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 1254, "(1)" line 230, ".input.spin", state 1262, "(1)" line 234, ".input.spin", state 1274, "(1)" line 238, ".input.spin", state 1282, "(1)" line 253, ".input.spin", state 1308, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 1321, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 261, ".input.spin", state 1330, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 1346, "(1)" line 230, ".input.spin", state 1354, "(1)" line 234, ".input.spin", state 1366, "(1)" line 238, ".input.spin", state 1374, "(1)" line 249, ".input.spin", state 1405, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 253, ".input.spin", state 1414, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 1427, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 261, ".input.spin", state 1436, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 1452, "(1)" line 230, ".input.spin", state 1460, "(1)" line 234, ".input.spin", state 1472, "(1)" line 238, ".input.spin", state 1480, "(1)" line 253, ".input.spin", state 1506, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 1519, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 261, ".input.spin", state 1528, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 1544, "(1)" line 230, ".input.spin", state 1552, "(1)" line 234, ".input.spin", state 1564, "(1)" line 238, ".input.spin", state 1572, "(1)" line 249, ".input.spin", state 1603, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))" line 253, ".input.spin", state 1612, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))" line 257, ".input.spin", state 1625, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))" line 261, ".input.spin", state 1634, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))" line 226, ".input.spin", state 1650, "(1)" line 230, ".input.spin", state 1658, "(1)" line 234, ".input.spin", state 1670, "(1)" line 238, ".input.spin", state 1678, "(1)" line 1203, ".input.spin", state 1694, "-end-" (103 of 1694 states) unreached in proctype :init: (0 of 78 states) pan: elapsed time 4.43e+03 seconds pan: rate 3486.0658 states/second pan: avg transition delay 1.038e-06 usec cp .input.spin asserts.spin.input cp .input.spin.trail asserts.spin.input.trail