X-Git-Url: https://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu-controldataflow-alpha-ipi%2Furcu_free_no_mb.log;fp=formal-model%2Furcu-controldataflow-alpha-ipi%2Furcu_free_no_mb.log;h=0000000000000000000000000000000000000000;hp=fbb91fe6c107eb9503baafa178c36abf0cca7a34;hb=5e32821aa6d74b755730c19a8aa66404d2c367c9;hpb=41e967af0a4bd23a88b87be39a6c7f7d68a9e2ca

diff --git a/formal-model/urcu-controldataflow-alpha-ipi/urcu_free_no_mb.log b/formal-model/urcu-controldataflow-alpha-ipi/urcu_free_no_mb.log
deleted file mode 100644
index fbb91fe..0000000
--- a/formal-model/urcu-controldataflow-alpha-ipi/urcu_free_no_mb.log
+++ /dev/null
@@ -1,824 +0,0 @@
-make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-alpha-ipi'
-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 -DCOLLAPSE -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 1362)
-Depth=    9193 States=    1e+06 Transitions= 2.02e+08 Memory=   513.615	t=    308 R=   3e+03
-Depth=    9193 States=    2e+06 Transitions= 4.02e+08 Memory=   560.100	t=    617 R=   3e+03
-pan: claim violated! (at depth 1482)
-pan: wrote .input.spin.trail
-
-(Spin Version 5.1.7 -- 23 December 2008)
-Warning: Search not completed
-	+ Partial Order Reduction
-	+ Compression
-
-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 80 byte, depth reached 9193, errors: 1
-  2638623 states, stored
-5.0906949e+08 states, matched
-5.1170812e+08 transitions (= stored+matched)
-2.7495835e+09 atomic steps
-hash conflicts: 3.3187407e+08 (resolved)
-
-Stats on memory usage (in Megabytes):
-  291.901	equivalent memory usage for states (stored*(State-vector + overhead))
-  123.793	actual memory usage for states (compression: 42.41%)
-         	state-vector as stored = 13 byte + 36 byte overhead
-    8.000	memory used for hash table (-w20)
-  457.764	memory used for DFS stack (-m10000000)
-  589.494	total actual memory usage
-
-nr of templates: [ globals chans procs ]
-collapse counts: [ 39337 2870 221 2 2 ]
-unreached in proctype urcu_reader
-	line 894, "pan.___", state 12, "((i<1))"
-	line 894, "pan.___", state 12, "((i>=1))"
-	line 268, "pan.___", state 61, "cache_dirty_urcu_gp_ctr = 0"
-	line 276, "pan.___", state 83, "cache_dirty_rcu_ptr = 0"
-	line 280, "pan.___", state 92, "cache_dirty_rcu_data[i] = 0"
-	line 245, "pan.___", state 108, "(1)"
-	line 249, "pan.___", state 116, "(1)"
-	line 253, "pan.___", state 128, "(1)"
-	line 257, "pan.___", state 136, "(1)"
-	line 407, "pan.___", state 162, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 194, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 208, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 227, "(1)"
-	line 434, "pan.___", state 257, "(1)"
-	line 438, "pan.___", state 270, "(1)"
-	line 696, "pan.___", state 291, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
-	line 407, "pan.___", state 298, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 330, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 344, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 363, "(1)"
-	line 434, "pan.___", state 393, "(1)"
-	line 438, "pan.___", state 406, "(1)"
-	line 407, "pan.___", state 427, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 459, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 473, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 492, "(1)"
-	line 434, "pan.___", state 522, "(1)"
-	line 438, "pan.___", state 535, "(1)"
-	line 407, "pan.___", state 558, "cache_dirty_urcu_gp_ctr = 0"
-	line 407, "pan.___", state 560, "(1)"
-	line 407, "pan.___", state 561, "(cache_dirty_urcu_gp_ctr)"
-	line 407, "pan.___", state 561, "else"
-	line 407, "pan.___", state 564, "(1)"
-	line 411, "pan.___", state 572, "cache_dirty_urcu_active_readers = 0"
-	line 411, "pan.___", state 574, "(1)"
-	line 411, "pan.___", state 575, "(cache_dirty_urcu_active_readers)"
-	line 411, "pan.___", state 575, "else"
-	line 411, "pan.___", state 578, "(1)"
-	line 411, "pan.___", state 579, "(1)"
-	line 411, "pan.___", state 579, "(1)"
-	line 409, "pan.___", state 584, "((i<1))"
-	line 409, "pan.___", state 584, "((i>=1))"
-	line 416, "pan.___", state 590, "cache_dirty_rcu_ptr = 0"
-	line 416, "pan.___", state 592, "(1)"
-	line 416, "pan.___", state 593, "(cache_dirty_rcu_ptr)"
-	line 416, "pan.___", state 593, "else"
-	line 416, "pan.___", state 596, "(1)"
-	line 416, "pan.___", state 597, "(1)"
-	line 416, "pan.___", state 597, "(1)"
-	line 420, "pan.___", state 604, "cache_dirty_rcu_data[i] = 0"
-	line 420, "pan.___", state 606, "(1)"
-	line 420, "pan.___", state 607, "(cache_dirty_rcu_data[i])"
-	line 420, "pan.___", state 607, "else"
-	line 420, "pan.___", state 610, "(1)"
-	line 420, "pan.___", state 611, "(1)"
-	line 420, "pan.___", state 611, "(1)"
-	line 418, "pan.___", state 616, "((i<2))"
-	line 418, "pan.___", state 616, "((i>=2))"
-	line 425, "pan.___", state 623, "(1)"
-	line 425, "pan.___", state 624, "(!(cache_dirty_urcu_gp_ctr))"
-	line 425, "pan.___", state 624, "else"
-	line 425, "pan.___", state 627, "(1)"
-	line 425, "pan.___", state 628, "(1)"
-	line 425, "pan.___", state 628, "(1)"
-	line 429, "pan.___", state 636, "(1)"
-	line 429, "pan.___", state 637, "(!(cache_dirty_urcu_active_readers))"
-	line 429, "pan.___", state 637, "else"
-	line 429, "pan.___", state 640, "(1)"
-	line 429, "pan.___", state 641, "(1)"
-	line 429, "pan.___", state 641, "(1)"
-	line 427, "pan.___", state 646, "((i<1))"
-	line 427, "pan.___", state 646, "((i>=1))"
-	line 434, "pan.___", state 653, "(1)"
-	line 434, "pan.___", state 654, "(!(cache_dirty_rcu_ptr))"
-	line 434, "pan.___", state 654, "else"
-	line 434, "pan.___", state 657, "(1)"
-	line 434, "pan.___", state 658, "(1)"
-	line 434, "pan.___", state 658, "(1)"
-	line 438, "pan.___", state 666, "(1)"
-	line 438, "pan.___", state 667, "(!(cache_dirty_rcu_data[i]))"
-	line 438, "pan.___", state 667, "else"
-	line 438, "pan.___", state 670, "(1)"
-	line 438, "pan.___", state 671, "(1)"
-	line 438, "pan.___", state 671, "(1)"
-	line 436, "pan.___", state 676, "((i<2))"
-	line 436, "pan.___", state 676, "((i>=2))"
-	line 446, "pan.___", state 680, "(1)"
-	line 446, "pan.___", state 680, "(1)"
-	line 696, "pan.___", state 683, "cached_urcu_active_readers = (tmp+1)"
-	line 696, "pan.___", state 684, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
-	line 696, "pan.___", state 685, "(1)"
-	line 407, "pan.___", state 692, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 724, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 738, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 757, "(1)"
-	line 434, "pan.___", state 787, "(1)"
-	line 438, "pan.___", state 800, "(1)"
-	line 407, "pan.___", state 828, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 860, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 874, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 893, "(1)"
-	line 434, "pan.___", state 923, "(1)"
-	line 438, "pan.___", state 936, "(1)"
-	line 407, "pan.___", state 957, "cache_dirty_urcu_gp_ctr = 0"
-	line 407, "pan.___", state 959, "(1)"
-	line 407, "pan.___", state 960, "(cache_dirty_urcu_gp_ctr)"
-	line 407, "pan.___", state 960, "else"
-	line 407, "pan.___", state 963, "(1)"
-	line 411, "pan.___", state 971, "cache_dirty_urcu_active_readers = 0"
-	line 411, "pan.___", state 973, "(1)"
-	line 411, "pan.___", state 974, "(cache_dirty_urcu_active_readers)"
-	line 411, "pan.___", state 974, "else"
-	line 411, "pan.___", state 977, "(1)"
-	line 411, "pan.___", state 978, "(1)"
-	line 411, "pan.___", state 978, "(1)"
-	line 409, "pan.___", state 983, "((i<1))"
-	line 409, "pan.___", state 983, "((i>=1))"
-	line 416, "pan.___", state 989, "cache_dirty_rcu_ptr = 0"
-	line 416, "pan.___", state 991, "(1)"
-	line 416, "pan.___", state 992, "(cache_dirty_rcu_ptr)"
-	line 416, "pan.___", state 992, "else"
-	line 416, "pan.___", state 995, "(1)"
-	line 416, "pan.___", state 996, "(1)"
-	line 416, "pan.___", state 996, "(1)"
-	line 420, "pan.___", state 1003, "cache_dirty_rcu_data[i] = 0"
-	line 420, "pan.___", state 1005, "(1)"
-	line 420, "pan.___", state 1006, "(cache_dirty_rcu_data[i])"
-	line 420, "pan.___", state 1006, "else"
-	line 420, "pan.___", state 1009, "(1)"
-	line 420, "pan.___", state 1010, "(1)"
-	line 420, "pan.___", state 1010, "(1)"
-	line 418, "pan.___", state 1015, "((i<2))"
-	line 418, "pan.___", state 1015, "((i>=2))"
-	line 425, "pan.___", state 1022, "(1)"
-	line 425, "pan.___", state 1023, "(!(cache_dirty_urcu_gp_ctr))"
-	line 425, "pan.___", state 1023, "else"
-	line 425, "pan.___", state 1026, "(1)"
-	line 425, "pan.___", state 1027, "(1)"
-	line 425, "pan.___", state 1027, "(1)"
-	line 429, "pan.___", state 1035, "(1)"
-	line 429, "pan.___", state 1036, "(!(cache_dirty_urcu_active_readers))"
-	line 429, "pan.___", state 1036, "else"
-	line 429, "pan.___", state 1039, "(1)"
-	line 429, "pan.___", state 1040, "(1)"
-	line 429, "pan.___", state 1040, "(1)"
-	line 427, "pan.___", state 1045, "((i<1))"
-	line 427, "pan.___", state 1045, "((i>=1))"
-	line 434, "pan.___", state 1052, "(1)"
-	line 434, "pan.___", state 1053, "(!(cache_dirty_rcu_ptr))"
-	line 434, "pan.___", state 1053, "else"
-	line 434, "pan.___", state 1056, "(1)"
-	line 434, "pan.___", state 1057, "(1)"
-	line 434, "pan.___", state 1057, "(1)"
-	line 438, "pan.___", state 1065, "(1)"
-	line 438, "pan.___", state 1066, "(!(cache_dirty_rcu_data[i]))"
-	line 438, "pan.___", state 1066, "else"
-	line 438, "pan.___", state 1069, "(1)"
-	line 438, "pan.___", state 1070, "(1)"
-	line 438, "pan.___", state 1070, "(1)"
-	line 436, "pan.___", state 1075, "((i<2))"
-	line 436, "pan.___", state 1075, "((i>=2))"
-	line 446, "pan.___", state 1079, "(1)"
-	line 446, "pan.___", state 1079, "(1)"
-	line 704, "pan.___", state 1083, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
-	line 407, "pan.___", state 1088, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 1120, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 1134, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 1153, "(1)"
-	line 434, "pan.___", state 1183, "(1)"
-	line 438, "pan.___", state 1196, "(1)"
-	line 407, "pan.___", state 1220, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 1252, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 1266, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 1285, "(1)"
-	line 434, "pan.___", state 1315, "(1)"
-	line 438, "pan.___", state 1328, "(1)"
-	line 407, "pan.___", state 1353, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 1385, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 1399, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 1418, "(1)"
-	line 434, "pan.___", state 1448, "(1)"
-	line 438, "pan.___", state 1461, "(1)"
-	line 407, "pan.___", state 1482, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 1514, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 1528, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 1547, "(1)"
-	line 434, "pan.___", state 1577, "(1)"
-	line 438, "pan.___", state 1590, "(1)"
-	line 407, "pan.___", state 1616, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 1648, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 1662, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 1681, "(1)"
-	line 434, "pan.___", state 1711, "(1)"
-	line 438, "pan.___", state 1724, "(1)"
-	line 407, "pan.___", state 1745, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 1777, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 1791, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 1810, "(1)"
-	line 434, "pan.___", state 1840, "(1)"
-	line 438, "pan.___", state 1853, "(1)"
-	line 407, "pan.___", state 1877, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 1909, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 1923, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 1942, "(1)"
-	line 434, "pan.___", state 1972, "(1)"
-	line 438, "pan.___", state 1985, "(1)"
-	line 743, "pan.___", state 2006, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
-	line 407, "pan.___", state 2013, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 2045, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 2059, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 2078, "(1)"
-	line 434, "pan.___", state 2108, "(1)"
-	line 438, "pan.___", state 2121, "(1)"
-	line 407, "pan.___", state 2142, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 2174, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 2188, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 2207, "(1)"
-	line 434, "pan.___", state 2237, "(1)"
-	line 438, "pan.___", state 2250, "(1)"
-	line 407, "pan.___", state 2273, "cache_dirty_urcu_gp_ctr = 0"
-	line 407, "pan.___", state 2275, "(1)"
-	line 407, "pan.___", state 2276, "(cache_dirty_urcu_gp_ctr)"
-	line 407, "pan.___", state 2276, "else"
-	line 407, "pan.___", state 2279, "(1)"
-	line 411, "pan.___", state 2287, "cache_dirty_urcu_active_readers = 0"
-	line 411, "pan.___", state 2289, "(1)"
-	line 411, "pan.___", state 2290, "(cache_dirty_urcu_active_readers)"
-	line 411, "pan.___", state 2290, "else"
-	line 411, "pan.___", state 2293, "(1)"
-	line 411, "pan.___", state 2294, "(1)"
-	line 411, "pan.___", state 2294, "(1)"
-	line 409, "pan.___", state 2299, "((i<1))"
-	line 409, "pan.___", state 2299, "((i>=1))"
-	line 416, "pan.___", state 2305, "cache_dirty_rcu_ptr = 0"
-	line 416, "pan.___", state 2307, "(1)"
-	line 416, "pan.___", state 2308, "(cache_dirty_rcu_ptr)"
-	line 416, "pan.___", state 2308, "else"
-	line 416, "pan.___", state 2311, "(1)"
-	line 416, "pan.___", state 2312, "(1)"
-	line 416, "pan.___", state 2312, "(1)"
-	line 420, "pan.___", state 2319, "cache_dirty_rcu_data[i] = 0"
-	line 420, "pan.___", state 2321, "(1)"
-	line 420, "pan.___", state 2322, "(cache_dirty_rcu_data[i])"
-	line 420, "pan.___", state 2322, "else"
-	line 420, "pan.___", state 2325, "(1)"
-	line 420, "pan.___", state 2326, "(1)"
-	line 420, "pan.___", state 2326, "(1)"
-	line 418, "pan.___", state 2331, "((i<2))"
-	line 418, "pan.___", state 2331, "((i>=2))"
-	line 425, "pan.___", state 2338, "(1)"
-	line 425, "pan.___", state 2339, "(!(cache_dirty_urcu_gp_ctr))"
-	line 425, "pan.___", state 2339, "else"
-	line 425, "pan.___", state 2342, "(1)"
-	line 425, "pan.___", state 2343, "(1)"
-	line 425, "pan.___", state 2343, "(1)"
-	line 429, "pan.___", state 2351, "(1)"
-	line 429, "pan.___", state 2352, "(!(cache_dirty_urcu_active_readers))"
-	line 429, "pan.___", state 2352, "else"
-	line 429, "pan.___", state 2355, "(1)"
-	line 429, "pan.___", state 2356, "(1)"
-	line 429, "pan.___", state 2356, "(1)"
-	line 427, "pan.___", state 2361, "((i<1))"
-	line 427, "pan.___", state 2361, "((i>=1))"
-	line 434, "pan.___", state 2368, "(1)"
-	line 434, "pan.___", state 2369, "(!(cache_dirty_rcu_ptr))"
-	line 434, "pan.___", state 2369, "else"
-	line 434, "pan.___", state 2372, "(1)"
-	line 434, "pan.___", state 2373, "(1)"
-	line 434, "pan.___", state 2373, "(1)"
-	line 438, "pan.___", state 2381, "(1)"
-	line 438, "pan.___", state 2382, "(!(cache_dirty_rcu_data[i]))"
-	line 438, "pan.___", state 2382, "else"
-	line 438, "pan.___", state 2385, "(1)"
-	line 438, "pan.___", state 2386, "(1)"
-	line 438, "pan.___", state 2386, "(1)"
-	line 436, "pan.___", state 2391, "((i<2))"
-	line 436, "pan.___", state 2391, "((i>=2))"
-	line 446, "pan.___", state 2395, "(1)"
-	line 446, "pan.___", state 2395, "(1)"
-	line 743, "pan.___", state 2398, "cached_urcu_active_readers = (tmp+1)"
-	line 743, "pan.___", state 2399, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
-	line 743, "pan.___", state 2400, "(1)"
-	line 407, "pan.___", state 2407, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 2439, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 2453, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 2472, "(1)"
-	line 434, "pan.___", state 2502, "(1)"
-	line 438, "pan.___", state 2515, "(1)"
-	line 407, "pan.___", state 2542, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 2574, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 2588, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 2607, "(1)"
-	line 434, "pan.___", state 2637, "(1)"
-	line 438, "pan.___", state 2650, "(1)"
-	line 407, "pan.___", state 2671, "cache_dirty_urcu_gp_ctr = 0"
-	line 416, "pan.___", state 2703, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 2717, "cache_dirty_rcu_data[i] = 0"
-	line 425, "pan.___", state 2736, "(1)"
-	line 434, "pan.___", state 2766, "(1)"
-	line 438, "pan.___", state 2779, "(1)"
-	line 245, "pan.___", state 2812, "(1)"
-	line 253, "pan.___", state 2832, "(1)"
-	line 257, "pan.___", state 2840, "(1)"
-	line 245, "pan.___", state 2855, "(1)"
-	line 253, "pan.___", state 2875, "(1)"
-	line 257, "pan.___", state 2883, "(1)"
-	line 929, "pan.___", state 2900, "-end-"
-	(246 of 2900 states)
-unreached in proctype urcu_writer
-	line 1018, "pan.___", state 12, "((i<1))"
-	line 1018, "pan.___", state 12, "((i>=1))"
-	line 407, "pan.___", state 47, "cache_dirty_urcu_gp_ctr = 0"
-	line 407, "pan.___", state 53, "(1)"
-	line 411, "pan.___", state 61, "cache_dirty_urcu_active_readers = 0"
-	line 411, "pan.___", state 67, "(1)"
-	line 411, "pan.___", state 68, "(1)"
-	line 411, "pan.___", state 68, "(1)"
-	line 409, "pan.___", state 73, "((i<1))"
-	line 409, "pan.___", state 73, "((i>=1))"
-	line 416, "pan.___", state 79, "cache_dirty_rcu_ptr = 0"
-	line 416, "pan.___", state 85, "(1)"
-	line 416, "pan.___", state 86, "(1)"
-	line 416, "pan.___", state 86, "(1)"
-	line 420, "pan.___", state 99, "(1)"
-	line 420, "pan.___", state 100, "(1)"
-	line 420, "pan.___", state 100, "(1)"
-	line 418, "pan.___", state 105, "((i<2))"
-	line 418, "pan.___", state 105, "((i>=2))"
-	line 425, "pan.___", state 112, "(1)"
-	line 425, "pan.___", state 113, "(!(cache_dirty_urcu_gp_ctr))"
-	line 425, "pan.___", state 113, "else"
-	line 425, "pan.___", state 116, "(1)"
-	line 425, "pan.___", state 117, "(1)"
-	line 425, "pan.___", state 117, "(1)"
-	line 429, "pan.___", state 125, "(1)"
-	line 429, "pan.___", state 126, "(!(cache_dirty_urcu_active_readers))"
-	line 429, "pan.___", state 126, "else"
-	line 429, "pan.___", state 129, "(1)"
-	line 429, "pan.___", state 130, "(1)"
-	line 429, "pan.___", state 130, "(1)"
-	line 427, "pan.___", state 135, "((i<1))"
-	line 427, "pan.___", state 135, "((i>=1))"
-	line 434, "pan.___", state 142, "(1)"
-	line 434, "pan.___", state 143, "(!(cache_dirty_rcu_ptr))"
-	line 434, "pan.___", state 143, "else"
-	line 434, "pan.___", state 146, "(1)"
-	line 434, "pan.___", state 147, "(1)"
-	line 434, "pan.___", state 147, "(1)"
-	line 438, "pan.___", state 155, "(1)"
-	line 438, "pan.___", state 156, "(!(cache_dirty_rcu_data[i]))"
-	line 438, "pan.___", state 156, "else"
-	line 438, "pan.___", state 159, "(1)"
-	line 438, "pan.___", state 160, "(1)"
-	line 438, "pan.___", state 160, "(1)"
-	line 436, "pan.___", state 165, "((i<2))"
-	line 436, "pan.___", state 165, "((i>=2))"
-	line 446, "pan.___", state 169, "(1)"
-	line 446, "pan.___", state 169, "(1)"
-	line 268, "pan.___", state 178, "cache_dirty_urcu_gp_ctr = 0"
-	line 272, "pan.___", state 187, "cache_dirty_urcu_active_readers = 0"
-	line 270, "pan.___", state 195, "((i<1))"
-	line 270, "pan.___", state 195, "((i>=1))"
-	line 276, "pan.___", state 200, "cache_dirty_rcu_ptr = 0"
-	line 1088, "pan.___", state 228, "old_data = cached_rcu_ptr"
-	line 1099, "pan.___", state 232, "_proc_urcu_writer = (_proc_urcu_writer|(1<<4))"
-	line 407, "pan.___", state 240, "cache_dirty_urcu_gp_ctr = 0"
-	line 407, "pan.___", state 246, "(1)"
-	line 411, "pan.___", state 254, "cache_dirty_urcu_active_readers = 0"
-	line 411, "pan.___", state 260, "(1)"
-	line 411, "pan.___", state 261, "(1)"
-	line 411, "pan.___", state 261, "(1)"
-	line 409, "pan.___", state 266, "((i<1))"
-	line 409, "pan.___", state 266, "((i>=1))"
-	line 416, "pan.___", state 274, "(1)"
-	line 416, "pan.___", state 275, "(cache_dirty_rcu_ptr)"
-	line 416, "pan.___", state 275, "else"
-	line 416, "pan.___", state 278, "(1)"
-	line 416, "pan.___", state 279, "(1)"
-	line 416, "pan.___", state 279, "(1)"
-	line 420, "pan.___", state 286, "cache_dirty_rcu_data[i] = 0"
-	line 420, "pan.___", state 292, "(1)"
-	line 420, "pan.___", state 293, "(1)"
-	line 420, "pan.___", state 293, "(1)"
-	line 418, "pan.___", state 298, "((i<2))"
-	line 418, "pan.___", state 298, "((i>=2))"
-	line 425, "pan.___", state 305, "(1)"
-	line 425, "pan.___", state 306, "(!(cache_dirty_urcu_gp_ctr))"
-	line 425, "pan.___", state 306, "else"
-	line 425, "pan.___", state 309, "(1)"
-	line 425, "pan.___", state 310, "(1)"
-	line 425, "pan.___", state 310, "(1)"
-	line 429, "pan.___", state 318, "(1)"
-	line 429, "pan.___", state 319, "(!(cache_dirty_urcu_active_readers))"
-	line 429, "pan.___", state 319, "else"
-	line 429, "pan.___", state 322, "(1)"
-	line 429, "pan.___", state 323, "(1)"
-	line 429, "pan.___", state 323, "(1)"
-	line 427, "pan.___", state 328, "((i<1))"
-	line 427, "pan.___", state 328, "((i>=1))"
-	line 434, "pan.___", state 335, "(1)"
-	line 434, "pan.___", state 336, "(!(cache_dirty_rcu_ptr))"
-	line 434, "pan.___", state 336, "else"
-	line 434, "pan.___", state 339, "(1)"
-	line 434, "pan.___", state 340, "(1)"
-	line 434, "pan.___", state 340, "(1)"
-	line 438, "pan.___", state 348, "(1)"
-	line 438, "pan.___", state 349, "(!(cache_dirty_rcu_data[i]))"
-	line 438, "pan.___", state 349, "else"
-	line 438, "pan.___", state 352, "(1)"
-	line 438, "pan.___", state 353, "(1)"
-	line 438, "pan.___", state 353, "(1)"
-	line 436, "pan.___", state 358, "((i<2))"
-	line 436, "pan.___", state 358, "((i>=2))"
-	line 446, "pan.___", state 362, "(1)"
-	line 446, "pan.___", state 362, "(1)"
-	line 407, "pan.___", state 373, "(1)"
-	line 407, "pan.___", state 374, "(cache_dirty_urcu_gp_ctr)"
-	line 407, "pan.___", state 374, "else"
-	line 407, "pan.___", state 377, "(1)"
-	line 411, "pan.___", state 385, "cache_dirty_urcu_active_readers = 0"
-	line 411, "pan.___", state 391, "(1)"
-	line 411, "pan.___", state 392, "(1)"
-	line 411, "pan.___", state 392, "(1)"
-	line 409, "pan.___", state 397, "((i<1))"
-	line 409, "pan.___", state 397, "((i>=1))"
-	line 416, "pan.___", state 403, "cache_dirty_rcu_ptr = 0"
-	line 416, "pan.___", state 409, "(1)"
-	line 416, "pan.___", state 410, "(1)"
-	line 416, "pan.___", state 410, "(1)"
-	line 420, "pan.___", state 417, "cache_dirty_rcu_data[i] = 0"
-	line 420, "pan.___", state 423, "(1)"
-	line 420, "pan.___", state 424, "(1)"
-	line 420, "pan.___", state 424, "(1)"
-	line 418, "pan.___", state 429, "((i<2))"
-	line 418, "pan.___", state 429, "((i>=2))"
-	line 425, "pan.___", state 436, "(1)"
-	line 425, "pan.___", state 437, "(!(cache_dirty_urcu_gp_ctr))"
-	line 425, "pan.___", state 437, "else"
-	line 425, "pan.___", state 440, "(1)"
-	line 425, "pan.___", state 441, "(1)"
-	line 425, "pan.___", state 441, "(1)"
-	line 429, "pan.___", state 449, "(1)"
-	line 429, "pan.___", state 450, "(!(cache_dirty_urcu_active_readers))"
-	line 429, "pan.___", state 450, "else"
-	line 429, "pan.___", state 453, "(1)"
-	line 429, "pan.___", state 454, "(1)"
-	line 429, "pan.___", state 454, "(1)"
-	line 427, "pan.___", state 459, "((i<1))"
-	line 427, "pan.___", state 459, "((i>=1))"
-	line 434, "pan.___", state 466, "(1)"
-	line 434, "pan.___", state 467, "(!(cache_dirty_rcu_ptr))"
-	line 434, "pan.___", state 467, "else"
-	line 434, "pan.___", state 470, "(1)"
-	line 434, "pan.___", state 471, "(1)"
-	line 434, "pan.___", state 471, "(1)"
-	line 438, "pan.___", state 479, "(1)"
-	line 438, "pan.___", state 480, "(!(cache_dirty_rcu_data[i]))"
-	line 438, "pan.___", state 480, "else"
-	line 438, "pan.___", state 483, "(1)"
-	line 438, "pan.___", state 484, "(1)"
-	line 438, "pan.___", state 484, "(1)"
-	line 436, "pan.___", state 489, "((i<2))"
-	line 436, "pan.___", state 489, "((i>=2))"
-	line 446, "pan.___", state 493, "(1)"
-	line 446, "pan.___", state 493, "(1)"
-	line 1153, "pan.___", state 504, "_proc_urcu_writer = (_proc_urcu_writer&~((1<<9)))"
-	line 1158, "pan.___", state 505, "_proc_urcu_writer = (_proc_urcu_writer&~(((1<<8)|(1<<7))))"
-	line 407, "pan.___", state 510, "cache_dirty_urcu_gp_ctr = 0"
-	line 407, "pan.___", state 516, "(1)"
-	line 411, "pan.___", state 524, "cache_dirty_urcu_active_readers = 0"
-	line 411, "pan.___", state 530, "(1)"
-	line 411, "pan.___", state 531, "(1)"
-	line 411, "pan.___", state 531, "(1)"
-	line 409, "pan.___", state 536, "((i<1))"
-	line 409, "pan.___", state 536, "((i>=1))"
-	line 416, "pan.___", state 542, "cache_dirty_rcu_ptr = 0"
-	line 416, "pan.___", state 548, "(1)"
-	line 416, "pan.___", state 549, "(1)"
-	line 416, "pan.___", state 549, "(1)"
-	line 420, "pan.___", state 556, "cache_dirty_rcu_data[i] = 0"
-	line 420, "pan.___", state 562, "(1)"
-	line 420, "pan.___", state 563, "(1)"
-	line 420, "pan.___", state 563, "(1)"
-	line 418, "pan.___", state 568, "((i<2))"
-	line 418, "pan.___", state 568, "((i>=2))"
-	line 425, "pan.___", state 575, "(1)"
-	line 425, "pan.___", state 576, "(!(cache_dirty_urcu_gp_ctr))"
-	line 425, "pan.___", state 576, "else"
-	line 425, "pan.___", state 579, "(1)"
-	line 425, "pan.___", state 580, "(1)"
-	line 425, "pan.___", state 580, "(1)"
-	line 429, "pan.___", state 588, "(1)"
-	line 429, "pan.___", state 589, "(!(cache_dirty_urcu_active_readers))"
-	line 429, "pan.___", state 589, "else"
-	line 429, "pan.___", state 592, "(1)"
-	line 429, "pan.___", state 593, "(1)"
-	line 429, "pan.___", state 593, "(1)"
-	line 427, "pan.___", state 598, "((i<1))"
-	line 427, "pan.___", state 598, "((i>=1))"
-	line 434, "pan.___", state 605, "(1)"
-	line 434, "pan.___", state 606, "(!(cache_dirty_rcu_ptr))"
-	line 434, "pan.___", state 606, "else"
-	line 434, "pan.___", state 609, "(1)"
-	line 434, "pan.___", state 610, "(1)"
-	line 434, "pan.___", state 610, "(1)"
-	line 438, "pan.___", state 618, "(1)"
-	line 438, "pan.___", state 619, "(!(cache_dirty_rcu_data[i]))"
-	line 438, "pan.___", state 619, "else"
-	line 438, "pan.___", state 622, "(1)"
-	line 438, "pan.___", state 623, "(1)"
-	line 438, "pan.___", state 623, "(1)"
-	line 446, "pan.___", state 632, "(1)"
-	line 446, "pan.___", state 632, "(1)"
-	line 407, "pan.___", state 639, "cache_dirty_urcu_gp_ctr = 0"
-	line 411, "pan.___", state 653, "cache_dirty_urcu_active_readers = 0"
-	line 416, "pan.___", state 671, "cache_dirty_rcu_ptr = 0"
-	line 425, "pan.___", state 704, "(1)"
-	line 429, "pan.___", state 717, "(1)"
-	line 434, "pan.___", state 734, "(1)"
-	line 438, "pan.___", state 747, "(1)"
-	line 411, "pan.___", state 784, "cache_dirty_urcu_active_readers = 0"
-	line 416, "pan.___", state 802, "cache_dirty_rcu_ptr = 0"
-	line 420, "pan.___", state 816, "cache_dirty_rcu_data[i] = 0"
-	line 429, "pan.___", state 848, "(1)"
-	line 434, "pan.___", state 865, "(1)"
-	line 438, "pan.___", state 878, "(1)"
-	line 1235, "pan.___", state 905, "_proc_urcu_writer = (_proc_urcu_writer|(1<<13))"
-	line 268, "pan.___", state 933, "cache_dirty_urcu_gp_ctr = 0"
-	line 268, "pan.___", state 935, "(1)"
-	line 272, "pan.___", state 942, "cache_dirty_urcu_active_readers = 0"
-	line 272, "pan.___", state 944, "(1)"
-	line 272, "pan.___", state 945, "(cache_dirty_urcu_active_readers)"
-	line 272, "pan.___", state 945, "else"
-	line 270, "pan.___", state 950, "((i<1))"
-	line 270, "pan.___", state 950, "((i>=1))"
-	line 276, "pan.___", state 955, "cache_dirty_rcu_ptr = 0"
-	line 276, "pan.___", state 957, "(1)"
-	line 276, "pan.___", state 958, "(cache_dirty_rcu_ptr)"
-	line 276, "pan.___", state 958, "else"
-	line 280, "pan.___", state 964, "cache_dirty_rcu_data[i] = 0"
-	line 280, "pan.___", state 966, "(1)"
-	line 280, "pan.___", state 967, "(cache_dirty_rcu_data[i])"
-	line 280, "pan.___", state 967, "else"
-	line 278, "pan.___", state 972, "((i<2))"
-	line 278, "pan.___", state 972, "((i>=2))"
-	line 245, "pan.___", state 980, "(1)"
-	line 249, "pan.___", state 988, "(1)"
-	line 249, "pan.___", state 989, "(!(cache_dirty_urcu_active_readers))"
-	line 249, "pan.___", state 989, "else"
-	line 247, "pan.___", state 994, "((i<1))"
-	line 247, "pan.___", state 994, "((i>=1))"
-	line 253, "pan.___", state 1000, "(1)"
-	line 253, "pan.___", state 1001, "(!(cache_dirty_rcu_ptr))"
-	line 253, "pan.___", state 1001, "else"
-	line 257, "pan.___", state 1008, "(1)"
-	line 257, "pan.___", state 1009, "(!(cache_dirty_rcu_data[i]))"
-	line 257, "pan.___", state 1009, "else"
-	line 262, "pan.___", state 1018, "(!(cache_dirty_urcu_gp_ctr))"
-	line 262, "pan.___", state 1018, "else"
-	line 1289, "pan.___", state 1034, "((i<1))"
-	line 1289, "pan.___", state 1034, "((i>=1))"
-	line 268, "pan.___", state 1039, "cache_dirty_urcu_gp_ctr = 0"
-	line 268, "pan.___", state 1041, "(1)"
-	line 272, "pan.___", state 1048, "cache_dirty_urcu_active_readers = 0"
-	line 272, "pan.___", state 1050, "(1)"
-	line 272, "pan.___", state 1051, "(cache_dirty_urcu_active_readers)"
-	line 272, "pan.___", state 1051, "else"
-	line 270, "pan.___", state 1056, "((i<1))"
-	line 270, "pan.___", state 1056, "((i>=1))"
-	line 276, "pan.___", state 1061, "cache_dirty_rcu_ptr = 0"
-	line 276, "pan.___", state 1063, "(1)"
-	line 276, "pan.___", state 1064, "(cache_dirty_rcu_ptr)"
-	line 276, "pan.___", state 1064, "else"
-	line 280, "pan.___", state 1070, "cache_dirty_rcu_data[i] = 0"
-	line 280, "pan.___", state 1072, "(1)"
-	line 280, "pan.___", state 1073, "(cache_dirty_rcu_data[i])"
-	line 280, "pan.___", state 1073, "else"
-	line 278, "pan.___", state 1078, "((i<2))"
-	line 278, "pan.___", state 1078, "((i>=2))"
-	line 245, "pan.___", state 1086, "(1)"
-	line 249, "pan.___", state 1094, "(1)"
-	line 249, "pan.___", state 1095, "(!(cache_dirty_urcu_active_readers))"
-	line 249, "pan.___", state 1095, "else"
-	line 247, "pan.___", state 1100, "((i<1))"
-	line 247, "pan.___", state 1100, "((i>=1))"
-	line 253, "pan.___", state 1106, "(1)"
-	line 253, "pan.___", state 1107, "(!(cache_dirty_rcu_ptr))"
-	line 253, "pan.___", state 1107, "else"
-	line 257, "pan.___", state 1114, "(1)"
-	line 257, "pan.___", state 1115, "(!(cache_dirty_rcu_data[i]))"
-	line 257, "pan.___", state 1115, "else"
-	line 262, "pan.___", state 1124, "(!(cache_dirty_urcu_gp_ctr))"
-	line 262, "pan.___", state 1124, "else"
-	line 295, "pan.___", state 1126, "(cache_dirty_urcu_gp_ctr)"
-	line 295, "pan.___", state 1126, "else"
-	line 1289, "pan.___", state 1127, "(cache_dirty_urcu_gp_ctr)"
-	line 1289, "pan.___", state 1127, "else"
-	line 268, "pan.___", state 1131, "cache_dirty_urcu_gp_ctr = 0"
-	line 268, "pan.___", state 1133, "(1)"
-	line 272, "pan.___", state 1140, "cache_dirty_urcu_active_readers = 0"
-	line 272, "pan.___", state 1142, "(1)"
-	line 272, "pan.___", state 1143, "(cache_dirty_urcu_active_readers)"
-	line 272, "pan.___", state 1143, "else"
-	line 270, "pan.___", state 1148, "((i<1))"
-	line 270, "pan.___", state 1148, "((i>=1))"
-	line 276, "pan.___", state 1153, "cache_dirty_rcu_ptr = 0"
-	line 276, "pan.___", state 1155, "(1)"
-	line 276, "pan.___", state 1156, "(cache_dirty_rcu_ptr)"
-	line 276, "pan.___", state 1156, "else"
-	line 280, "pan.___", state 1162, "cache_dirty_rcu_data[i] = 0"
-	line 280, "pan.___", state 1164, "(1)"
-	line 280, "pan.___", state 1165, "(cache_dirty_rcu_data[i])"
-	line 280, "pan.___", state 1165, "else"
-	line 278, "pan.___", state 1170, "((i<2))"
-	line 278, "pan.___", state 1170, "((i>=2))"
-	line 245, "pan.___", state 1178, "(1)"
-	line 249, "pan.___", state 1186, "(1)"
-	line 249, "pan.___", state 1187, "(!(cache_dirty_urcu_active_readers))"
-	line 249, "pan.___", state 1187, "else"
-	line 247, "pan.___", state 1192, "((i<1))"
-	line 247, "pan.___", state 1192, "((i>=1))"
-	line 253, "pan.___", state 1198, "(1)"
-	line 253, "pan.___", state 1199, "(!(cache_dirty_rcu_ptr))"
-	line 253, "pan.___", state 1199, "else"
-	line 257, "pan.___", state 1206, "(1)"
-	line 257, "pan.___", state 1207, "(!(cache_dirty_rcu_data[i]))"
-	line 257, "pan.___", state 1207, "else"
-	line 262, "pan.___", state 1216, "(!(cache_dirty_urcu_gp_ctr))"
-	line 262, "pan.___", state 1216, "else"
-	line 1293, "pan.___", state 1219, "i = 0"
-	line 1293, "pan.___", state 1221, "reader_barrier = 1"
-	line 1293, "pan.___", state 1232, "((i<1))"
-	line 1293, "pan.___", state 1232, "((i>=1))"
-	line 268, "pan.___", state 1237, "cache_dirty_urcu_gp_ctr = 0"
-	line 268, "pan.___", state 1239, "(1)"
-	line 272, "pan.___", state 1246, "cache_dirty_urcu_active_readers = 0"
-	line 272, "pan.___", state 1248, "(1)"
-	line 272, "pan.___", state 1249, "(cache_dirty_urcu_active_readers)"
-	line 272, "pan.___", state 1249, "else"
-	line 270, "pan.___", state 1254, "((i<1))"
-	line 270, "pan.___", state 1254, "((i>=1))"
-	line 276, "pan.___", state 1259, "cache_dirty_rcu_ptr = 0"
-	line 276, "pan.___", state 1261, "(1)"
-	line 276, "pan.___", state 1262, "(cache_dirty_rcu_ptr)"
-	line 276, "pan.___", state 1262, "else"
-	line 280, "pan.___", state 1268, "cache_dirty_rcu_data[i] = 0"
-	line 280, "pan.___", state 1270, "(1)"
-	line 280, "pan.___", state 1271, "(cache_dirty_rcu_data[i])"
-	line 280, "pan.___", state 1271, "else"
-	line 278, "pan.___", state 1276, "((i<2))"
-	line 278, "pan.___", state 1276, "((i>=2))"
-	line 245, "pan.___", state 1284, "(1)"
-	line 249, "pan.___", state 1292, "(1)"
-	line 249, "pan.___", state 1293, "(!(cache_dirty_urcu_active_readers))"
-	line 249, "pan.___", state 1293, "else"
-	line 247, "pan.___", state 1298, "((i<1))"
-	line 247, "pan.___", state 1298, "((i>=1))"
-	line 253, "pan.___", state 1304, "(1)"
-	line 253, "pan.___", state 1305, "(!(cache_dirty_rcu_ptr))"
-	line 253, "pan.___", state 1305, "else"
-	line 257, "pan.___", state 1312, "(1)"
-	line 257, "pan.___", state 1313, "(!(cache_dirty_rcu_data[i]))"
-	line 257, "pan.___", state 1313, "else"
-	line 262, "pan.___", state 1322, "(!(cache_dirty_urcu_gp_ctr))"
-	line 262, "pan.___", state 1322, "else"
-	line 295, "pan.___", state 1324, "(cache_dirty_urcu_gp_ctr)"
-	line 295, "pan.___", state 1324, "else"
-	line 1293, "pan.___", state 1325, "(cache_dirty_urcu_gp_ctr)"
-	line 1293, "pan.___", state 1325, "else"
-	line 272, "pan.___", state 1338, "cache_dirty_urcu_active_readers = 0"
-	line 276, "pan.___", state 1351, "cache_dirty_rcu_ptr = 0"
-	line 280, "pan.___", state 1360, "cache_dirty_rcu_data[i] = 0"
-	line 245, "pan.___", state 1376, "(1)"
-	line 249, "pan.___", state 1384, "(1)"
-	line 253, "pan.___", state 1396, "(1)"
-	line 257, "pan.___", state 1404, "(1)"
-	line 268, "pan.___", state 1435, "cache_dirty_urcu_gp_ctr = 0"
-	line 272, "pan.___", state 1444, "cache_dirty_urcu_active_readers = 0"
-	line 276, "pan.___", state 1457, "cache_dirty_rcu_ptr = 0"
-	line 280, "pan.___", state 1466, "cache_dirty_rcu_data[i] = 0"
-	line 245, "pan.___", state 1482, "(1)"
-	line 249, "pan.___", state 1490, "(1)"
-	line 253, "pan.___", state 1502, "(1)"
-	line 257, "pan.___", state 1510, "(1)"
-	line 268, "pan.___", state 1527, "cache_dirty_urcu_gp_ctr = 0"
-	line 268, "pan.___", state 1529, "(1)"
-	line 272, "pan.___", state 1536, "cache_dirty_urcu_active_readers = 0"
-	line 272, "pan.___", state 1538, "(1)"
-	line 272, "pan.___", state 1539, "(cache_dirty_urcu_active_readers)"
-	line 272, "pan.___", state 1539, "else"
-	line 270, "pan.___", state 1544, "((i<1))"
-	line 270, "pan.___", state 1544, "((i>=1))"
-	line 276, "pan.___", state 1549, "cache_dirty_rcu_ptr = 0"
-	line 276, "pan.___", state 1551, "(1)"
-	line 276, "pan.___", state 1552, "(cache_dirty_rcu_ptr)"
-	line 276, "pan.___", state 1552, "else"
-	line 280, "pan.___", state 1558, "cache_dirty_rcu_data[i] = 0"
-	line 280, "pan.___", state 1560, "(1)"
-	line 280, "pan.___", state 1561, "(cache_dirty_rcu_data[i])"
-	line 280, "pan.___", state 1561, "else"
-	line 278, "pan.___", state 1566, "((i<2))"
-	line 278, "pan.___", state 1566, "((i>=2))"
-	line 245, "pan.___", state 1574, "(1)"
-	line 249, "pan.___", state 1582, "(1)"
-	line 249, "pan.___", state 1583, "(!(cache_dirty_urcu_active_readers))"
-	line 249, "pan.___", state 1583, "else"
-	line 247, "pan.___", state 1588, "((i<1))"
-	line 247, "pan.___", state 1588, "((i>=1))"
-	line 253, "pan.___", state 1594, "(1)"
-	line 253, "pan.___", state 1595, "(!(cache_dirty_rcu_ptr))"
-	line 253, "pan.___", state 1595, "else"
-	line 257, "pan.___", state 1602, "(1)"
-	line 257, "pan.___", state 1603, "(!(cache_dirty_rcu_data[i]))"
-	line 257, "pan.___", state 1603, "else"
-	line 262, "pan.___", state 1612, "(!(cache_dirty_urcu_gp_ctr))"
-	line 262, "pan.___", state 1612, "else"
-	line 1300, "pan.___", state 1615, "i = 0"
-	line 1300, "pan.___", state 1617, "reader_barrier = 1"
-	line 1300, "pan.___", state 1628, "((i<1))"
-	line 1300, "pan.___", state 1628, "((i>=1))"
-	line 268, "pan.___", state 1633, "cache_dirty_urcu_gp_ctr = 0"
-	line 268, "pan.___", state 1635, "(1)"
-	line 272, "pan.___", state 1642, "cache_dirty_urcu_active_readers = 0"
-	line 272, "pan.___", state 1644, "(1)"
-	line 272, "pan.___", state 1645, "(cache_dirty_urcu_active_readers)"
-	line 272, "pan.___", state 1645, "else"
-	line 270, "pan.___", state 1650, "((i<1))"
-	line 270, "pan.___", state 1650, "((i>=1))"
-	line 276, "pan.___", state 1655, "cache_dirty_rcu_ptr = 0"
-	line 276, "pan.___", state 1657, "(1)"
-	line 276, "pan.___", state 1658, "(cache_dirty_rcu_ptr)"
-	line 276, "pan.___", state 1658, "else"
-	line 280, "pan.___", state 1664, "cache_dirty_rcu_data[i] = 0"
-	line 280, "pan.___", state 1666, "(1)"
-	line 280, "pan.___", state 1667, "(cache_dirty_rcu_data[i])"
-	line 280, "pan.___", state 1667, "else"
-	line 278, "pan.___", state 1672, "((i<2))"
-	line 278, "pan.___", state 1672, "((i>=2))"
-	line 245, "pan.___", state 1680, "(1)"
-	line 249, "pan.___", state 1688, "(1)"
-	line 249, "pan.___", state 1689, "(!(cache_dirty_urcu_active_readers))"
-	line 249, "pan.___", state 1689, "else"
-	line 247, "pan.___", state 1694, "((i<1))"
-	line 247, "pan.___", state 1694, "((i>=1))"
-	line 253, "pan.___", state 1700, "(1)"
-	line 253, "pan.___", state 1701, "(!(cache_dirty_rcu_ptr))"
-	line 253, "pan.___", state 1701, "else"
-	line 257, "pan.___", state 1708, "(1)"
-	line 257, "pan.___", state 1709, "(!(cache_dirty_rcu_data[i]))"
-	line 257, "pan.___", state 1709, "else"
-	line 262, "pan.___", state 1718, "(!(cache_dirty_urcu_gp_ctr))"
-	line 262, "pan.___", state 1718, "else"
-	line 295, "pan.___", state 1720, "(cache_dirty_urcu_gp_ctr)"
-	line 295, "pan.___", state 1720, "else"
-	line 1300, "pan.___", state 1721, "(cache_dirty_urcu_gp_ctr)"
-	line 1300, "pan.___", state 1721, "else"
-	line 1304, "pan.___", state 1724, "-end-"
-	(312 of 1724 states)
-unreached in proctype :init:
-	line 1319, "pan.___", state 13, "((i<1))"
-	line 1319, "pan.___", state 13, "((i>=1))"
-	(1 of 28 states)
-unreached in proctype :never:
-	line 1367, "pan.___", state 8, "-end-"
-	(1 of 8 states)
-
-pan: elapsed time 792 seconds
-pan: rate 3330.8797 states/second
-pan: avg transition delay 1.5481e-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-alpha-ipi'