make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-intel-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=    4473 States=    1e+06 Transitions= 2.37e+07 Memory=   542.619	t=   57.3 R=   2e+04
Depth=    4540 States=    2e+06 Transitions=  4.8e+07 Memory=   618.889	t=    117 R=   2e+04
Depth=    4540 States=    3e+06 Transitions= 7.25e+07 Memory=   695.158	t=    178 R=   2e+04
pan: resizing hashtable to -w22..  done

(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 4540, errors: 0
  3841511 states, stored
 90242688 states, matched
 94084199 transitions (= stored+matched)
1.5073578e+09 atomic steps
hash conflicts:  63759942 (resolved)

Stats on memory usage (in Megabytes):
  366.355	equivalent memory usage for states (stored*(State-vector + overhead))
  300.680	actual memory usage for states (compression: 82.07%)
         	state-vector as stored = 54 byte + 28 byte overhead
   32.000	memory used for hash table (-w22)
  457.764	memory used for DFS stack (-m10000000)
  790.440	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 248, ".input.spin", state 81, "(1)"
	line 256, ".input.spin", state 101, "(1)"
	line 260, ".input.spin", state 109, "(1)"
	line 596, ".input.spin", state 128, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
	line 410, ".input.spin", state 135, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 167, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 181, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 199, "(1)"
	line 256, ".input.spin", state 219, "(1)"
	line 260, ".input.spin", state 227, "(1)"
	line 410, ".input.spin", state 246, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 278, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 292, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 310, "(1)"
	line 256, ".input.spin", state 330, "(1)"
	line 260, ".input.spin", state 338, "(1)"
	line 410, ".input.spin", state 359, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 410, ".input.spin", state 361, "(1)"
	line 410, ".input.spin", state 362, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 410, ".input.spin", state 362, "else"
	line 410, ".input.spin", state 365, "(1)"
	line 414, ".input.spin", state 373, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 375, "(1)"
	line 414, ".input.spin", state 376, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 414, ".input.spin", state 376, "else"
	line 414, ".input.spin", state 379, "(1)"
	line 414, ".input.spin", state 380, "(1)"
	line 414, ".input.spin", state 380, "(1)"
	line 412, ".input.spin", state 385, "((i<1))"
	line 412, ".input.spin", state 385, "((i>=1))"
	line 419, ".input.spin", state 391, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 393, "(1)"
	line 419, ".input.spin", state 394, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 419, ".input.spin", state 394, "else"
	line 419, ".input.spin", state 397, "(1)"
	line 419, ".input.spin", state 398, "(1)"
	line 419, ".input.spin", state 398, "(1)"
	line 423, ".input.spin", state 405, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 407, "(1)"
	line 423, ".input.spin", state 408, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 423, ".input.spin", state 408, "else"
	line 423, ".input.spin", state 411, "(1)"
	line 423, ".input.spin", state 412, "(1)"
	line 423, ".input.spin", state 412, "(1)"
	line 421, ".input.spin", state 417, "((i<2))"
	line 421, ".input.spin", state 417, "((i>=2))"
	line 248, ".input.spin", state 423, "(1)"
	line 252, ".input.spin", state 431, "(1)"
	line 252, ".input.spin", state 432, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 252, ".input.spin", state 432, "else"
	line 250, ".input.spin", state 437, "((i<1))"
	line 250, ".input.spin", state 437, "((i>=1))"
	line 256, ".input.spin", state 443, "(1)"
	line 256, ".input.spin", state 444, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 256, ".input.spin", state 444, "else"
	line 260, ".input.spin", state 451, "(1)"
	line 260, ".input.spin", state 452, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 260, ".input.spin", state 452, "else"
	line 258, ".input.spin", state 457, "((i<2))"
	line 258, ".input.spin", state 457, "((i>=2))"
	line 265, ".input.spin", state 461, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 265, ".input.spin", state 461, "else"
	line 430, ".input.spin", state 463, "(1)"
	line 430, ".input.spin", state 463, "(1)"
	line 596, ".input.spin", state 466, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
	line 596, ".input.spin", state 467, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
	line 596, ".input.spin", state 468, "(1)"
	line 271, ".input.spin", state 472, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 275, ".input.spin", state 483, "(1)"
	line 279, ".input.spin", state 494, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 503, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 519, "(1)"
	line 252, ".input.spin", state 527, "(1)"
	line 256, ".input.spin", state 539, "(1)"
	line 260, ".input.spin", state 547, "(1)"
	line 410, ".input.spin", state 565, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 579, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 597, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 611, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 629, "(1)"
	line 252, ".input.spin", state 637, "(1)"
	line 256, ".input.spin", state 649, "(1)"
	line 260, ".input.spin", state 657, "(1)"
	line 410, ".input.spin", state 683, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 715, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 729, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 747, "(1)"
	line 256, ".input.spin", state 767, "(1)"
	line 260, ".input.spin", state 775, "(1)"
	line 410, ".input.spin", state 794, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 410, ".input.spin", state 796, "(1)"
	line 410, ".input.spin", state 797, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 410, ".input.spin", state 797, "else"
	line 410, ".input.spin", state 800, "(1)"
	line 414, ".input.spin", state 808, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 810, "(1)"
	line 414, ".input.spin", state 811, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 414, ".input.spin", state 811, "else"
	line 414, ".input.spin", state 814, "(1)"
	line 414, ".input.spin", state 815, "(1)"
	line 414, ".input.spin", state 815, "(1)"
	line 412, ".input.spin", state 820, "((i<1))"
	line 412, ".input.spin", state 820, "((i>=1))"
	line 419, ".input.spin", state 826, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 828, "(1)"
	line 419, ".input.spin", state 829, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 419, ".input.spin", state 829, "else"
	line 419, ".input.spin", state 832, "(1)"
	line 419, ".input.spin", state 833, "(1)"
	line 419, ".input.spin", state 833, "(1)"
	line 423, ".input.spin", state 840, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 842, "(1)"
	line 423, ".input.spin", state 843, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 423, ".input.spin", state 843, "else"
	line 423, ".input.spin", state 846, "(1)"
	line 423, ".input.spin", state 847, "(1)"
	line 423, ".input.spin", state 847, "(1)"
	line 421, ".input.spin", state 852, "((i<2))"
	line 421, ".input.spin", state 852, "((i>=2))"
	line 248, ".input.spin", state 858, "(1)"
	line 252, ".input.spin", state 866, "(1)"
	line 252, ".input.spin", state 867, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 252, ".input.spin", state 867, "else"
	line 250, ".input.spin", state 872, "((i<1))"
	line 250, ".input.spin", state 872, "((i>=1))"
	line 256, ".input.spin", state 878, "(1)"
	line 256, ".input.spin", state 879, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 256, ".input.spin", state 879, "else"
	line 260, ".input.spin", state 886, "(1)"
	line 260, ".input.spin", state 887, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 260, ".input.spin", state 887, "else"
	line 258, ".input.spin", state 892, "((i<2))"
	line 258, ".input.spin", state 892, "((i>=2))"
	line 265, ".input.spin", state 896, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 265, ".input.spin", state 896, "else"
	line 430, ".input.spin", state 898, "(1)"
	line 430, ".input.spin", state 898, "(1)"
	line 604, ".input.spin", state 902, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
	line 410, ".input.spin", state 907, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 921, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 939, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 953, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 971, "(1)"
	line 252, ".input.spin", state 979, "(1)"
	line 256, ".input.spin", state 991, "(1)"
	line 260, ".input.spin", state 999, "(1)"
	line 410, ".input.spin", state 1021, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1053, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1067, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1085, "(1)"
	line 256, ".input.spin", state 1105, "(1)"
	line 260, ".input.spin", state 1113, "(1)"
	line 410, ".input.spin", state 1136, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1168, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1182, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1200, "(1)"
	line 256, ".input.spin", state 1220, "(1)"
	line 260, ".input.spin", state 1228, "(1)"
	line 410, ".input.spin", state 1247, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1279, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1293, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1311, "(1)"
	line 256, ".input.spin", state 1331, "(1)"
	line 260, ".input.spin", state 1339, "(1)"
	line 271, ".input.spin", state 1360, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 1382, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 1391, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1407, "(1)"
	line 252, ".input.spin", state 1415, "(1)"
	line 256, ".input.spin", state 1427, "(1)"
	line 260, ".input.spin", state 1435, "(1)"
	line 410, ".input.spin", state 1453, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 1467, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1485, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1499, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1517, "(1)"
	line 252, ".input.spin", state 1525, "(1)"
	line 256, ".input.spin", state 1537, "(1)"
	line 260, ".input.spin", state 1545, "(1)"
	line 410, ".input.spin", state 1564, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 1578, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1596, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1610, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1628, "(1)"
	line 252, ".input.spin", state 1636, "(1)"
	line 256, ".input.spin", state 1648, "(1)"
	line 260, ".input.spin", state 1656, "(1)"
	line 410, ".input.spin", state 1678, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1710, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1724, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1742, "(1)"
	line 256, ".input.spin", state 1762, "(1)"
	line 260, ".input.spin", state 1770, "(1)"
	line 643, ".input.spin", state 1789, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
	line 410, ".input.spin", state 1796, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1828, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1842, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1860, "(1)"
	line 256, ".input.spin", state 1880, "(1)"
	line 260, ".input.spin", state 1888, "(1)"
	line 410, ".input.spin", state 1907, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 1939, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 1953, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1971, "(1)"
	line 256, ".input.spin", state 1991, "(1)"
	line 260, ".input.spin", state 1999, "(1)"
	line 410, ".input.spin", state 2020, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 410, ".input.spin", state 2022, "(1)"
	line 410, ".input.spin", state 2023, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 410, ".input.spin", state 2023, "else"
	line 410, ".input.spin", state 2026, "(1)"
	line 414, ".input.spin", state 2034, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 2036, "(1)"
	line 414, ".input.spin", state 2037, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 414, ".input.spin", state 2037, "else"
	line 414, ".input.spin", state 2040, "(1)"
	line 414, ".input.spin", state 2041, "(1)"
	line 414, ".input.spin", state 2041, "(1)"
	line 412, ".input.spin", state 2046, "((i<1))"
	line 412, ".input.spin", state 2046, "((i>=1))"
	line 419, ".input.spin", state 2052, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2054, "(1)"
	line 419, ".input.spin", state 2055, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 419, ".input.spin", state 2055, "else"
	line 419, ".input.spin", state 2058, "(1)"
	line 419, ".input.spin", state 2059, "(1)"
	line 419, ".input.spin", state 2059, "(1)"
	line 423, ".input.spin", state 2066, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2068, "(1)"
	line 423, ".input.spin", state 2069, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 423, ".input.spin", state 2069, "else"
	line 423, ".input.spin", state 2072, "(1)"
	line 423, ".input.spin", state 2073, "(1)"
	line 423, ".input.spin", state 2073, "(1)"
	line 421, ".input.spin", state 2078, "((i<2))"
	line 421, ".input.spin", state 2078, "((i>=2))"
	line 248, ".input.spin", state 2084, "(1)"
	line 252, ".input.spin", state 2092, "(1)"
	line 252, ".input.spin", state 2093, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 252, ".input.spin", state 2093, "else"
	line 250, ".input.spin", state 2098, "((i<1))"
	line 250, ".input.spin", state 2098, "((i>=1))"
	line 256, ".input.spin", state 2104, "(1)"
	line 256, ".input.spin", state 2105, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 256, ".input.spin", state 2105, "else"
	line 260, ".input.spin", state 2112, "(1)"
	line 260, ".input.spin", state 2113, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 260, ".input.spin", state 2113, "else"
	line 258, ".input.spin", state 2118, "((i<2))"
	line 258, ".input.spin", state 2118, "((i>=2))"
	line 265, ".input.spin", state 2122, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 265, ".input.spin", state 2122, "else"
	line 430, ".input.spin", state 2124, "(1)"
	line 430, ".input.spin", state 2124, "(1)"
	line 643, ".input.spin", state 2127, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
	line 643, ".input.spin", state 2128, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
	line 643, ".input.spin", state 2129, "(1)"
	line 271, ".input.spin", state 2133, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 2155, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 2164, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 2180, "(1)"
	line 252, ".input.spin", state 2188, "(1)"
	line 256, ".input.spin", state 2200, "(1)"
	line 260, ".input.spin", state 2208, "(1)"
	line 410, ".input.spin", state 2226, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 2240, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2258, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2272, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 2290, "(1)"
	line 252, ".input.spin", state 2298, "(1)"
	line 256, ".input.spin", state 2310, "(1)"
	line 260, ".input.spin", state 2318, "(1)"
	line 271, ".input.spin", state 2340, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 275, ".input.spin", state 2349, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 2362, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 2371, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 2387, "(1)"
	line 252, ".input.spin", state 2395, "(1)"
	line 256, ".input.spin", state 2407, "(1)"
	line 260, ".input.spin", state 2415, "(1)"
	line 410, ".input.spin", state 2433, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 2447, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2465, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2479, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 2497, "(1)"
	line 252, ".input.spin", state 2505, "(1)"
	line 256, ".input.spin", state 2517, "(1)"
	line 260, ".input.spin", state 2525, "(1)"
	line 410, ".input.spin", state 2544, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 2558, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 2576, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 2590, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 2608, "(1)"
	line 252, ".input.spin", state 2616, "(1)"
	line 256, ".input.spin", state 2628, "(1)"
	line 260, ".input.spin", state 2636, "(1)"
	line 248, ".input.spin", state 2667, "(1)"
	line 256, ".input.spin", state 2687, "(1)"
	line 260, ".input.spin", state 2695, "(1)"
	line 248, ".input.spin", state 2710, "(1)"
	line 252, ".input.spin", state 2718, "(1)"
	line 256, ".input.spin", state 2730, "(1)"
	line 260, ".input.spin", state 2738, "(1)"
	line 897, ".input.spin", state 2755, "-end-"
	(259 of 2755 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 248, ".input.spin", state 82, "(1)"
	line 252, ".input.spin", state 90, "(1)"
	line 256, ".input.spin", state 102, "(1)"
	line 271, ".input.spin", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 275, ".input.spin", state 140, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 153, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 410, ".input.spin", state 193, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 414, ".input.spin", state 207, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 225, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 239, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 257, "(1)"
	line 252, ".input.spin", state 265, "(1)"
	line 256, ".input.spin", state 277, "(1)"
	line 260, ".input.spin", state 285, "(1)"
	line 414, ".input.spin", state 320, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 338, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 352, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 252, ".input.spin", state 378, "(1)"
	line 256, ".input.spin", state 390, "(1)"
	line 260, ".input.spin", state 398, "(1)"
	line 414, ".input.spin", state 441, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 459, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 473, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 252, ".input.spin", state 499, "(1)"
	line 256, ".input.spin", state 511, "(1)"
	line 260, ".input.spin", state 519, "(1)"
	line 414, ".input.spin", state 552, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 570, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 584, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 252, ".input.spin", state 610, "(1)"
	line 256, ".input.spin", state 622, "(1)"
	line 260, ".input.spin", state 630, "(1)"
	line 414, ".input.spin", state 665, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 419, ".input.spin", state 683, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 423, ".input.spin", state 697, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 252, ".input.spin", state 723, "(1)"
	line 256, ".input.spin", state 735, "(1)"
	line 260, ".input.spin", state 743, "(1)"
	line 271, ".input.spin", state 796, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 275, ".input.spin", state 805, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 820, "(1)"
	line 283, ".input.spin", state 827, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 843, "(1)"
	line 252, ".input.spin", state 851, "(1)"
	line 256, ".input.spin", state 863, "(1)"
	line 260, ".input.spin", state 871, "(1)"
	line 275, ".input.spin", state 896, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 909, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 918, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 934, "(1)"
	line 252, ".input.spin", state 942, "(1)"
	line 256, ".input.spin", state 954, "(1)"
	line 260, ".input.spin", state 962, "(1)"
	line 275, ".input.spin", state 987, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 1000, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 1009, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1025, "(1)"
	line 252, ".input.spin", state 1033, "(1)"
	line 256, ".input.spin", state 1045, "(1)"
	line 260, ".input.spin", state 1053, "(1)"
	line 275, ".input.spin", state 1078, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 279, ".input.spin", state 1091, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 283, ".input.spin", state 1100, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 248, ".input.spin", state 1116, "(1)"
	line 252, ".input.spin", state 1124, "(1)"
	line 256, ".input.spin", state 1136, "(1)"
	line 260, ".input.spin", state 1144, "(1)"
	line 1236, ".input.spin", state 1159, "-end-"
	(71 of 1159 states)
unreached in proctype :init:
	(0 of 78 states)

pan: elapsed time 231 seconds
pan: rate 16628.478 states/second
pan: avg transition delay 2.4555e-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-intel-no-ipi'