X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu%2Fresult-signal-over-writer%2Furcu_progress_reader.log;fp=formal-model%2Furcu%2Fresult-signal-over-writer%2Furcu_progress_reader.log;h=a1a61224d0f9ca9a6052e785ac356fc0cd7617e1;hb=8baf2c9506f8e4bbac913c7ea2a8b2e9a3cd0932;hp=0000000000000000000000000000000000000000;hpb=fa5b67244cb2c3733d2c0195d3ad239d97ec2dc3;p=urcu.git

diff --git a/formal-model/urcu/result-signal-over-writer/urcu_progress_reader.log b/formal-model/urcu/result-signal-over-writer/urcu_progress_reader.log
new file mode 100644
index 0000000..a1a6122
--- /dev/null
+++ b/formal-model/urcu/result-signal-over-writer/urcu_progress_reader.log
@@ -0,0 +1,348 @@
+make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
+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_progress.ltl | grep -v ^//`)" >> pan.ltl
+cp urcu_progress_reader.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 -f -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 742)
+depth 12: Claim reached state 9 (line 747)
+depth 86: Claim reached state 9 (line 746)
+
+(Spin Version 5.1.7 -- 23 December 2008)
+	+ Partial Order Reduction
+
+Full statespace search for:
+	never claim         	+
+	assertion violations	+ (if within scope of claim)
+	acceptance   cycles 	+ (fairness enabled)
+	invalid end states	- (disabled by never claim)
+
+State-vector 56 byte, depth reached 10679, errors: 0
+    38182 states, stored (88898 visited)
+   997091 states, matched
+  1085989 transitions (= visited+matched)
+  3694897 atomic steps
+hash conflicts:      9602 (resolved)
+
+Stats on memory usage (in Megabytes):
+    3.059	equivalent memory usage for states (stored*(State-vector + overhead))
+    2.930	actual memory usage for states (compression: 95.79%)
+         	state-vector as stored = 52 byte + 28 byte overhead
+    8.000	memory used for hash table (-w20)
+  457.764	memory used for DFS stack (-m10000000)
+  468.596	total actual memory usage
+
+unreached in proctype urcu_reader_sig
+	line 402, "pan.___", state 330, "(1)"
+	line 613, "pan.___", state 411, "-end-"
+	(2 of 411 states)
+unreached in proctype urcu_writer
+	line 398, "pan.___", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 407, "pan.___", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 408, "pan.___", state 59, "(1)"
+	line 417, "pan.___", state 89, "(1)"
+	line 398, "pan.___", state 115, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 408, "pan.___", state 160, "(1)"
+	line 651, "pan.___", state 213, "(1)"
+	line 174, "pan.___", state 222, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 178, "pan.___", state 233, "(1)"
+	line 159, "pan.___", state 254, "(1)"
+	line 163, "pan.___", state 262, "(1)"
+	line 167, "pan.___", state 274, "(1)"
+	line 174, "pan.___", state 285, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
+	line 178, "pan.___", state 294, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
+	line 182, "pan.___", state 307, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
+	line 159, "pan.___", state 317, "(1)"
+	line 163, "pan.___", state 325, "(1)"
+	line 167, "pan.___", state 337, "(1)"
+	line 174, "pan.___", state 352, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 178, "pan.___", state 361, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
+	line 182, "pan.___", state 374, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 159, "pan.___", state 384, "(1)"
+	line 163, "pan.___", state 392, "(1)"
+	line 167, "pan.___", state 404, "(1)"
+	line 398, "pan.___", state 425, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 402, "pan.___", state 441, "(1)"
+	line 407, "pan.___", state 457, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 408, "pan.___", state 470, "(1)"
+	line 417, "pan.___", state 500, "(1)"
+	line 398, "pan.___", state 526, "(1)"
+	line 402, "pan.___", state 540, "(1)"
+	line 407, "pan.___", state 556, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 417, "pan.___", state 599, "(1)"
+	line 402, "pan.___", state 640, "(1)"
+	line 407, "pan.___", state 656, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 417, "pan.___", state 699, "(1)"
+	line 174, "pan.___", state 720, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 174, "pan.___", state 722, "(1)"
+	line 178, "pan.___", state 729, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
+	line 178, "pan.___", state 731, "(1)"
+	line 178, "pan.___", state 732, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
+	line 178, "pan.___", state 732, "else"
+	line 176, "pan.___", state 737, "((j<1))"
+	line 176, "pan.___", state 737, "((j>=1))"
+	line 182, "pan.___", state 742, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 159, "pan.___", state 752, "(1)"
+	line 163, "pan.___", state 760, "(1)"
+	line 163, "pan.___", state 761, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
+	line 163, "pan.___", state 761, "else"
+	line 161, "pan.___", state 766, "((j<1))"
+	line 161, "pan.___", state 766, "((j>=1))"
+	line 167, "pan.___", state 772, "(1)"
+	line 167, "pan.___", state 773, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
+	line 167, "pan.___", state 773, "else"
+	line 169, "pan.___", state 776, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
+	line 169, "pan.___", state 776, "else"
+	line 174, "pan.___", state 783, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
+	line 174, "pan.___", state 785, "(1)"
+	line 178, "pan.___", state 792, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
+	line 178, "pan.___", state 794, "(1)"
+	line 178, "pan.___", state 795, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
+	line 178, "pan.___", state 795, "else"
+	line 176, "pan.___", state 800, "((j<1))"
+	line 176, "pan.___", state 800, "((j>=1))"
+	line 182, "pan.___", state 805, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
+	line 159, "pan.___", state 815, "(1)"
+	line 163, "pan.___", state 823, "(1)"
+	line 163, "pan.___", state 824, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
+	line 163, "pan.___", state 824, "else"
+	line 161, "pan.___", state 829, "((j<1))"
+	line 161, "pan.___", state 829, "((j>=1))"
+	line 167, "pan.___", state 835, "(1)"
+	line 167, "pan.___", state 836, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
+	line 167, "pan.___", state 836, "else"
+	line 169, "pan.___", state 839, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
+	line 169, "pan.___", state 839, "else"
+	line 201, "pan.___", state 841, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
+	line 201, "pan.___", state 841, "else"
+	line 213, "pan.___", state 845, "((i<1))"
+	line 213, "pan.___", state 845, "((i>=1))"
+	line 174, "pan.___", state 850, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 174, "pan.___", state 852, "(1)"
+	line 178, "pan.___", state 859, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
+	line 178, "pan.___", state 861, "(1)"
+	line 178, "pan.___", state 862, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
+	line 178, "pan.___", state 862, "else"
+	line 176, "pan.___", state 867, "((j<1))"
+	line 176, "pan.___", state 867, "((j>=1))"
+	line 182, "pan.___", state 872, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 159, "pan.___", state 882, "(1)"
+	line 163, "pan.___", state 890, "(1)"
+	line 163, "pan.___", state 891, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
+	line 163, "pan.___", state 891, "else"
+	line 161, "pan.___", state 896, "((j<1))"
+	line 161, "pan.___", state 896, "((j>=1))"
+	line 167, "pan.___", state 902, "(1)"
+	line 167, "pan.___", state 903, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
+	line 167, "pan.___", state 903, "else"
+	line 169, "pan.___", state 906, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
+	line 169, "pan.___", state 906, "else"
+	line 201, "pan.___", state 908, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
+	line 201, "pan.___", state 908, "else"
+	line 220, "pan.___", state 909, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
+	line 220, "pan.___", state 909, "else"
+	line 355, "pan.___", state 915, "((sighand_exec==1))"
+	line 355, "pan.___", state 915, "else"
+	line 361, "pan.___", state 918, "sighand_exec = 1"
+	line 398, "pan.___", state 931, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 398, "pan.___", state 933, "(1)"
+	line 398, "pan.___", state 934, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
+	line 398, "pan.___", state 934, "else"
+	line 398, "pan.___", state 937, "(1)"
+	line 402, "pan.___", state 945, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
+	line 402, "pan.___", state 947, "(1)"
+	line 402, "pan.___", state 948, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
+	line 402, "pan.___", state 948, "else"
+	line 402, "pan.___", state 951, "(1)"
+	line 402, "pan.___", state 952, "(1)"
+	line 402, "pan.___", state 952, "(1)"
+	line 400, "pan.___", state 957, "((i<1))"
+	line 400, "pan.___", state 957, "((i>=1))"
+	line 407, "pan.___", state 963, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 408, "pan.___", state 976, "(1)"
+	line 408, "pan.___", state 977, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
+	line 408, "pan.___", state 977, "else"
+	line 408, "pan.___", state 980, "(1)"
+	line 408, "pan.___", state 981, "(1)"
+	line 408, "pan.___", state 981, "(1)"
+	line 412, "pan.___", state 989, "(1)"
+	line 412, "pan.___", state 990, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
+	line 412, "pan.___", state 990, "else"
+	line 412, "pan.___", state 993, "(1)"
+	line 412, "pan.___", state 994, "(1)"
+	line 412, "pan.___", state 994, "(1)"
+	line 410, "pan.___", state 999, "((i<1))"
+	line 410, "pan.___", state 999, "((i>=1))"
+	line 417, "pan.___", state 1006, "(1)"
+	line 417, "pan.___", state 1007, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
+	line 417, "pan.___", state 1007, "else"
+	line 417, "pan.___", state 1010, "(1)"
+	line 417, "pan.___", state 1011, "(1)"
+	line 417, "pan.___", state 1011, "(1)"
+	line 419, "pan.___", state 1014, "(1)"
+	line 419, "pan.___", state 1014, "(1)"
+	line 361, "pan.___", state 1023, "sighand_exec = 1"
+	line 402, "pan.___", state 1054, "(1)"
+	line 407, "pan.___", state 1070, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 417, "pan.___", state 1113, "(1)"
+	line 402, "pan.___", state 1151, "(1)"
+	line 407, "pan.___", state 1167, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 417, "pan.___", state 1210, "(1)"
+	line 398, "pan.___", state 1236, "(1)"
+	line 402, "pan.___", state 1250, "(1)"
+	line 407, "pan.___", state 1266, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 417, "pan.___", state 1309, "(1)"
+	line 402, "pan.___", state 1350, "(1)"
+	line 407, "pan.___", state 1366, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 417, "pan.___", state 1409, "(1)"
+	line 174, "pan.___", state 1430, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 174, "pan.___", state 1432, "(1)"
+	line 178, "pan.___", state 1439, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
+	line 178, "pan.___", state 1441, "(1)"
+	line 178, "pan.___", state 1442, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
+	line 178, "pan.___", state 1442, "else"
+	line 176, "pan.___", state 1447, "((j<1))"
+	line 176, "pan.___", state 1447, "((j>=1))"
+	line 182, "pan.___", state 1452, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 159, "pan.___", state 1462, "(1)"
+	line 163, "pan.___", state 1470, "(1)"
+	line 163, "pan.___", state 1471, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
+	line 163, "pan.___", state 1471, "else"
+	line 161, "pan.___", state 1476, "((j<1))"
+	line 161, "pan.___", state 1476, "((j>=1))"
+	line 167, "pan.___", state 1482, "(1)"
+	line 167, "pan.___", state 1483, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
+	line 167, "pan.___", state 1483, "else"
+	line 169, "pan.___", state 1486, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
+	line 169, "pan.___", state 1486, "else"
+	line 174, "pan.___", state 1493, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
+	line 174, "pan.___", state 1495, "(1)"
+	line 178, "pan.___", state 1502, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
+	line 178, "pan.___", state 1504, "(1)"
+	line 178, "pan.___", state 1505, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
+	line 178, "pan.___", state 1505, "else"
+	line 176, "pan.___", state 1510, "((j<1))"
+	line 176, "pan.___", state 1510, "((j>=1))"
+	line 182, "pan.___", state 1515, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
+	line 159, "pan.___", state 1525, "(1)"
+	line 163, "pan.___", state 1533, "(1)"
+	line 163, "pan.___", state 1534, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
+	line 163, "pan.___", state 1534, "else"
+	line 161, "pan.___", state 1539, "((j<1))"
+	line 161, "pan.___", state 1539, "((j>=1))"
+	line 167, "pan.___", state 1545, "(1)"
+	line 167, "pan.___", state 1546, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
+	line 167, "pan.___", state 1546, "else"
+	line 169, "pan.___", state 1549, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
+	line 169, "pan.___", state 1549, "else"
+	line 201, "pan.___", state 1551, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
+	line 201, "pan.___", state 1551, "else"
+	line 213, "pan.___", state 1555, "((i<1))"
+	line 213, "pan.___", state 1555, "((i>=1))"
+	line 174, "pan.___", state 1560, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 174, "pan.___", state 1562, "(1)"
+	line 178, "pan.___", state 1569, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
+	line 178, "pan.___", state 1571, "(1)"
+	line 178, "pan.___", state 1572, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
+	line 178, "pan.___", state 1572, "else"
+	line 176, "pan.___", state 1577, "((j<1))"
+	line 176, "pan.___", state 1577, "((j>=1))"
+	line 182, "pan.___", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 159, "pan.___", state 1592, "(1)"
+	line 163, "pan.___", state 1600, "(1)"
+	line 163, "pan.___", state 1601, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
+	line 163, "pan.___", state 1601, "else"
+	line 161, "pan.___", state 1606, "((j<1))"
+	line 161, "pan.___", state 1606, "((j>=1))"
+	line 167, "pan.___", state 1612, "(1)"
+	line 167, "pan.___", state 1613, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
+	line 167, "pan.___", state 1613, "else"
+	line 169, "pan.___", state 1616, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
+	line 169, "pan.___", state 1616, "else"
+	line 201, "pan.___", state 1618, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
+	line 201, "pan.___", state 1618, "else"
+	line 220, "pan.___", state 1619, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
+	line 220, "pan.___", state 1619, "else"
+	line 355, "pan.___", state 1625, "((sighand_exec==1))"
+	line 355, "pan.___", state 1625, "else"
+	line 361, "pan.___", state 1628, "sighand_exec = 1"
+	line 398, "pan.___", state 1641, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 398, "pan.___", state 1643, "(1)"
+	line 398, "pan.___", state 1644, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
+	line 398, "pan.___", state 1644, "else"
+	line 398, "pan.___", state 1647, "(1)"
+	line 402, "pan.___", state 1655, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
+	line 402, "pan.___", state 1657, "(1)"
+	line 402, "pan.___", state 1658, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
+	line 402, "pan.___", state 1658, "else"
+	line 402, "pan.___", state 1661, "(1)"
+	line 402, "pan.___", state 1662, "(1)"
+	line 402, "pan.___", state 1662, "(1)"
+	line 400, "pan.___", state 1667, "((i<1))"
+	line 400, "pan.___", state 1667, "((i>=1))"
+	line 407, "pan.___", state 1673, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 408, "pan.___", state 1686, "(1)"
+	line 408, "pan.___", state 1687, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
+	line 408, "pan.___", state 1687, "else"
+	line 408, "pan.___", state 1690, "(1)"
+	line 408, "pan.___", state 1691, "(1)"
+	line 408, "pan.___", state 1691, "(1)"
+	line 412, "pan.___", state 1699, "(1)"
+	line 412, "pan.___", state 1700, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
+	line 412, "pan.___", state 1700, "else"
+	line 412, "pan.___", state 1703, "(1)"
+	line 412, "pan.___", state 1704, "(1)"
+	line 412, "pan.___", state 1704, "(1)"
+	line 410, "pan.___", state 1709, "((i<1))"
+	line 410, "pan.___", state 1709, "((i>=1))"
+	line 417, "pan.___", state 1716, "(1)"
+	line 417, "pan.___", state 1717, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
+	line 417, "pan.___", state 1717, "else"
+	line 417, "pan.___", state 1720, "(1)"
+	line 417, "pan.___", state 1721, "(1)"
+	line 417, "pan.___", state 1721, "(1)"
+	line 419, "pan.___", state 1724, "(1)"
+	line 419, "pan.___", state 1724, "(1)"
+	line 361, "pan.___", state 1733, "sighand_exec = 1"
+	line 178, "pan.___", state 1758, "(1)"
+	line 182, "pan.___", state 1769, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 159, "pan.___", state 1779, "(1)"
+	line 163, "pan.___", state 1787, "(1)"
+	line 167, "pan.___", state 1799, "(1)"
+	line 174, "pan.___", state 1810, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
+	line 178, "pan.___", state 1819, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
+	line 182, "pan.___", state 1832, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
+	line 159, "pan.___", state 1842, "(1)"
+	line 163, "pan.___", state 1850, "(1)"
+	line 167, "pan.___", state 1862, "(1)"
+	line 174, "pan.___", state 1877, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
+	line 178, "pan.___", state 1886, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
+	line 182, "pan.___", state 1899, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
+	line 159, "pan.___", state 1909, "(1)"
+	line 163, "pan.___", state 1917, "(1)"
+	line 167, "pan.___", state 1929, "(1)"
+	line 701, "pan.___", state 1968, "-end-"
+	(215 of 1968 states)
+unreached in proctype :init:
+	(0 of 46 states)
+unreached in proctype :never:
+	line 749, "pan.___", state 11, "-end-"
+	(1 of 11 states)
+
+pan: elapsed time 0.85 seconds
+pan: rate 104585.88 states/second
+pan: avg transition delay 7.827e-07 usec
+cp .input.spin urcu_progress_reader.spin.input
+cp .input.spin.trail urcu_progress_reader.spin.input.trail
+make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'