formal-model/urcu-nosched-model/result-signal-over-writer/urcu_progress_reader.log

   1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
   2 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
   3 touch .input.define
   4 cat .input.define > pan.ltl
   5 cat DEFINES >> pan.ltl
   6 spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
   7 cp urcu_progress_reader.define .input.define
   8 cat .input.define > .input.spin
   9 cat DEFINES >> .input.spin
  10 cat urcu.spin >> .input.spin
  11 rm -f .input.spin.trail
  12 spin -a -X -N pan.ltl .input.spin
  13 Exit-Status 0
  14 gcc -O2 -w -DHASH64 -o pan pan.c
  15 ./pan -a -f -v -c1 -X -m10000000 -w20
  16 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
  17 (never claims generated from LTL formulae are stutter-invariant)
  18 depth 0: Claim reached state 5 (line 742)
  19 depth 12: Claim reached state 9 (line 747)
  20 depth 86: Claim reached state 9 (line 746)
  21
  22 (Spin Version 5.1.7 -- 23 December 2008)
  23         + Partial Order Reduction
  24
  25 Full statespace search for:
  26         never claim             +
  27         assertion violations    + (if within scope of claim)
  28         acceptance   cycles     + (fairness enabled)
  29         invalid end states      - (disabled by never claim)
  30
  31 State-vector 56 byte, depth reached 10679, errors: 0
  32     38182 states, stored (88898 visited)
  33    997091 states, matched
  34   1085989 transitions (= visited+matched)
  35   3694897 atomic steps
  36 hash conflicts:      9602 (resolved)
  37
  38 Stats on memory usage (in Megabytes):
  39     3.059       equivalent memory usage for states (stored*(State-vector + overhead))
  40     2.930       actual memory usage for states (compression: 95.79%)
  41                 state-vector as stored = 52 byte + 28 byte overhead
  42     8.000       memory used for hash table (-w20)
  43   457.764       memory used for DFS stack (-m10000000)
  44   468.596       total actual memory usage
  45
  46 unreached in proctype urcu_reader_sig
  47         line 402, "pan.___", state 330, "(1)"
  48         line 613, "pan.___", state 411, "-end-"
  49         (2 of 411 states)
  50 unreached in proctype urcu_writer
  51         line 398, "pan.___", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  52         line 407, "pan.___", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  53         line 408, "pan.___", state 59, "(1)"
  54         line 417, "pan.___", state 89, "(1)"
  55         line 398, "pan.___", state 115, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  56         line 408, "pan.___", state 160, "(1)"
  57         line 651, "pan.___", state 213, "(1)"
  58         line 174, "pan.___", state 222, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  59         line 178, "pan.___", state 233, "(1)"
  60         line 159, "pan.___", state 254, "(1)"
  61         line 163, "pan.___", state 262, "(1)"
  62         line 167, "pan.___", state 274, "(1)"
  63         line 174, "pan.___", state 285, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
  64         line 178, "pan.___", state 294, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
  65         line 182, "pan.___", state 307, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
  66         line 159, "pan.___", state 317, "(1)"
  67         line 163, "pan.___", state 325, "(1)"
  68         line 167, "pan.___", state 337, "(1)"
  69         line 174, "pan.___", state 352, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  70         line 178, "pan.___", state 361, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
  71         line 182, "pan.___", state 374, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  72         line 159, "pan.___", state 384, "(1)"
  73         line 163, "pan.___", state 392, "(1)"
  74         line 167, "pan.___", state 404, "(1)"
  75         line 398, "pan.___", state 425, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  76         line 402, "pan.___", state 441, "(1)"
  77         line 407, "pan.___", state 457, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  78         line 408, "pan.___", state 470, "(1)"
  79         line 417, "pan.___", state 500, "(1)"
  80         line 398, "pan.___", state 526, "(1)"
  81         line 402, "pan.___", state 540, "(1)"
  82         line 407, "pan.___", state 556, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  83         line 417, "pan.___", state 599, "(1)"
  84         line 402, "pan.___", state 640, "(1)"
  85         line 407, "pan.___", state 656, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  86         line 417, "pan.___", state 699, "(1)"
  87         line 174, "pan.___", state 720, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  88         line 174, "pan.___", state 722, "(1)"
  89         line 178, "pan.___", state 729, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
  90         line 178, "pan.___", state 731, "(1)"
  91         line 178, "pan.___", state 732, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
  92         line 178, "pan.___", state 732, "else"
  93         line 176, "pan.___", state 737, "((j<1))"
  94         line 176, "pan.___", state 737, "((j>=1))"
  95         line 182, "pan.___", state 742, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  96         line 159, "pan.___", state 752, "(1)"
  97         line 163, "pan.___", state 760, "(1)"
  98         line 163, "pan.___", state 761, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
  99         line 163, "pan.___", state 761, "else"
 100         line 161, "pan.___", state 766, "((j<1))"
 101         line 161, "pan.___", state 766, "((j>=1))"
 102         line 167, "pan.___", state 772, "(1)"
 103         line 167, "pan.___", state 773, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 104         line 167, "pan.___", state 773, "else"
 105         line 169, "pan.___", state 776, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 106         line 169, "pan.___", state 776, "else"
 107         line 174, "pan.___", state 783, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 108         line 174, "pan.___", state 785, "(1)"
 109         line 178, "pan.___", state 792, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
 110         line 178, "pan.___", state 794, "(1)"
 111         line 178, "pan.___", state 795, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
 112         line 178, "pan.___", state 795, "else"
 113         line 176, "pan.___", state 800, "((j<1))"
 114         line 176, "pan.___", state 800, "((j>=1))"
 115         line 182, "pan.___", state 805, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 116         line 159, "pan.___", state 815, "(1)"
 117         line 163, "pan.___", state 823, "(1)"
 118         line 163, "pan.___", state 824, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
 119         line 163, "pan.___", state 824, "else"
 120         line 161, "pan.___", state 829, "((j<1))"
 121         line 161, "pan.___", state 829, "((j>=1))"
 122         line 167, "pan.___", state 835, "(1)"
 123         line 167, "pan.___", state 836, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
 124         line 167, "pan.___", state 836, "else"
 125         line 169, "pan.___", state 839, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
 126         line 169, "pan.___", state 839, "else"
 127         line 201, "pan.___", state 841, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
 128         line 201, "pan.___", state 841, "else"
 129         line 213, "pan.___", state 845, "((i<1))"
 130         line 213, "pan.___", state 845, "((i>=1))"
 131         line 174, "pan.___", state 850, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 132         line 174, "pan.___", state 852, "(1)"
 133         line 178, "pan.___", state 859, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 134         line 178, "pan.___", state 861, "(1)"
 135         line 178, "pan.___", state 862, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 136         line 178, "pan.___", state 862, "else"
 137         line 176, "pan.___", state 867, "((j<1))"
 138         line 176, "pan.___", state 867, "((j>=1))"
 139         line 182, "pan.___", state 872, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 140         line 159, "pan.___", state 882, "(1)"
 141         line 163, "pan.___", state 890, "(1)"
 142         line 163, "pan.___", state 891, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 143         line 163, "pan.___", state 891, "else"
 144         line 161, "pan.___", state 896, "((j<1))"
 145         line 161, "pan.___", state 896, "((j>=1))"
 146         line 167, "pan.___", state 902, "(1)"
 147         line 167, "pan.___", state 903, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 148         line 167, "pan.___", state 903, "else"
 149         line 169, "pan.___", state 906, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 150         line 169, "pan.___", state 906, "else"
 151         line 201, "pan.___", state 908, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 152         line 201, "pan.___", state 908, "else"
 153         line 220, "pan.___", state 909, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 154         line 220, "pan.___", state 909, "else"
 155         line 355, "pan.___", state 915, "((sighand_exec==1))"
 156         line 355, "pan.___", state 915, "else"
 157         line 361, "pan.___", state 918, "sighand_exec = 1"
 158         line 398, "pan.___", state 931, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 159         line 398, "pan.___", state 933, "(1)"
 160         line 398, "pan.___", state 934, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 161         line 398, "pan.___", state 934, "else"
 162         line 398, "pan.___", state 937, "(1)"
 163         line 402, "pan.___", state 945, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 164         line 402, "pan.___", state 947, "(1)"
 165         line 402, "pan.___", state 948, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 166         line 402, "pan.___", state 948, "else"
 167         line 402, "pan.___", state 951, "(1)"
 168         line 402, "pan.___", state 952, "(1)"
 169         line 402, "pan.___", state 952, "(1)"
 170         line 400, "pan.___", state 957, "((i<1))"
 171         line 400, "pan.___", state 957, "((i>=1))"
 172         line 407, "pan.___", state 963, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 173         line 408, "pan.___", state 976, "(1)"
 174         line 408, "pan.___", state 977, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 175         line 408, "pan.___", state 977, "else"
 176         line 408, "pan.___", state 980, "(1)"
 177         line 408, "pan.___", state 981, "(1)"
 178         line 408, "pan.___", state 981, "(1)"
 179         line 412, "pan.___", state 989, "(1)"
 180         line 412, "pan.___", state 990, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 181         line 412, "pan.___", state 990, "else"
 182         line 412, "pan.___", state 993, "(1)"
 183         line 412, "pan.___", state 994, "(1)"
 184         line 412, "pan.___", state 994, "(1)"
 185         line 410, "pan.___", state 999, "((i<1))"
 186         line 410, "pan.___", state 999, "((i>=1))"
 187         line 417, "pan.___", state 1006, "(1)"
 188         line 417, "pan.___", state 1007, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 189         line 417, "pan.___", state 1007, "else"
 190         line 417, "pan.___", state 1010, "(1)"
 191         line 417, "pan.___", state 1011, "(1)"
 192         line 417, "pan.___", state 1011, "(1)"
 193         line 419, "pan.___", state 1014, "(1)"
 194         line 419, "pan.___", state 1014, "(1)"
 195         line 361, "pan.___", state 1023, "sighand_exec = 1"
 196         line 402, "pan.___", state 1054, "(1)"
 197         line 407, "pan.___", state 1070, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 198         line 417, "pan.___", state 1113, "(1)"
 199         line 402, "pan.___", state 1151, "(1)"
 200         line 407, "pan.___", state 1167, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 201         line 417, "pan.___", state 1210, "(1)"
 202         line 398, "pan.___", state 1236, "(1)"
 203         line 402, "pan.___", state 1250, "(1)"
 204         line 407, "pan.___", state 1266, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 205         line 417, "pan.___", state 1309, "(1)"
 206         line 402, "pan.___", state 1350, "(1)"
 207         line 407, "pan.___", state 1366, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 208         line 417, "pan.___", state 1409, "(1)"
 209         line 174, "pan.___", state 1430, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 210         line 174, "pan.___", state 1432, "(1)"
 211         line 178, "pan.___", state 1439, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 212         line 178, "pan.___", state 1441, "(1)"
 213         line 178, "pan.___", state 1442, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 214         line 178, "pan.___", state 1442, "else"
 215         line 176, "pan.___", state 1447, "((j<1))"
 216         line 176, "pan.___", state 1447, "((j>=1))"
 217         line 182, "pan.___", state 1452, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 218         line 159, "pan.___", state 1462, "(1)"
 219         line 163, "pan.___", state 1470, "(1)"
 220         line 163, "pan.___", state 1471, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 221         line 163, "pan.___", state 1471, "else"
 222         line 161, "pan.___", state 1476, "((j<1))"
 223         line 161, "pan.___", state 1476, "((j>=1))"
 224         line 167, "pan.___", state 1482, "(1)"
 225         line 167, "pan.___", state 1483, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 226         line 167, "pan.___", state 1483, "else"
 227         line 169, "pan.___", state 1486, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 228         line 169, "pan.___", state 1486, "else"
 229         line 174, "pan.___", state 1493, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 230         line 174, "pan.___", state 1495, "(1)"
 231         line 178, "pan.___", state 1502, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
 232         line 178, "pan.___", state 1504, "(1)"
 233         line 178, "pan.___", state 1505, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
 234         line 178, "pan.___", state 1505, "else"
 235         line 176, "pan.___", state 1510, "((j<1))"
 236         line 176, "pan.___", state 1510, "((j>=1))"
 237         line 182, "pan.___", state 1515, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 238         line 159, "pan.___", state 1525, "(1)"
 239         line 163, "pan.___", state 1533, "(1)"
 240         line 163, "pan.___", state 1534, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
 241         line 163, "pan.___", state 1534, "else"
 242         line 161, "pan.___", state 1539, "((j<1))"
 243         line 161, "pan.___", state 1539, "((j>=1))"
 244         line 167, "pan.___", state 1545, "(1)"
 245         line 167, "pan.___", state 1546, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
 246         line 167, "pan.___", state 1546, "else"
 247         line 169, "pan.___", state 1549, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
 248         line 169, "pan.___", state 1549, "else"
 249         line 201, "pan.___", state 1551, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
 250         line 201, "pan.___", state 1551, "else"
 251         line 213, "pan.___", state 1555, "((i<1))"
 252         line 213, "pan.___", state 1555, "((i>=1))"
 253         line 174, "pan.___", state 1560, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 254         line 174, "pan.___", state 1562, "(1)"
 255         line 178, "pan.___", state 1569, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 256         line 178, "pan.___", state 1571, "(1)"
 257         line 178, "pan.___", state 1572, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 258         line 178, "pan.___", state 1572, "else"
 259         line 176, "pan.___", state 1577, "((j<1))"
 260         line 176, "pan.___", state 1577, "((j>=1))"
 261         line 182, "pan.___", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 262         line 159, "pan.___", state 1592, "(1)"
 263         line 163, "pan.___", state 1600, "(1)"
 264         line 163, "pan.___", state 1601, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 265         line 163, "pan.___", state 1601, "else"
 266         line 161, "pan.___", state 1606, "((j<1))"
 267         line 161, "pan.___", state 1606, "((j>=1))"
 268         line 167, "pan.___", state 1612, "(1)"
 269         line 167, "pan.___", state 1613, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 270         line 167, "pan.___", state 1613, "else"
 271         line 169, "pan.___", state 1616, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 272         line 169, "pan.___", state 1616, "else"
 273         line 201, "pan.___", state 1618, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 274         line 201, "pan.___", state 1618, "else"
 275         line 220, "pan.___", state 1619, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 276         line 220, "pan.___", state 1619, "else"
 277         line 355, "pan.___", state 1625, "((sighand_exec==1))"
 278         line 355, "pan.___", state 1625, "else"
 279         line 361, "pan.___", state 1628, "sighand_exec = 1"
 280         line 398, "pan.___", state 1641, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 281         line 398, "pan.___", state 1643, "(1)"
 282         line 398, "pan.___", state 1644, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 283         line 398, "pan.___", state 1644, "else"
 284         line 398, "pan.___", state 1647, "(1)"
 285         line 402, "pan.___", state 1655, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 286         line 402, "pan.___", state 1657, "(1)"
 287         line 402, "pan.___", state 1658, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 288         line 402, "pan.___", state 1658, "else"
 289         line 402, "pan.___", state 1661, "(1)"
 290         line 402, "pan.___", state 1662, "(1)"
 291         line 402, "pan.___", state 1662, "(1)"
 292         line 400, "pan.___", state 1667, "((i<1))"
 293         line 400, "pan.___", state 1667, "((i>=1))"
 294         line 407, "pan.___", state 1673, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 295         line 408, "pan.___", state 1686, "(1)"
 296         line 408, "pan.___", state 1687, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 297         line 408, "pan.___", state 1687, "else"
 298         line 408, "pan.___", state 1690, "(1)"
 299         line 408, "pan.___", state 1691, "(1)"
 300         line 408, "pan.___", state 1691, "(1)"
 301         line 412, "pan.___", state 1699, "(1)"
 302         line 412, "pan.___", state 1700, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 303         line 412, "pan.___", state 1700, "else"
 304         line 412, "pan.___", state 1703, "(1)"
 305         line 412, "pan.___", state 1704, "(1)"
 306         line 412, "pan.___", state 1704, "(1)"
 307         line 410, "pan.___", state 1709, "((i<1))"
 308         line 410, "pan.___", state 1709, "((i>=1))"
 309         line 417, "pan.___", state 1716, "(1)"
 310         line 417, "pan.___", state 1717, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 311         line 417, "pan.___", state 1717, "else"
 312         line 417, "pan.___", state 1720, "(1)"
 313         line 417, "pan.___", state 1721, "(1)"
 314         line 417, "pan.___", state 1721, "(1)"
 315         line 419, "pan.___", state 1724, "(1)"
 316         line 419, "pan.___", state 1724, "(1)"
 317         line 361, "pan.___", state 1733, "sighand_exec = 1"
 318         line 178, "pan.___", state 1758, "(1)"
 319         line 182, "pan.___", state 1769, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 320         line 159, "pan.___", state 1779, "(1)"
 321         line 163, "pan.___", state 1787, "(1)"
 322         line 167, "pan.___", state 1799, "(1)"
 323         line 174, "pan.___", state 1810, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 324         line 178, "pan.___", state 1819, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
 325         line 182, "pan.___", state 1832, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 326         line 159, "pan.___", state 1842, "(1)"
 327         line 163, "pan.___", state 1850, "(1)"
 328         line 167, "pan.___", state 1862, "(1)"
 329         line 174, "pan.___", state 1877, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 330         line 178, "pan.___", state 1886, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 331         line 182, "pan.___", state 1899, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 332         line 159, "pan.___", state 1909, "(1)"
 333         line 163, "pan.___", state 1917, "(1)"
 334         line 167, "pan.___", state 1929, "(1)"
 335         line 701, "pan.___", state 1968, "-end-"
 336         (215 of 1968 states)
 337 unreached in proctype :init:
 338         (0 of 46 states)
 339 unreached in proctype :never:
 340         line 749, "pan.___", state 11, "-end-"
 341         (1 of 11 states)
 342
 343 pan: elapsed time 0.85 seconds
 344 pan: rate 104585.88 states/second
 345 pan: avg transition delay 7.827e-07 usec
 346 cp .input.spin urcu_progress_reader.spin.input
 347 cp .input.spin.trail urcu_progress_reader.spin.input.trail
 348 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'