make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
rm -f pan* trail.out .input.spin* *.spin.trail .input.define
cat DEFINES > .input.spin
cat urcu.spin >> .input.spin
rm -f .input.spin.trail
spin -a -X .input.spin
Exit-Status 0
gcc -O2 -w -DHASH64 -DSAFETY -o pan pan.c
./pan -v -c1 -X -m10000000 -w20

(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 48 byte, depth reached 2084, errors: 0
   847558 states, stored
  9221089 states, matched
 10068647 transitions (= stored+matched)
 36786866 atomic steps
hash conflicts:   2126850 (resolved)

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

unreached in proctype urcu_reader
	line 398, ".input.spin", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 61, "(1)"
	line 417, ".input.spin", state 91, "(1)"
	line 398, ".input.spin", state 106, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 138, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 151, "(1)"
	line 417, ".input.spin", state 181, "(1)"
	line 398, ".input.spin", state 197, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 229, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 242, "(1)"
	line 417, ".input.spin", state 272, "(1)"
	line 398, ".input.spin", state 315, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 347, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 360, "(1)"
	line 417, ".input.spin", state 390, "(1)"
	line 539, ".input.spin", state 414, "-end-"
	(17 of 414 states)
unreached in proctype urcu_writer
	line 398, ".input.spin", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 402, ".input.spin", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 59, "(1)"
	line 412, ".input.spin", state 72, "(1)"
	line 417, ".input.spin", state 89, "(1)"
	line 398, ".input.spin", state 108, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 402, ".input.spin", state 122, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 153, "(1)"
	line 412, ".input.spin", state 166, "(1)"
	line 651, ".input.spin", state 199, "(1)"
	line 174, ".input.spin", state 208, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 178, ".input.spin", state 217, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 159, ".input.spin", state 240, "(1)"
	line 163, ".input.spin", state 248, "(1)"
	line 167, ".input.spin", state 260, "(1)"
	line 174, ".input.spin", state 271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
	line 182, ".input.spin", state 293, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
	line 159, ".input.spin", state 303, "(1)"
	line 163, ".input.spin", state 311, "(1)"
	line 167, ".input.spin", state 323, "(1)"
	line 174, ".input.spin", state 338, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 178, ".input.spin", state 347, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 182, ".input.spin", state 360, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 159, ".input.spin", state 370, "(1)"
	line 163, ".input.spin", state 378, "(1)"
	line 167, ".input.spin", state 390, "(1)"
	line 398, ".input.spin", state 404, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 402, ".input.spin", state 418, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 436, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 449, "(1)"
	line 412, ".input.spin", state 462, "(1)"
	line 417, ".input.spin", state 479, "(1)"
	line 398, ".input.spin", state 498, "(1)"
	line 402, ".input.spin", state 510, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 528, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 412, ".input.spin", state 554, "(1)"
	line 417, ".input.spin", state 571, "(1)"
	line 402, ".input.spin", state 603, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 621, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 412, ".input.spin", state 647, "(1)"
	line 417, ".input.spin", state 664, "(1)"
	line 178, ".input.spin", state 687, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 182, ".input.spin", state 700, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 159, ".input.spin", state 710, "(1)"
	line 163, ".input.spin", state 718, "(1)"
	line 167, ".input.spin", state 730, "(1)"
	line 174, ".input.spin", state 741, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
	line 182, ".input.spin", state 763, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
	line 159, ".input.spin", state 773, "(1)"
	line 163, ".input.spin", state 781, "(1)"
	line 167, ".input.spin", state 793, "(1)"
	line 174, ".input.spin", state 808, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 178, ".input.spin", state 817, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 182, ".input.spin", state 830, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 159, ".input.spin", state 840, "(1)"
	line 163, ".input.spin", state 848, "(1)"
	line 167, ".input.spin", state 860, "(1)"
	line 398, ".input.spin", state 882, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 884, "(1)"
	line 398, ".input.spin", state 885, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 398, ".input.spin", state 885, "else"
	line 398, ".input.spin", state 888, "(1)"
	line 402, ".input.spin", state 896, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 402, ".input.spin", state 898, "(1)"
	line 402, ".input.spin", state 899, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 402, ".input.spin", state 899, "else"
	line 402, ".input.spin", state 902, "(1)"
	line 402, ".input.spin", state 903, "(1)"
	line 402, ".input.spin", state 903, "(1)"
	line 400, ".input.spin", state 908, "((i<1))"
	line 400, ".input.spin", state 908, "((i>=1))"
	line 407, ".input.spin", state 914, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 927, "(1)"
	line 408, ".input.spin", state 928, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 408, ".input.spin", state 928, "else"
	line 408, ".input.spin", state 931, "(1)"
	line 408, ".input.spin", state 932, "(1)"
	line 408, ".input.spin", state 932, "(1)"
	line 412, ".input.spin", state 940, "(1)"
	line 412, ".input.spin", state 941, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 412, ".input.spin", state 941, "else"
	line 412, ".input.spin", state 944, "(1)"
	line 412, ".input.spin", state 945, "(1)"
	line 412, ".input.spin", state 945, "(1)"
	line 410, ".input.spin", state 950, "((i<1))"
	line 410, ".input.spin", state 950, "((i>=1))"
	line 417, ".input.spin", state 957, "(1)"
	line 417, ".input.spin", state 958, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
	line 417, ".input.spin", state 958, "else"
	line 417, ".input.spin", state 961, "(1)"
	line 417, ".input.spin", state 962, "(1)"
	line 417, ".input.spin", state 962, "(1)"
	line 419, ".input.spin", state 965, "(1)"
	line 419, ".input.spin", state 965, "(1)"
	line 402, ".input.spin", state 996, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1014, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 412, ".input.spin", state 1040, "(1)"
	line 417, ".input.spin", state 1057, "(1)"
	line 402, ".input.spin", state 1086, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1104, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 412, ".input.spin", state 1130, "(1)"
	line 417, ".input.spin", state 1147, "(1)"
	line 398, ".input.spin", state 1166, "(1)"
	line 402, ".input.spin", state 1178, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1196, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 412, ".input.spin", state 1222, "(1)"
	line 417, ".input.spin", state 1239, "(1)"
	line 402, ".input.spin", state 1271, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 407, ".input.spin", state 1289, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 412, ".input.spin", state 1315, "(1)"
	line 417, ".input.spin", state 1332, "(1)"
	line 178, ".input.spin", state 1355, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 182, ".input.spin", state 1368, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 159, ".input.spin", state 1378, "(1)"
	line 163, ".input.spin", state 1386, "(1)"
	line 167, ".input.spin", state 1398, "(1)"
	line 174, ".input.spin", state 1409, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
	line 182, ".input.spin", state 1431, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
	line 159, ".input.spin", state 1441, "(1)"
	line 163, ".input.spin", state 1449, "(1)"
	line 167, ".input.spin", state 1461, "(1)"
	line 174, ".input.spin", state 1476, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 178, ".input.spin", state 1485, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 182, ".input.spin", state 1498, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 159, ".input.spin", state 1508, "(1)"
	line 163, ".input.spin", state 1516, "(1)"
	line 167, ".input.spin", state 1528, "(1)"
	line 398, ".input.spin", state 1550, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 398, ".input.spin", state 1552, "(1)"
	line 398, ".input.spin", state 1553, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 398, ".input.spin", state 1553, "else"
	line 398, ".input.spin", state 1556, "(1)"
	line 402, ".input.spin", state 1564, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 402, ".input.spin", state 1566, "(1)"
	line 402, ".input.spin", state 1567, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 402, ".input.spin", state 1567, "else"
	line 402, ".input.spin", state 1570, "(1)"
	line 402, ".input.spin", state 1571, "(1)"
	line 402, ".input.spin", state 1571, "(1)"
	line 400, ".input.spin", state 1576, "((i<1))"
	line 400, ".input.spin", state 1576, "((i>=1))"
	line 407, ".input.spin", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 408, ".input.spin", state 1595, "(1)"
	line 408, ".input.spin", state 1596, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 408, ".input.spin", state 1596, "else"
	line 408, ".input.spin", state 1599, "(1)"
	line 408, ".input.spin", state 1600, "(1)"
	line 408, ".input.spin", state 1600, "(1)"
	line 412, ".input.spin", state 1608, "(1)"
	line 412, ".input.spin", state 1609, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 412, ".input.spin", state 1609, "else"
	line 412, ".input.spin", state 1612, "(1)"
	line 412, ".input.spin", state 1613, "(1)"
	line 412, ".input.spin", state 1613, "(1)"
	line 410, ".input.spin", state 1618, "((i<1))"
	line 410, ".input.spin", state 1618, "((i>=1))"
	line 417, ".input.spin", state 1625, "(1)"
	line 417, ".input.spin", state 1626, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
	line 417, ".input.spin", state 1626, "else"
	line 417, ".input.spin", state 1629, "(1)"
	line 417, ".input.spin", state 1630, "(1)"
	line 417, ".input.spin", state 1630, "(1)"
	line 419, ".input.spin", state 1633, "(1)"
	line 419, ".input.spin", state 1633, "(1)"
	line 178, ".input.spin", state 1658, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 182, ".input.spin", state 1671, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 159, ".input.spin", state 1681, "(1)"
	line 163, ".input.spin", state 1689, "(1)"
	line 167, ".input.spin", state 1701, "(1)"
	line 174, ".input.spin", state 1712, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
	line 182, ".input.spin", state 1734, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
	line 159, ".input.spin", state 1744, "(1)"
	line 163, ".input.spin", state 1752, "(1)"
	line 167, ".input.spin", state 1764, "(1)"
	line 174, ".input.spin", state 1779, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 178, ".input.spin", state 1788, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 182, ".input.spin", state 1801, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
	line 159, ".input.spin", state 1811, "(1)"
	line 163, ".input.spin", state 1819, "(1)"
	line 167, ".input.spin", state 1831, "(1)"
	line 701, ".input.spin", state 1856, "-end-"
	(158 of 1856 states)
unreached in proctype :init:
	(0 of 46 states)

pan: elapsed time 6.68 seconds
pan: rate 126879.94 states/second
pan: avg transition delay 6.6345e-07 usec
cp .input.spin asserts.spin.input
cp .input.spin.trail asserts.spin.input.trail
make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'