formal-model/results/urcu-controldataflow-ipi-intel/urcu_free_single_flip.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_free.ltl | grep -v ^//`)" >> pan.ltl
   7 cp urcu_free_single_flip.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 -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 1272)
  19 Depth=    6479 States=    1e+06 Transitions= 6.49e+06 Memory=   550.432 t=     16 R=   6e+04
  20 Depth=    6479 States=    2e+06 Transitions= 1.29e+07 Memory=   634.318 t=   32.2 R=   6e+04
  21 Depth=    6479 States=    3e+06 Transitions= 2.07e+07 Memory=   718.303 t=     53 R=   6e+04
  22 pan: resizing hashtable to -w22..  done
  23 Depth=    6479 States=    4e+06 Transitions= 2.91e+07 Memory=   833.311 t=   75.3 R=   5e+04
  24 Depth=    6479 States=    5e+06 Transitions= 3.67e+07 Memory=   917.295 t=   95.1 R=   5e+04
  25 pan: claim violated! (at depth 1254)
  26 pan: wrote .input.spin.trail
  27
  28 (Spin Version 5.1.7 -- 23 December 2008)
  29 Warning: Search not completed
  30         + Partial Order Reduction
  31
  32 Full statespace search for:
  33         never claim             +
  34         assertion violations    + (if within scope of claim)
  35         acceptance   cycles     + (fairness disabled)
  36         invalid end states      - (disabled by never claim)
  37
  38 State-vector 88 byte, depth reached 6479, errors: 1
  39   5383072 states, stored
  40  34108932 states, matched
  41  39492004 transitions (= stored+matched)
  42 5.5430124e+08 atomic steps
  43 hash conflicts:  29860557 (resolved)
  44
  45 Stats on memory usage (in Megabytes):
  46   595.509       equivalent memory usage for states (stored*(State-vector + overhead))
  47   460.005       actual memory usage for states (compression: 77.25%)
  48                 state-vector as stored = 62 byte + 28 byte overhead
  49    32.000       memory used for hash table (-w22)
  50   457.764       memory used for DFS stack (-m10000000)
  51   949.424       total actual memory usage
  52
  53 unreached in proctype urcu_reader
  54         line 262, "pan.___", state 30, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  55         line 270, "pan.___", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  56         line 274, "pan.___", state 61, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  57         line 239, "pan.___", state 77, "(1)"
  58         line 243, "pan.___", state 85, "(1)"
  59         line 247, "pan.___", state 97, "(1)"
  60         line 251, "pan.___", state 105, "(1)"
  61         line 401, "pan.___", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  62         line 410, "pan.___", state 163, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  63         line 414, "pan.___", state 177, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  64         line 239, "pan.___", state 195, "(1)"
  65         line 247, "pan.___", state 215, "(1)"
  66         line 251, "pan.___", state 223, "(1)"
  67         line 680, "pan.___", state 242, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  68         line 401, "pan.___", state 249, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  69         line 410, "pan.___", state 281, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  70         line 414, "pan.___", state 295, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  71         line 239, "pan.___", state 313, "(1)"
  72         line 247, "pan.___", state 333, "(1)"
  73         line 251, "pan.___", state 341, "(1)"
  74         line 401, "pan.___", state 360, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  75         line 410, "pan.___", state 392, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  76         line 414, "pan.___", state 406, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  77         line 239, "pan.___", state 424, "(1)"
  78         line 247, "pan.___", state 444, "(1)"
  79         line 251, "pan.___", state 452, "(1)"
  80         line 401, "pan.___", state 473, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  81         line 401, "pan.___", state 475, "(1)"
  82         line 401, "pan.___", state 476, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
  83         line 401, "pan.___", state 476, "else"
  84         line 401, "pan.___", state 479, "(1)"
  85         line 405, "pan.___", state 487, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  86         line 405, "pan.___", state 489, "(1)"
  87         line 405, "pan.___", state 490, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
  88         line 405, "pan.___", state 490, "else"
  89         line 405, "pan.___", state 493, "(1)"
  90         line 405, "pan.___", state 494, "(1)"
  91         line 405, "pan.___", state 494, "(1)"
  92         line 403, "pan.___", state 499, "((i<1))"
  93         line 403, "pan.___", state 499, "((i>=1))"
  94         line 410, "pan.___", state 505, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  95         line 410, "pan.___", state 507, "(1)"
  96         line 410, "pan.___", state 508, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
  97         line 410, "pan.___", state 508, "else"
  98         line 410, "pan.___", state 511, "(1)"
  99         line 410, "pan.___", state 512, "(1)"
 100         line 410, "pan.___", state 512, "(1)"
 101         line 414, "pan.___", state 519, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 102         line 414, "pan.___", state 521, "(1)"
 103         line 414, "pan.___", state 522, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 104         line 414, "pan.___", state 522, "else"
 105         line 414, "pan.___", state 525, "(1)"
 106         line 414, "pan.___", state 526, "(1)"
 107         line 414, "pan.___", state 526, "(1)"
 108         line 412, "pan.___", state 531, "((i<2))"
 109         line 412, "pan.___", state 531, "((i>=2))"
 110         line 239, "pan.___", state 537, "(1)"
 111         line 243, "pan.___", state 545, "(1)"
 112         line 243, "pan.___", state 546, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 113         line 243, "pan.___", state 546, "else"
 114         line 241, "pan.___", state 551, "((i<1))"
 115         line 241, "pan.___", state 551, "((i>=1))"
 116         line 247, "pan.___", state 557, "(1)"
 117         line 247, "pan.___", state 558, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 118         line 247, "pan.___", state 558, "else"
 119         line 251, "pan.___", state 565, "(1)"
 120         line 251, "pan.___", state 566, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 121         line 251, "pan.___", state 566, "else"
 122         line 249, "pan.___", state 571, "((i<2))"
 123         line 249, "pan.___", state 571, "((i>=2))"
 124         line 256, "pan.___", state 575, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 125         line 256, "pan.___", state 575, "else"
 126         line 421, "pan.___", state 577, "(1)"
 127         line 421, "pan.___", state 577, "(1)"
 128         line 680, "pan.___", state 580, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 129         line 680, "pan.___", state 581, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 130         line 680, "pan.___", state 582, "(1)"
 131         line 401, "pan.___", state 589, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 132         line 410, "pan.___", state 621, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 133         line 414, "pan.___", state 635, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 134         line 239, "pan.___", state 653, "(1)"
 135         line 247, "pan.___", state 673, "(1)"
 136         line 251, "pan.___", state 681, "(1)"
 137         line 401, "pan.___", state 707, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 138         line 401, "pan.___", state 709, "(1)"
 139         line 401, "pan.___", state 710, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 140         line 401, "pan.___", state 710, "else"
 141         line 401, "pan.___", state 713, "(1)"
 142         line 405, "pan.___", state 721, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 143         line 405, "pan.___", state 723, "(1)"
 144         line 405, "pan.___", state 724, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 145         line 405, "pan.___", state 724, "else"
 146         line 405, "pan.___", state 727, "(1)"
 147         line 405, "pan.___", state 728, "(1)"
 148         line 405, "pan.___", state 728, "(1)"
 149         line 403, "pan.___", state 733, "((i<1))"
 150         line 403, "pan.___", state 733, "((i>=1))"
 151         line 410, "pan.___", state 739, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 152         line 410, "pan.___", state 741, "(1)"
 153         line 410, "pan.___", state 742, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 154         line 410, "pan.___", state 742, "else"
 155         line 410, "pan.___", state 745, "(1)"
 156         line 410, "pan.___", state 746, "(1)"
 157         line 410, "pan.___", state 746, "(1)"
 158         line 414, "pan.___", state 753, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 159         line 414, "pan.___", state 755, "(1)"
 160         line 414, "pan.___", state 756, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 161         line 414, "pan.___", state 756, "else"
 162         line 414, "pan.___", state 759, "(1)"
 163         line 414, "pan.___", state 760, "(1)"
 164         line 414, "pan.___", state 760, "(1)"
 165         line 412, "pan.___", state 765, "((i<2))"
 166         line 412, "pan.___", state 765, "((i>=2))"
 167         line 239, "pan.___", state 771, "(1)"
 168         line 243, "pan.___", state 779, "(1)"
 169         line 243, "pan.___", state 780, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 170         line 243, "pan.___", state 780, "else"
 171         line 241, "pan.___", state 785, "((i<1))"
 172         line 241, "pan.___", state 785, "((i>=1))"
 173         line 247, "pan.___", state 791, "(1)"
 174         line 247, "pan.___", state 792, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 175         line 247, "pan.___", state 792, "else"
 176         line 251, "pan.___", state 799, "(1)"
 177         line 251, "pan.___", state 800, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 178         line 251, "pan.___", state 800, "else"
 179         line 256, "pan.___", state 809, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 180         line 256, "pan.___", state 809, "else"
 181         line 421, "pan.___", state 811, "(1)"
 182         line 421, "pan.___", state 811, "(1)"
 183         line 401, "pan.___", state 818, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 184         line 401, "pan.___", state 820, "(1)"
 185         line 401, "pan.___", state 821, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 186         line 401, "pan.___", state 821, "else"
 187         line 401, "pan.___", state 824, "(1)"
 188         line 405, "pan.___", state 832, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 189         line 405, "pan.___", state 834, "(1)"
 190         line 405, "pan.___", state 835, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 191         line 405, "pan.___", state 835, "else"
 192         line 405, "pan.___", state 838, "(1)"
 193         line 405, "pan.___", state 839, "(1)"
 194         line 405, "pan.___", state 839, "(1)"
 195         line 403, "pan.___", state 844, "((i<1))"
 196         line 403, "pan.___", state 844, "((i>=1))"
 197         line 410, "pan.___", state 850, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 198         line 410, "pan.___", state 852, "(1)"
 199         line 410, "pan.___", state 853, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 200         line 410, "pan.___", state 853, "else"
 201         line 410, "pan.___", state 856, "(1)"
 202         line 410, "pan.___", state 857, "(1)"
 203         line 410, "pan.___", state 857, "(1)"
 204         line 414, "pan.___", state 864, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 205         line 414, "pan.___", state 866, "(1)"
 206         line 414, "pan.___", state 867, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 207         line 414, "pan.___", state 867, "else"
 208         line 414, "pan.___", state 870, "(1)"
 209         line 414, "pan.___", state 871, "(1)"
 210         line 414, "pan.___", state 871, "(1)"
 211         line 412, "pan.___", state 876, "((i<2))"
 212         line 412, "pan.___", state 876, "((i>=2))"
 213         line 239, "pan.___", state 882, "(1)"
 214         line 243, "pan.___", state 890, "(1)"
 215         line 243, "pan.___", state 891, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 216         line 243, "pan.___", state 891, "else"
 217         line 241, "pan.___", state 896, "((i<1))"
 218         line 241, "pan.___", state 896, "((i>=1))"
 219         line 247, "pan.___", state 902, "(1)"
 220         line 247, "pan.___", state 903, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 221         line 247, "pan.___", state 903, "else"
 222         line 251, "pan.___", state 910, "(1)"
 223         line 251, "pan.___", state 911, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 224         line 251, "pan.___", state 911, "else"
 225         line 249, "pan.___", state 916, "((i<2))"
 226         line 249, "pan.___", state 916, "((i>=2))"
 227         line 256, "pan.___", state 920, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 228         line 256, "pan.___", state 920, "else"
 229         line 421, "pan.___", state 922, "(1)"
 230         line 421, "pan.___", state 922, "(1)"
 231         line 688, "pan.___", state 926, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
 232         line 401, "pan.___", state 931, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 233         line 410, "pan.___", state 963, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 234         line 414, "pan.___", state 977, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 235         line 239, "pan.___", state 995, "(1)"
 236         line 247, "pan.___", state 1015, "(1)"
 237         line 251, "pan.___", state 1023, "(1)"
 238         line 401, "pan.___", state 1045, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 239         line 410, "pan.___", state 1077, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 240         line 414, "pan.___", state 1091, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 241         line 239, "pan.___", state 1109, "(1)"
 242         line 247, "pan.___", state 1129, "(1)"
 243         line 251, "pan.___", state 1137, "(1)"
 244         line 401, "pan.___", state 1160, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 245         line 410, "pan.___", state 1192, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 246         line 414, "pan.___", state 1206, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 247         line 239, "pan.___", state 1224, "(1)"
 248         line 247, "pan.___", state 1244, "(1)"
 249         line 251, "pan.___", state 1252, "(1)"
 250         line 401, "pan.___", state 1271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 251         line 410, "pan.___", state 1303, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 252         line 414, "pan.___", state 1317, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 253         line 239, "pan.___", state 1335, "(1)"
 254         line 247, "pan.___", state 1355, "(1)"
 255         line 251, "pan.___", state 1363, "(1)"
 256         line 401, "pan.___", state 1387, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 257         line 410, "pan.___", state 1419, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 258         line 414, "pan.___", state 1433, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 259         line 239, "pan.___", state 1451, "(1)"
 260         line 247, "pan.___", state 1471, "(1)"
 261         line 251, "pan.___", state 1479, "(1)"
 262         line 401, "pan.___", state 1498, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 263         line 410, "pan.___", state 1530, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 264         line 414, "pan.___", state 1544, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 265         line 239, "pan.___", state 1562, "(1)"
 266         line 247, "pan.___", state 1582, "(1)"
 267         line 251, "pan.___", state 1590, "(1)"
 268         line 401, "pan.___", state 1612, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 269         line 410, "pan.___", state 1644, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 270         line 414, "pan.___", state 1658, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 271         line 239, "pan.___", state 1676, "(1)"
 272         line 247, "pan.___", state 1696, "(1)"
 273         line 251, "pan.___", state 1704, "(1)"
 274         line 727, "pan.___", state 1723, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
 275         line 401, "pan.___", state 1730, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 276         line 410, "pan.___", state 1762, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 277         line 414, "pan.___", state 1776, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 278         line 239, "pan.___", state 1794, "(1)"
 279         line 247, "pan.___", state 1814, "(1)"
 280         line 251, "pan.___", state 1822, "(1)"
 281         line 401, "pan.___", state 1841, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 282         line 410, "pan.___", state 1873, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 283         line 414, "pan.___", state 1887, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 284         line 239, "pan.___", state 1905, "(1)"
 285         line 247, "pan.___", state 1925, "(1)"
 286         line 251, "pan.___", state 1933, "(1)"
 287         line 401, "pan.___", state 1954, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 288         line 401, "pan.___", state 1956, "(1)"
 289         line 401, "pan.___", state 1957, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 290         line 401, "pan.___", state 1957, "else"
 291         line 401, "pan.___", state 1960, "(1)"
 292         line 405, "pan.___", state 1968, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 293         line 405, "pan.___", state 1970, "(1)"
 294         line 405, "pan.___", state 1971, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 295         line 405, "pan.___", state 1971, "else"
 296         line 405, "pan.___", state 1974, "(1)"
 297         line 405, "pan.___", state 1975, "(1)"
 298         line 405, "pan.___", state 1975, "(1)"
 299         line 403, "pan.___", state 1980, "((i<1))"
 300         line 403, "pan.___", state 1980, "((i>=1))"
 301         line 410, "pan.___", state 1986, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 302         line 410, "pan.___", state 1988, "(1)"
 303         line 410, "pan.___", state 1989, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 304         line 410, "pan.___", state 1989, "else"
 305         line 410, "pan.___", state 1992, "(1)"
 306         line 410, "pan.___", state 1993, "(1)"
 307         line 410, "pan.___", state 1993, "(1)"
 308         line 414, "pan.___", state 2000, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 309         line 414, "pan.___", state 2002, "(1)"
 310         line 414, "pan.___", state 2003, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 311         line 414, "pan.___", state 2003, "else"
 312         line 414, "pan.___", state 2006, "(1)"
 313         line 414, "pan.___", state 2007, "(1)"
 314         line 414, "pan.___", state 2007, "(1)"
 315         line 412, "pan.___", state 2012, "((i<2))"
 316         line 412, "pan.___", state 2012, "((i>=2))"
 317         line 239, "pan.___", state 2018, "(1)"
 318         line 243, "pan.___", state 2026, "(1)"
 319         line 243, "pan.___", state 2027, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 320         line 243, "pan.___", state 2027, "else"
 321         line 241, "pan.___", state 2032, "((i<1))"
 322         line 241, "pan.___", state 2032, "((i>=1))"
 323         line 247, "pan.___", state 2038, "(1)"
 324         line 247, "pan.___", state 2039, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 325         line 247, "pan.___", state 2039, "else"
 326         line 251, "pan.___", state 2046, "(1)"
 327         line 251, "pan.___", state 2047, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 328         line 251, "pan.___", state 2047, "else"
 329         line 249, "pan.___", state 2052, "((i<2))"
 330         line 249, "pan.___", state 2052, "((i>=2))"
 331         line 256, "pan.___", state 2056, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 332         line 256, "pan.___", state 2056, "else"
 333         line 421, "pan.___", state 2058, "(1)"
 334         line 421, "pan.___", state 2058, "(1)"
 335         line 727, "pan.___", state 2061, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 336         line 727, "pan.___", state 2062, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
 337         line 727, "pan.___", state 2063, "(1)"
 338         line 401, "pan.___", state 2070, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 339         line 410, "pan.___", state 2102, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 340         line 414, "pan.___", state 2116, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 341         line 239, "pan.___", state 2134, "(1)"
 342         line 247, "pan.___", state 2154, "(1)"
 343         line 251, "pan.___", state 2162, "(1)"
 344         line 401, "pan.___", state 2187, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 345         line 410, "pan.___", state 2219, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 346         line 414, "pan.___", state 2233, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 347         line 239, "pan.___", state 2251, "(1)"
 348         line 247, "pan.___", state 2271, "(1)"
 349         line 251, "pan.___", state 2279, "(1)"
 350         line 401, "pan.___", state 2298, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 351         line 410, "pan.___", state 2330, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 352         line 414, "pan.___", state 2344, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 353         line 239, "pan.___", state 2362, "(1)"
 354         line 247, "pan.___", state 2382, "(1)"
 355         line 251, "pan.___", state 2390, "(1)"
 356         line 239, "pan.___", state 2421, "(1)"
 357         line 247, "pan.___", state 2441, "(1)"
 358         line 251, "pan.___", state 2449, "(1)"
 359         line 239, "pan.___", state 2464, "(1)"
 360         line 247, "pan.___", state 2484, "(1)"
 361         line 251, "pan.___", state 2492, "(1)"
 362         line 887, "pan.___", state 2509, "-end-"
 363         (246 of 2509 states)
 364 unreached in proctype urcu_writer
 365         line 401, "pan.___", state 22, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 366         line 405, "pan.___", state 36, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 367         line 410, "pan.___", state 54, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 368         line 239, "pan.___", state 86, "(1)"
 369         line 243, "pan.___", state 94, "(1)"
 370         line 247, "pan.___", state 106, "(1)"
 371         line 262, "pan.___", state 135, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 372         line 266, "pan.___", state 144, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 373         line 270, "pan.___", state 157, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 374         line 401, "pan.___", state 197, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 375         line 405, "pan.___", state 211, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 376         line 410, "pan.___", state 229, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 377         line 414, "pan.___", state 243, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 378         line 239, "pan.___", state 261, "(1)"
 379         line 243, "pan.___", state 269, "(1)"
 380         line 247, "pan.___", state 281, "(1)"
 381         line 251, "pan.___", state 289, "(1)"
 382         line 405, "pan.___", state 324, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 383         line 410, "pan.___", state 342, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 384         line 414, "pan.___", state 356, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 385         line 243, "pan.___", state 382, "(1)"
 386         line 247, "pan.___", state 394, "(1)"
 387         line 251, "pan.___", state 402, "(1)"
 388         line 401, "pan.___", state 429, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 389         line 401, "pan.___", state 431, "(1)"
 390         line 401, "pan.___", state 432, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 391         line 401, "pan.___", state 432, "else"
 392         line 401, "pan.___", state 435, "(1)"
 393         line 405, "pan.___", state 443, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 394         line 405, "pan.___", state 445, "(1)"
 395         line 405, "pan.___", state 446, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 396         line 405, "pan.___", state 446, "else"
 397         line 405, "pan.___", state 449, "(1)"
 398         line 405, "pan.___", state 450, "(1)"
 399         line 405, "pan.___", state 450, "(1)"
 400         line 403, "pan.___", state 455, "((i<1))"
 401         line 403, "pan.___", state 455, "((i>=1))"
 402         line 410, "pan.___", state 461, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 403         line 410, "pan.___", state 463, "(1)"
 404         line 410, "pan.___", state 464, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 405         line 410, "pan.___", state 464, "else"
 406         line 410, "pan.___", state 467, "(1)"
 407         line 410, "pan.___", state 468, "(1)"
 408         line 410, "pan.___", state 468, "(1)"
 409         line 414, "pan.___", state 475, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 410         line 414, "pan.___", state 477, "(1)"
 411         line 414, "pan.___", state 478, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 412         line 414, "pan.___", state 478, "else"
 413         line 414, "pan.___", state 481, "(1)"
 414         line 414, "pan.___", state 482, "(1)"
 415         line 414, "pan.___", state 482, "(1)"
 416         line 412, "pan.___", state 487, "((i<2))"
 417         line 412, "pan.___", state 487, "((i>=2))"
 418         line 239, "pan.___", state 493, "(1)"
 419         line 243, "pan.___", state 501, "(1)"
 420         line 243, "pan.___", state 502, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 421         line 243, "pan.___", state 502, "else"
 422         line 241, "pan.___", state 507, "((i<1))"
 423         line 241, "pan.___", state 507, "((i>=1))"
 424         line 247, "pan.___", state 513, "(1)"
 425         line 247, "pan.___", state 514, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 426         line 247, "pan.___", state 514, "else"
 427         line 251, "pan.___", state 521, "(1)"
 428         line 251, "pan.___", state 522, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 429         line 251, "pan.___", state 522, "else"
 430         line 256, "pan.___", state 531, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 431         line 256, "pan.___", state 531, "else"
 432         line 421, "pan.___", state 533, "(1)"
 433         line 421, "pan.___", state 533, "(1)"
 434         line 401, "pan.___", state 540, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 435         line 401, "pan.___", state 542, "(1)"
 436         line 401, "pan.___", state 543, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 437         line 401, "pan.___", state 543, "else"
 438         line 401, "pan.___", state 546, "(1)"
 439         line 405, "pan.___", state 554, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 440         line 405, "pan.___", state 556, "(1)"
 441         line 405, "pan.___", state 557, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 442         line 405, "pan.___", state 557, "else"
 443         line 405, "pan.___", state 560, "(1)"
 444         line 405, "pan.___", state 561, "(1)"
 445         line 405, "pan.___", state 561, "(1)"
 446         line 403, "pan.___", state 566, "((i<1))"
 447         line 403, "pan.___", state 566, "((i>=1))"
 448         line 410, "pan.___", state 572, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 449         line 410, "pan.___", state 574, "(1)"
 450         line 410, "pan.___", state 575, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 451         line 410, "pan.___", state 575, "else"
 452         line 410, "pan.___", state 578, "(1)"
 453         line 410, "pan.___", state 579, "(1)"
 454         line 410, "pan.___", state 579, "(1)"
 455         line 414, "pan.___", state 586, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 456         line 414, "pan.___", state 588, "(1)"
 457         line 414, "pan.___", state 589, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 458         line 414, "pan.___", state 589, "else"
 459         line 414, "pan.___", state 592, "(1)"
 460         line 414, "pan.___", state 593, "(1)"
 461         line 414, "pan.___", state 593, "(1)"
 462         line 412, "pan.___", state 598, "((i<2))"
 463         line 412, "pan.___", state 598, "((i>=2))"
 464         line 239, "pan.___", state 604, "(1)"
 465         line 243, "pan.___", state 612, "(1)"
 466         line 243, "pan.___", state 613, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 467         line 243, "pan.___", state 613, "else"
 468         line 241, "pan.___", state 618, "((i<1))"
 469         line 241, "pan.___", state 618, "((i>=1))"
 470         line 247, "pan.___", state 624, "(1)"
 471         line 247, "pan.___", state 625, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 472         line 247, "pan.___", state 625, "else"
 473         line 251, "pan.___", state 632, "(1)"
 474         line 251, "pan.___", state 633, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 475         line 251, "pan.___", state 633, "else"
 476         line 249, "pan.___", state 638, "((i<2))"
 477         line 249, "pan.___", state 638, "((i>=2))"
 478         line 256, "pan.___", state 642, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 479         line 256, "pan.___", state 642, "else"
 480         line 421, "pan.___", state 644, "(1)"
 481         line 421, "pan.___", state 644, "(1)"
 482         line 1095, "pan.___", state 648, "_proc_urcu_writer = (_proc_urcu_writer|(1<<10))"
 483         line 401, "pan.___", state 653, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 484         line 401, "pan.___", state 655, "(1)"
 485         line 401, "pan.___", state 656, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 486         line 401, "pan.___", state 656, "else"
 487         line 401, "pan.___", state 659, "(1)"
 488         line 405, "pan.___", state 667, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 489         line 405, "pan.___", state 669, "(1)"
 490         line 405, "pan.___", state 670, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 491         line 405, "pan.___", state 670, "else"
 492         line 405, "pan.___", state 673, "(1)"
 493         line 405, "pan.___", state 674, "(1)"
 494         line 405, "pan.___", state 674, "(1)"
 495         line 403, "pan.___", state 679, "((i<1))"
 496         line 403, "pan.___", state 679, "((i>=1))"
 497         line 410, "pan.___", state 685, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 498         line 410, "pan.___", state 687, "(1)"
 499         line 410, "pan.___", state 688, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 500         line 410, "pan.___", state 688, "else"
 501         line 410, "pan.___", state 691, "(1)"
 502         line 410, "pan.___", state 692, "(1)"
 503         line 410, "pan.___", state 692, "(1)"
 504         line 414, "pan.___", state 699, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 505         line 414, "pan.___", state 701, "(1)"
 506         line 414, "pan.___", state 702, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 507         line 414, "pan.___", state 702, "else"
 508         line 414, "pan.___", state 705, "(1)"
 509         line 414, "pan.___", state 706, "(1)"
 510         line 414, "pan.___", state 706, "(1)"
 511         line 412, "pan.___", state 711, "((i<2))"
 512         line 412, "pan.___", state 711, "((i>=2))"
 513         line 239, "pan.___", state 717, "(1)"
 514         line 243, "pan.___", state 725, "(1)"
 515         line 243, "pan.___", state 726, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 516         line 243, "pan.___", state 726, "else"
 517         line 241, "pan.___", state 731, "((i<1))"
 518         line 241, "pan.___", state 731, "((i>=1))"
 519         line 247, "pan.___", state 737, "(1)"
 520         line 247, "pan.___", state 738, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 521         line 247, "pan.___", state 738, "else"
 522         line 251, "pan.___", state 745, "(1)"
 523         line 251, "pan.___", state 746, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 524         line 251, "pan.___", state 746, "else"
 525         line 249, "pan.___", state 751, "((i<2))"
 526         line 249, "pan.___", state 751, "((i>=2))"
 527         line 256, "pan.___", state 755, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 528         line 256, "pan.___", state 755, "else"
 529         line 421, "pan.___", state 757, "(1)"
 530         line 421, "pan.___", state 757, "(1)"
 531         line 1110, "pan.___", state 762, "_proc_urcu_writer = (_proc_urcu_writer|(1<<11))"
 532         line 1105, "pan.___", state 763, "(((tmp2&((1<<7)-1))&&((tmp2^0)&(1<<7))))"
 533         line 1105, "pan.___", state 763, "else"
 534         line 1130, "pan.___", state 767, "_proc_urcu_writer = (_proc_urcu_writer&~(((1<<12)|(1<<11))))"
 535         line 262, "pan.___", state 798, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 536         line 266, "pan.___", state 807, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 537         line 270, "pan.___", state 822, "(1)"
 538         line 274, "pan.___", state 829, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 539         line 239, "pan.___", state 845, "(1)"
 540         line 243, "pan.___", state 853, "(1)"
 541         line 247, "pan.___", state 865, "(1)"
 542         line 251, "pan.___", state 873, "(1)"
 543         line 262, "pan.___", state 904, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 544         line 266, "pan.___", state 913, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 545         line 270, "pan.___", state 926, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 546         line 274, "pan.___", state 935, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 547         line 239, "pan.___", state 951, "(1)"
 548         line 243, "pan.___", state 959, "(1)"
 549         line 247, "pan.___", state 971, "(1)"
 550         line 251, "pan.___", state 979, "(1)"
 551         line 266, "pan.___", state 1005, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 552         line 270, "pan.___", state 1018, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 553         line 274, "pan.___", state 1027, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 554         line 239, "pan.___", state 1043, "(1)"
 555         line 243, "pan.___", state 1051, "(1)"
 556         line 247, "pan.___", state 1063, "(1)"
 557         line 251, "pan.___", state 1071, "(1)"
 558         line 262, "pan.___", state 1102, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 559         line 266, "pan.___", state 1111, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 560         line 270, "pan.___", state 1124, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 561         line 274, "pan.___", state 1133, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 562         line 239, "pan.___", state 1149, "(1)"
 563         line 243, "pan.___", state 1157, "(1)"
 564         line 247, "pan.___", state 1169, "(1)"
 565         line 251, "pan.___", state 1177, "(1)"
 566         line 262, "pan.___", state 1194, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 567         line 262, "pan.___", state 1196, "(1)"
 568         line 266, "pan.___", state 1203, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 569         line 266, "pan.___", state 1205, "(1)"
 570         line 266, "pan.___", state 1206, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 571         line 266, "pan.___", state 1206, "else"
 572         line 264, "pan.___", state 1211, "((i<1))"
 573         line 264, "pan.___", state 1211, "((i>=1))"
 574         line 270, "pan.___", state 1216, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 575         line 270, "pan.___", state 1218, "(1)"
 576         line 270, "pan.___", state 1219, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 577         line 270, "pan.___", state 1219, "else"
 578         line 274, "pan.___", state 1225, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 579         line 274, "pan.___", state 1227, "(1)"
 580         line 274, "pan.___", state 1228, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 581         line 274, "pan.___", state 1228, "else"
 582         line 272, "pan.___", state 1233, "((i<2))"
 583         line 272, "pan.___", state 1233, "((i>=2))"
 584         line 239, "pan.___", state 1241, "(1)"
 585         line 243, "pan.___", state 1249, "(1)"
 586         line 243, "pan.___", state 1250, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 587         line 243, "pan.___", state 1250, "else"
 588         line 241, "pan.___", state 1255, "((i<1))"
 589         line 241, "pan.___", state 1255, "((i>=1))"
 590         line 247, "pan.___", state 1261, "(1)"
 591         line 247, "pan.___", state 1262, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 592         line 247, "pan.___", state 1262, "else"
 593         line 251, "pan.___", state 1269, "(1)"
 594         line 251, "pan.___", state 1270, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 595         line 251, "pan.___", state 1270, "else"
 596         line 256, "pan.___", state 1279, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 597         line 256, "pan.___", state 1279, "else"
 598         line 1206, "pan.___", state 1282, "i = 0"
 599         line 1206, "pan.___", state 1284, "reader_barrier = 1"
 600         line 1206, "pan.___", state 1295, "((i<1))"
 601         line 1206, "pan.___", state 1295, "((i>=1))"
 602         line 262, "pan.___", state 1300, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 603         line 262, "pan.___", state 1302, "(1)"
 604         line 266, "pan.___", state 1309, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 605         line 266, "pan.___", state 1311, "(1)"
 606         line 266, "pan.___", state 1312, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 607         line 266, "pan.___", state 1312, "else"
 608         line 264, "pan.___", state 1317, "((i<1))"
 609         line 264, "pan.___", state 1317, "((i>=1))"
 610         line 270, "pan.___", state 1322, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 611         line 270, "pan.___", state 1324, "(1)"
 612         line 270, "pan.___", state 1325, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 613         line 270, "pan.___", state 1325, "else"
 614         line 274, "pan.___", state 1331, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 615         line 274, "pan.___", state 1333, "(1)"
 616         line 274, "pan.___", state 1334, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 617         line 274, "pan.___", state 1334, "else"
 618         line 272, "pan.___", state 1339, "((i<2))"
 619         line 272, "pan.___", state 1339, "((i>=2))"
 620         line 239, "pan.___", state 1347, "(1)"
 621         line 243, "pan.___", state 1355, "(1)"
 622         line 243, "pan.___", state 1356, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 623         line 243, "pan.___", state 1356, "else"
 624         line 241, "pan.___", state 1361, "((i<1))"
 625         line 241, "pan.___", state 1361, "((i>=1))"
 626         line 247, "pan.___", state 1367, "(1)"
 627         line 247, "pan.___", state 1368, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 628         line 247, "pan.___", state 1368, "else"
 629         line 251, "pan.___", state 1375, "(1)"
 630         line 251, "pan.___", state 1376, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 631         line 251, "pan.___", state 1376, "else"
 632         line 256, "pan.___", state 1385, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 633         line 256, "pan.___", state 1385, "else"
 634         line 289, "pan.___", state 1387, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 635         line 289, "pan.___", state 1387, "else"
 636         line 1206, "pan.___", state 1388, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 637         line 1206, "pan.___", state 1388, "else"
 638         line 266, "pan.___", state 1401, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 639         line 270, "pan.___", state 1414, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 640         line 274, "pan.___", state 1423, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 641         line 239, "pan.___", state 1439, "(1)"
 642         line 243, "pan.___", state 1447, "(1)"
 643         line 247, "pan.___", state 1459, "(1)"
 644         line 251, "pan.___", state 1467, "(1)"
 645         line 262, "pan.___", state 1498, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 646         line 266, "pan.___", state 1507, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 647         line 270, "pan.___", state 1520, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 648         line 274, "pan.___", state 1529, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 649         line 239, "pan.___", state 1545, "(1)"
 650         line 243, "pan.___", state 1553, "(1)"
 651         line 247, "pan.___", state 1565, "(1)"
 652         line 251, "pan.___", state 1573, "(1)"
 653         line 1214, "pan.___", state 1589, "-end-"
 654         (218 of 1589 states)
 655 unreached in proctype :init:
 656         line 1225, "pan.___", state 9, "((j<2))"
 657         line 1225, "pan.___", state 9, "((j>=2))"
 658         line 1226, "pan.___", state 20, "((j<2))"
 659         line 1226, "pan.___", state 20, "((j>=2))"
 660         line 1231, "pan.___", state 33, "((j<2))"
 661         line 1231, "pan.___", state 33, "((j>=2))"
 662         line 1229, "pan.___", state 43, "((i<1))"
 663         line 1229, "pan.___", state 43, "((i>=1))"
 664         line 1239, "pan.___", state 54, "((j<2))"
 665         line 1239, "pan.___", state 54, "((j>=2))"
 666         line 1243, "pan.___", state 67, "((j<2))"
 667         line 1243, "pan.___", state 67, "((j>=2))"
 668         (6 of 78 states)
 669 unreached in proctype :never:
 670         line 1277, "pan.___", state 8, "-end-"
 671         (1 of 8 states)
 672
 673 pan: elapsed time 102 seconds
 674 pan: rate 52558.797 states/second
 675 pan: avg transition delay 2.5934e-06 usec
 676 cp .input.spin urcu_free_single_flip.spin.input
 677 cp .input.spin.trail urcu_free_single_flip.spin.input.trail
 678 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'