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 40 byte, depth reached 7872, errors: 0
    20128 states, stored
   191477 states, matched
   211605 transitions (= stored+matched)
   712166 atomic steps
hash conflicts:       942 (resolved)

Stats on memory usage (in Megabytes):
    1.305	equivalent memory usage for states (stored*(State-vector + overhead))
    1.467	actual memory usage for states (unsuccessful compression: 112.36%)
         	state-vector as stored = 48 byte + 28 byte overhead
    8.000	memory used for hash table (-w20)
  457.764	memory used for DFS stack (-m10000000)
  467.229	total actual memory usage

unreached in proctype urcu_reader_sig
	line 401, ".input.spin", state 330, "(1)"
	line 612, ".input.spin", state 411, "-end-"
	(2 of 411 states)
unreached in proctype urcu_writer
	line 397, ".input.spin", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 406, ".input.spin", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 407, ".input.spin", state 59, "(1)"
	line 416, ".input.spin", state 89, "(1)"
	line 397, ".input.spin", state 115, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 407, ".input.spin", state 160, "(1)"
	line 650, ".input.spin", state 213, "(1)"
	line 173, ".input.spin", state 222, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 177, ".input.spin", state 233, "(1)"
	line 158, ".input.spin", state 254, "(1)"
	line 162, ".input.spin", state 262, "(1)"
	line 166, ".input.spin", state 274, "(1)"
	line 173, ".input.spin", state 285, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
	line 177, ".input.spin", state 294, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
	line 181, ".input.spin", state 307, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
	line 158, ".input.spin", state 317, "(1)"
	line 162, ".input.spin", state 325, "(1)"
	line 166, ".input.spin", state 337, "(1)"
	line 173, ".input.spin", state 352, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 177, ".input.spin", state 361, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
	line 181, ".input.spin", state 374, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 158, ".input.spin", state 384, "(1)"
	line 162, ".input.spin", state 392, "(1)"
	line 166, ".input.spin", state 404, "(1)"
	line 397, ".input.spin", state 425, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 401, ".input.spin", state 441, "(1)"
	line 406, ".input.spin", state 457, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 407, ".input.spin", state 470, "(1)"
	line 416, ".input.spin", state 500, "(1)"
	line 397, ".input.spin", state 526, "(1)"
	line 401, ".input.spin", state 540, "(1)"
	line 406, ".input.spin", state 556, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 416, ".input.spin", state 599, "(1)"
	line 401, ".input.spin", state 640, "(1)"
	line 406, ".input.spin", state 656, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 416, ".input.spin", state 699, "(1)"
	line 173, ".input.spin", state 720, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 173, ".input.spin", state 722, "(1)"
	line 177, ".input.spin", state 729, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
	line 177, ".input.spin", state 731, "(1)"
	line 177, ".input.spin", state 732, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
	line 177, ".input.spin", state 732, "else"
	line 175, ".input.spin", state 737, "((j<1))"
	line 175, ".input.spin", state 737, "((j>=1))"
	line 181, ".input.spin", state 742, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 158, ".input.spin", state 752, "(1)"
	line 162, ".input.spin", state 760, "(1)"
	line 162, ".input.spin", state 761, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
	line 162, ".input.spin", state 761, "else"
	line 160, ".input.spin", state 766, "((j<1))"
	line 160, ".input.spin", state 766, "((j>=1))"
	line 166, ".input.spin", state 772, "(1)"
	line 166, ".input.spin", state 773, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
	line 166, ".input.spin", state 773, "else"
	line 168, ".input.spin", state 776, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
	line 168, ".input.spin", state 776, "else"
	line 173, ".input.spin", state 783, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
	line 173, ".input.spin", state 785, "(1)"
	line 177, ".input.spin", state 792, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
	line 177, ".input.spin", state 794, "(1)"
	line 177, ".input.spin", state 795, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
	line 177, ".input.spin", state 795, "else"
	line 175, ".input.spin", state 800, "((j<1))"
	line 175, ".input.spin", state 800, "((j>=1))"
	line 181, ".input.spin", state 805, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
	line 158, ".input.spin", state 815, "(1)"
	line 162, ".input.spin", state 823, "(1)"
	line 162, ".input.spin", state 824, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
	line 162, ".input.spin", state 824, "else"
	line 160, ".input.spin", state 829, "((j<1))"
	line 160, ".input.spin", state 829, "((j>=1))"
	line 166, ".input.spin", state 835, "(1)"
	line 166, ".input.spin", state 836, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
	line 166, ".input.spin", state 836, "else"
	line 168, ".input.spin", state 839, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
	line 168, ".input.spin", state 839, "else"
	line 200, ".input.spin", state 841, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
	line 200, ".input.spin", state 841, "else"
	line 212, ".input.spin", state 845, "((i<1))"
	line 212, ".input.spin", state 845, "((i>=1))"
	line 173, ".input.spin", state 850, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 173, ".input.spin", state 852, "(1)"
	line 177, ".input.spin", state 859, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
	line 177, ".input.spin", state 861, "(1)"
	line 177, ".input.spin", state 862, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
	line 177, ".input.spin", state 862, "else"
	line 175, ".input.spin", state 867, "((j<1))"
	line 175, ".input.spin", state 867, "((j>=1))"
	line 181, ".input.spin", state 872, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 158, ".input.spin", state 882, "(1)"
	line 162, ".input.spin", state 890, "(1)"
	line 162, ".input.spin", state 891, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
	line 162, ".input.spin", state 891, "else"
	line 160, ".input.spin", state 896, "((j<1))"
	line 160, ".input.spin", state 896, "((j>=1))"
	line 166, ".input.spin", state 902, "(1)"
	line 166, ".input.spin", state 903, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
	line 166, ".input.spin", state 903, "else"
	line 168, ".input.spin", state 906, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
	line 168, ".input.spin", state 906, "else"
	line 200, ".input.spin", state 908, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
	line 200, ".input.spin", state 908, "else"
	line 219, ".input.spin", state 909, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
	line 219, ".input.spin", state 909, "else"
	line 354, ".input.spin", state 915, "((sighand_exec==1))"
	line 354, ".input.spin", state 915, "else"
	line 360, ".input.spin", state 918, "sighand_exec = 1"
	line 397, ".input.spin", state 931, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 397, ".input.spin", state 933, "(1)"
	line 397, ".input.spin", state 934, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
	line 397, ".input.spin", state 934, "else"
	line 397, ".input.spin", state 937, "(1)"
	line 401, ".input.spin", state 945, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
	line 401, ".input.spin", state 947, "(1)"
	line 401, ".input.spin", state 948, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
	line 401, ".input.spin", state 948, "else"
	line 401, ".input.spin", state 951, "(1)"
	line 401, ".input.spin", state 952, "(1)"
	line 401, ".input.spin", state 952, "(1)"
	line 399, ".input.spin", state 957, "((i<1))"
	line 399, ".input.spin", state 957, "((i>=1))"
	line 406, ".input.spin", state 963, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 407, ".input.spin", state 976, "(1)"
	line 407, ".input.spin", state 977, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
	line 407, ".input.spin", state 977, "else"
	line 407, ".input.spin", state 980, "(1)"
	line 407, ".input.spin", state 981, "(1)"
	line 407, ".input.spin", state 981, "(1)"
	line 411, ".input.spin", state 989, "(1)"
	line 411, ".input.spin", state 990, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
	line 411, ".input.spin", state 990, "else"
	line 411, ".input.spin", state 993, "(1)"
	line 411, ".input.spin", state 994, "(1)"
	line 411, ".input.spin", state 994, "(1)"
	line 409, ".input.spin", state 999, "((i<1))"
	line 409, ".input.spin", state 999, "((i>=1))"
	line 416, ".input.spin", state 1006, "(1)"
	line 416, ".input.spin", state 1007, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
	line 416, ".input.spin", state 1007, "else"
	line 416, ".input.spin", state 1010, "(1)"
	line 416, ".input.spin", state 1011, "(1)"
	line 416, ".input.spin", state 1011, "(1)"
	line 418, ".input.spin", state 1014, "(1)"
	line 418, ".input.spin", state 1014, "(1)"
	line 360, ".input.spin", state 1023, "sighand_exec = 1"
	line 401, ".input.spin", state 1054, "(1)"
	line 406, ".input.spin", state 1070, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 416, ".input.spin", state 1113, "(1)"
	line 401, ".input.spin", state 1151, "(1)"
	line 406, ".input.spin", state 1167, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 416, ".input.spin", state 1210, "(1)"
	line 397, ".input.spin", state 1236, "(1)"
	line 401, ".input.spin", state 1250, "(1)"
	line 406, ".input.spin", state 1266, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 416, ".input.spin", state 1309, "(1)"
	line 401, ".input.spin", state 1350, "(1)"
	line 406, ".input.spin", state 1366, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 416, ".input.spin", state 1409, "(1)"
	line 173, ".input.spin", state 1430, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 173, ".input.spin", state 1432, "(1)"
	line 177, ".input.spin", state 1439, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
	line 177, ".input.spin", state 1441, "(1)"
	line 177, ".input.spin", state 1442, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
	line 177, ".input.spin", state 1442, "else"
	line 175, ".input.spin", state 1447, "((j<1))"
	line 175, ".input.spin", state 1447, "((j>=1))"
	line 181, ".input.spin", state 1452, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 158, ".input.spin", state 1462, "(1)"
	line 162, ".input.spin", state 1470, "(1)"
	line 162, ".input.spin", state 1471, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
	line 162, ".input.spin", state 1471, "else"
	line 160, ".input.spin", state 1476, "((j<1))"
	line 160, ".input.spin", state 1476, "((j>=1))"
	line 166, ".input.spin", state 1482, "(1)"
	line 166, ".input.spin", state 1483, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
	line 166, ".input.spin", state 1483, "else"
	line 168, ".input.spin", state 1486, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
	line 168, ".input.spin", state 1486, "else"
	line 173, ".input.spin", state 1493, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
	line 173, ".input.spin", state 1495, "(1)"
	line 177, ".input.spin", state 1502, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
	line 177, ".input.spin", state 1504, "(1)"
	line 177, ".input.spin", state 1505, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
	line 177, ".input.spin", state 1505, "else"
	line 175, ".input.spin", state 1510, "((j<1))"
	line 175, ".input.spin", state 1510, "((j>=1))"
	line 181, ".input.spin", state 1515, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
	line 158, ".input.spin", state 1525, "(1)"
	line 162, ".input.spin", state 1533, "(1)"
	line 162, ".input.spin", state 1534, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
	line 162, ".input.spin", state 1534, "else"
	line 160, ".input.spin", state 1539, "((j<1))"
	line 160, ".input.spin", state 1539, "((j>=1))"
	line 166, ".input.spin", state 1545, "(1)"
	line 166, ".input.spin", state 1546, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
	line 166, ".input.spin", state 1546, "else"
	line 168, ".input.spin", state 1549, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
	line 168, ".input.spin", state 1549, "else"
	line 200, ".input.spin", state 1551, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
	line 200, ".input.spin", state 1551, "else"
	line 212, ".input.spin", state 1555, "((i<1))"
	line 212, ".input.spin", state 1555, "((i>=1))"
	line 173, ".input.spin", state 1560, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 173, ".input.spin", state 1562, "(1)"
	line 177, ".input.spin", state 1569, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
	line 177, ".input.spin", state 1571, "(1)"
	line 177, ".input.spin", state 1572, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
	line 177, ".input.spin", state 1572, "else"
	line 175, ".input.spin", state 1577, "((j<1))"
	line 175, ".input.spin", state 1577, "((j>=1))"
	line 181, ".input.spin", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 158, ".input.spin", state 1592, "(1)"
	line 162, ".input.spin", state 1600, "(1)"
	line 162, ".input.spin", state 1601, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
	line 162, ".input.spin", state 1601, "else"
	line 160, ".input.spin", state 1606, "((j<1))"
	line 160, ".input.spin", state 1606, "((j>=1))"
	line 166, ".input.spin", state 1612, "(1)"
	line 166, ".input.spin", state 1613, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
	line 166, ".input.spin", state 1613, "else"
	line 168, ".input.spin", state 1616, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
	line 168, ".input.spin", state 1616, "else"
	line 200, ".input.spin", state 1618, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
	line 200, ".input.spin", state 1618, "else"
	line 219, ".input.spin", state 1619, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
	line 219, ".input.spin", state 1619, "else"
	line 354, ".input.spin", state 1625, "((sighand_exec==1))"
	line 354, ".input.spin", state 1625, "else"
	line 360, ".input.spin", state 1628, "sighand_exec = 1"
	line 397, ".input.spin", state 1641, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 397, ".input.spin", state 1643, "(1)"
	line 397, ".input.spin", state 1644, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
	line 397, ".input.spin", state 1644, "else"
	line 397, ".input.spin", state 1647, "(1)"
	line 401, ".input.spin", state 1655, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
	line 401, ".input.spin", state 1657, "(1)"
	line 401, ".input.spin", state 1658, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
	line 401, ".input.spin", state 1658, "else"
	line 401, ".input.spin", state 1661, "(1)"
	line 401, ".input.spin", state 1662, "(1)"
	line 401, ".input.spin", state 1662, "(1)"
	line 399, ".input.spin", state 1667, "((i<1))"
	line 399, ".input.spin", state 1667, "((i>=1))"
	line 406, ".input.spin", state 1673, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 407, ".input.spin", state 1686, "(1)"
	line 407, ".input.spin", state 1687, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
	line 407, ".input.spin", state 1687, "else"
	line 407, ".input.spin", state 1690, "(1)"
	line 407, ".input.spin", state 1691, "(1)"
	line 407, ".input.spin", state 1691, "(1)"
	line 411, ".input.spin", state 1699, "(1)"
	line 411, ".input.spin", state 1700, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
	line 411, ".input.spin", state 1700, "else"
	line 411, ".input.spin", state 1703, "(1)"
	line 411, ".input.spin", state 1704, "(1)"
	line 411, ".input.spin", state 1704, "(1)"
	line 409, ".input.spin", state 1709, "((i<1))"
	line 409, ".input.spin", state 1709, "((i>=1))"
	line 416, ".input.spin", state 1716, "(1)"
	line 416, ".input.spin", state 1717, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
	line 416, ".input.spin", state 1717, "else"
	line 416, ".input.spin", state 1720, "(1)"
	line 416, ".input.spin", state 1721, "(1)"
	line 416, ".input.spin", state 1721, "(1)"
	line 418, ".input.spin", state 1724, "(1)"
	line 418, ".input.spin", state 1724, "(1)"
	line 360, ".input.spin", state 1733, "sighand_exec = 1"
	line 177, ".input.spin", state 1758, "(1)"
	line 181, ".input.spin", state 1769, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 158, ".input.spin", state 1779, "(1)"
	line 162, ".input.spin", state 1787, "(1)"
	line 166, ".input.spin", state 1799, "(1)"
	line 173, ".input.spin", state 1810, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
	line 177, ".input.spin", state 1819, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
	line 181, ".input.spin", state 1832, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
	line 158, ".input.spin", state 1842, "(1)"
	line 162, ".input.spin", state 1850, "(1)"
	line 166, ".input.spin", state 1862, "(1)"
	line 173, ".input.spin", state 1877, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
	line 177, ".input.spin", state 1886, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
	line 181, ".input.spin", state 1899, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
	line 158, ".input.spin", state 1909, "(1)"
	line 162, ".input.spin", state 1917, "(1)"
	line 166, ".input.spin", state 1929, "(1)"
	line 700, ".input.spin", state 1968, "-end-"
	(215 of 1968 states)
unreached in proctype :init:
	(0 of 46 states)

pan: elapsed time 0.12 seconds
pan: rate 167733.33 states/second
pan: avg transition delay 5.6709e-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'