formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_progress_writer_error.log

   1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
   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_writer_error.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 1246)
  19 depth 23: Claim reached state 9 (line 1251)
  20 depth 51: Claim reached state 9 (line 1250)
  21 pan: acceptance cycle (at depth 1200)
  22 pan: wrote .input.spin.trail
  23
  24 (Spin Version 5.1.7 -- 23 December 2008)
  25 Warning: Search not completed
  26         + Partial Order Reduction
  27
  28 Full statespace search for:
  29         never claim             +
  30         assertion violations    + (if within scope of claim)
  31         acceptance   cycles     + (fairness enabled)
  32         invalid end states      - (disabled by never claim)
  33
  34 State-vector 88 byte, depth reached 3997, errors: 1
  35     26291 states, stored (59381 visited)
  36  11000989 states, matched
  37  11060370 transitions (= visited+matched)
  38  60052117 atomic steps
  39 hash conflicts:     84608 (resolved)
  40
  41 Stats on memory usage (in Megabytes):
  42     2.908       equivalent memory usage for states (stored*(State-vector + overhead))
  43     2.889       actual memory usage for states (compression: 99.33%)
  44                 state-vector as stored = 87 byte + 28 byte overhead
  45     8.000       memory used for hash table (-w20)
  46   457.764       memory used for DFS stack (-m10000000)
  47   468.596       total actual memory usage
  48
  49 unreached in proctype urcu_reader
  50         line 648, "pan.___", state 20, "(1)"
  51         line 251, "pan.___", state 32, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  52         line 259, "pan.___", state 54, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  53         line 263, "pan.___", state 63, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  54         line 228, "pan.___", state 79, "(1)"
  55         line 232, "pan.___", state 87, "(1)"
  56         line 236, "pan.___", state 99, "(1)"
  57         line 240, "pan.___", state 107, "(1)"
  58         line 388, "pan.___", state 133, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  59         line 397, "pan.___", state 165, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  60         line 401, "pan.___", state 179, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  61         line 405, "pan.___", state 198, "(1)"
  62         line 414, "pan.___", state 228, "(1)"
  63         line 418, "pan.___", state 241, "(1)"
  64         line 664, "pan.___", state 262, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  65         line 388, "pan.___", state 269, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  66         line 397, "pan.___", state 301, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  67         line 401, "pan.___", state 315, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  68         line 405, "pan.___", state 334, "(1)"
  69         line 414, "pan.___", state 364, "(1)"
  70         line 418, "pan.___", state 377, "(1)"
  71         line 388, "pan.___", state 398, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  72         line 397, "pan.___", state 430, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  73         line 401, "pan.___", state 444, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  74         line 405, "pan.___", state 463, "(1)"
  75         line 414, "pan.___", state 493, "(1)"
  76         line 418, "pan.___", state 506, "(1)"
  77         line 388, "pan.___", state 529, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  78         line 388, "pan.___", state 531, "(1)"
  79         line 388, "pan.___", state 532, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
  80         line 388, "pan.___", state 532, "else"
  81         line 388, "pan.___", state 535, "(1)"
  82         line 392, "pan.___", state 543, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  83         line 392, "pan.___", state 545, "(1)"
  84         line 392, "pan.___", state 546, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
  85         line 392, "pan.___", state 546, "else"
  86         line 392, "pan.___", state 549, "(1)"
  87         line 392, "pan.___", state 550, "(1)"
  88         line 392, "pan.___", state 550, "(1)"
  89         line 390, "pan.___", state 555, "((i<1))"
  90         line 390, "pan.___", state 555, "((i>=1))"
  91         line 397, "pan.___", state 561, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  92         line 397, "pan.___", state 563, "(1)"
  93         line 397, "pan.___", state 564, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
  94         line 397, "pan.___", state 564, "else"
  95         line 397, "pan.___", state 567, "(1)"
  96         line 397, "pan.___", state 568, "(1)"
  97         line 397, "pan.___", state 568, "(1)"
  98         line 401, "pan.___", state 575, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  99         line 401, "pan.___", state 577, "(1)"
 100         line 401, "pan.___", state 578, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 101         line 401, "pan.___", state 578, "else"
 102         line 401, "pan.___", state 581, "(1)"
 103         line 401, "pan.___", state 582, "(1)"
 104         line 401, "pan.___", state 582, "(1)"
 105         line 399, "pan.___", state 587, "((i<2))"
 106         line 399, "pan.___", state 587, "((i>=2))"
 107         line 405, "pan.___", state 594, "(1)"
 108         line 405, "pan.___", state 595, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 109         line 405, "pan.___", state 595, "else"
 110         line 405, "pan.___", state 598, "(1)"
 111         line 405, "pan.___", state 599, "(1)"
 112         line 405, "pan.___", state 599, "(1)"
 113         line 409, "pan.___", state 607, "(1)"
 114         line 409, "pan.___", state 608, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 115         line 409, "pan.___", state 608, "else"
 116         line 409, "pan.___", state 611, "(1)"
 117         line 409, "pan.___", state 612, "(1)"
 118         line 409, "pan.___", state 612, "(1)"
 119         line 407, "pan.___", state 617, "((i<1))"
 120         line 407, "pan.___", state 617, "((i>=1))"
 121         line 414, "pan.___", state 624, "(1)"
 122         line 414, "pan.___", state 625, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 123         line 414, "pan.___", state 625, "else"
 124         line 414, "pan.___", state 628, "(1)"
 125         line 414, "pan.___", state 629, "(1)"
 126         line 414, "pan.___", state 629, "(1)"
 127         line 418, "pan.___", state 637, "(1)"
 128         line 418, "pan.___", state 638, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 129         line 418, "pan.___", state 638, "else"
 130         line 418, "pan.___", state 641, "(1)"
 131         line 418, "pan.___", state 642, "(1)"
 132         line 418, "pan.___", state 642, "(1)"
 133         line 416, "pan.___", state 647, "((i<2))"
 134         line 416, "pan.___", state 647, "((i>=2))"
 135         line 423, "pan.___", state 651, "(1)"
 136         line 423, "pan.___", state 651, "(1)"
 137         line 664, "pan.___", state 654, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 138         line 664, "pan.___", state 655, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 139         line 664, "pan.___", state 656, "(1)"
 140         line 388, "pan.___", state 663, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 141         line 397, "pan.___", state 695, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 142         line 401, "pan.___", state 709, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 143         line 405, "pan.___", state 728, "(1)"
 144         line 414, "pan.___", state 758, "(1)"
 145         line 418, "pan.___", state 771, "(1)"
 146         line 388, "pan.___", state 799, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 147         line 388, "pan.___", state 801, "(1)"
 148         line 388, "pan.___", state 802, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 149         line 388, "pan.___", state 802, "else"
 150         line 388, "pan.___", state 805, "(1)"
 151         line 392, "pan.___", state 813, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 152         line 392, "pan.___", state 815, "(1)"
 153         line 392, "pan.___", state 816, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 154         line 392, "pan.___", state 816, "else"
 155         line 392, "pan.___", state 819, "(1)"
 156         line 392, "pan.___", state 820, "(1)"
 157         line 392, "pan.___", state 820, "(1)"
 158         line 390, "pan.___", state 825, "((i<1))"
 159         line 390, "pan.___", state 825, "((i>=1))"
 160         line 397, "pan.___", state 831, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 161         line 397, "pan.___", state 833, "(1)"
 162         line 397, "pan.___", state 834, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 163         line 397, "pan.___", state 834, "else"
 164         line 397, "pan.___", state 837, "(1)"
 165         line 397, "pan.___", state 838, "(1)"
 166         line 397, "pan.___", state 838, "(1)"
 167         line 401, "pan.___", state 845, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 168         line 401, "pan.___", state 847, "(1)"
 169         line 401, "pan.___", state 848, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 170         line 401, "pan.___", state 848, "else"
 171         line 401, "pan.___", state 851, "(1)"
 172         line 401, "pan.___", state 852, "(1)"
 173         line 401, "pan.___", state 852, "(1)"
 174         line 399, "pan.___", state 857, "((i<2))"
 175         line 399, "pan.___", state 857, "((i>=2))"
 176         line 405, "pan.___", state 864, "(1)"
 177         line 405, "pan.___", state 865, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 178         line 405, "pan.___", state 865, "else"
 179         line 405, "pan.___", state 868, "(1)"
 180         line 405, "pan.___", state 869, "(1)"
 181         line 405, "pan.___", state 869, "(1)"
 182         line 409, "pan.___", state 877, "(1)"
 183         line 409, "pan.___", state 878, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 184         line 409, "pan.___", state 878, "else"
 185         line 409, "pan.___", state 881, "(1)"
 186         line 409, "pan.___", state 882, "(1)"
 187         line 409, "pan.___", state 882, "(1)"
 188         line 407, "pan.___", state 887, "((i<1))"
 189         line 407, "pan.___", state 887, "((i>=1))"
 190         line 414, "pan.___", state 894, "(1)"
 191         line 414, "pan.___", state 895, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 192         line 414, "pan.___", state 895, "else"
 193         line 414, "pan.___", state 898, "(1)"
 194         line 414, "pan.___", state 899, "(1)"
 195         line 414, "pan.___", state 899, "(1)"
 196         line 418, "pan.___", state 907, "(1)"
 197         line 418, "pan.___", state 908, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 198         line 418, "pan.___", state 908, "else"
 199         line 418, "pan.___", state 911, "(1)"
 200         line 418, "pan.___", state 912, "(1)"
 201         line 418, "pan.___", state 912, "(1)"
 202         line 423, "pan.___", state 921, "(1)"
 203         line 423, "pan.___", state 921, "(1)"
 204         line 388, "pan.___", state 928, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 205         line 388, "pan.___", state 930, "(1)"
 206         line 388, "pan.___", state 931, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 207         line 388, "pan.___", state 931, "else"
 208         line 388, "pan.___", state 934, "(1)"
 209         line 392, "pan.___", state 942, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 210         line 392, "pan.___", state 944, "(1)"
 211         line 392, "pan.___", state 945, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 212         line 392, "pan.___", state 945, "else"
 213         line 392, "pan.___", state 948, "(1)"
 214         line 392, "pan.___", state 949, "(1)"
 215         line 392, "pan.___", state 949, "(1)"
 216         line 390, "pan.___", state 954, "((i<1))"
 217         line 390, "pan.___", state 954, "((i>=1))"
 218         line 397, "pan.___", state 960, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 219         line 397, "pan.___", state 962, "(1)"
 220         line 397, "pan.___", state 963, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 221         line 397, "pan.___", state 963, "else"
 222         line 397, "pan.___", state 966, "(1)"
 223         line 397, "pan.___", state 967, "(1)"
 224         line 397, "pan.___", state 967, "(1)"
 225         line 401, "pan.___", state 974, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 226         line 401, "pan.___", state 976, "(1)"
 227         line 401, "pan.___", state 977, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 228         line 401, "pan.___", state 977, "else"
 229         line 401, "pan.___", state 980, "(1)"
 230         line 401, "pan.___", state 981, "(1)"
 231         line 401, "pan.___", state 981, "(1)"
 232         line 399, "pan.___", state 986, "((i<2))"
 233         line 399, "pan.___", state 986, "((i>=2))"
 234         line 405, "pan.___", state 993, "(1)"
 235         line 405, "pan.___", state 994, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 236         line 405, "pan.___", state 994, "else"
 237         line 405, "pan.___", state 997, "(1)"
 238         line 405, "pan.___", state 998, "(1)"
 239         line 405, "pan.___", state 998, "(1)"
 240         line 409, "pan.___", state 1006, "(1)"
 241         line 409, "pan.___", state 1007, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 242         line 409, "pan.___", state 1007, "else"
 243         line 409, "pan.___", state 1010, "(1)"
 244         line 409, "pan.___", state 1011, "(1)"
 245         line 409, "pan.___", state 1011, "(1)"
 246         line 407, "pan.___", state 1016, "((i<1))"
 247         line 407, "pan.___", state 1016, "((i>=1))"
 248         line 414, "pan.___", state 1023, "(1)"
 249         line 414, "pan.___", state 1024, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 250         line 414, "pan.___", state 1024, "else"
 251         line 414, "pan.___", state 1027, "(1)"
 252         line 414, "pan.___", state 1028, "(1)"
 253         line 414, "pan.___", state 1028, "(1)"
 254         line 418, "pan.___", state 1036, "(1)"
 255         line 418, "pan.___", state 1037, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 256         line 418, "pan.___", state 1037, "else"
 257         line 418, "pan.___", state 1040, "(1)"
 258         line 418, "pan.___", state 1041, "(1)"
 259         line 418, "pan.___", state 1041, "(1)"
 260         line 416, "pan.___", state 1046, "((i<2))"
 261         line 416, "pan.___", state 1046, "((i>=2))"
 262         line 423, "pan.___", state 1050, "(1)"
 263         line 423, "pan.___", state 1050, "(1)"
 264         line 672, "pan.___", state 1054, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
 265         line 388, "pan.___", state 1059, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 266         line 397, "pan.___", state 1091, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 267         line 401, "pan.___", state 1105, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 268         line 405, "pan.___", state 1124, "(1)"
 269         line 414, "pan.___", state 1154, "(1)"
 270         line 418, "pan.___", state 1167, "(1)"
 271         line 388, "pan.___", state 1191, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 272         line 397, "pan.___", state 1223, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 273         line 401, "pan.___", state 1237, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 274         line 405, "pan.___", state 1256, "(1)"
 275         line 414, "pan.___", state 1286, "(1)"
 276         line 418, "pan.___", state 1299, "(1)"
 277         line 388, "pan.___", state 1324, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 278         line 397, "pan.___", state 1356, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 279         line 401, "pan.___", state 1370, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 280         line 405, "pan.___", state 1389, "(1)"
 281         line 414, "pan.___", state 1419, "(1)"
 282         line 418, "pan.___", state 1432, "(1)"
 283         line 388, "pan.___", state 1453, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 284         line 397, "pan.___", state 1485, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 285         line 401, "pan.___", state 1499, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 286         line 405, "pan.___", state 1518, "(1)"
 287         line 414, "pan.___", state 1548, "(1)"
 288         line 418, "pan.___", state 1561, "(1)"
 289         line 388, "pan.___", state 1587, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 290         line 397, "pan.___", state 1619, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 291         line 401, "pan.___", state 1633, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 292         line 405, "pan.___", state 1652, "(1)"
 293         line 414, "pan.___", state 1682, "(1)"
 294         line 418, "pan.___", state 1695, "(1)"
 295         line 388, "pan.___", state 1716, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 296         line 397, "pan.___", state 1748, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 297         line 401, "pan.___", state 1762, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 298         line 405, "pan.___", state 1781, "(1)"
 299         line 414, "pan.___", state 1811, "(1)"
 300         line 418, "pan.___", state 1824, "(1)"
 301         line 388, "pan.___", state 1848, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 302         line 397, "pan.___", state 1880, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 303         line 401, "pan.___", state 1894, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 304         line 405, "pan.___", state 1913, "(1)"
 305         line 414, "pan.___", state 1943, "(1)"
 306         line 418, "pan.___", state 1956, "(1)"
 307         line 711, "pan.___", state 1977, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
 308         line 388, "pan.___", state 1984, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 309         line 397, "pan.___", state 2016, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 310         line 401, "pan.___", state 2030, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 311         line 405, "pan.___", state 2049, "(1)"
 312         line 414, "pan.___", state 2079, "(1)"
 313         line 418, "pan.___", state 2092, "(1)"
 314         line 388, "pan.___", state 2113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 315         line 397, "pan.___", state 2145, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 316         line 401, "pan.___", state 2159, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 317         line 405, "pan.___", state 2178, "(1)"
 318         line 414, "pan.___", state 2208, "(1)"
 319         line 418, "pan.___", state 2221, "(1)"
 320         line 388, "pan.___", state 2244, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 321         line 388, "pan.___", state 2246, "(1)"
 322         line 388, "pan.___", state 2247, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 323         line 388, "pan.___", state 2247, "else"
 324         line 388, "pan.___", state 2250, "(1)"
 325         line 392, "pan.___", state 2258, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 326         line 392, "pan.___", state 2260, "(1)"
 327         line 392, "pan.___", state 2261, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 328         line 392, "pan.___", state 2261, "else"
 329         line 392, "pan.___", state 2264, "(1)"
 330         line 392, "pan.___", state 2265, "(1)"
 331         line 392, "pan.___", state 2265, "(1)"
 332         line 390, "pan.___", state 2270, "((i<1))"
 333         line 390, "pan.___", state 2270, "((i>=1))"
 334         line 397, "pan.___", state 2276, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 335         line 397, "pan.___", state 2278, "(1)"
 336         line 397, "pan.___", state 2279, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 337         line 397, "pan.___", state 2279, "else"
 338         line 397, "pan.___", state 2282, "(1)"
 339         line 397, "pan.___", state 2283, "(1)"
 340         line 397, "pan.___", state 2283, "(1)"
 341         line 401, "pan.___", state 2290, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 342         line 401, "pan.___", state 2292, "(1)"
 343         line 401, "pan.___", state 2293, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 344         line 401, "pan.___", state 2293, "else"
 345         line 401, "pan.___", state 2296, "(1)"
 346         line 401, "pan.___", state 2297, "(1)"
 347         line 401, "pan.___", state 2297, "(1)"
 348         line 399, "pan.___", state 2302, "((i<2))"
 349         line 399, "pan.___", state 2302, "((i>=2))"
 350         line 405, "pan.___", state 2309, "(1)"
 351         line 405, "pan.___", state 2310, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 352         line 405, "pan.___", state 2310, "else"
 353         line 405, "pan.___", state 2313, "(1)"
 354         line 405, "pan.___", state 2314, "(1)"
 355         line 405, "pan.___", state 2314, "(1)"
 356         line 409, "pan.___", state 2322, "(1)"
 357         line 409, "pan.___", state 2323, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 358         line 409, "pan.___", state 2323, "else"
 359         line 409, "pan.___", state 2326, "(1)"
 360         line 409, "pan.___", state 2327, "(1)"
 361         line 409, "pan.___", state 2327, "(1)"
 362         line 407, "pan.___", state 2332, "((i<1))"
 363         line 407, "pan.___", state 2332, "((i>=1))"
 364         line 414, "pan.___", state 2339, "(1)"
 365         line 414, "pan.___", state 2340, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 366         line 414, "pan.___", state 2340, "else"
 367         line 414, "pan.___", state 2343, "(1)"
 368         line 414, "pan.___", state 2344, "(1)"
 369         line 414, "pan.___", state 2344, "(1)"
 370         line 418, "pan.___", state 2352, "(1)"
 371         line 418, "pan.___", state 2353, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 372         line 418, "pan.___", state 2353, "else"
 373         line 418, "pan.___", state 2356, "(1)"
 374         line 418, "pan.___", state 2357, "(1)"
 375         line 418, "pan.___", state 2357, "(1)"
 376         line 416, "pan.___", state 2362, "((i<2))"
 377         line 416, "pan.___", state 2362, "((i>=2))"
 378         line 423, "pan.___", state 2366, "(1)"
 379         line 423, "pan.___", state 2366, "(1)"
 380         line 711, "pan.___", state 2369, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 381         line 711, "pan.___", state 2370, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
 382         line 711, "pan.___", state 2371, "(1)"
 383         line 388, "pan.___", state 2378, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 384         line 397, "pan.___", state 2410, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 385         line 401, "pan.___", state 2424, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 386         line 405, "pan.___", state 2443, "(1)"
 387         line 414, "pan.___", state 2473, "(1)"
 388         line 418, "pan.___", state 2486, "(1)"
 389         line 388, "pan.___", state 2513, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 390         line 397, "pan.___", state 2545, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 391         line 401, "pan.___", state 2559, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 392         line 405, "pan.___", state 2578, "(1)"
 393         line 414, "pan.___", state 2608, "(1)"
 394         line 418, "pan.___", state 2621, "(1)"
 395         line 388, "pan.___", state 2642, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 396         line 397, "pan.___", state 2674, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 397         line 401, "pan.___", state 2688, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 398         line 405, "pan.___", state 2707, "(1)"
 399         line 414, "pan.___", state 2737, "(1)"
 400         line 418, "pan.___", state 2750, "(1)"
 401         line 228, "pan.___", state 2783, "(1)"
 402         line 236, "pan.___", state 2803, "(1)"
 403         line 240, "pan.___", state 2811, "(1)"
 404         line 228, "pan.___", state 2826, "(1)"
 405         line 236, "pan.___", state 2846, "(1)"
 406         line 240, "pan.___", state 2854, "(1)"
 407         line 871, "pan.___", state 2871, "-end-"
 408         (279 of 2871 states)
 409 unreached in proctype urcu_writer
 410         line 388, "pan.___", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 411         line 388, "pan.___", state 24, "(1)"
 412         line 392, "pan.___", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 413         line 392, "pan.___", state 38, "(1)"
 414         line 392, "pan.___", state 39, "(1)"
 415         line 392, "pan.___", state 39, "(1)"
 416         line 390, "pan.___", state 44, "((i<1))"
 417         line 390, "pan.___", state 44, "((i>=1))"
 418         line 397, "pan.___", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 419         line 397, "pan.___", state 56, "(1)"
 420         line 397, "pan.___", state 57, "(1)"
 421         line 397, "pan.___", state 57, "(1)"
 422         line 401, "pan.___", state 64, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 423         line 401, "pan.___", state 70, "(1)"
 424         line 401, "pan.___", state 71, "(1)"
 425         line 401, "pan.___", state 71, "(1)"
 426         line 399, "pan.___", state 76, "((i<2))"
 427         line 399, "pan.___", state 76, "((i>=2))"
 428         line 405, "pan.___", state 83, "(1)"
 429         line 405, "pan.___", state 84, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 430         line 405, "pan.___", state 84, "else"
 431         line 405, "pan.___", state 87, "(1)"
 432         line 405, "pan.___", state 88, "(1)"
 433         line 405, "pan.___", state 88, "(1)"
 434         line 409, "pan.___", state 96, "(1)"
 435         line 409, "pan.___", state 97, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 436         line 409, "pan.___", state 97, "else"
 437         line 409, "pan.___", state 100, "(1)"
 438         line 409, "pan.___", state 101, "(1)"
 439         line 409, "pan.___", state 101, "(1)"
 440         line 407, "pan.___", state 106, "((i<1))"
 441         line 407, "pan.___", state 106, "((i>=1))"
 442         line 414, "pan.___", state 113, "(1)"
 443         line 414, "pan.___", state 114, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 444         line 414, "pan.___", state 114, "else"
 445         line 414, "pan.___", state 117, "(1)"
 446         line 414, "pan.___", state 118, "(1)"
 447         line 414, "pan.___", state 118, "(1)"
 448         line 418, "pan.___", state 126, "(1)"
 449         line 418, "pan.___", state 127, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 450         line 418, "pan.___", state 127, "else"
 451         line 418, "pan.___", state 130, "(1)"
 452         line 418, "pan.___", state 131, "(1)"
 453         line 418, "pan.___", state 131, "(1)"
 454         line 416, "pan.___", state 136, "((i<2))"
 455         line 416, "pan.___", state 136, "((i>=2))"
 456         line 423, "pan.___", state 140, "(1)"
 457         line 423, "pan.___", state 140, "(1)"
 458         line 251, "pan.___", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 459         line 255, "pan.___", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 460         line 253, "pan.___", state 166, "((i<1))"
 461         line 253, "pan.___", state 166, "((i>=1))"
 462         line 259, "pan.___", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 463         line 994, "pan.___", state 199, "old_data = cached_rcu_ptr.val[_pid]"
 464         line 388, "pan.___", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 465         line 392, "pan.___", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 466         line 397, "pan.___", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 467         line 401, "pan.___", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 468         line 405, "pan.___", state 276, "(1)"
 469         line 409, "pan.___", state 289, "(1)"
 470         line 414, "pan.___", state 306, "(1)"
 471         line 418, "pan.___", state 319, "(1)"
 472         line 392, "pan.___", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 473         line 397, "pan.___", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 474         line 401, "pan.___", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 475         line 409, "pan.___", state 420, "(1)"
 476         line 414, "pan.___", state 437, "(1)"
 477         line 418, "pan.___", state 450, "(1)"
 478         line 392, "pan.___", state 491, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 479         line 397, "pan.___", state 509, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 480         line 401, "pan.___", state 523, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 481         line 409, "pan.___", state 555, "(1)"
 482         line 414, "pan.___", state 572, "(1)"
 483         line 418, "pan.___", state 585, "(1)"
 484         line 392, "pan.___", state 619, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 485         line 397, "pan.___", state 637, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 486         line 401, "pan.___", state 651, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 487         line 409, "pan.___", state 683, "(1)"
 488         line 414, "pan.___", state 700, "(1)"
 489         line 418, "pan.___", state 713, "(1)"
 490         line 392, "pan.___", state 748, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 491         line 397, "pan.___", state 766, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 492         line 401, "pan.___", state 780, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 493         line 409, "pan.___", state 812, "(1)"
 494         line 414, "pan.___", state 829, "(1)"
 495         line 418, "pan.___", state 842, "(1)"
 496         line 392, "pan.___", state 879, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 497         line 397, "pan.___", state 897, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 498         line 401, "pan.___", state 911, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 499         line 409, "pan.___", state 943, "(1)"
 500         line 414, "pan.___", state 960, "(1)"
 501         line 418, "pan.___", state 973, "(1)"
 502         line 388, "pan.___", state 999, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 503         line 388, "pan.___", state 1001, "(1)"
 504         line 388, "pan.___", state 1002, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 505         line 388, "pan.___", state 1002, "else"
 506         line 388, "pan.___", state 1005, "(1)"
 507         line 392, "pan.___", state 1013, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 508         line 392, "pan.___", state 1015, "(1)"
 509         line 392, "pan.___", state 1016, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 510         line 392, "pan.___", state 1016, "else"
 511         line 392, "pan.___", state 1019, "(1)"
 512         line 392, "pan.___", state 1020, "(1)"
 513         line 392, "pan.___", state 1020, "(1)"
 514         line 390, "pan.___", state 1025, "((i<1))"
 515         line 390, "pan.___", state 1025, "((i>=1))"
 516         line 397, "pan.___", state 1031, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 517         line 397, "pan.___", state 1033, "(1)"
 518         line 397, "pan.___", state 1034, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 519         line 397, "pan.___", state 1034, "else"
 520         line 397, "pan.___", state 1037, "(1)"
 521         line 397, "pan.___", state 1038, "(1)"
 522         line 397, "pan.___", state 1038, "(1)"
 523         line 401, "pan.___", state 1045, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 524         line 401, "pan.___", state 1047, "(1)"
 525         line 401, "pan.___", state 1048, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 526         line 401, "pan.___", state 1048, "else"
 527         line 401, "pan.___", state 1051, "(1)"
 528         line 401, "pan.___", state 1052, "(1)"
 529         line 401, "pan.___", state 1052, "(1)"
 530         line 399, "pan.___", state 1057, "((i<2))"
 531         line 399, "pan.___", state 1057, "((i>=2))"
 532         line 405, "pan.___", state 1064, "(1)"
 533         line 405, "pan.___", state 1065, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 534         line 405, "pan.___", state 1065, "else"
 535         line 405, "pan.___", state 1068, "(1)"
 536         line 405, "pan.___", state 1069, "(1)"
 537         line 405, "pan.___", state 1069, "(1)"
 538         line 409, "pan.___", state 1077, "(1)"
 539         line 409, "pan.___", state 1078, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 540         line 409, "pan.___", state 1078, "else"
 541         line 409, "pan.___", state 1081, "(1)"
 542         line 409, "pan.___", state 1082, "(1)"
 543         line 409, "pan.___", state 1082, "(1)"
 544         line 407, "pan.___", state 1087, "((i<1))"
 545         line 407, "pan.___", state 1087, "((i>=1))"
 546         line 414, "pan.___", state 1094, "(1)"
 547         line 414, "pan.___", state 1095, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 548         line 414, "pan.___", state 1095, "else"
 549         line 414, "pan.___", state 1098, "(1)"
 550         line 414, "pan.___", state 1099, "(1)"
 551         line 414, "pan.___", state 1099, "(1)"
 552         line 418, "pan.___", state 1107, "(1)"
 553         line 418, "pan.___", state 1108, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 554         line 418, "pan.___", state 1108, "else"
 555         line 418, "pan.___", state 1111, "(1)"
 556         line 418, "pan.___", state 1112, "(1)"
 557         line 418, "pan.___", state 1112, "(1)"
 558         line 423, "pan.___", state 1121, "(1)"
 559         line 423, "pan.___", state 1121, "(1)"
 560         line 251, "pan.___", state 1153, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 561         line 255, "pan.___", state 1162, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 562         line 253, "pan.___", state 1170, "((i<1))"
 563         line 253, "pan.___", state 1170, "((i>=1))"
 564         line 259, "pan.___", state 1177, "(1)"
 565         line 259, "pan.___", state 1178, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 566         line 259, "pan.___", state 1178, "else"
 567         line 263, "pan.___", state 1184, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 568         line 261, "pan.___", state 1192, "((i<2))"
 569         line 261, "pan.___", state 1192, "((i>=2))"
 570         line 228, "pan.___", state 1200, "(1)"
 571         line 232, "pan.___", state 1208, "(1)"
 572         line 232, "pan.___", state 1209, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 573         line 232, "pan.___", state 1209, "else"
 574         line 230, "pan.___", state 1214, "((i<1))"
 575         line 230, "pan.___", state 1214, "((i>=1))"
 576         line 236, "pan.___", state 1220, "(1)"
 577         line 236, "pan.___", state 1221, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 578         line 236, "pan.___", state 1221, "else"
 579         line 240, "pan.___", state 1228, "(1)"
 580         line 240, "pan.___", state 1229, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 581         line 240, "pan.___", state 1229, "else"
 582         line 245, "pan.___", state 1238, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 583         line 245, "pan.___", state 1238, "else"
 584         line 251, "pan.___", state 1259, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 585         line 255, "pan.___", state 1268, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 586         line 259, "pan.___", state 1281, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 587         line 263, "pan.___", state 1290, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 588         line 228, "pan.___", state 1306, "(1)"
 589         line 232, "pan.___", state 1314, "(1)"
 590         line 236, "pan.___", state 1326, "(1)"
 591         line 240, "pan.___", state 1334, "(1)"
 592         line 255, "pan.___", state 1360, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 593         line 259, "pan.___", state 1373, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 594         line 263, "pan.___", state 1382, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 595         line 228, "pan.___", state 1398, "(1)"
 596         line 232, "pan.___", state 1406, "(1)"
 597         line 236, "pan.___", state 1418, "(1)"
 598         line 240, "pan.___", state 1426, "(1)"
 599         line 251, "pan.___", state 1457, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 600         line 255, "pan.___", state 1466, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 601         line 259, "pan.___", state 1479, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 602         line 263, "pan.___", state 1488, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 603         line 228, "pan.___", state 1504, "(1)"
 604         line 232, "pan.___", state 1512, "(1)"
 605         line 236, "pan.___", state 1524, "(1)"
 606         line 240, "pan.___", state 1532, "(1)"
 607         line 1192, "pan.___", state 1548, "-end-"
 608         (154 of 1548 states)
 609 unreached in proctype :init:
 610         (0 of 78 states)
 611 unreached in proctype :never:
 612         line 1253, "pan.___", state 11, "-end-"
 613         (1 of 11 states)
 614
 615 pan: elapsed time 14 seconds
 616 pan: rate 4238.4725 states/second
 617 pan: avg transition delay 1.2667e-06 usec
 618 cp .input.spin urcu_progress_writer_error.spin.input
 619 cp .input.spin.trail urcu_progress_writer_error.spin.input.trail
 620 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'