+++ /dev/null
-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_writer.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 28: 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
- 38555 states, stored (92500 visited)
- 1044204 states, matched
- 1136704 transitions (= visited+matched)
- 3867169 atomic steps
-hash conflicts: 8572 (resolved)
-
-Stats on memory usage (in Megabytes):
- 3.089 equivalent memory usage for states (stored*(State-vector + overhead))
- 2.930 actual memory usage for states (compression: 94.87%)
- 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.89 seconds
-pan: rate 103932.58 states/second
-pan: avg transition delay 7.8297e-07 usec
-cp .input.spin urcu_progress_writer.spin.input
-cp .input.spin.trail urcu_progress_writer.spin.input.trail
-make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
projects / urcu.git / blobdiff