make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
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=    5407 States=    1e+06 Transitions= 5.87e+06 Memory=   542.717	t=   11.7 R=   9e+04
Depth=    5407 States=    2e+06 Transitions= 1.64e+07 Memory=   618.986	t=   35.3 R=   6e+04
Depth=    5407 States=    3e+06 Transitions= 3.29e+07 Memory=   695.256	t=   74.2 R=   4e+04
pan: resizing hashtable to -w22..  done
Depth=    5407 States=    4e+06 Transitions= 4.33e+07 Memory=   802.647	t=   97.9 R=   4e+04
Depth=    5407 States=    5e+06 Transitions=  5.2e+07 Memory=   878.916	t=    117 R=   4e+04
Depth=    5407 States=    6e+06 Transitions= 5.99e+07 Memory=   955.186	t=    134 R=   4e+04
Depth=    5407 States=    7e+06 Transitions= 7.13e+07 Memory=  1031.455	t=    160 R=   4e+04
Depth=    5407 States=    8e+06 Transitions= 8.71e+07 Memory=  1107.822	t=    198 R=   4e+04
Depth=    5407 States=    9e+06 Transitions= 9.81e+07 Memory=  1184.092	t=    223 R=   4e+04
pan: resizing hashtable to -w24..  done
Depth=    5407 States=    1e+07 Transitions= 1.07e+08 Memory=  1384.455	t=    244 R=   4e+04
Depth=    5407 States=  1.1e+07 Transitions= 1.14e+08 Memory=  1460.725	t=    260 R=   4e+04
Depth=    5407 States=  1.2e+07 Transitions= 1.27e+08 Memory=  1536.994	t=    288 R=   4e+04

(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 5407, errors: 0
 12141896 states, stored
1.1623987e+08 states, matched
1.2838176e+08 transitions (= stored+matched)
1.9407117e+09 atomic steps
hash conflicts:  98957892 (resolved)

Stats on memory usage (in Megabytes):
 1157.941	equivalent memory usage for states (stored*(State-vector + overhead))
  962.219	actual memory usage for states (compression: 83.10%)
         	state-vector as stored = 55 byte + 28 byte overhead
  128.000	memory used for hash table (-w24)
  457.764	memory used for DFS stack (-m10000000)
 1547.834	total actual memory usage

unreached in proctype urcu_reader
	line 261, ".input.spin", state 30, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 273, ".input.spin", state 61, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 77, "(1)"
	line 242, ".input.spin", state 85, "(1)"
	line 246, ".input.spin", state 97, "(1)"
	line 250, ".input.spin", state 105, "(1)"
	line 400, ".input.spin", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 163, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 177, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 195, "(1)"
	line 246, ".input.spin", state 215, "(1)"
	line 250, ".input.spin", state 223, "(1)"
	line 679, ".input.spin", state 242, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
	line 400, ".input.spin", state 249, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 281, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 295, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 313, "(1)"
	line 246, ".input.spin", state 333, "(1)"
	line 250, ".input.spin", state 341, "(1)"
	line 400, ".input.spin", state 360, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 392, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 406, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 424, "(1)"
	line 246, ".input.spin", state 444, "(1)"
	line 250, ".input.spin", state 452, "(1)"
	line 400, ".input.spin", state 473, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 400, ".input.spin", state 475, "(1)"
	line 400, ".input.spin", state 476, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 400, ".input.spin", state 476, "else"
	line 400, ".input.spin", state 479, "(1)"
	line 404, ".input.spin", state 487, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 404, ".input.spin", state 489, "(1)"
	line 404, ".input.spin", state 490, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 404, ".input.spin", state 490, "else"
	line 404, ".input.spin", state 493, "(1)"
	line 404, ".input.spin", state 494, "(1)"
	line 404, ".input.spin", state 494, "(1)"
	line 402, ".input.spin", state 499, "((i<1))"
	line 402, ".input.spin", state 499, "((i>=1))"
	line 409, ".input.spin", state 505, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 507, "(1)"
	line 409, ".input.spin", state 508, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 409, ".input.spin", state 508, "else"
	line 409, ".input.spin", state 511, "(1)"
	line 409, ".input.spin", state 512, "(1)"
	line 409, ".input.spin", state 512, "(1)"
	line 413, ".input.spin", state 519, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 521, "(1)"
	line 413, ".input.spin", state 522, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 413, ".input.spin", state 522, "else"
	line 413, ".input.spin", state 525, "(1)"
	line 413, ".input.spin", state 526, "(1)"
	line 413, ".input.spin", state 526, "(1)"
	line 411, ".input.spin", state 531, "((i<2))"
	line 411, ".input.spin", state 531, "((i>=2))"
	line 238, ".input.spin", state 537, "(1)"
	line 242, ".input.spin", state 545, "(1)"
	line 242, ".input.spin", state 546, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 242, ".input.spin", state 546, "else"
	line 240, ".input.spin", state 551, "((i<1))"
	line 240, ".input.spin", state 551, "((i>=1))"
	line 246, ".input.spin", state 557, "(1)"
	line 246, ".input.spin", state 558, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 246, ".input.spin", state 558, "else"
	line 250, ".input.spin", state 565, "(1)"
	line 250, ".input.spin", state 566, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 250, ".input.spin", state 566, "else"
	line 248, ".input.spin", state 571, "((i<2))"
	line 248, ".input.spin", state 571, "((i>=2))"
	line 255, ".input.spin", state 575, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 255, ".input.spin", state 575, "else"
	line 420, ".input.spin", state 577, "(1)"
	line 420, ".input.spin", state 577, "(1)"
	line 679, ".input.spin", state 580, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
	line 679, ".input.spin", state 581, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
	line 679, ".input.spin", state 582, "(1)"
	line 400, ".input.spin", state 589, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 621, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 635, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 653, "(1)"
	line 246, ".input.spin", state 673, "(1)"
	line 250, ".input.spin", state 681, "(1)"
	line 400, ".input.spin", state 707, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 400, ".input.spin", state 709, "(1)"
	line 400, ".input.spin", state 710, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 400, ".input.spin", state 710, "else"
	line 400, ".input.spin", state 713, "(1)"
	line 404, ".input.spin", state 721, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 404, ".input.spin", state 723, "(1)"
	line 404, ".input.spin", state 724, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 404, ".input.spin", state 724, "else"
	line 404, ".input.spin", state 727, "(1)"
	line 404, ".input.spin", state 728, "(1)"
	line 404, ".input.spin", state 728, "(1)"
	line 402, ".input.spin", state 733, "((i<1))"
	line 402, ".input.spin", state 733, "((i>=1))"
	line 409, ".input.spin", state 739, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 741, "(1)"
	line 409, ".input.spin", state 742, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 409, ".input.spin", state 742, "else"
	line 409, ".input.spin", state 745, "(1)"
	line 409, ".input.spin", state 746, "(1)"
	line 409, ".input.spin", state 746, "(1)"
	line 413, ".input.spin", state 753, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 755, "(1)"
	line 413, ".input.spin", state 756, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 413, ".input.spin", state 756, "else"
	line 413, ".input.spin", state 759, "(1)"
	line 413, ".input.spin", state 760, "(1)"
	line 413, ".input.spin", state 760, "(1)"
	line 411, ".input.spin", state 765, "((i<2))"
	line 411, ".input.spin", state 765, "((i>=2))"
	line 238, ".input.spin", state 771, "(1)"
	line 242, ".input.spin", state 779, "(1)"
	line 242, ".input.spin", state 780, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 242, ".input.spin", state 780, "else"
	line 240, ".input.spin", state 785, "((i<1))"
	line 240, ".input.spin", state 785, "((i>=1))"
	line 246, ".input.spin", state 791, "(1)"
	line 246, ".input.spin", state 792, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 246, ".input.spin", state 792, "else"
	line 250, ".input.spin", state 799, "(1)"
	line 250, ".input.spin", state 800, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 250, ".input.spin", state 800, "else"
	line 255, ".input.spin", state 809, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 255, ".input.spin", state 809, "else"
	line 420, ".input.spin", state 811, "(1)"
	line 420, ".input.spin", state 811, "(1)"
	line 400, ".input.spin", state 818, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 400, ".input.spin", state 820, "(1)"
	line 400, ".input.spin", state 821, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 400, ".input.spin", state 821, "else"
	line 400, ".input.spin", state 824, "(1)"
	line 404, ".input.spin", state 832, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 404, ".input.spin", state 834, "(1)"
	line 404, ".input.spin", state 835, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 404, ".input.spin", state 835, "else"
	line 404, ".input.spin", state 838, "(1)"
	line 404, ".input.spin", state 839, "(1)"
	line 404, ".input.spin", state 839, "(1)"
	line 402, ".input.spin", state 844, "((i<1))"
	line 402, ".input.spin", state 844, "((i>=1))"
	line 409, ".input.spin", state 850, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 852, "(1)"
	line 409, ".input.spin", state 853, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 409, ".input.spin", state 853, "else"
	line 409, ".input.spin", state 856, "(1)"
	line 409, ".input.spin", state 857, "(1)"
	line 409, ".input.spin", state 857, "(1)"
	line 413, ".input.spin", state 864, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 866, "(1)"
	line 413, ".input.spin", state 867, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 413, ".input.spin", state 867, "else"
	line 413, ".input.spin", state 870, "(1)"
	line 413, ".input.spin", state 871, "(1)"
	line 413, ".input.spin", state 871, "(1)"
	line 411, ".input.spin", state 876, "((i<2))"
	line 411, ".input.spin", state 876, "((i>=2))"
	line 238, ".input.spin", state 882, "(1)"
	line 242, ".input.spin", state 890, "(1)"
	line 242, ".input.spin", state 891, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 242, ".input.spin", state 891, "else"
	line 240, ".input.spin", state 896, "((i<1))"
	line 240, ".input.spin", state 896, "((i>=1))"
	line 246, ".input.spin", state 902, "(1)"
	line 246, ".input.spin", state 903, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 246, ".input.spin", state 903, "else"
	line 250, ".input.spin", state 910, "(1)"
	line 250, ".input.spin", state 911, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 250, ".input.spin", state 911, "else"
	line 248, ".input.spin", state 916, "((i<2))"
	line 248, ".input.spin", state 916, "((i>=2))"
	line 255, ".input.spin", state 920, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 255, ".input.spin", state 920, "else"
	line 420, ".input.spin", state 922, "(1)"
	line 420, ".input.spin", state 922, "(1)"
	line 687, ".input.spin", state 926, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
	line 400, ".input.spin", state 931, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 963, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 977, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 995, "(1)"
	line 246, ".input.spin", state 1015, "(1)"
	line 250, ".input.spin", state 1023, "(1)"
	line 400, ".input.spin", state 1045, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1077, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 1091, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1109, "(1)"
	line 246, ".input.spin", state 1129, "(1)"
	line 250, ".input.spin", state 1137, "(1)"
	line 400, ".input.spin", state 1160, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1192, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 1206, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1224, "(1)"
	line 246, ".input.spin", state 1244, "(1)"
	line 250, ".input.spin", state 1252, "(1)"
	line 400, ".input.spin", state 1271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1303, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 1317, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1335, "(1)"
	line 246, ".input.spin", state 1355, "(1)"
	line 250, ".input.spin", state 1363, "(1)"
	line 400, ".input.spin", state 1387, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1419, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 1433, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1451, "(1)"
	line 246, ".input.spin", state 1471, "(1)"
	line 250, ".input.spin", state 1479, "(1)"
	line 400, ".input.spin", state 1498, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1530, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 1544, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1562, "(1)"
	line 246, ".input.spin", state 1582, "(1)"
	line 250, ".input.spin", state 1590, "(1)"
	line 400, ".input.spin", state 1612, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1644, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 1658, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1676, "(1)"
	line 246, ".input.spin", state 1696, "(1)"
	line 250, ".input.spin", state 1704, "(1)"
	line 726, ".input.spin", state 1723, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
	line 400, ".input.spin", state 1730, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1762, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 1776, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1794, "(1)"
	line 246, ".input.spin", state 1814, "(1)"
	line 250, ".input.spin", state 1822, "(1)"
	line 400, ".input.spin", state 1841, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1873, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 1887, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1905, "(1)"
	line 246, ".input.spin", state 1925, "(1)"
	line 250, ".input.spin", state 1933, "(1)"
	line 400, ".input.spin", state 1954, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 400, ".input.spin", state 1956, "(1)"
	line 400, ".input.spin", state 1957, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
	line 400, ".input.spin", state 1957, "else"
	line 400, ".input.spin", state 1960, "(1)"
	line 404, ".input.spin", state 1968, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 404, ".input.spin", state 1970, "(1)"
	line 404, ".input.spin", state 1971, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
	line 404, ".input.spin", state 1971, "else"
	line 404, ".input.spin", state 1974, "(1)"
	line 404, ".input.spin", state 1975, "(1)"
	line 404, ".input.spin", state 1975, "(1)"
	line 402, ".input.spin", state 1980, "((i<1))"
	line 402, ".input.spin", state 1980, "((i>=1))"
	line 409, ".input.spin", state 1986, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 1988, "(1)"
	line 409, ".input.spin", state 1989, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
	line 409, ".input.spin", state 1989, "else"
	line 409, ".input.spin", state 1992, "(1)"
	line 409, ".input.spin", state 1993, "(1)"
	line 409, ".input.spin", state 1993, "(1)"
	line 413, ".input.spin", state 2000, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 2002, "(1)"
	line 413, ".input.spin", state 2003, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
	line 413, ".input.spin", state 2003, "else"
	line 413, ".input.spin", state 2006, "(1)"
	line 413, ".input.spin", state 2007, "(1)"
	line 413, ".input.spin", state 2007, "(1)"
	line 411, ".input.spin", state 2012, "((i<2))"
	line 411, ".input.spin", state 2012, "((i>=2))"
	line 238, ".input.spin", state 2018, "(1)"
	line 242, ".input.spin", state 2026, "(1)"
	line 242, ".input.spin", state 2027, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
	line 242, ".input.spin", state 2027, "else"
	line 240, ".input.spin", state 2032, "((i<1))"
	line 240, ".input.spin", state 2032, "((i>=1))"
	line 246, ".input.spin", state 2038, "(1)"
	line 246, ".input.spin", state 2039, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
	line 246, ".input.spin", state 2039, "else"
	line 250, ".input.spin", state 2046, "(1)"
	line 250, ".input.spin", state 2047, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
	line 250, ".input.spin", state 2047, "else"
	line 248, ".input.spin", state 2052, "((i<2))"
	line 248, ".input.spin", state 2052, "((i>=2))"
	line 255, ".input.spin", state 2056, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
	line 255, ".input.spin", state 2056, "else"
	line 420, ".input.spin", state 2058, "(1)"
	line 420, ".input.spin", state 2058, "(1)"
	line 726, ".input.spin", state 2061, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
	line 726, ".input.spin", state 2062, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
	line 726, ".input.spin", state 2063, "(1)"
	line 400, ".input.spin", state 2070, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 2102, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 2116, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 2134, "(1)"
	line 246, ".input.spin", state 2154, "(1)"
	line 250, ".input.spin", state 2162, "(1)"
	line 400, ".input.spin", state 2187, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 2219, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 2233, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 2251, "(1)"
	line 246, ".input.spin", state 2271, "(1)"
	line 250, ".input.spin", state 2279, "(1)"
	line 400, ".input.spin", state 2298, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 2330, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 2344, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 2362, "(1)"
	line 246, ".input.spin", state 2382, "(1)"
	line 250, ".input.spin", state 2390, "(1)"
	line 238, ".input.spin", state 2421, "(1)"
	line 246, ".input.spin", state 2441, "(1)"
	line 250, ".input.spin", state 2449, "(1)"
	line 238, ".input.spin", state 2464, "(1)"
	line 246, ".input.spin", state 2484, "(1)"
	line 250, ".input.spin", state 2492, "(1)"
	line 886, ".input.spin", state 2509, "-end-"
	(246 of 2509 states)
unreached in proctype urcu_writer
	line 400, ".input.spin", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 404, ".input.spin", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 82, "(1)"
	line 242, ".input.spin", state 90, "(1)"
	line 246, ".input.spin", state 102, "(1)"
	line 261, ".input.spin", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 265, ".input.spin", state 140, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 153, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 400, ".input.spin", state 193, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 404, ".input.spin", state 207, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 225, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 239, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 257, "(1)"
	line 242, ".input.spin", state 265, "(1)"
	line 246, ".input.spin", state 277, "(1)"
	line 250, ".input.spin", state 285, "(1)"
	line 404, ".input.spin", state 320, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 338, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 352, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 242, ".input.spin", state 378, "(1)"
	line 246, ".input.spin", state 390, "(1)"
	line 250, ".input.spin", state 398, "(1)"
	line 404, ".input.spin", state 440, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 458, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 472, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 242, ".input.spin", state 498, "(1)"
	line 246, ".input.spin", state 510, "(1)"
	line 250, ".input.spin", state 518, "(1)"
	line 404, ".input.spin", state 551, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 569, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 583, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 242, ".input.spin", state 609, "(1)"
	line 246, ".input.spin", state 621, "(1)"
	line 250, ".input.spin", state 629, "(1)"
	line 404, ".input.spin", state 664, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 409, ".input.spin", state 682, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 413, ".input.spin", state 696, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 242, ".input.spin", state 722, "(1)"
	line 246, ".input.spin", state 734, "(1)"
	line 250, ".input.spin", state 742, "(1)"
	line 261, ".input.spin", state 795, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 265, ".input.spin", state 804, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 819, "(1)"
	line 273, ".input.spin", state 826, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 842, "(1)"
	line 242, ".input.spin", state 850, "(1)"
	line 246, ".input.spin", state 862, "(1)"
	line 250, ".input.spin", state 870, "(1)"
	line 261, ".input.spin", state 901, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 265, ".input.spin", state 910, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 923, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 273, ".input.spin", state 932, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 948, "(1)"
	line 242, ".input.spin", state 956, "(1)"
	line 246, ".input.spin", state 968, "(1)"
	line 250, ".input.spin", state 976, "(1)"
	line 265, ".input.spin", state 1002, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 1015, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 273, ".input.spin", state 1024, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1040, "(1)"
	line 242, ".input.spin", state 1048, "(1)"
	line 246, ".input.spin", state 1060, "(1)"
	line 250, ".input.spin", state 1068, "(1)"
	line 261, ".input.spin", state 1099, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 265, ".input.spin", state 1108, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 1121, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 273, ".input.spin", state 1130, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1146, "(1)"
	line 242, ".input.spin", state 1154, "(1)"
	line 246, ".input.spin", state 1166, "(1)"
	line 250, ".input.spin", state 1174, "(1)"
	line 265, ".input.spin", state 1200, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 1213, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 273, ".input.spin", state 1222, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1238, "(1)"
	line 242, ".input.spin", state 1246, "(1)"
	line 246, ".input.spin", state 1258, "(1)"
	line 250, ".input.spin", state 1266, "(1)"
	line 261, ".input.spin", state 1297, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 265, ".input.spin", state 1306, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 1319, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 273, ".input.spin", state 1328, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1344, "(1)"
	line 242, ".input.spin", state 1352, "(1)"
	line 246, ".input.spin", state 1364, "(1)"
	line 250, ".input.spin", state 1372, "(1)"
	line 265, ".input.spin", state 1398, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 1411, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 273, ".input.spin", state 1420, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1436, "(1)"
	line 242, ".input.spin", state 1444, "(1)"
	line 246, ".input.spin", state 1456, "(1)"
	line 250, ".input.spin", state 1464, "(1)"
	line 261, ".input.spin", state 1495, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
	line 265, ".input.spin", state 1504, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
	line 269, ".input.spin", state 1517, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
	line 273, ".input.spin", state 1526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
	line 238, ".input.spin", state 1542, "(1)"
	line 242, ".input.spin", state 1550, "(1)"
	line 246, ".input.spin", state 1562, "(1)"
	line 250, ".input.spin", state 1570, "(1)"
	line 1213, ".input.spin", state 1586, "-end-"
	(103 of 1586 states)
unreached in proctype :init:
	(0 of 78 states)

pan: elapsed time 291 seconds
pan: rate 41688.913 states/second
pan: avg transition delay 2.2686e-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'