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=    4311 States=    1e+06 Transitions= 4.65e+08 Memory=   542.717	t=    480 R=   2e+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 4311, errors: 0
  1884295 states, stored
9.0500014e+08 states, matched
9.0688444e+08 transitions (= stored+matched)
5.3819272e+09 atomic steps
hash conflicts: 4.4436974e+08 (resolved)

Stats on memory usage (in Megabytes):
  179.700	equivalent memory usage for states (stored*(State-vector + overhead))
  144.496	actual memory usage for states (compression: 80.41%)
         	state-vector as stored = 52 byte + 28 byte overhead
    8.000	memory used for hash table (-w20)
  457.764	memory used for DFS stack (-m10000000)
  610.197	total actual memory usage

unreached in proctype urcu_reader
	line 394, ".input.spin", state 17, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 49, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 63, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 82, "(1)"
	line 420, ".input.spin", state 112, "(1)"
	line 424, ".input.spin", state 125, "(1)"
	line 575, ".input.spin", state 146, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
	line 394, ".input.spin", state 153, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 185, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 199, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 218, "(1)"
	line 420, ".input.spin", state 248, "(1)"
	line 424, ".input.spin", state 261, "(1)"
	line 394, ".input.spin", state 282, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 314, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 328, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 347, "(1)"
	line 420, ".input.spin", state 377, "(1)"
	line 424, ".input.spin", state 390, "(1)"
	line 394, ".input.spin", state 413, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 394, ".input.spin", state 415, "(1)"
	line 394, ".input.spin", state 416, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 394, ".input.spin", state 416, "else"
	line 394, ".input.spin", state 419, "(1)"
	line 398, ".input.spin", state 427, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 429, "(1)"
	line 398, ".input.spin", state 430, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 398, ".input.spin", state 430, "else"
	line 398, ".input.spin", state 433, "(1)"
	line 398, ".input.spin", state 434, "(1)"
	line 398, ".input.spin", state 434, "(1)"
	line 396, ".input.spin", state 439, "((i<1))"
	line 396, ".input.spin", state 439, "((i>=1))"
	line 403, ".input.spin", state 445, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 447, "(1)"
	line 403, ".input.spin", state 448, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 403, ".input.spin", state 448, "else"
	line 403, ".input.spin", state 451, "(1)"
	line 403, ".input.spin", state 452, "(1)"
	line 403, ".input.spin", state 452, "(1)"
	line 407, ".input.spin", state 459, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 461, "(1)"
	line 407, ".input.spin", state 462, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 407, ".input.spin", state 462, "else"
	line 407, ".input.spin", state 465, "(1)"
	line 407, ".input.spin", state 466, "(1)"
	line 407, ".input.spin", state 466, "(1)"
	line 405, ".input.spin", state 471, "((i<2))"
	line 405, ".input.spin", state 471, "((i>=2))"
	line 411, ".input.spin", state 478, "(1)"
	line 411, ".input.spin", state 479, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 411, ".input.spin", state 479, "else"
	line 411, ".input.spin", state 482, "(1)"
	line 411, ".input.spin", state 483, "(1)"
	line 411, ".input.spin", state 483, "(1)"
	line 415, ".input.spin", state 491, "(1)"
	line 415, ".input.spin", state 492, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 415, ".input.spin", state 492, "else"
	line 415, ".input.spin", state 495, "(1)"
	line 415, ".input.spin", state 496, "(1)"
	line 415, ".input.spin", state 496, "(1)"
	line 413, ".input.spin", state 501, "((i<1))"
	line 413, ".input.spin", state 501, "((i>=1))"
	line 420, ".input.spin", state 508, "(1)"
	line 420, ".input.spin", state 509, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 420, ".input.spin", state 509, "else"
	line 420, ".input.spin", state 512, "(1)"
	line 420, ".input.spin", state 513, "(1)"
	line 420, ".input.spin", state 513, "(1)"
	line 424, ".input.spin", state 521, "(1)"
	line 424, ".input.spin", state 522, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 424, ".input.spin", state 522, "else"
	line 424, ".input.spin", state 525, "(1)"
	line 424, ".input.spin", state 526, "(1)"
	line 424, ".input.spin", state 526, "(1)"
	line 422, ".input.spin", state 531, "((i<2))"
	line 422, ".input.spin", state 531, "((i>=2))"
	line 429, ".input.spin", state 535, "(1)"
	line 429, ".input.spin", state 535, "(1)"
	line 575, ".input.spin", state 538, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
	line 575, ".input.spin", state 539, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
	line 575, ".input.spin", state 540, "(1)"
	line 249, ".input.spin", state 544, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 253, ".input.spin", state 555, "(1)"
	line 257, ".input.spin", state 566, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 261, ".input.spin", state 575, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 226, ".input.spin", state 591, "(1)"
	line 230, ".input.spin", state 599, "(1)"
	line 234, ".input.spin", state 611, "(1)"
	line 238, ".input.spin", state 619, "(1)"
	line 394, ".input.spin", state 637, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 651, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 669, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 683, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 702, "(1)"
	line 415, ".input.spin", state 715, "(1)"
	line 420, ".input.spin", state 732, "(1)"
	line 424, ".input.spin", state 745, "(1)"
	line 394, ".input.spin", state 773, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 394, ".input.spin", state 775, "(1)"
	line 394, ".input.spin", state 776, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 394, ".input.spin", state 776, "else"
	line 394, ".input.spin", state 779, "(1)"
	line 398, ".input.spin", state 787, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 789, "(1)"
	line 398, ".input.spin", state 790, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 398, ".input.spin", state 790, "else"
	line 398, ".input.spin", state 793, "(1)"
	line 398, ".input.spin", state 794, "(1)"
	line 398, ".input.spin", state 794, "(1)"
	line 396, ".input.spin", state 799, "((i<1))"
	line 396, ".input.spin", state 799, "((i>=1))"
	line 403, ".input.spin", state 805, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 807, "(1)"
	line 403, ".input.spin", state 808, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 403, ".input.spin", state 808, "else"
	line 403, ".input.spin", state 811, "(1)"
	line 403, ".input.spin", state 812, "(1)"
	line 403, ".input.spin", state 812, "(1)"
	line 407, ".input.spin", state 819, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 821, "(1)"
	line 407, ".input.spin", state 822, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 407, ".input.spin", state 822, "else"
	line 407, ".input.spin", state 825, "(1)"
	line 407, ".input.spin", state 826, "(1)"
	line 407, ".input.spin", state 826, "(1)"
	line 405, ".input.spin", state 831, "((i<2))"
	line 405, ".input.spin", state 831, "((i>=2))"
	line 411, ".input.spin", state 838, "(1)"
	line 411, ".input.spin", state 839, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 411, ".input.spin", state 839, "else"
	line 411, ".input.spin", state 842, "(1)"
	line 411, ".input.spin", state 843, "(1)"
	line 411, ".input.spin", state 843, "(1)"
	line 415, ".input.spin", state 851, "(1)"
	line 415, ".input.spin", state 852, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 415, ".input.spin", state 852, "else"
	line 415, ".input.spin", state 855, "(1)"
	line 415, ".input.spin", state 856, "(1)"
	line 415, ".input.spin", state 856, "(1)"
	line 413, ".input.spin", state 861, "((i<1))"
	line 413, ".input.spin", state 861, "((i>=1))"
	line 420, ".input.spin", state 868, "(1)"
	line 420, ".input.spin", state 869, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 420, ".input.spin", state 869, "else"
	line 420, ".input.spin", state 872, "(1)"
	line 420, ".input.spin", state 873, "(1)"
	line 420, ".input.spin", state 873, "(1)"
	line 424, ".input.spin", state 881, "(1)"
	line 424, ".input.spin", state 882, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 424, ".input.spin", state 882, "else"
	line 424, ".input.spin", state 885, "(1)"
	line 424, ".input.spin", state 886, "(1)"
	line 424, ".input.spin", state 886, "(1)"
	line 429, ".input.spin", state 895, "(1)"
	line 429, ".input.spin", state 895, "(1)"
	line 394, ".input.spin", state 902, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 394, ".input.spin", state 904, "(1)"
	line 394, ".input.spin", state 905, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 394, ".input.spin", state 905, "else"
	line 394, ".input.spin", state 908, "(1)"
	line 398, ".input.spin", state 916, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 918, "(1)"
	line 398, ".input.spin", state 919, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 398, ".input.spin", state 919, "else"
	line 398, ".input.spin", state 922, "(1)"
	line 398, ".input.spin", state 923, "(1)"
	line 398, ".input.spin", state 923, "(1)"
	line 396, ".input.spin", state 928, "((i<1))"
	line 396, ".input.spin", state 928, "((i>=1))"
	line 403, ".input.spin", state 934, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 936, "(1)"
	line 403, ".input.spin", state 937, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 403, ".input.spin", state 937, "else"
	line 403, ".input.spin", state 940, "(1)"
	line 403, ".input.spin", state 941, "(1)"
	line 403, ".input.spin", state 941, "(1)"
	line 407, ".input.spin", state 948, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 950, "(1)"
	line 407, ".input.spin", state 951, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 407, ".input.spin", state 951, "else"
	line 407, ".input.spin", state 954, "(1)"
	line 407, ".input.spin", state 955, "(1)"
	line 407, ".input.spin", state 955, "(1)"
	line 405, ".input.spin", state 960, "((i<2))"
	line 405, ".input.spin", state 960, "((i>=2))"
	line 411, ".input.spin", state 967, "(1)"
	line 411, ".input.spin", state 968, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 411, ".input.spin", state 968, "else"
	line 411, ".input.spin", state 971, "(1)"
	line 411, ".input.spin", state 972, "(1)"
	line 411, ".input.spin", state 972, "(1)"
	line 415, ".input.spin", state 980, "(1)"
	line 415, ".input.spin", state 981, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 415, ".input.spin", state 981, "else"
	line 415, ".input.spin", state 984, "(1)"
	line 415, ".input.spin", state 985, "(1)"
	line 415, ".input.spin", state 985, "(1)"
	line 413, ".input.spin", state 990, "((i<1))"
	line 413, ".input.spin", state 990, "((i>=1))"
	line 420, ".input.spin", state 997, "(1)"
	line 420, ".input.spin", state 998, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 420, ".input.spin", state 998, "else"
	line 420, ".input.spin", state 1001, "(1)"
	line 420, ".input.spin", state 1002, "(1)"
	line 420, ".input.spin", state 1002, "(1)"
	line 424, ".input.spin", state 1010, "(1)"
	line 424, ".input.spin", state 1011, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 424, ".input.spin", state 1011, "else"
	line 424, ".input.spin", state 1014, "(1)"
	line 424, ".input.spin", state 1015, "(1)"
	line 424, ".input.spin", state 1015, "(1)"
	line 422, ".input.spin", state 1020, "((i<2))"
	line 422, ".input.spin", state 1020, "((i>=2))"
	line 429, ".input.spin", state 1024, "(1)"
	line 429, ".input.spin", state 1024, "(1)"
	line 583, ".input.spin", state 1028, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
	line 394, ".input.spin", state 1033, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 1047, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 1065, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1079, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 1098, "(1)"
	line 415, ".input.spin", state 1111, "(1)"
	line 420, ".input.spin", state 1128, "(1)"
	line 424, ".input.spin", state 1141, "(1)"
	line 394, ".input.spin", state 1165, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 1197, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1211, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 1230, "(1)"
	line 420, ".input.spin", state 1260, "(1)"
	line 424, ".input.spin", state 1273, "(1)"
	line 394, ".input.spin", state 1298, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 1330, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1344, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 1363, "(1)"
	line 420, ".input.spin", state 1393, "(1)"
	line 424, ".input.spin", state 1406, "(1)"
	line 394, ".input.spin", state 1427, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 1459, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1473, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 1492, "(1)"
	line 420, ".input.spin", state 1522, "(1)"
	line 424, ".input.spin", state 1535, "(1)"
	line 249, ".input.spin", state 1558, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 257, ".input.spin", state 1580, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 261, ".input.spin", state 1589, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 226, ".input.spin", state 1605, "(1)"
	line 230, ".input.spin", state 1613, "(1)"
	line 234, ".input.spin", state 1625, "(1)"
	line 238, ".input.spin", state 1633, "(1)"
	line 394, ".input.spin", state 1651, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 1665, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 1683, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1697, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 1716, "(1)"
	line 415, ".input.spin", state 1729, "(1)"
	line 420, ".input.spin", state 1746, "(1)"
	line 424, ".input.spin", state 1759, "(1)"
	line 394, ".input.spin", state 1780, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 1794, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 1812, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1826, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 1845, "(1)"
	line 415, ".input.spin", state 1858, "(1)"
	line 420, ".input.spin", state 1875, "(1)"
	line 424, ".input.spin", state 1888, "(1)"
	line 394, ".input.spin", state 1912, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 1928, "(1)"
	line 403, ".input.spin", state 1944, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1958, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 1977, "(1)"
	line 420, ".input.spin", state 2007, "(1)"
	line 424, ".input.spin", state 2020, "(1)"
	line 622, ".input.spin", state 2041, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
	line 394, ".input.spin", state 2048, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 2080, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 2094, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 2113, "(1)"
	line 420, ".input.spin", state 2143, "(1)"
	line 424, ".input.spin", state 2156, "(1)"
	line 394, ".input.spin", state 2177, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 2209, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 2223, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 2242, "(1)"
	line 420, ".input.spin", state 2272, "(1)"
	line 424, ".input.spin", state 2285, "(1)"
	line 394, ".input.spin", state 2308, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 394, ".input.spin", state 2310, "(1)"
	line 394, ".input.spin", state 2311, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 394, ".input.spin", state 2311, "else"
	line 394, ".input.spin", state 2314, "(1)"
	line 398, ".input.spin", state 2322, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 2324, "(1)"
	line 398, ".input.spin", state 2325, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 398, ".input.spin", state 2325, "else"
	line 398, ".input.spin", state 2328, "(1)"
	line 398, ".input.spin", state 2329, "(1)"
	line 398, ".input.spin", state 2329, "(1)"
	line 396, ".input.spin", state 2334, "((i<1))"
	line 396, ".input.spin", state 2334, "((i>=1))"
	line 403, ".input.spin", state 2340, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 2342, "(1)"
	line 403, ".input.spin", state 2343, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 403, ".input.spin", state 2343, "else"
	line 403, ".input.spin", state 2346, "(1)"
	line 403, ".input.spin", state 2347, "(1)"
	line 403, ".input.spin", state 2347, "(1)"
	line 407, ".input.spin", state 2354, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 2356, "(1)"
	line 407, ".input.spin", state 2357, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 407, ".input.spin", state 2357, "else"
	line 407, ".input.spin", state 2360, "(1)"
	line 407, ".input.spin", state 2361, "(1)"
	line 407, ".input.spin", state 2361, "(1)"
	line 405, ".input.spin", state 2366, "((i<2))"
	line 405, ".input.spin", state 2366, "((i>=2))"
	line 411, ".input.spin", state 2373, "(1)"
	line 411, ".input.spin", state 2374, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 411, ".input.spin", state 2374, "else"
	line 411, ".input.spin", state 2377, "(1)"
	line 411, ".input.spin", state 2378, "(1)"
	line 411, ".input.spin", state 2378, "(1)"
	line 415, ".input.spin", state 2386, "(1)"
	line 415, ".input.spin", state 2387, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 415, ".input.spin", state 2387, "else"
	line 415, ".input.spin", state 2390, "(1)"
	line 415, ".input.spin", state 2391, "(1)"
	line 415, ".input.spin", state 2391, "(1)"
	line 413, ".input.spin", state 2396, "((i<1))"
	line 413, ".input.spin", state 2396, "((i>=1))"
	line 420, ".input.spin", state 2403, "(1)"
	line 420, ".input.spin", state 2404, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 420, ".input.spin", state 2404, "else"
	line 420, ".input.spin", state 2407, "(1)"
	line 420, ".input.spin", state 2408, "(1)"
	line 420, ".input.spin", state 2408, "(1)"
	line 424, ".input.spin", state 2416, "(1)"
	line 424, ".input.spin", state 2417, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 424, ".input.spin", state 2417, "else"
	line 424, ".input.spin", state 2420, "(1)"
	line 424, ".input.spin", state 2421, "(1)"
	line 424, ".input.spin", state 2421, "(1)"
	line 422, ".input.spin", state 2426, "((i<2))"
	line 422, ".input.spin", state 2426, "((i>=2))"
	line 429, ".input.spin", state 2430, "(1)"
	line 429, ".input.spin", state 2430, "(1)"
	line 622, ".input.spin", state 2433, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
	line 622, ".input.spin", state 2434, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
	line 622, ".input.spin", state 2435, "(1)"
	line 249, ".input.spin", state 2439, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 253, ".input.spin", state 2450, "(1)"
	line 257, ".input.spin", state 2461, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 261, ".input.spin", state 2470, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 226, ".input.spin", state 2486, "(1)"
	line 230, ".input.spin", state 2494, "(1)"
	line 234, ".input.spin", state 2506, "(1)"
	line 238, ".input.spin", state 2514, "(1)"
	line 394, ".input.spin", state 2532, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 2546, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 2564, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 2578, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 2597, "(1)"
	line 415, ".input.spin", state 2610, "(1)"
	line 420, ".input.spin", state 2627, "(1)"
	line 424, ".input.spin", state 2640, "(1)"
	line 249, ".input.spin", state 2664, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 253, ".input.spin", state 2673, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 257, ".input.spin", state 2686, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 261, ".input.spin", state 2695, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 226, ".input.spin", state 2711, "(1)"
	line 230, ".input.spin", state 2719, "(1)"
	line 234, ".input.spin", state 2731, "(1)"
	line 238, ".input.spin", state 2739, "(1)"
	line 394, ".input.spin", state 2757, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 2771, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 2789, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 2803, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 2822, "(1)"
	line 415, ".input.spin", state 2835, "(1)"
	line 420, ".input.spin", state 2852, "(1)"
	line 424, ".input.spin", state 2865, "(1)"
	line 394, ".input.spin", state 2886, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 2900, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 403, ".input.spin", state 2918, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 2932, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 411, ".input.spin", state 2951, "(1)"
	line 415, ".input.spin", state 2964, "(1)"
	line 420, ".input.spin", state 2981, "(1)"
	line 424, ".input.spin", state 2994, "(1)"
	line 226, ".input.spin", state 3027, "(1)"
	line 234, ".input.spin", state 3047, "(1)"
	line 238, ".input.spin", state 3055, "(1)"
	line 226, ".input.spin", state 3070, "(1)"
	line 230, ".input.spin", state 3078, "(1)"
	line 234, ".input.spin", state 3090, "(1)"
	line 238, ".input.spin", state 3098, "(1)"
	line 876, ".input.spin", state 3115, "-end-"
	(318 of 3115 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 253, ".input.spin", state 1003, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 257, ".input.spin", state 1016, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 261, ".input.spin", state 1025, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 226, ".input.spin", state 1041, "(1)"
	line 230, ".input.spin", state 1049, "(1)"
	line 234, ".input.spin", state 1061, "(1)"
	line 238, ".input.spin", state 1069, "(1)"
	line 253, ".input.spin", state 1094, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 257, ".input.spin", state 1107, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 261, ".input.spin", state 1116, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 226, ".input.spin", state 1132, "(1)"
	line 230, ".input.spin", state 1140, "(1)"
	line 234, ".input.spin", state 1152, "(1)"
	line 238, ".input.spin", state 1160, "(1)"
	line 253, ".input.spin", state 1185, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 257, ".input.spin", state 1198, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 261, ".input.spin", state 1207, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 226, ".input.spin", state 1223, "(1)"
	line 230, ".input.spin", state 1231, "(1)"
	line 234, ".input.spin", state 1243, "(1)"
	line 238, ".input.spin", state 1251, "(1)"
	line 1203, ".input.spin", state 1266, "-end-"
	(71 of 1266 states)
unreached in proctype :init:
	(0 of 78 states)

pan: elapsed time 944 seconds
pan: rate 1995.0819 states/second
pan: avg transition delay 1.0414e-06 usec
cp .input.spin asserts.spin.input
cp .input.spin.trail asserts.spin.input.trail