make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-min-progress'
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 -DCOLLAPSE -DSAFETY -o pan pan.c
./pan -v -c1 -X -m10000000 -w20
Depth=    3250 States=    1e+06 Transitions= 2.74e+08 Memory=   500.529	t=    357 R=   3e+03
Depth=    3250 States=    2e+06 Transitions= 5.69e+08 Memory=   537.248	t=    774 R=   3e+03

(Spin Version 5.1.7 -- 23 December 2008)
	+ Partial Order Reduction
	+ Compression

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 72 byte, depth reached 3250, errors: 0
  2668047 states, stored
7.3166567e+08 states, matched
7.3433372e+08 transitions (= stored+matched)
4.2954757e+09 atomic steps
hash conflicts: 4.8630608e+08 (resolved)

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

nr of templates: [ globals chans procs ]
collapse counts: [ 25912 2128 1970 2 ]
unreached in proctype urcu_reader
	line 267, ".input.spin", state 55, "cache_dirty_urcu_gp_ctr = 0"
	line 275, ".input.spin", state 77, "cache_dirty_rcu_ptr = 0"
	line 279, ".input.spin", state 86, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 102, "(1)"
	line 248, ".input.spin", state 110, "(1)"
	line 252, ".input.spin", state 122, "(1)"
	line 256, ".input.spin", state 130, "(1)"
	line 403, ".input.spin", state 156, "cache_dirty_urcu_gp_ctr = 0"
	line 412, ".input.spin", state 188, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 202, "cache_dirty_rcu_data[i] = 0"
	line 421, ".input.spin", state 221, "(1)"
	line 430, ".input.spin", state 251, "(1)"
	line 434, ".input.spin", state 264, "(1)"
	line 613, ".input.spin", state 285, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
	line 403, ".input.spin", state 292, "cache_dirty_urcu_gp_ctr = 0"
	line 412, ".input.spin", state 324, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 338, "cache_dirty_rcu_data[i] = 0"
	line 421, ".input.spin", state 357, "(1)"
	line 430, ".input.spin", state 387, "(1)"
	line 434, ".input.spin", state 400, "(1)"
	line 403, ".input.spin", state 421, "cache_dirty_urcu_gp_ctr = 0"
	line 412, ".input.spin", state 453, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 467, "cache_dirty_rcu_data[i] = 0"
	line 421, ".input.spin", state 486, "(1)"
	line 430, ".input.spin", state 516, "(1)"
	line 434, ".input.spin", state 529, "(1)"
	line 403, ".input.spin", state 552, "cache_dirty_urcu_gp_ctr = 0"
	line 403, ".input.spin", state 554, "(1)"
	line 403, ".input.spin", state 555, "(cache_dirty_urcu_gp_ctr)"
	line 403, ".input.spin", state 555, "else"
	line 403, ".input.spin", state 558, "(1)"
	line 407, ".input.spin", state 566, "cache_dirty_urcu_active_readers = 0"
	line 407, ".input.spin", state 568, "(1)"
	line 407, ".input.spin", state 569, "(cache_dirty_urcu_active_readers)"
	line 407, ".input.spin", state 569, "else"
	line 407, ".input.spin", state 572, "(1)"
	line 407, ".input.spin", state 573, "(1)"
	line 407, ".input.spin", state 573, "(1)"
	line 405, ".input.spin", state 578, "((i<1))"
	line 405, ".input.spin", state 578, "((i>=1))"
	line 412, ".input.spin", state 584, "cache_dirty_rcu_ptr = 0"
	line 412, ".input.spin", state 586, "(1)"
	line 412, ".input.spin", state 587, "(cache_dirty_rcu_ptr)"
	line 412, ".input.spin", state 587, "else"
	line 412, ".input.spin", state 590, "(1)"
	line 412, ".input.spin", state 591, "(1)"
	line 412, ".input.spin", state 591, "(1)"
	line 416, ".input.spin", state 598, "cache_dirty_rcu_data[i] = 0"
	line 416, ".input.spin", state 600, "(1)"
	line 416, ".input.spin", state 601, "(cache_dirty_rcu_data[i])"
	line 416, ".input.spin", state 601, "else"
	line 416, ".input.spin", state 604, "(1)"
	line 416, ".input.spin", state 605, "(1)"
	line 416, ".input.spin", state 605, "(1)"
	line 414, ".input.spin", state 610, "((i<2))"
	line 414, ".input.spin", state 610, "((i>=2))"
	line 421, ".input.spin", state 617, "(1)"
	line 421, ".input.spin", state 618, "(!(cache_dirty_urcu_gp_ctr))"
	line 421, ".input.spin", state 618, "else"
	line 421, ".input.spin", state 621, "(1)"
	line 421, ".input.spin", state 622, "(1)"
	line 421, ".input.spin", state 622, "(1)"
	line 425, ".input.spin", state 630, "(1)"
	line 425, ".input.spin", state 631, "(!(cache_dirty_urcu_active_readers))"
	line 425, ".input.spin", state 631, "else"
	line 425, ".input.spin", state 634, "(1)"
	line 425, ".input.spin", state 635, "(1)"
	line 425, ".input.spin", state 635, "(1)"
	line 423, ".input.spin", state 640, "((i<1))"
	line 423, ".input.spin", state 640, "((i>=1))"
	line 430, ".input.spin", state 647, "(1)"
	line 430, ".input.spin", state 648, "(!(cache_dirty_rcu_ptr))"
	line 430, ".input.spin", state 648, "else"
	line 430, ".input.spin", state 651, "(1)"
	line 430, ".input.spin", state 652, "(1)"
	line 430, ".input.spin", state 652, "(1)"
	line 434, ".input.spin", state 660, "(1)"
	line 434, ".input.spin", state 661, "(!(cache_dirty_rcu_data[i]))"
	line 434, ".input.spin", state 661, "else"
	line 434, ".input.spin", state 664, "(1)"
	line 434, ".input.spin", state 665, "(1)"
	line 434, ".input.spin", state 665, "(1)"
	line 432, ".input.spin", state 670, "((i<2))"
	line 432, ".input.spin", state 670, "((i>=2))"
	line 442, ".input.spin", state 674, "(1)"
	line 442, ".input.spin", state 674, "(1)"
	line 613, ".input.spin", state 677, "cached_urcu_active_readers = (tmp+1)"
	line 613, ".input.spin", state 678, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
	line 613, ".input.spin", state 679, "(1)"
	line 403, ".input.spin", state 686, "cache_dirty_urcu_gp_ctr = 0"
	line 412, ".input.spin", state 718, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 732, "cache_dirty_rcu_data[i] = 0"
	line 421, ".input.spin", state 751, "(1)"
	line 430, ".input.spin", state 781, "(1)"
	line 434, ".input.spin", state 794, "(1)"
	line 403, ".input.spin", state 821, "cache_dirty_urcu_gp_ctr = 0"
	line 412, ".input.spin", state 853, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 867, "cache_dirty_rcu_data[i] = 0"
	line 421, ".input.spin", state 886, "(1)"
	line 430, ".input.spin", state 916, "(1)"
	line 434, ".input.spin", state 929, "(1)"
	line 403, ".input.spin", state 950, "cache_dirty_urcu_gp_ctr = 0"
	line 412, ".input.spin", state 982, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 996, "cache_dirty_rcu_data[i] = 0"
	line 421, ".input.spin", state 1015, "(1)"
	line 430, ".input.spin", state 1045, "(1)"
	line 434, ".input.spin", state 1058, "(1)"
	line 244, ".input.spin", state 1091, "(1)"
	line 252, ".input.spin", state 1111, "(1)"
	line 256, ".input.spin", state 1119, "(1)"
	line 747, ".input.spin", state 1136, "-end-"
	(91 of 1136 states)
unreached in proctype urcu_writer
	line 403, ".input.spin", state 45, "cache_dirty_urcu_gp_ctr = 0"
	line 407, ".input.spin", state 59, "cache_dirty_urcu_active_readers = 0"
	line 412, ".input.spin", state 77, "cache_dirty_rcu_ptr = 0"
	line 421, ".input.spin", state 110, "(1)"
	line 425, ".input.spin", state 123, "(1)"
	line 430, ".input.spin", state 140, "(1)"
	line 267, ".input.spin", state 176, "cache_dirty_urcu_gp_ctr = 0"
	line 271, ".input.spin", state 185, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 198, "cache_dirty_rcu_ptr = 0"
	line 403, ".input.spin", state 238, "cache_dirty_urcu_gp_ctr = 0"
	line 407, ".input.spin", state 252, "cache_dirty_urcu_active_readers = 0"
	line 412, ".input.spin", state 270, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 284, "cache_dirty_rcu_data[i] = 0"
	line 421, ".input.spin", state 303, "(1)"
	line 425, ".input.spin", state 316, "(1)"
	line 430, ".input.spin", state 333, "(1)"
	line 434, ".input.spin", state 346, "(1)"
	line 407, ".input.spin", state 383, "cache_dirty_urcu_active_readers = 0"
	line 412, ".input.spin", state 401, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 415, "cache_dirty_rcu_data[i] = 0"
	line 425, ".input.spin", state 447, "(1)"
	line 430, ".input.spin", state 464, "(1)"
	line 434, ".input.spin", state 477, "(1)"
	line 407, ".input.spin", state 522, "cache_dirty_urcu_active_readers = 0"
	line 412, ".input.spin", state 540, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 554, "cache_dirty_rcu_data[i] = 0"
	line 425, ".input.spin", state 586, "(1)"
	line 430, ".input.spin", state 603, "(1)"
	line 434, ".input.spin", state 616, "(1)"
	line 407, ".input.spin", state 651, "cache_dirty_urcu_active_readers = 0"
	line 412, ".input.spin", state 669, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 683, "cache_dirty_rcu_data[i] = 0"
	line 425, ".input.spin", state 715, "(1)"
	line 430, ".input.spin", state 732, "(1)"
	line 434, ".input.spin", state 745, "(1)"
	line 407, ".input.spin", state 782, "cache_dirty_urcu_active_readers = 0"
	line 412, ".input.spin", state 800, "cache_dirty_rcu_ptr = 0"
	line 416, ".input.spin", state 814, "cache_dirty_rcu_data[i] = 0"
	line 425, ".input.spin", state 846, "(1)"
	line 430, ".input.spin", state 863, "(1)"
	line 434, ".input.spin", state 876, "(1)"
	line 267, ".input.spin", state 931, "cache_dirty_urcu_gp_ctr = 0"
	line 271, ".input.spin", state 940, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 955, "(1)"
	line 279, ".input.spin", state 962, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 978, "(1)"
	line 248, ".input.spin", state 986, "(1)"
	line 252, ".input.spin", state 998, "(1)"
	line 256, ".input.spin", state 1006, "(1)"
	line 267, ".input.spin", state 1037, "cache_dirty_urcu_gp_ctr = 0"
	line 271, ".input.spin", state 1046, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 1059, "cache_dirty_rcu_ptr = 0"
	line 279, ".input.spin", state 1068, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 1084, "(1)"
	line 248, ".input.spin", state 1092, "(1)"
	line 252, ".input.spin", state 1104, "(1)"
	line 256, ".input.spin", state 1112, "(1)"
	line 271, ".input.spin", state 1138, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 1151, "cache_dirty_rcu_ptr = 0"
	line 279, ".input.spin", state 1160, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 1176, "(1)"
	line 248, ".input.spin", state 1184, "(1)"
	line 252, ".input.spin", state 1196, "(1)"
	line 256, ".input.spin", state 1204, "(1)"
	line 267, ".input.spin", state 1235, "cache_dirty_urcu_gp_ctr = 0"
	line 271, ".input.spin", state 1244, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 1257, "cache_dirty_rcu_ptr = 0"
	line 279, ".input.spin", state 1266, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 1282, "(1)"
	line 248, ".input.spin", state 1290, "(1)"
	line 252, ".input.spin", state 1302, "(1)"
	line 256, ".input.spin", state 1310, "(1)"
	line 271, ".input.spin", state 1336, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 1349, "cache_dirty_rcu_ptr = 0"
	line 279, ".input.spin", state 1358, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 1374, "(1)"
	line 248, ".input.spin", state 1382, "(1)"
	line 252, ".input.spin", state 1394, "(1)"
	line 256, ".input.spin", state 1402, "(1)"
	line 267, ".input.spin", state 1433, "cache_dirty_urcu_gp_ctr = 0"
	line 271, ".input.spin", state 1442, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 1455, "cache_dirty_rcu_ptr = 0"
	line 279, ".input.spin", state 1464, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 1480, "(1)"
	line 248, ".input.spin", state 1488, "(1)"
	line 252, ".input.spin", state 1500, "(1)"
	line 256, ".input.spin", state 1508, "(1)"
	line 271, ".input.spin", state 1534, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 1547, "cache_dirty_rcu_ptr = 0"
	line 279, ".input.spin", state 1556, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 1572, "(1)"
	line 248, ".input.spin", state 1580, "(1)"
	line 252, ".input.spin", state 1592, "(1)"
	line 256, ".input.spin", state 1600, "(1)"
	line 267, ".input.spin", state 1631, "cache_dirty_urcu_gp_ctr = 0"
	line 271, ".input.spin", state 1640, "cache_dirty_urcu_active_readers = 0"
	line 275, ".input.spin", state 1653, "cache_dirty_rcu_ptr = 0"
	line 279, ".input.spin", state 1662, "cache_dirty_rcu_data[i] = 0"
	line 244, ".input.spin", state 1678, "(1)"
	line 248, ".input.spin", state 1686, "(1)"
	line 252, ".input.spin", state 1698, "(1)"
	line 256, ".input.spin", state 1706, "(1)"
	line 1122, ".input.spin", state 1722, "-end-"
	(103 of 1722 states)
unreached in proctype :init:
	(0 of 26 states)

pan: elapsed time 1.01e+03 seconds
pan: rate  2639.775 states/second
pan: avg transition delay 1.3764e-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-min-progress'