X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Fresults%2Furcu-controldataflow-ipi-intel%2Furcu_free_no_mb.log;fp=formal-model%2Fresults%2Furcu-controldataflow-ipi-intel%2Furcu_free_no_mb.log;h=15f7bc2377d81abfde20eb6992eca391fd4bb1b1;hb=f2b3a82d7569463cc9b28bdd0943f06984197b6a;hp=0000000000000000000000000000000000000000;hpb=f24274b95c646682a448694eb0c759311cb7a5af;p=urcu.git

diff --git a/formal-model/results/urcu-controldataflow-ipi-intel/urcu_free_no_mb.log b/formal-model/results/urcu-controldataflow-ipi-intel/urcu_free_no_mb.log
new file mode 100644
index 0000000..15f7bc2
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-ipi-intel/urcu_free_no_mb.log
@@ -0,0 +1,624 @@
+make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
+rm -f pan* trail.out .input.spin* *.spin.trail .input.define
+touch .input.define
+cat .input.define >> pan.ltl
+cat DEFINES >> pan.ltl
+spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl
+cp urcu_free_no_mb.define .input.define
+cat .input.define > .input.spin
+cat DEFINES >> .input.spin
+cat urcu.spin >> .input.spin
+rm -f .input.spin.trail
+spin -a -X -N pan.ltl .input.spin
+Exit-Status 0
+gcc -O2 -w -DHASH64 -o pan pan.c
+./pan -a -v -c1 -X -m10000000 -w20
+warning: for p.o. reduction to be valid the never claim must be stutter-invariant
+(never claims generated from LTL formulae are stutter-invariant)
+depth 0: Claim reached state 5 (line 1272)
+Depth=    5327 States=    1e+06 Transitions= 7.34e+06 Memory=   550.432	t=   18.2 R=   6e+04
+pan: claim violated! (at depth 1301)
+pan: wrote .input.spin.trail
+
+(Spin Version 5.1.7 -- 23 December 2008)
+Warning: Search not completed
+	+ Partial Order Reduction
+
+Full statespace search for:
+	never claim         	+
+	assertion violations	+ (if within scope of claim)
+	acceptance   cycles 	+ (fairness disabled)
+	invalid end states	- (disabled by never claim)
+
+State-vector 88 byte, depth reached 5456, errors: 1
+  1674433 states, stored
+ 12624035 states, matched
+ 14298468 transitions (= stored+matched)
+2.0423758e+08 atomic steps
+hash conflicts:   6074438 (resolved)
+
+Stats on memory usage (in Megabytes):
+  185.236	equivalent memory usage for states (stored*(State-vector + overhead))
+  141.360	actual memory usage for states (compression: 76.31%)
+         	state-vector as stored = 61 byte + 28 byte overhead
+    8.000	memory used for hash table (-w20)
+  457.764	memory used for DFS stack (-m10000000)
+  606.975	total actual memory usage
+
+unreached in proctype urcu_reader
+	line 262, "pan.___", state 34, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 270, "pan.___", state 56, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 65, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 81, "(1)"
+	line 243, "pan.___", state 89, "(1)"
+	line 247, "pan.___", state 101, "(1)"
+	line 251, "pan.___", state 109, "(1)"
+	line 401, "pan.___", state 135, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 167, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 181, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 199, "(1)"
+	line 247, "pan.___", state 219, "(1)"
+	line 251, "pan.___", state 227, "(1)"
+	line 689, "pan.___", state 246, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
+	line 401, "pan.___", state 253, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 285, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 299, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 317, "(1)"
+	line 247, "pan.___", state 337, "(1)"
+	line 251, "pan.___", state 345, "(1)"
+	line 401, "pan.___", state 364, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 396, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 410, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 428, "(1)"
+	line 247, "pan.___", state 448, "(1)"
+	line 251, "pan.___", state 456, "(1)"
+	line 401, "pan.___", state 477, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 401, "pan.___", state 479, "(1)"
+	line 401, "pan.___", state 480, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
+	line 401, "pan.___", state 480, "else"
+	line 401, "pan.___", state 483, "(1)"
+	line 405, "pan.___", state 491, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 405, "pan.___", state 493, "(1)"
+	line 405, "pan.___", state 494, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
+	line 405, "pan.___", state 494, "else"
+	line 405, "pan.___", state 497, "(1)"
+	line 405, "pan.___", state 498, "(1)"
+	line 405, "pan.___", state 498, "(1)"
+	line 403, "pan.___", state 503, "((i<1))"
+	line 403, "pan.___", state 503, "((i>=1))"
+	line 410, "pan.___", state 509, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 511, "(1)"
+	line 410, "pan.___", state 512, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
+	line 410, "pan.___", state 512, "else"
+	line 410, "pan.___", state 515, "(1)"
+	line 410, "pan.___", state 516, "(1)"
+	line 410, "pan.___", state 516, "(1)"
+	line 414, "pan.___", state 523, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 525, "(1)"
+	line 414, "pan.___", state 526, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
+	line 414, "pan.___", state 526, "else"
+	line 414, "pan.___", state 529, "(1)"
+	line 414, "pan.___", state 530, "(1)"
+	line 414, "pan.___", state 530, "(1)"
+	line 412, "pan.___", state 535, "((i<2))"
+	line 412, "pan.___", state 535, "((i>=2))"
+	line 239, "pan.___", state 541, "(1)"
+	line 243, "pan.___", state 549, "(1)"
+	line 243, "pan.___", state 550, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 550, "else"
+	line 241, "pan.___", state 555, "((i<1))"
+	line 241, "pan.___", state 555, "((i>=1))"
+	line 247, "pan.___", state 561, "(1)"
+	line 247, "pan.___", state 562, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 562, "else"
+	line 251, "pan.___", state 569, "(1)"
+	line 251, "pan.___", state 570, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 570, "else"
+	line 249, "pan.___", state 575, "((i<2))"
+	line 249, "pan.___", state 575, "((i>=2))"
+	line 256, "pan.___", state 579, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 579, "else"
+	line 421, "pan.___", state 581, "(1)"
+	line 421, "pan.___", state 581, "(1)"
+	line 689, "pan.___", state 584, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
+	line 689, "pan.___", state 585, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
+	line 689, "pan.___", state 586, "(1)"
+	line 401, "pan.___", state 593, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 625, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 639, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 657, "(1)"
+	line 247, "pan.___", state 677, "(1)"
+	line 251, "pan.___", state 685, "(1)"
+	line 401, "pan.___", state 711, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 401, "pan.___", state 713, "(1)"
+	line 401, "pan.___", state 714, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
+	line 401, "pan.___", state 714, "else"
+	line 401, "pan.___", state 717, "(1)"
+	line 405, "pan.___", state 725, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 405, "pan.___", state 727, "(1)"
+	line 405, "pan.___", state 728, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
+	line 405, "pan.___", state 728, "else"
+	line 405, "pan.___", state 731, "(1)"
+	line 405, "pan.___", state 732, "(1)"
+	line 405, "pan.___", state 732, "(1)"
+	line 403, "pan.___", state 737, "((i<1))"
+	line 403, "pan.___", state 737, "((i>=1))"
+	line 410, "pan.___", state 743, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 745, "(1)"
+	line 410, "pan.___", state 746, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
+	line 410, "pan.___", state 746, "else"
+	line 410, "pan.___", state 749, "(1)"
+	line 410, "pan.___", state 750, "(1)"
+	line 410, "pan.___", state 750, "(1)"
+	line 414, "pan.___", state 757, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 759, "(1)"
+	line 414, "pan.___", state 760, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
+	line 414, "pan.___", state 760, "else"
+	line 414, "pan.___", state 763, "(1)"
+	line 414, "pan.___", state 764, "(1)"
+	line 414, "pan.___", state 764, "(1)"
+	line 412, "pan.___", state 769, "((i<2))"
+	line 412, "pan.___", state 769, "((i>=2))"
+	line 239, "pan.___", state 775, "(1)"
+	line 243, "pan.___", state 783, "(1)"
+	line 243, "pan.___", state 784, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 784, "else"
+	line 241, "pan.___", state 789, "((i<1))"
+	line 241, "pan.___", state 789, "((i>=1))"
+	line 247, "pan.___", state 795, "(1)"
+	line 247, "pan.___", state 796, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 796, "else"
+	line 251, "pan.___", state 803, "(1)"
+	line 251, "pan.___", state 804, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 804, "else"
+	line 256, "pan.___", state 813, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 813, "else"
+	line 421, "pan.___", state 815, "(1)"
+	line 421, "pan.___", state 815, "(1)"
+	line 401, "pan.___", state 822, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 401, "pan.___", state 824, "(1)"
+	line 401, "pan.___", state 825, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
+	line 401, "pan.___", state 825, "else"
+	line 401, "pan.___", state 828, "(1)"
+	line 405, "pan.___", state 836, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 405, "pan.___", state 838, "(1)"
+	line 405, "pan.___", state 839, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
+	line 405, "pan.___", state 839, "else"
+	line 405, "pan.___", state 842, "(1)"
+	line 405, "pan.___", state 843, "(1)"
+	line 405, "pan.___", state 843, "(1)"
+	line 403, "pan.___", state 848, "((i<1))"
+	line 403, "pan.___", state 848, "((i>=1))"
+	line 410, "pan.___", state 854, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 856, "(1)"
+	line 410, "pan.___", state 857, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
+	line 410, "pan.___", state 857, "else"
+	line 410, "pan.___", state 860, "(1)"
+	line 410, "pan.___", state 861, "(1)"
+	line 410, "pan.___", state 861, "(1)"
+	line 414, "pan.___", state 868, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 870, "(1)"
+	line 414, "pan.___", state 871, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
+	line 414, "pan.___", state 871, "else"
+	line 414, "pan.___", state 874, "(1)"
+	line 414, "pan.___", state 875, "(1)"
+	line 414, "pan.___", state 875, "(1)"
+	line 412, "pan.___", state 880, "((i<2))"
+	line 412, "pan.___", state 880, "((i>=2))"
+	line 239, "pan.___", state 886, "(1)"
+	line 243, "pan.___", state 894, "(1)"
+	line 243, "pan.___", state 895, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 895, "else"
+	line 241, "pan.___", state 900, "((i<1))"
+	line 241, "pan.___", state 900, "((i>=1))"
+	line 247, "pan.___", state 906, "(1)"
+	line 247, "pan.___", state 907, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 907, "else"
+	line 251, "pan.___", state 914, "(1)"
+	line 251, "pan.___", state 915, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 915, "else"
+	line 249, "pan.___", state 920, "((i<2))"
+	line 249, "pan.___", state 920, "((i>=2))"
+	line 256, "pan.___", state 924, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 924, "else"
+	line 421, "pan.___", state 926, "(1)"
+	line 421, "pan.___", state 926, "(1)"
+	line 697, "pan.___", state 930, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
+	line 401, "pan.___", state 935, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 967, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 981, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 999, "(1)"
+	line 247, "pan.___", state 1019, "(1)"
+	line 251, "pan.___", state 1027, "(1)"
+	line 401, "pan.___", state 1049, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1081, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 1095, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1113, "(1)"
+	line 247, "pan.___", state 1133, "(1)"
+	line 251, "pan.___", state 1141, "(1)"
+	line 401, "pan.___", state 1164, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1196, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 1210, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1228, "(1)"
+	line 247, "pan.___", state 1248, "(1)"
+	line 251, "pan.___", state 1256, "(1)"
+	line 401, "pan.___", state 1275, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1307, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 1321, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1339, "(1)"
+	line 247, "pan.___", state 1359, "(1)"
+	line 251, "pan.___", state 1367, "(1)"
+	line 401, "pan.___", state 1391, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1423, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 1437, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1455, "(1)"
+	line 247, "pan.___", state 1475, "(1)"
+	line 251, "pan.___", state 1483, "(1)"
+	line 401, "pan.___", state 1502, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1534, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 1548, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1566, "(1)"
+	line 247, "pan.___", state 1586, "(1)"
+	line 251, "pan.___", state 1594, "(1)"
+	line 401, "pan.___", state 1616, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1648, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 1662, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1680, "(1)"
+	line 247, "pan.___", state 1700, "(1)"
+	line 251, "pan.___", state 1708, "(1)"
+	line 736, "pan.___", state 1727, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
+	line 401, "pan.___", state 1734, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1766, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 1780, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1798, "(1)"
+	line 247, "pan.___", state 1818, "(1)"
+	line 251, "pan.___", state 1826, "(1)"
+	line 401, "pan.___", state 1845, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1877, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 1891, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1909, "(1)"
+	line 247, "pan.___", state 1929, "(1)"
+	line 251, "pan.___", state 1937, "(1)"
+	line 401, "pan.___", state 1958, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 401, "pan.___", state 1960, "(1)"
+	line 401, "pan.___", state 1961, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
+	line 401, "pan.___", state 1961, "else"
+	line 401, "pan.___", state 1964, "(1)"
+	line 405, "pan.___", state 1972, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 405, "pan.___", state 1974, "(1)"
+	line 405, "pan.___", state 1975, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
+	line 405, "pan.___", state 1975, "else"
+	line 405, "pan.___", state 1978, "(1)"
+	line 405, "pan.___", state 1979, "(1)"
+	line 405, "pan.___", state 1979, "(1)"
+	line 403, "pan.___", state 1984, "((i<1))"
+	line 403, "pan.___", state 1984, "((i>=1))"
+	line 410, "pan.___", state 1990, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 1992, "(1)"
+	line 410, "pan.___", state 1993, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
+	line 410, "pan.___", state 1993, "else"
+	line 410, "pan.___", state 1996, "(1)"
+	line 410, "pan.___", state 1997, "(1)"
+	line 410, "pan.___", state 1997, "(1)"
+	line 414, "pan.___", state 2004, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 2006, "(1)"
+	line 414, "pan.___", state 2007, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
+	line 414, "pan.___", state 2007, "else"
+	line 414, "pan.___", state 2010, "(1)"
+	line 414, "pan.___", state 2011, "(1)"
+	line 414, "pan.___", state 2011, "(1)"
+	line 412, "pan.___", state 2016, "((i<2))"
+	line 412, "pan.___", state 2016, "((i>=2))"
+	line 239, "pan.___", state 2022, "(1)"
+	line 243, "pan.___", state 2030, "(1)"
+	line 243, "pan.___", state 2031, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 2031, "else"
+	line 241, "pan.___", state 2036, "((i<1))"
+	line 241, "pan.___", state 2036, "((i>=1))"
+	line 247, "pan.___", state 2042, "(1)"
+	line 247, "pan.___", state 2043, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 2043, "else"
+	line 251, "pan.___", state 2050, "(1)"
+	line 251, "pan.___", state 2051, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 2051, "else"
+	line 249, "pan.___", state 2056, "((i<2))"
+	line 249, "pan.___", state 2056, "((i>=2))"
+	line 256, "pan.___", state 2060, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 2060, "else"
+	line 421, "pan.___", state 2062, "(1)"
+	line 421, "pan.___", state 2062, "(1)"
+	line 736, "pan.___", state 2065, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
+	line 736, "pan.___", state 2066, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
+	line 736, "pan.___", state 2067, "(1)"
+	line 401, "pan.___", state 2074, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 2106, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 2120, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 2138, "(1)"
+	line 247, "pan.___", state 2158, "(1)"
+	line 251, "pan.___", state 2166, "(1)"
+	line 401, "pan.___", state 2191, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 2223, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 2237, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 2255, "(1)"
+	line 247, "pan.___", state 2275, "(1)"
+	line 251, "pan.___", state 2283, "(1)"
+	line 401, "pan.___", state 2302, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 2334, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 2348, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 2366, "(1)"
+	line 247, "pan.___", state 2386, "(1)"
+	line 251, "pan.___", state 2394, "(1)"
+	line 239, "pan.___", state 2425, "(1)"
+	line 247, "pan.___", state 2445, "(1)"
+	line 251, "pan.___", state 2453, "(1)"
+	line 239, "pan.___", state 2468, "(1)"
+	line 247, "pan.___", state 2488, "(1)"
+	line 251, "pan.___", state 2496, "(1)"
+	line 887, "pan.___", state 2513, "-end-"
+	(246 of 2513 states)
+unreached in proctype urcu_writer
+	line 401, "pan.___", state 20, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 401, "pan.___", state 26, "(1)"
+	line 405, "pan.___", state 34, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 405, "pan.___", state 40, "(1)"
+	line 405, "pan.___", state 41, "(1)"
+	line 405, "pan.___", state 41, "(1)"
+	line 403, "pan.___", state 46, "((i<1))"
+	line 403, "pan.___", state 46, "((i>=1))"
+	line 410, "pan.___", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 410, "pan.___", state 58, "(1)"
+	line 410, "pan.___", state 59, "(1)"
+	line 410, "pan.___", state 59, "(1)"
+	line 414, "pan.___", state 72, "(1)"
+	line 414, "pan.___", state 73, "(1)"
+	line 414, "pan.___", state 73, "(1)"
+	line 412, "pan.___", state 78, "((i<2))"
+	line 412, "pan.___", state 78, "((i>=2))"
+	line 239, "pan.___", state 84, "(1)"
+	line 243, "pan.___", state 92, "(1)"
+	line 243, "pan.___", state 93, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 93, "else"
+	line 241, "pan.___", state 98, "((i<1))"
+	line 241, "pan.___", state 98, "((i>=1))"
+	line 247, "pan.___", state 104, "(1)"
+	line 247, "pan.___", state 105, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 105, "else"
+	line 251, "pan.___", state 112, "(1)"
+	line 251, "pan.___", state 113, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 113, "else"
+	line 249, "pan.___", state 118, "((i<2))"
+	line 249, "pan.___", state 118, "((i>=2))"
+	line 256, "pan.___", state 122, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 122, "else"
+	line 421, "pan.___", state 124, "(1)"
+	line 421, "pan.___", state 124, "(1)"
+	line 262, "pan.___", state 133, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 266, "pan.___", state 142, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 264, "pan.___", state 150, "((i<1))"
+	line 264, "pan.___", state 150, "((i>=1))"
+	line 270, "pan.___", state 155, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 1010, "pan.___", state 183, "old_data = cached_rcu_ptr.val[_pid]"
+	line 1021, "pan.___", state 187, "_proc_urcu_writer = (_proc_urcu_writer|(1<<4))"
+	line 401, "pan.___", state 195, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 401, "pan.___", state 201, "(1)"
+	line 405, "pan.___", state 209, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 405, "pan.___", state 215, "(1)"
+	line 405, "pan.___", state 216, "(1)"
+	line 405, "pan.___", state 216, "(1)"
+	line 410, "pan.___", state 229, "(1)"
+	line 414, "pan.___", state 241, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 259, "(1)"
+	line 243, "pan.___", state 267, "(1)"
+	line 251, "pan.___", state 287, "(1)"
+	line 421, "pan.___", state 299, "(1)"
+	line 421, "pan.___", state 299, "(1)"
+	line 405, "pan.___", state 322, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 354, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 243, "pan.___", state 380, "(1)"
+	line 251, "pan.___", state 400, "(1)"
+	line 405, "pan.___", state 442, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 243, "pan.___", state 500, "(1)"
+	line 405, "pan.___", state 553, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 243, "pan.___", state 611, "(1)"
+	line 405, "pan.___", state 666, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 414, "pan.___", state 698, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 243, "pan.___", state 724, "(1)"
+	line 251, "pan.___", state 744, "(1)"
+	line 1145, "pan.___", state 769, "_proc_urcu_writer = (_proc_urcu_writer|(1<<13))"
+	line 262, "pan.___", state 797, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 262, "pan.___", state 799, "(1)"
+	line 266, "pan.___", state 806, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 266, "pan.___", state 808, "(1)"
+	line 266, "pan.___", state 809, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
+	line 266, "pan.___", state 809, "else"
+	line 264, "pan.___", state 814, "((i<1))"
+	line 264, "pan.___", state 814, "((i>=1))"
+	line 270, "pan.___", state 819, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 270, "pan.___", state 821, "(1)"
+	line 270, "pan.___", state 822, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
+	line 270, "pan.___", state 822, "else"
+	line 274, "pan.___", state 828, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 830, "(1)"
+	line 274, "pan.___", state 831, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
+	line 274, "pan.___", state 831, "else"
+	line 272, "pan.___", state 836, "((i<2))"
+	line 272, "pan.___", state 836, "((i>=2))"
+	line 239, "pan.___", state 844, "(1)"
+	line 243, "pan.___", state 852, "(1)"
+	line 243, "pan.___", state 853, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 853, "else"
+	line 241, "pan.___", state 858, "((i<1))"
+	line 241, "pan.___", state 858, "((i>=1))"
+	line 247, "pan.___", state 864, "(1)"
+	line 247, "pan.___", state 865, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 865, "else"
+	line 251, "pan.___", state 872, "(1)"
+	line 251, "pan.___", state 873, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 873, "else"
+	line 256, "pan.___", state 882, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 882, "else"
+	line 1199, "pan.___", state 898, "((i<1))"
+	line 1199, "pan.___", state 898, "((i>=1))"
+	line 262, "pan.___", state 903, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 262, "pan.___", state 905, "(1)"
+	line 266, "pan.___", state 912, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 266, "pan.___", state 914, "(1)"
+	line 266, "pan.___", state 915, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
+	line 266, "pan.___", state 915, "else"
+	line 264, "pan.___", state 920, "((i<1))"
+	line 264, "pan.___", state 920, "((i>=1))"
+	line 270, "pan.___", state 925, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 270, "pan.___", state 927, "(1)"
+	line 270, "pan.___", state 928, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
+	line 270, "pan.___", state 928, "else"
+	line 274, "pan.___", state 934, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 936, "(1)"
+	line 274, "pan.___", state 937, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
+	line 274, "pan.___", state 937, "else"
+	line 272, "pan.___", state 942, "((i<2))"
+	line 272, "pan.___", state 942, "((i>=2))"
+	line 239, "pan.___", state 950, "(1)"
+	line 243, "pan.___", state 958, "(1)"
+	line 243, "pan.___", state 959, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 959, "else"
+	line 241, "pan.___", state 964, "((i<1))"
+	line 241, "pan.___", state 964, "((i>=1))"
+	line 247, "pan.___", state 970, "(1)"
+	line 247, "pan.___", state 971, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 971, "else"
+	line 251, "pan.___", state 978, "(1)"
+	line 251, "pan.___", state 979, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 979, "else"
+	line 256, "pan.___", state 988, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 988, "else"
+	line 289, "pan.___", state 990, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
+	line 289, "pan.___", state 990, "else"
+	line 1199, "pan.___", state 991, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
+	line 1199, "pan.___", state 991, "else"
+	line 266, "pan.___", state 1004, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 270, "pan.___", state 1017, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 1026, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1042, "(1)"
+	line 243, "pan.___", state 1050, "(1)"
+	line 247, "pan.___", state 1062, "(1)"
+	line 251, "pan.___", state 1070, "(1)"
+	line 262, "pan.___", state 1101, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 266, "pan.___", state 1110, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 270, "pan.___", state 1123, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 1132, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1148, "(1)"
+	line 243, "pan.___", state 1156, "(1)"
+	line 247, "pan.___", state 1168, "(1)"
+	line 251, "pan.___", state 1176, "(1)"
+	line 266, "pan.___", state 1202, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 1224, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1240, "(1)"
+	line 243, "pan.___", state 1248, "(1)"
+	line 247, "pan.___", state 1260, "(1)"
+	line 251, "pan.___", state 1268, "(1)"
+	line 262, "pan.___", state 1299, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 266, "pan.___", state 1308, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 270, "pan.___", state 1321, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 1330, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 239, "pan.___", state 1346, "(1)"
+	line 243, "pan.___", state 1354, "(1)"
+	line 247, "pan.___", state 1366, "(1)"
+	line 251, "pan.___", state 1374, "(1)"
+	line 262, "pan.___", state 1391, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 262, "pan.___", state 1393, "(1)"
+	line 266, "pan.___", state 1400, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 266, "pan.___", state 1402, "(1)"
+	line 266, "pan.___", state 1403, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
+	line 266, "pan.___", state 1403, "else"
+	line 264, "pan.___", state 1408, "((i<1))"
+	line 264, "pan.___", state 1408, "((i>=1))"
+	line 270, "pan.___", state 1413, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 270, "pan.___", state 1415, "(1)"
+	line 270, "pan.___", state 1416, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
+	line 270, "pan.___", state 1416, "else"
+	line 274, "pan.___", state 1422, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 1424, "(1)"
+	line 274, "pan.___", state 1425, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
+	line 274, "pan.___", state 1425, "else"
+	line 272, "pan.___", state 1430, "((i<2))"
+	line 272, "pan.___", state 1430, "((i>=2))"
+	line 239, "pan.___", state 1438, "(1)"
+	line 243, "pan.___", state 1446, "(1)"
+	line 243, "pan.___", state 1447, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 1447, "else"
+	line 241, "pan.___", state 1452, "((i<1))"
+	line 241, "pan.___", state 1452, "((i>=1))"
+	line 247, "pan.___", state 1458, "(1)"
+	line 247, "pan.___", state 1459, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 1459, "else"
+	line 251, "pan.___", state 1466, "(1)"
+	line 251, "pan.___", state 1467, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 1467, "else"
+	line 256, "pan.___", state 1476, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 1476, "else"
+	line 1210, "pan.___", state 1479, "i = 0"
+	line 1210, "pan.___", state 1481, "reader_barrier = 1"
+	line 1210, "pan.___", state 1492, "((i<1))"
+	line 1210, "pan.___", state 1492, "((i>=1))"
+	line 262, "pan.___", state 1497, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
+	line 262, "pan.___", state 1499, "(1)"
+	line 266, "pan.___", state 1506, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
+	line 266, "pan.___", state 1508, "(1)"
+	line 266, "pan.___", state 1509, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
+	line 266, "pan.___", state 1509, "else"
+	line 264, "pan.___", state 1514, "((i<1))"
+	line 264, "pan.___", state 1514, "((i>=1))"
+	line 270, "pan.___", state 1519, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
+	line 270, "pan.___", state 1521, "(1)"
+	line 270, "pan.___", state 1522, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
+	line 270, "pan.___", state 1522, "else"
+	line 274, "pan.___", state 1528, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
+	line 274, "pan.___", state 1530, "(1)"
+	line 274, "pan.___", state 1531, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
+	line 274, "pan.___", state 1531, "else"
+	line 272, "pan.___", state 1536, "((i<2))"
+	line 272, "pan.___", state 1536, "((i>=2))"
+	line 239, "pan.___", state 1544, "(1)"
+	line 243, "pan.___", state 1552, "(1)"
+	line 243, "pan.___", state 1553, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
+	line 243, "pan.___", state 1553, "else"
+	line 241, "pan.___", state 1558, "((i<1))"
+	line 241, "pan.___", state 1558, "((i>=1))"
+	line 247, "pan.___", state 1564, "(1)"
+	line 247, "pan.___", state 1565, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
+	line 247, "pan.___", state 1565, "else"
+	line 251, "pan.___", state 1572, "(1)"
+	line 251, "pan.___", state 1573, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
+	line 251, "pan.___", state 1573, "else"
+	line 256, "pan.___", state 1582, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
+	line 256, "pan.___", state 1582, "else"
+	line 289, "pan.___", state 1584, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
+	line 289, "pan.___", state 1584, "else"
+	line 1210, "pan.___", state 1585, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
+	line 1210, "pan.___", state 1585, "else"
+	line 1214, "pan.___", state 1588, "-end-"
+	(179 of 1588 states)
+unreached in proctype :init:
+	line 1225, "pan.___", state 9, "((j<2))"
+	line 1225, "pan.___", state 9, "((j>=2))"
+	line 1226, "pan.___", state 20, "((j<2))"
+	line 1226, "pan.___", state 20, "((j>=2))"
+	line 1231, "pan.___", state 33, "((j<2))"
+	line 1231, "pan.___", state 33, "((j>=2))"
+	line 1229, "pan.___", state 43, "((i<1))"
+	line 1229, "pan.___", state 43, "((i>=1))"
+	line 1239, "pan.___", state 54, "((j<2))"
+	line 1239, "pan.___", state 54, "((j>=2))"
+	line 1243, "pan.___", state 67, "((j<2))"
+	line 1243, "pan.___", state 67, "((j>=2))"
+	(6 of 78 states)
+unreached in proctype :never:
+	line 1277, "pan.___", state 8, "-end-"
+	(1 of 8 states)
+
+pan: elapsed time 36.6 seconds
+pan: rate 45762.039 states/second
+pan: avg transition delay 2.559e-06 usec
+cp .input.spin urcu_free_no_mb.spin.input
+cp .input.spin.trail urcu_free_no_mb.spin.input.trail
+make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'