formal-model/results/urcu-controldataflow-ipi/urcu_progress_reader.log

   1 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
   2 touch .input.define
   3 cat .input.define > pan.ltl
   4 cat DEFINES >> pan.ltl
   5 spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
   6 cp urcu_progress_reader.define .input.define
   7 cat .input.define > .input.spin
   8 cat DEFINES >> .input.spin
   9 cat urcu.spin >> .input.spin
  10 rm -f .input.spin.trail
  11 spin -a -X -N pan.ltl .input.spin
  12 Exit-Status 0
  13 gcc -O2 -w -DHASH64 -o pan pan.c
  14 ./pan -a -f -v -c1 -X -m10000000 -w20
  15 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
  16 (never claims generated from LTL formulae are stutter-invariant)
  17 depth 0: Claim reached state 5 (line 1258)
  18 depth 23: Claim reached state 9 (line 1263)
  19 depth 137: Claim reached state 9 (line 1262)
  20 Depth=   31896 States=    1e+06 Transitions= 1.91e+08 Memory=   519.963 t=    240 R=   4e+03
  21 Depth=   35611 States=    2e+06 Transitions= 3.82e+08 Memory=   572.111 t=    484 R=   4e+03
  22 Depth=   35611 States=    3e+06 Transitions= 6.15e+08 Memory=   623.869 t=    790 R=   4e+03
  23 pan: resizing hashtable to -w22..  done
  24 Depth=   35611 States=    4e+06 Transitions= 8.15e+08 Memory=   707.236 t= 1.04e+03 R=   4e+03
  25 Depth=   35611 States=    5e+06 Transitions=    1e+09 Memory=   760.557 t= 1.28e+03 R=   4e+03
  26 Depth=   35611 States=    6e+06 Transitions= 1.33e+09 Memory=   808.408 t= 1.71e+03 R=   4e+03
  27 Depth=   35611 States=    7e+06 Transitions= 1.79e+09 Memory=   854.014 t= 2.32e+03 R=   3e+03
  28 Depth=   35611 States=    8e+06 Transitions= 2.33e+09 Memory=   898.740 t= 3.05e+03 R=   3e+03
  29 Depth=   35611 States=    9e+06 Transitions= 2.72e+09 Memory=   947.276 t= 3.57e+03 R=   3e+03
  30 pan: resizing hashtable to -w24..  done
  31 Depth=   35611 States=    1e+07 Transitions= 3.17e+09 Memory=  1119.123 t= 4.17e+03 R=   2e+03
  32 Depth=   35611 States=  1.1e+07 Transitions= 3.43e+09 Memory=  1167.854 t= 4.5e+03 R=   2e+03
  33 Depth=   35611 States=  1.2e+07 Transitions= 3.67e+09 Memory=  1219.221 t= 4.81e+03 R=   2e+03
  34 Depth=   35611 States=  1.3e+07 Transitions= 4.19e+09 Memory=  1262.776 t= 5.49e+03 R=   2e+03
  35 Depth=   35611 States=  1.4e+07 Transitions= 5.17e+09 Memory=  1311.213 t= 6.83e+03 R=   2e+03
  36 Depth=   35611 States=  1.5e+07 Transitions= 6.13e+09 Memory=  1349.006 t= 8.12e+03 R=   2e+03
  37 Depth=   35611 States=  1.6e+07 Transitions= 6.65e+09 Memory=  1393.635 t= 8.82e+03 R=   2e+03
  38 Depth=   35611 States=  1.7e+07 Transitions= 7.12e+09 Memory=  1441.779 t= 9.45e+03 R=   2e+03
  39 Depth=   35611 States=  1.8e+07 Transitions= 7.52e+09 Memory=  1486.408 t= 9.98e+03 R=   2e+03
  40 Depth=   35611 States=  1.9e+07 Transitions= 8.03e+09 Memory=  1534.162 t= 1.07e+04 R=   2e+03
  41 Depth=   35611 States=    2e+07 Transitions=  8.6e+09 Memory=  1579.768 t= 1.14e+04 R=   2e+03
  42 Depth=   35611 States=  2.1e+07 Transitions=    9e+09 Memory=  1629.475 t= 1.2e+04 R=   2e+03
  43 Depth=   35611 States=  2.2e+07 Transitions= 9.32e+09 Memory=  1676.545 t= 1.24e+04 R=   2e+03
  44 Depth=   35611 States=  2.3e+07 Transitions= 9.66e+09 Memory=  1724.494 t= 1.29e+04 R=   2e+03
  45 Depth=   35611 States=  2.4e+07 Transitions=    1e+10 Memory=  1774.299 t= 1.34e+04 R=   2e+03
  46 Depth=   35611 States=  2.5e+07 Transitions= 1.03e+10 Memory=  1822.151 t= 1.37e+04 R=   2e+03
  47 Depth=   35611 States=  2.6e+07 Transitions= 1.07e+10 Memory=  1871.272 t= 1.42e+04 R=   2e+03
  48 Depth=   35611 States=  2.7e+07 Transitions= 1.09e+10 Memory=  1921.272 t= 1.45e+04 R=   2e+03
  49 Depth=   35611 States=  2.8e+07 Transitions= 1.13e+10 Memory=  1969.904 t= 1.51e+04 R=   2e+03
  50 Depth=   35611 States=  2.9e+07 Transitions= 1.15e+10 Memory=  2019.709 t= 1.54e+04 R=   2e+03
  51 Depth=   35611 States=    3e+07 Transitions=  1.2e+10 Memory=  2063.654 t= 1.6e+04 R=   2e+03
  52 Depth=   35611 States=  3.1e+07 Transitions= 1.23e+10 Memory=  2110.920 t= 1.65e+04 R=   2e+03
  53 Depth=   35611 States=  3.2e+07 Transitions= 1.29e+10 Memory=  2156.721 t= 1.73e+04 R=   2e+03
  54 Depth=   35611 States=  3.3e+07 Transitions= 1.35e+10 Memory=  2200.276 t= 1.8e+04 R=   2e+03
  55 Depth=   35611 States=  3.4e+07 Transitions=  1.4e+10 Memory=  2245.881 t= 1.87e+04 R=   2e+03
  56 pan: resizing hashtable to -w26..  done
  57 Depth=   35611 States=  3.5e+07 Transitions= 1.43e+10 Memory=  2790.498 t= 1.91e+04 R=   2e+03
  58 Depth=   35611 States=  3.6e+07 Transitions= 1.45e+10 Memory=  2841.182 t= 1.94e+04 R=   2e+03
  59 Depth=   35611 States=  3.7e+07 Transitions= 1.49e+10 Memory=  2887.861 t= 1.99e+04 R=   2e+03
  60 Depth=   35611 States=  3.8e+07 Transitions= 1.57e+10 Memory=  2934.346 t= 2.1e+04 R=   2e+03
  61 Depth=   35611 States=  3.9e+07 Transitions= 1.67e+10 Memory=  2977.608 t= 2.23e+04 R=   2e+03
  62 Depth=   35611 States=    4e+07 Transitions= 1.74e+10 Memory=  3017.158 t= 2.33e+04 R=   2e+03
  63 Depth=   35611 States=  4.1e+07 Transitions= 1.81e+10 Memory=  3061.104 t= 2.42e+04 R=   2e+03
  64 Depth=   35611 States=  4.2e+07 Transitions= 1.83e+10 Memory=  3109.932 t= 2.45e+04 R=   2e+03
  65 Depth=   35611 States=  4.3e+07 Transitions= 1.88e+10 Memory=  3156.416 t= 2.51e+04 R=   2e+03
  66 Depth=   35611 States=  4.4e+07 Transitions= 1.93e+10 Memory=  3203.389 t= 2.58e+04 R=   2e+03
  67 Depth=   35611 States=  4.5e+07 Transitions= 1.98e+10 Memory=  3249.580 t= 2.65e+04 R=   2e+03
  68 Depth=   35611 States=  4.6e+07 Transitions= 2.02e+10 Memory=  3297.920 t= 2.69e+04 R=   2e+03
  69 Depth=   35611 States=  4.7e+07 Transitions= 2.06e+10 Memory=  3347.236 t= 2.75e+04 R=   2e+03
  70 Depth=   35611 States=  4.8e+07 Transitions= 2.09e+10 Memory=  3395.772 t= 2.79e+04 R=   2e+03
  71 Depth=   35611 States=  4.9e+07 Transitions= 2.12e+10 Memory=  3443.818 t= 2.83e+04 R=   2e+03
  72 Depth=   35611 States=    5e+07 Transitions= 2.15e+10 Memory=  3492.549 t= 2.87e+04 R=   2e+03
  73 Depth=   35611 States=  5.1e+07 Transitions= 2.18e+10 Memory=  3540.303 t= 2.91e+04 R=   2e+03
  74 Depth=   35611 States=  5.2e+07 Transitions= 2.21e+10 Memory=  3591.377 t= 2.95e+04 R=   2e+03
  75 Depth=   35611 States=  5.3e+07 Transitions= 2.24e+10 Memory=  3639.326 t=  3e+04 R=   2e+03
  76 Depth=   35611 States=  5.4e+07 Transitions= 2.27e+10 Memory=  3687.373 t= 3.04e+04 R=   2e+03
  77 Depth=   35611 States=  5.5e+07 Transitions= 2.31e+10 Memory=  3733.662 t= 3.09e+04 R=   2e+03
  78 Depth=   35611 States=  5.6e+07 Transitions= 2.37e+10 Memory=  3779.561 t= 3.16e+04 R=   2e+03
  79 Depth=   35611 States=  5.7e+07 Transitions= 2.42e+10 Memory=  3823.213 t= 3.24e+04 R=   2e+03
  80 Depth=   35611 States=  5.8e+07 Transitions= 2.47e+10 Memory=  3869.795 t= 3.3e+04 R=   2e+03
  81 Depth=   35611 States=  5.9e+07 Transitions= 2.52e+10 Memory=  3916.084 t= 3.37e+04 R=   2e+03
  82
  83 (Spin Version 5.1.7 -- 23 December 2008)
  84         + Partial Order Reduction
  85
  86 Full statespace search for:
  87         never claim             +
  88         assertion violations    + (if within scope of claim)
  89         acceptance   cycles     + (fairness enabled)
  90         invalid end states      - (disabled by never claim)
  91
  92 State-vector 88 byte, depth reached 35611, errors: 0
  93  33837266 states, stored (5.99297e+07 visited)
  94 2.557894e+10 states, matched
  95 2.563887e+10 transitions (= visited+matched)
  96 1.4922421e+11 atomic steps
  97 hash conflicts: 9.616061e+09 (resolved)
  98
  99 Stats on memory usage (in Megabytes):
 100  3743.289       equivalent memory usage for states (stored*(State-vector + overhead))
 101  2990.875       actual memory usage for states (compression: 79.90%)
 102                 state-vector as stored = 65 byte + 28 byte overhead
 103   512.000       memory used for hash table (-w26)
 104   457.764       memory used for DFS stack (-m10000000)
 105     1.683       memory lost to fragmentation
 106  3958.955       total actual memory usage
 107
 108 unreached in proctype urcu_reader
 109         line 250, "pan.___", state 30, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 110         line 258, "pan.___", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 111         line 262, "pan.___", state 61, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 112         line 227, "pan.___", state 77, "(1)"
 113         line 231, "pan.___", state 85, "(1)"
 114         line 235, "pan.___", state 97, "(1)"
 115         line 239, "pan.___", state 105, "(1)"
 116         line 395, "pan.___", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 117         line 404, "pan.___", state 163, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 118         line 408, "pan.___", state 177, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 119         line 412, "pan.___", state 196, "(1)"
 120         line 421, "pan.___", state 226, "(1)"
 121         line 425, "pan.___", state 239, "(1)"
 122         line 670, "pan.___", state 260, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
 123         line 395, "pan.___", state 267, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 124         line 404, "pan.___", state 299, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 125         line 408, "pan.___", state 313, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 126         line 412, "pan.___", state 332, "(1)"
 127         line 421, "pan.___", state 362, "(1)"
 128         line 425, "pan.___", state 375, "(1)"
 129         line 395, "pan.___", state 396, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 130         line 404, "pan.___", state 428, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 131         line 408, "pan.___", state 442, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 132         line 412, "pan.___", state 461, "(1)"
 133         line 421, "pan.___", state 491, "(1)"
 134         line 425, "pan.___", state 504, "(1)"
 135         line 395, "pan.___", state 527, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 136         line 395, "pan.___", state 529, "(1)"
 137         line 395, "pan.___", state 530, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 138         line 395, "pan.___", state 530, "else"
 139         line 395, "pan.___", state 533, "(1)"
 140         line 399, "pan.___", state 541, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 141         line 399, "pan.___", state 543, "(1)"
 142         line 399, "pan.___", state 544, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 143         line 399, "pan.___", state 544, "else"
 144         line 399, "pan.___", state 547, "(1)"
 145         line 399, "pan.___", state 548, "(1)"
 146         line 399, "pan.___", state 548, "(1)"
 147         line 397, "pan.___", state 553, "((i<1))"
 148         line 397, "pan.___", state 553, "((i>=1))"
 149         line 404, "pan.___", state 559, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 150         line 404, "pan.___", state 561, "(1)"
 151         line 404, "pan.___", state 562, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 152         line 404, "pan.___", state 562, "else"
 153         line 404, "pan.___", state 565, "(1)"
 154         line 404, "pan.___", state 566, "(1)"
 155         line 404, "pan.___", state 566, "(1)"
 156         line 408, "pan.___", state 573, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 157         line 408, "pan.___", state 575, "(1)"
 158         line 408, "pan.___", state 576, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 159         line 408, "pan.___", state 576, "else"
 160         line 408, "pan.___", state 579, "(1)"
 161         line 408, "pan.___", state 580, "(1)"
 162         line 408, "pan.___", state 580, "(1)"
 163         line 406, "pan.___", state 585, "((i<2))"
 164         line 406, "pan.___", state 585, "((i>=2))"
 165         line 412, "pan.___", state 592, "(1)"
 166         line 412, "pan.___", state 593, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 167         line 412, "pan.___", state 593, "else"
 168         line 412, "pan.___", state 596, "(1)"
 169         line 412, "pan.___", state 597, "(1)"
 170         line 412, "pan.___", state 597, "(1)"
 171         line 416, "pan.___", state 605, "(1)"
 172         line 416, "pan.___", state 606, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 173         line 416, "pan.___", state 606, "else"
 174         line 416, "pan.___", state 609, "(1)"
 175         line 416, "pan.___", state 610, "(1)"
 176         line 416, "pan.___", state 610, "(1)"
 177         line 414, "pan.___", state 615, "((i<1))"
 178         line 414, "pan.___", state 615, "((i>=1))"
 179         line 421, "pan.___", state 622, "(1)"
 180         line 421, "pan.___", state 623, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 181         line 421, "pan.___", state 623, "else"
 182         line 421, "pan.___", state 626, "(1)"
 183         line 421, "pan.___", state 627, "(1)"
 184         line 421, "pan.___", state 627, "(1)"
 185         line 425, "pan.___", state 635, "(1)"
 186         line 425, "pan.___", state 636, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 187         line 425, "pan.___", state 636, "else"
 188         line 425, "pan.___", state 639, "(1)"
 189         line 425, "pan.___", state 640, "(1)"
 190         line 425, "pan.___", state 640, "(1)"
 191         line 423, "pan.___", state 645, "((i<2))"
 192         line 423, "pan.___", state 645, "((i>=2))"
 193         line 430, "pan.___", state 649, "(1)"
 194         line 430, "pan.___", state 649, "(1)"
 195         line 670, "pan.___", state 652, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 196         line 670, "pan.___", state 653, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 197         line 670, "pan.___", state 654, "(1)"
 198         line 395, "pan.___", state 661, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 199         line 404, "pan.___", state 693, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 200         line 408, "pan.___", state 707, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 201         line 412, "pan.___", state 726, "(1)"
 202         line 421, "pan.___", state 756, "(1)"
 203         line 425, "pan.___", state 769, "(1)"
 204         line 395, "pan.___", state 797, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 205         line 395, "pan.___", state 799, "(1)"
 206         line 395, "pan.___", state 800, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 207         line 395, "pan.___", state 800, "else"
 208         line 395, "pan.___", state 803, "(1)"
 209         line 399, "pan.___", state 811, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 210         line 399, "pan.___", state 813, "(1)"
 211         line 399, "pan.___", state 814, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 212         line 399, "pan.___", state 814, "else"
 213         line 399, "pan.___", state 817, "(1)"
 214         line 399, "pan.___", state 818, "(1)"
 215         line 399, "pan.___", state 818, "(1)"
 216         line 397, "pan.___", state 823, "((i<1))"
 217         line 397, "pan.___", state 823, "((i>=1))"
 218         line 404, "pan.___", state 829, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 219         line 404, "pan.___", state 831, "(1)"
 220         line 404, "pan.___", state 832, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 221         line 404, "pan.___", state 832, "else"
 222         line 404, "pan.___", state 835, "(1)"
 223         line 404, "pan.___", state 836, "(1)"
 224         line 404, "pan.___", state 836, "(1)"
 225         line 408, "pan.___", state 843, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 226         line 408, "pan.___", state 845, "(1)"
 227         line 408, "pan.___", state 846, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 228         line 408, "pan.___", state 846, "else"
 229         line 408, "pan.___", state 849, "(1)"
 230         line 408, "pan.___", state 850, "(1)"
 231         line 408, "pan.___", state 850, "(1)"
 232         line 406, "pan.___", state 855, "((i<2))"
 233         line 406, "pan.___", state 855, "((i>=2))"
 234         line 412, "pan.___", state 862, "(1)"
 235         line 412, "pan.___", state 863, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 236         line 412, "pan.___", state 863, "else"
 237         line 412, "pan.___", state 866, "(1)"
 238         line 412, "pan.___", state 867, "(1)"
 239         line 412, "pan.___", state 867, "(1)"
 240         line 416, "pan.___", state 875, "(1)"
 241         line 416, "pan.___", state 876, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 242         line 416, "pan.___", state 876, "else"
 243         line 416, "pan.___", state 879, "(1)"
 244         line 416, "pan.___", state 880, "(1)"
 245         line 416, "pan.___", state 880, "(1)"
 246         line 414, "pan.___", state 885, "((i<1))"
 247         line 414, "pan.___", state 885, "((i>=1))"
 248         line 421, "pan.___", state 892, "(1)"
 249         line 421, "pan.___", state 893, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 250         line 421, "pan.___", state 893, "else"
 251         line 421, "pan.___", state 896, "(1)"
 252         line 421, "pan.___", state 897, "(1)"
 253         line 421, "pan.___", state 897, "(1)"
 254         line 425, "pan.___", state 905, "(1)"
 255         line 425, "pan.___", state 906, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 256         line 425, "pan.___", state 906, "else"
 257         line 425, "pan.___", state 909, "(1)"
 258         line 425, "pan.___", state 910, "(1)"
 259         line 425, "pan.___", state 910, "(1)"
 260         line 430, "pan.___", state 919, "(1)"
 261         line 430, "pan.___", state 919, "(1)"
 262         line 395, "pan.___", state 926, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 263         line 395, "pan.___", state 928, "(1)"
 264         line 395, "pan.___", state 929, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 265         line 395, "pan.___", state 929, "else"
 266         line 395, "pan.___", state 932, "(1)"
 267         line 399, "pan.___", state 940, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 268         line 399, "pan.___", state 942, "(1)"
 269         line 399, "pan.___", state 943, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 270         line 399, "pan.___", state 943, "else"
 271         line 399, "pan.___", state 946, "(1)"
 272         line 399, "pan.___", state 947, "(1)"
 273         line 399, "pan.___", state 947, "(1)"
 274         line 397, "pan.___", state 952, "((i<1))"
 275         line 397, "pan.___", state 952, "((i>=1))"
 276         line 404, "pan.___", state 958, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 277         line 404, "pan.___", state 960, "(1)"
 278         line 404, "pan.___", state 961, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 279         line 404, "pan.___", state 961, "else"
 280         line 404, "pan.___", state 964, "(1)"
 281         line 404, "pan.___", state 965, "(1)"
 282         line 404, "pan.___", state 965, "(1)"
 283         line 408, "pan.___", state 972, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 284         line 408, "pan.___", state 974, "(1)"
 285         line 408, "pan.___", state 975, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 286         line 408, "pan.___", state 975, "else"
 287         line 408, "pan.___", state 978, "(1)"
 288         line 408, "pan.___", state 979, "(1)"
 289         line 408, "pan.___", state 979, "(1)"
 290         line 406, "pan.___", state 984, "((i<2))"
 291         line 406, "pan.___", state 984, "((i>=2))"
 292         line 412, "pan.___", state 991, "(1)"
 293         line 412, "pan.___", state 992, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 294         line 412, "pan.___", state 992, "else"
 295         line 412, "pan.___", state 995, "(1)"
 296         line 412, "pan.___", state 996, "(1)"
 297         line 412, "pan.___", state 996, "(1)"
 298         line 416, "pan.___", state 1004, "(1)"
 299         line 416, "pan.___", state 1005, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 300         line 416, "pan.___", state 1005, "else"
 301         line 416, "pan.___", state 1008, "(1)"
 302         line 416, "pan.___", state 1009, "(1)"
 303         line 416, "pan.___", state 1009, "(1)"
 304         line 414, "pan.___", state 1014, "((i<1))"
 305         line 414, "pan.___", state 1014, "((i>=1))"
 306         line 421, "pan.___", state 1021, "(1)"
 307         line 421, "pan.___", state 1022, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 308         line 421, "pan.___", state 1022, "else"
 309         line 421, "pan.___", state 1025, "(1)"
 310         line 421, "pan.___", state 1026, "(1)"
 311         line 421, "pan.___", state 1026, "(1)"
 312         line 425, "pan.___", state 1034, "(1)"
 313         line 425, "pan.___", state 1035, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 314         line 425, "pan.___", state 1035, "else"
 315         line 425, "pan.___", state 1038, "(1)"
 316         line 425, "pan.___", state 1039, "(1)"
 317         line 425, "pan.___", state 1039, "(1)"
 318         line 423, "pan.___", state 1044, "((i<2))"
 319         line 423, "pan.___", state 1044, "((i>=2))"
 320         line 430, "pan.___", state 1048, "(1)"
 321         line 430, "pan.___", state 1048, "(1)"
 322         line 678, "pan.___", state 1052, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
 323         line 395, "pan.___", state 1057, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 324         line 404, "pan.___", state 1089, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 325         line 408, "pan.___", state 1103, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 326         line 412, "pan.___", state 1122, "(1)"
 327         line 421, "pan.___", state 1152, "(1)"
 328         line 425, "pan.___", state 1165, "(1)"
 329         line 395, "pan.___", state 1189, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 330         line 404, "pan.___", state 1221, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 331         line 408, "pan.___", state 1235, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 332         line 412, "pan.___", state 1254, "(1)"
 333         line 421, "pan.___", state 1284, "(1)"
 334         line 425, "pan.___", state 1297, "(1)"
 335         line 395, "pan.___", state 1322, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 336         line 404, "pan.___", state 1354, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 337         line 408, "pan.___", state 1368, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 338         line 412, "pan.___", state 1387, "(1)"
 339         line 421, "pan.___", state 1417, "(1)"
 340         line 425, "pan.___", state 1430, "(1)"
 341         line 395, "pan.___", state 1451, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 342         line 404, "pan.___", state 1483, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 343         line 408, "pan.___", state 1497, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 344         line 412, "pan.___", state 1516, "(1)"
 345         line 421, "pan.___", state 1546, "(1)"
 346         line 425, "pan.___", state 1559, "(1)"
 347         line 395, "pan.___", state 1585, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 348         line 404, "pan.___", state 1617, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 349         line 408, "pan.___", state 1631, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 350         line 412, "pan.___", state 1650, "(1)"
 351         line 421, "pan.___", state 1680, "(1)"
 352         line 425, "pan.___", state 1693, "(1)"
 353         line 395, "pan.___", state 1714, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 354         line 404, "pan.___", state 1746, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 355         line 408, "pan.___", state 1760, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 356         line 412, "pan.___", state 1779, "(1)"
 357         line 421, "pan.___", state 1809, "(1)"
 358         line 425, "pan.___", state 1822, "(1)"
 359         line 395, "pan.___", state 1846, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 360         line 404, "pan.___", state 1878, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 361         line 408, "pan.___", state 1892, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 362         line 412, "pan.___", state 1911, "(1)"
 363         line 421, "pan.___", state 1941, "(1)"
 364         line 425, "pan.___", state 1954, "(1)"
 365         line 717, "pan.___", state 1975, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
 366         line 395, "pan.___", state 1982, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 367         line 404, "pan.___", state 2014, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 368         line 408, "pan.___", state 2028, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 369         line 412, "pan.___", state 2047, "(1)"
 370         line 421, "pan.___", state 2077, "(1)"
 371         line 425, "pan.___", state 2090, "(1)"
 372         line 395, "pan.___", state 2111, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 373         line 404, "pan.___", state 2143, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 374         line 408, "pan.___", state 2157, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 375         line 412, "pan.___", state 2176, "(1)"
 376         line 421, "pan.___", state 2206, "(1)"
 377         line 425, "pan.___", state 2219, "(1)"
 378         line 395, "pan.___", state 2242, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 379         line 395, "pan.___", state 2244, "(1)"
 380         line 395, "pan.___", state 2245, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 381         line 395, "pan.___", state 2245, "else"
 382         line 395, "pan.___", state 2248, "(1)"
 383         line 399, "pan.___", state 2256, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 384         line 399, "pan.___", state 2258, "(1)"
 385         line 399, "pan.___", state 2259, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 386         line 399, "pan.___", state 2259, "else"
 387         line 399, "pan.___", state 2262, "(1)"
 388         line 399, "pan.___", state 2263, "(1)"
 389         line 399, "pan.___", state 2263, "(1)"
 390         line 397, "pan.___", state 2268, "((i<1))"
 391         line 397, "pan.___", state 2268, "((i>=1))"
 392         line 404, "pan.___", state 2274, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 393         line 404, "pan.___", state 2276, "(1)"
 394         line 404, "pan.___", state 2277, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 395         line 404, "pan.___", state 2277, "else"
 396         line 404, "pan.___", state 2280, "(1)"
 397         line 404, "pan.___", state 2281, "(1)"
 398         line 404, "pan.___", state 2281, "(1)"
 399         line 408, "pan.___", state 2288, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 400         line 408, "pan.___", state 2290, "(1)"
 401         line 408, "pan.___", state 2291, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 402         line 408, "pan.___", state 2291, "else"
 403         line 408, "pan.___", state 2294, "(1)"
 404         line 408, "pan.___", state 2295, "(1)"
 405         line 408, "pan.___", state 2295, "(1)"
 406         line 406, "pan.___", state 2300, "((i<2))"
 407         line 406, "pan.___", state 2300, "((i>=2))"
 408         line 412, "pan.___", state 2307, "(1)"
 409         line 412, "pan.___", state 2308, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 410         line 412, "pan.___", state 2308, "else"
 411         line 412, "pan.___", state 2311, "(1)"
 412         line 412, "pan.___", state 2312, "(1)"
 413         line 412, "pan.___", state 2312, "(1)"
 414         line 416, "pan.___", state 2320, "(1)"
 415         line 416, "pan.___", state 2321, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 416         line 416, "pan.___", state 2321, "else"
 417         line 416, "pan.___", state 2324, "(1)"
 418         line 416, "pan.___", state 2325, "(1)"
 419         line 416, "pan.___", state 2325, "(1)"
 420         line 414, "pan.___", state 2330, "((i<1))"
 421         line 414, "pan.___", state 2330, "((i>=1))"
 422         line 421, "pan.___", state 2337, "(1)"
 423         line 421, "pan.___", state 2338, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 424         line 421, "pan.___", state 2338, "else"
 425         line 421, "pan.___", state 2341, "(1)"
 426         line 421, "pan.___", state 2342, "(1)"
 427         line 421, "pan.___", state 2342, "(1)"
 428         line 425, "pan.___", state 2350, "(1)"
 429         line 425, "pan.___", state 2351, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 430         line 425, "pan.___", state 2351, "else"
 431         line 425, "pan.___", state 2354, "(1)"
 432         line 425, "pan.___", state 2355, "(1)"
 433         line 425, "pan.___", state 2355, "(1)"
 434         line 423, "pan.___", state 2360, "((i<2))"
 435         line 423, "pan.___", state 2360, "((i>=2))"
 436         line 430, "pan.___", state 2364, "(1)"
 437         line 430, "pan.___", state 2364, "(1)"
 438         line 717, "pan.___", state 2367, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 439         line 717, "pan.___", state 2368, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
 440         line 717, "pan.___", state 2369, "(1)"
 441         line 395, "pan.___", state 2376, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 442         line 404, "pan.___", state 2408, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 443         line 408, "pan.___", state 2422, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 444         line 412, "pan.___", state 2441, "(1)"
 445         line 421, "pan.___", state 2471, "(1)"
 446         line 425, "pan.___", state 2484, "(1)"
 447         line 395, "pan.___", state 2511, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 448         line 404, "pan.___", state 2543, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 449         line 408, "pan.___", state 2557, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 450         line 412, "pan.___", state 2576, "(1)"
 451         line 421, "pan.___", state 2606, "(1)"
 452         line 425, "pan.___", state 2619, "(1)"
 453         line 395, "pan.___", state 2640, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 454         line 404, "pan.___", state 2672, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 455         line 408, "pan.___", state 2686, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 456         line 412, "pan.___", state 2705, "(1)"
 457         line 421, "pan.___", state 2735, "(1)"
 458         line 425, "pan.___", state 2748, "(1)"
 459         line 227, "pan.___", state 2781, "(1)"
 460         line 235, "pan.___", state 2801, "(1)"
 461         line 239, "pan.___", state 2809, "(1)"
 462         line 227, "pan.___", state 2824, "(1)"
 463         line 235, "pan.___", state 2844, "(1)"
 464         line 239, "pan.___", state 2852, "(1)"
 465         line 877, "pan.___", state 2869, "-end-"
 466         (278 of 2869 states)
 467 unreached in proctype urcu_writer
 468         line 395, "pan.___", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 469         line 399, "pan.___", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 470         line 404, "pan.___", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 471         line 412, "pan.___", state 83, "(1)"
 472         line 416, "pan.___", state 96, "(1)"
 473         line 421, "pan.___", state 113, "(1)"
 474         line 250, "pan.___", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 475         line 254, "pan.___", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 476         line 258, "pan.___", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 477         line 395, "pan.___", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 478         line 399, "pan.___", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 479         line 404, "pan.___", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 480         line 408, "pan.___", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 481         line 412, "pan.___", state 276, "(1)"
 482         line 416, "pan.___", state 289, "(1)"
 483         line 421, "pan.___", state 306, "(1)"
 484         line 425, "pan.___", state 319, "(1)"
 485         line 399, "pan.___", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 486         line 404, "pan.___", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 487         line 408, "pan.___", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 488         line 416, "pan.___", state 420, "(1)"
 489         line 421, "pan.___", state 437, "(1)"
 490         line 425, "pan.___", state 450, "(1)"
 491         line 399, "pan.___", state 494, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 492         line 404, "pan.___", state 512, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 493         line 408, "pan.___", state 526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 494         line 416, "pan.___", state 558, "(1)"
 495         line 421, "pan.___", state 575, "(1)"
 496         line 425, "pan.___", state 588, "(1)"
 497         line 399, "pan.___", state 623, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 498         line 404, "pan.___", state 641, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 499         line 408, "pan.___", state 655, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 500         line 416, "pan.___", state 687, "(1)"
 501         line 421, "pan.___", state 704, "(1)"
 502         line 425, "pan.___", state 717, "(1)"
 503         line 399, "pan.___", state 754, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 504         line 404, "pan.___", state 772, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 505         line 408, "pan.___", state 786, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 506         line 416, "pan.___", state 818, "(1)"
 507         line 421, "pan.___", state 835, "(1)"
 508         line 425, "pan.___", state 848, "(1)"
 509         line 250, "pan.___", state 898, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 510         line 254, "pan.___", state 907, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 511         line 258, "pan.___", state 920, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 512         line 227, "pan.___", state 945, "(1)"
 513         line 231, "pan.___", state 953, "(1)"
 514         line 235, "pan.___", state 965, "(1)"
 515         line 239, "pan.___", state 973, "(1)"
 516         line 250, "pan.___", state 1004, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 517         line 254, "pan.___", state 1013, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 518         line 258, "pan.___", state 1026, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 519         line 262, "pan.___", state 1035, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 520         line 227, "pan.___", state 1051, "(1)"
 521         line 231, "pan.___", state 1059, "(1)"
 522         line 235, "pan.___", state 1071, "(1)"
 523         line 239, "pan.___", state 1079, "(1)"
 524         line 250, "pan.___", state 1100, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 525         line 254, "pan.___", state 1109, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 526         line 258, "pan.___", state 1124, "(1)"
 527         line 262, "pan.___", state 1131, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 528         line 227, "pan.___", state 1147, "(1)"
 529         line 231, "pan.___", state 1155, "(1)"
 530         line 235, "pan.___", state 1167, "(1)"
 531         line 239, "pan.___", state 1175, "(1)"
 532         line 250, "pan.___", state 1206, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 533         line 254, "pan.___", state 1215, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 534         line 258, "pan.___", state 1228, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 535         line 262, "pan.___", state 1237, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 536         line 227, "pan.___", state 1253, "(1)"
 537         line 231, "pan.___", state 1261, "(1)"
 538         line 235, "pan.___", state 1273, "(1)"
 539         line 239, "pan.___", state 1281, "(1)"
 540         line 254, "pan.___", state 1307, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 541         line 258, "pan.___", state 1320, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 542         line 262, "pan.___", state 1329, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 543         line 227, "pan.___", state 1345, "(1)"
 544         line 231, "pan.___", state 1353, "(1)"
 545         line 235, "pan.___", state 1365, "(1)"
 546         line 239, "pan.___", state 1373, "(1)"
 547         line 250, "pan.___", state 1404, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 548         line 254, "pan.___", state 1413, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 549         line 258, "pan.___", state 1426, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 550         line 262, "pan.___", state 1435, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 551         line 227, "pan.___", state 1451, "(1)"
 552         line 231, "pan.___", state 1459, "(1)"
 553         line 235, "pan.___", state 1471, "(1)"
 554         line 239, "pan.___", state 1479, "(1)"
 555         line 254, "pan.___", state 1505, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 556         line 258, "pan.___", state 1518, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 557         line 262, "pan.___", state 1527, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 558         line 227, "pan.___", state 1543, "(1)"
 559         line 231, "pan.___", state 1551, "(1)"
 560         line 235, "pan.___", state 1563, "(1)"
 561         line 239, "pan.___", state 1571, "(1)"
 562         line 250, "pan.___", state 1602, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 563         line 254, "pan.___", state 1611, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 564         line 258, "pan.___", state 1624, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 565         line 262, "pan.___", state 1633, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 566         line 227, "pan.___", state 1649, "(1)"
 567         line 231, "pan.___", state 1657, "(1)"
 568         line 235, "pan.___", state 1669, "(1)"
 569         line 239, "pan.___", state 1677, "(1)"
 570         line 254, "pan.___", state 1703, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 571         line 258, "pan.___", state 1716, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 572         line 262, "pan.___", state 1725, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 573         line 227, "pan.___", state 1741, "(1)"
 574         line 231, "pan.___", state 1749, "(1)"
 575         line 235, "pan.___", state 1761, "(1)"
 576         line 239, "pan.___", state 1769, "(1)"
 577         line 250, "pan.___", state 1800, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 578         line 254, "pan.___", state 1809, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 579         line 258, "pan.___", state 1822, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 580         line 262, "pan.___", state 1831, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 581         line 227, "pan.___", state 1847, "(1)"
 582         line 231, "pan.___", state 1855, "(1)"
 583         line 235, "pan.___", state 1867, "(1)"
 584         line 239, "pan.___", state 1875, "(1)"
 585         line 1204, "pan.___", state 1891, "-end-"
 586         (118 of 1891 states)
 587 unreached in proctype :init:
 588         (0 of 78 states)
 589 unreached in proctype :never:
 590         line 1265, "pan.___", state 11, "-end-"
 591         (1 of 11 states)
 592
 593 pan: elapsed time 3.42e+04 seconds
 594 pan: rate 1751.5295 states/second
 595 pan: avg transition delay 1.3345e-06 usec
 596 cp .input.spin urcu_progress_reader.spin.input
 597 cp .input.spin.trail urcu_progress_reader.spin.input.trail