make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-alpha-no-ipi'
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=    4773 States=    1e+06 Transitions= 6.22e+08 Memory=   542.717	t=    624 R=   2e+03
Depth=    5040 States=    2e+06 Transitions=  1.3e+09 Memory=   618.986	t= 1.33e+03 R=   1e+03
Depth=    5040 States=    3e+06 Transitions= 1.95e+09 Memory=   695.256	t= 2.03e+03 R=   1e+03
pan: resizing hashtable to -w22..  done
Depth=    5040 States=    4e+06 Transitions= 2.64e+09 Memory=   802.647	t= 2.73e+03 R=   1e+03
Depth=    5040 States=    5e+06 Transitions=  3.3e+09 Memory=   878.916	t= 3.41e+03 R=   1e+03
Depth=    5141 States=    6e+06 Transitions= 3.99e+09 Memory=   955.186	t= 4.12e+03 R=   1e+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 5141, errors: 0
  6711104 states, stored
4.4393201e+09 states, matched
4.4460312e+09 transitions (= stored+matched)
2.5322962e+10 atomic steps
hash conflicts: 3.3332015e+09 (resolved)

Stats on memory usage (in Megabytes):
  640.021	equivalent memory usage for states (stored*(State-vector + overhead))
  519.783	actual memory usage for states (compression: 81.21%)
         	state-vector as stored = 53 byte + 28 byte overhead
   32.000	memory used for hash table (-w22)
  457.764	memory used for DFS stack (-m10000000)
 1009.483	total actual memory usage

unreached in proctype urcu_reader
	line 410, ".input.spin", state 17, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 49, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 63, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 82, "(1)"
	line 437, ".input.spin", state 112, "(1)"
	line 441, ".input.spin", state 125, "(1)"
	line 596, ".input.spin", state 146, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
	line 410, ".input.spin", state 153, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 185, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 199, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 218, "(1)"
	line 437, ".input.spin", state 248, "(1)"
	line 441, ".input.spin", state 261, "(1)"
	line 410, ".input.spin", state 282, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 314, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 328, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 347, "(1)"
	line 437, ".input.spin", state 377, "(1)"
	line 441, ".input.spin", state 390, "(1)"
	line 410, ".input.spin", state 413, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 410, ".input.spin", state 415, "(1)"
	line 410, ".input.spin", state 416, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 410, ".input.spin", state 416, "else"
	line 410, ".input.spin", state 419, "(1)"
	line 414, ".input.spin", state 427, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 429, "(1)"
	line 414, ".input.spin", state 430, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 414, ".input.spin", state 430, "else"
	line 414, ".input.spin", state 433, "(1)"
	line 414, ".input.spin", state 434, "(1)"
	line 414, ".input.spin", state 434, "(1)"
	line 412, ".input.spin", state 439, "((i<1))"
	line 412, ".input.spin", state 439, "((i>=1))"
	line 419, ".input.spin", state 445, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 447, "(1)"
	line 419, ".input.spin", state 448, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 419, ".input.spin", state 448, "else"
	line 419, ".input.spin", state 451, "(1)"
	line 419, ".input.spin", state 452, "(1)"
	line 419, ".input.spin", state 452, "(1)"
	line 423, ".input.spin", state 459, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 461, "(1)"
	line 423, ".input.spin", state 462, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 423, ".input.spin", state 462, "else"
	line 423, ".input.spin", state 465, "(1)"
	line 423, ".input.spin", state 466, "(1)"
	line 423, ".input.spin", state 466, "(1)"
	line 421, ".input.spin", state 471, "((i<2))"
	line 421, ".input.spin", state 471, "((i>=2))"
	line 428, ".input.spin", state 478, "(1)"
	line 428, ".input.spin", state 479, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 428, ".input.spin", state 479, "else"
	line 428, ".input.spin", state 482, "(1)"
	line 428, ".input.spin", state 483, "(1)"
	line 428, ".input.spin", state 483, "(1)"
	line 432, ".input.spin", state 491, "(1)"
	line 432, ".input.spin", state 492, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 432, ".input.spin", state 492, "else"
	line 432, ".input.spin", state 495, "(1)"
	line 432, ".input.spin", state 496, "(1)"
	line 432, ".input.spin", state 496, "(1)"
	line 430, ".input.spin", state 501, "((i<1))"
	line 430, ".input.spin", state 501, "((i>=1))"
	line 437, ".input.spin", state 508, "(1)"
	line 437, ".input.spin", state 509, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 437, ".input.spin", state 509, "else"
	line 437, ".input.spin", state 512, "(1)"
	line 437, ".input.spin", state 513, "(1)"
	line 437, ".input.spin", state 513, "(1)"
	line 441, ".input.spin", state 521, "(1)"
	line 441, ".input.spin", state 522, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 441, ".input.spin", state 522, "else"
	line 441, ".input.spin", state 525, "(1)"
	line 441, ".input.spin", state 526, "(1)"
	line 441, ".input.spin", state 526, "(1)"
	line 439, ".input.spin", state 531, "((i<2))"
	line 439, ".input.spin", state 531, "((i>=2))"
	line 449, ".input.spin", state 535, "(1)"
	line 449, ".input.spin", state 535, "(1)"
	line 596, ".input.spin", state 538, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
	line 596, ".input.spin", state 539, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
	line 596, ".input.spin", state 540, "(1)"
	line 271, ".input.spin", state 544, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 275, ".input.spin", state 555, "(1)"
	line 279, ".input.spin", state 566, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 575, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 591, "(1)"
	line 252, ".input.spin", state 599, "(1)"
	line 256, ".input.spin", state 611, "(1)"
	line 260, ".input.spin", state 619, "(1)"
	line 410, ".input.spin", state 637, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 651, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 669, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 683, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 702, "(1)"
	line 432, ".input.spin", state 715, "(1)"
	line 437, ".input.spin", state 732, "(1)"
	line 441, ".input.spin", state 745, "(1)"
	line 410, ".input.spin", state 773, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 805, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 819, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 838, "(1)"
	line 437, ".input.spin", state 868, "(1)"
	line 441, ".input.spin", state 881, "(1)"
	line 410, ".input.spin", state 902, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 410, ".input.spin", state 904, "(1)"
	line 410, ".input.spin", state 905, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 410, ".input.spin", state 905, "else"
	line 410, ".input.spin", state 908, "(1)"
	line 414, ".input.spin", state 916, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 918, "(1)"
	line 414, ".input.spin", state 919, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 414, ".input.spin", state 919, "else"
	line 414, ".input.spin", state 922, "(1)"
	line 414, ".input.spin", state 923, "(1)"
	line 414, ".input.spin", state 923, "(1)"
	line 412, ".input.spin", state 928, "((i<1))"
	line 412, ".input.spin", state 928, "((i>=1))"
	line 419, ".input.spin", state 934, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 936, "(1)"
	line 419, ".input.spin", state 937, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 419, ".input.spin", state 937, "else"
	line 419, ".input.spin", state 940, "(1)"
	line 419, ".input.spin", state 941, "(1)"
	line 419, ".input.spin", state 941, "(1)"
	line 423, ".input.spin", state 948, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 950, "(1)"
	line 423, ".input.spin", state 951, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 423, ".input.spin", state 951, "else"
	line 423, ".input.spin", state 954, "(1)"
	line 423, ".input.spin", state 955, "(1)"
	line 423, ".input.spin", state 955, "(1)"
	line 421, ".input.spin", state 960, "((i<2))"
	line 421, ".input.spin", state 960, "((i>=2))"
	line 428, ".input.spin", state 967, "(1)"
	line 428, ".input.spin", state 968, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 428, ".input.spin", state 968, "else"
	line 428, ".input.spin", state 971, "(1)"
	line 428, ".input.spin", state 972, "(1)"
	line 428, ".input.spin", state 972, "(1)"
	line 432, ".input.spin", state 980, "(1)"
	line 432, ".input.spin", state 981, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 432, ".input.spin", state 981, "else"
	line 432, ".input.spin", state 984, "(1)"
	line 432, ".input.spin", state 985, "(1)"
	line 432, ".input.spin", state 985, "(1)"
	line 430, ".input.spin", state 990, "((i<1))"
	line 430, ".input.spin", state 990, "((i>=1))"
	line 437, ".input.spin", state 997, "(1)"
	line 437, ".input.spin", state 998, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 437, ".input.spin", state 998, "else"
	line 437, ".input.spin", state 1001, "(1)"
	line 437, ".input.spin", state 1002, "(1)"
	line 437, ".input.spin", state 1002, "(1)"
	line 441, ".input.spin", state 1010, "(1)"
	line 441, ".input.spin", state 1011, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 441, ".input.spin", state 1011, "else"
	line 441, ".input.spin", state 1014, "(1)"
	line 441, ".input.spin", state 1015, "(1)"
	line 441, ".input.spin", state 1015, "(1)"
	line 439, ".input.spin", state 1020, "((i<2))"
	line 439, ".input.spin", state 1020, "((i>=2))"
	line 449, ".input.spin", state 1024, "(1)"
	line 449, ".input.spin", state 1024, "(1)"
	line 604, ".input.spin", state 1028, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
	line 410, ".input.spin", state 1033, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 1047, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1065, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1079, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 1098, "(1)"
	line 432, ".input.spin", state 1111, "(1)"
	line 437, ".input.spin", state 1128, "(1)"
	line 441, ".input.spin", state 1141, "(1)"
	line 410, ".input.spin", state 1165, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1197, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1211, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 1230, "(1)"
	line 437, ".input.spin", state 1260, "(1)"
	line 441, ".input.spin", state 1273, "(1)"
	line 410, ".input.spin", state 1298, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1330, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1344, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 1363, "(1)"
	line 437, ".input.spin", state 1393, "(1)"
	line 441, ".input.spin", state 1406, "(1)"
	line 410, ".input.spin", state 1427, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1459, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1473, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 1492, "(1)"
	line 437, ".input.spin", state 1522, "(1)"
	line 441, ".input.spin", state 1535, "(1)"
	line 271, ".input.spin", state 1558, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 1580, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 1589, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1605, "(1)"
	line 252, ".input.spin", state 1613, "(1)"
	line 256, ".input.spin", state 1625, "(1)"
	line 260, ".input.spin", state 1633, "(1)"
	line 410, ".input.spin", state 1651, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 1665, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1683, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1697, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 1716, "(1)"
	line 432, ".input.spin", state 1729, "(1)"
	line 437, ".input.spin", state 1746, "(1)"
	line 441, ".input.spin", state 1759, "(1)"
	line 410, ".input.spin", state 1780, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 1794, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1812, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1826, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 1845, "(1)"
	line 432, ".input.spin", state 1858, "(1)"
	line 437, ".input.spin", state 1875, "(1)"
	line 441, ".input.spin", state 1888, "(1)"
	line 410, ".input.spin", state 1912, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1944, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1958, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 1977, "(1)"
	line 437, ".input.spin", state 2007, "(1)"
	line 441, ".input.spin", state 2020, "(1)"
	line 643, ".input.spin", state 2041, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
	line 410, ".input.spin", state 2048, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2080, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2094, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 2113, "(1)"
	line 437, ".input.spin", state 2143, "(1)"
	line 441, ".input.spin", state 2156, "(1)"
	line 410, ".input.spin", state 2177, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2209, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2223, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 2242, "(1)"
	line 437, ".input.spin", state 2272, "(1)"
	line 441, ".input.spin", state 2285, "(1)"
	line 410, ".input.spin", state 2308, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 410, ".input.spin", state 2310, "(1)"
	line 410, ".input.spin", state 2311, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 410, ".input.spin", state 2311, "else"
	line 410, ".input.spin", state 2314, "(1)"
	line 414, ".input.spin", state 2322, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 2324, "(1)"
	line 414, ".input.spin", state 2325, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 414, ".input.spin", state 2325, "else"
	line 414, ".input.spin", state 2328, "(1)"
	line 414, ".input.spin", state 2329, "(1)"
	line 414, ".input.spin", state 2329, "(1)"
	line 412, ".input.spin", state 2334, "((i<1))"
	line 412, ".input.spin", state 2334, "((i>=1))"
	line 419, ".input.spin", state 2340, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2342, "(1)"
	line 419, ".input.spin", state 2343, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 419, ".input.spin", state 2343, "else"
	line 419, ".input.spin", state 2346, "(1)"
	line 419, ".input.spin", state 2347, "(1)"
	line 419, ".input.spin", state 2347, "(1)"
	line 423, ".input.spin", state 2354, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2356, "(1)"
	line 423, ".input.spin", state 2357, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 423, ".input.spin", state 2357, "else"
	line 423, ".input.spin", state 2360, "(1)"
	line 423, ".input.spin", state 2361, "(1)"
	line 423, ".input.spin", state 2361, "(1)"
	line 421, ".input.spin", state 2366, "((i<2))"
	line 421, ".input.spin", state 2366, "((i>=2))"
	line 428, ".input.spin", state 2373, "(1)"
	line 428, ".input.spin", state 2374, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 428, ".input.spin", state 2374, "else"
	line 428, ".input.spin", state 2377, "(1)"
	line 428, ".input.spin", state 2378, "(1)"
	line 428, ".input.spin", state 2378, "(1)"
	line 432, ".input.spin", state 2386, "(1)"
	line 432, ".input.spin", state 2387, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 432, ".input.spin", state 2387, "else"
	line 432, ".input.spin", state 2390, "(1)"
	line 432, ".input.spin", state 2391, "(1)"
	line 432, ".input.spin", state 2391, "(1)"
	line 430, ".input.spin", state 2396, "((i<1))"
	line 430, ".input.spin", state 2396, "((i>=1))"
	line 437, ".input.spin", state 2403, "(1)"
	line 437, ".input.spin", state 2404, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 437, ".input.spin", state 2404, "else"
	line 437, ".input.spin", state 2407, "(1)"
	line 437, ".input.spin", state 2408, "(1)"
	line 437, ".input.spin", state 2408, "(1)"
	line 441, ".input.spin", state 2416, "(1)"
	line 441, ".input.spin", state 2417, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 441, ".input.spin", state 2417, "else"
	line 441, ".input.spin", state 2420, "(1)"
	line 441, ".input.spin", state 2421, "(1)"
	line 441, ".input.spin", state 2421, "(1)"
	line 439, ".input.spin", state 2426, "((i<2))"
	line 439, ".input.spin", state 2426, "((i>=2))"
	line 449, ".input.spin", state 2430, "(1)"
	line 449, ".input.spin", state 2430, "(1)"
	line 643, ".input.spin", state 2433, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
	line 643, ".input.spin", state 2434, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
	line 643, ".input.spin", state 2435, "(1)"
	line 271, ".input.spin", state 2439, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 2461, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 2470, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 2486, "(1)"
	line 252, ".input.spin", state 2494, "(1)"
	line 256, ".input.spin", state 2506, "(1)"
	line 260, ".input.spin", state 2514, "(1)"
	line 410, ".input.spin", state 2532, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 2546, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2564, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2578, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 2597, "(1)"
	line 432, ".input.spin", state 2610, "(1)"
	line 437, ".input.spin", state 2627, "(1)"
	line 441, ".input.spin", state 2640, "(1)"
	line 271, ".input.spin", state 2664, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 275, ".input.spin", state 2673, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 2686, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 2695, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 2711, "(1)"
	line 252, ".input.spin", state 2719, "(1)"
	line 256, ".input.spin", state 2731, "(1)"
	line 260, ".input.spin", state 2739, "(1)"
	line 410, ".input.spin", state 2757, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 2771, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2789, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2803, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 2822, "(1)"
	line 432, ".input.spin", state 2835, "(1)"
	line 437, ".input.spin", state 2852, "(1)"
	line 441, ".input.spin", state 2865, "(1)"
	line 410, ".input.spin", state 2886, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 2900, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2918, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2932, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 2951, "(1)"
	line 432, ".input.spin", state 2964, "(1)"
	line 437, ".input.spin", state 2981, "(1)"
	line 441, ".input.spin", state 2994, "(1)"
	line 248, ".input.spin", state 3027, "(1)"
	line 256, ".input.spin", state 3047, "(1)"
	line 260, ".input.spin", state 3055, "(1)"
	line 248, ".input.spin", state 3070, "(1)"
	line 252, ".input.spin", state 3078, "(1)"
	line 256, ".input.spin", state 3090, "(1)"
	line 260, ".input.spin", state 3098, "(1)"
	line 897, ".input.spin", state 3115, "-end-"
	(283 of 3115 states)
unreached in proctype urcu_writer
	line 410, ".input.spin", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 83, "(1)"
	line 432, ".input.spin", state 96, "(1)"
	line 437, ".input.spin", state 113, "(1)"
	line 271, ".input.spin", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 275, ".input.spin", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 410, ".input.spin", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 428, ".input.spin", state 276, "(1)"
	line 432, ".input.spin", state 289, "(1)"
	line 437, ".input.spin", state 306, "(1)"
	line 441, ".input.spin", state 319, "(1)"
	line 414, ".input.spin", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 432, ".input.spin", state 420, "(1)"
	line 437, ".input.spin", state 437, "(1)"
	line 441, ".input.spin", state 450, "(1)"
	line 414, ".input.spin", state 495, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 513, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 527, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 432, ".input.spin", state 559, "(1)"
	line 437, ".input.spin", state 576, "(1)"
	line 441, ".input.spin", state 589, "(1)"
	line 414, ".input.spin", state 624, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 642, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 656, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 432, ".input.spin", state 688, "(1)"
	line 437, ".input.spin", state 705, "(1)"
	line 441, ".input.spin", state 718, "(1)"
	line 414, ".input.spin", state 755, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 773, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 787, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 432, ".input.spin", state 819, "(1)"
	line 437, ".input.spin", state 836, "(1)"
	line 441, ".input.spin", state 849, "(1)"
	line 271, ".input.spin", state 904, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 275, ".input.spin", state 913, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 928, "(1)"
	line 283, ".input.spin", state 935, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 951, "(1)"
	line 252, ".input.spin", state 959, "(1)"
	line 256, ".input.spin", state 971, "(1)"
	line 260, ".input.spin", state 979, "(1)"
	line 275, ".input.spin", state 1004, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 1017, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 1026, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1042, "(1)"
	line 252, ".input.spin", state 1050, "(1)"
	line 256, ".input.spin", state 1062, "(1)"
	line 260, ".input.spin", state 1070, "(1)"
	line 275, ".input.spin", state 1095, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 1108, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 1117, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1133, "(1)"
	line 252, ".input.spin", state 1141, "(1)"
	line 256, ".input.spin", state 1153, "(1)"
	line 260, ".input.spin", state 1161, "(1)"
	line 275, ".input.spin", state 1186, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 1199, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 1208, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1224, "(1)"
	line 252, ".input.spin", state 1232, "(1)"
	line 256, ".input.spin", state 1244, "(1)"
	line 260, ".input.spin", state 1252, "(1)"
	line 1236, ".input.spin", state 1267, "-end-"
	(71 of 1267 states)
unreached in proctype :init:
	(0 of 78 states)

pan: elapsed time 4.59e+03 seconds
pan: rate 1460.6376 states/second
pan: avg transition delay 1.0334e-06 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-controldataflow-alpha-no-ipi'