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

   1 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
   2 cat DEFINES > .input.spin
   3 cat urcu.spin >> .input.spin
   4 rm -f .input.spin.trail
   5 spin -a -X .input.spin
   6 Exit-Status 0
   7 gcc -O2 -w -DHASH64 -DSAFETY -o pan pan.c
   8 ./pan -v -c1 -X -m10000000 -w20
   9 Depth=    5832 States=    1e+06 Transitions= 1.25e+08 Memory=   542.717 t=    123 R=   8e+03
  10 Depth=    5832 States=    2e+06 Transitions= 4.09e+08 Memory=   618.986 t=    417 R=   5e+03
  11 Depth=    5832 States=    3e+06 Transitions= 6.64e+08 Memory=   695.256 t=    685 R=   4e+03
  12 pan: resizing hashtable to -w22..  done
  13 Depth=    5832 States=    4e+06 Transitions= 1.15e+09 Memory=   802.647 t= 1.2e+03 R=   3e+03
  14 Depth=    5832 States=    5e+06 Transitions= 1.46e+09 Memory=   878.916 t= 1.52e+03 R=   3e+03
  15 Depth=    5832 States=    6e+06 Transitions= 1.66e+09 Memory=   955.186 t= 1.72e+03 R=   3e+03
  16 Depth=    5832 States=    7e+06 Transitions= 1.86e+09 Memory=  1031.455 t= 1.93e+03 R=   4e+03
  17 Depth=    5832 States=    8e+06 Transitions= 2.13e+09 Memory=  1107.822 t= 2.22e+03 R=   4e+03
  18 Depth=    5832 States=    9e+06 Transitions= 2.38e+09 Memory=  1184.092 t= 2.49e+03 R=   4e+03
  19 pan: resizing hashtable to -w24..  done
  20 Depth=    5832 States=    1e+07 Transitions= 2.87e+09 Memory=  1384.455 t=  3e+03 R=   3e+03
  21 Depth=    5832 States=  1.1e+07 Transitions= 3.15e+09 Memory=  1460.725 t= 3.29e+03 R=   3e+03
  22 Depth=    5832 States=  1.2e+07 Transitions= 3.42e+09 Memory=  1536.994 t= 3.57e+03 R=   3e+03
  23 Depth=    5832 States=  1.3e+07 Transitions= 3.62e+09 Memory=  1613.361 t= 3.77e+03 R=   3e+03
  24 Depth=    5832 States=  1.4e+07 Transitions= 3.84e+09 Memory=  1689.631 t= 3.99e+03 R=   4e+03
  25 Depth=    5832 States=  1.5e+07 Transitions= 4.13e+09 Memory=  1765.901 t= 4.29e+03 R=   3e+03
  26
  27 (Spin Version 5.1.7 -- 23 December 2008)
  28         + Partial Order Reduction
  29
  30 Full statespace search for:
  31         never claim             - (none specified)
  32         assertion violations    +
  33         cycle checks            - (disabled by -DSAFETY)
  34         invalid end states      +
  35
  36 State-vector 72 byte, depth reached 5832, errors: 0
  37  15444143 states, stored
  38 4.2527754e+09 states, matched
  39 4.2682195e+09 transitions (= stored+matched)
  40 2.483245e+10 atomic steps
  41 hash conflicts: 2.790927e+09 (resolved)
  42
  43 Stats on memory usage (in Megabytes):
  44  1472.868       equivalent memory usage for states (stored*(State-vector + overhead))
  45  1214.135       actual memory usage for states (compression: 82.43%)
  46                 state-vector as stored = 54 byte + 28 byte overhead
  47   128.000       memory used for hash table (-w24)
  48   457.764       memory used for DFS stack (-m10000000)
  49  1799.787       total actual memory usage
  50
  51 unreached in proctype urcu_reader
  52         line 249, ".input.spin", state 30, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  53         line 257, ".input.spin", state 52, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  54         line 261, ".input.spin", state 61, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  55         line 226, ".input.spin", state 77, "(1)"
  56         line 230, ".input.spin", state 85, "(1)"
  57         line 234, ".input.spin", state 97, "(1)"
  58         line 238, ".input.spin", state 105, "(1)"
  59         line 394, ".input.spin", state 131, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  60         line 403, ".input.spin", state 163, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  61         line 407, ".input.spin", state 177, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  62         line 411, ".input.spin", state 196, "(1)"
  63         line 420, ".input.spin", state 226, "(1)"
  64         line 424, ".input.spin", state 239, "(1)"
  65         line 669, ".input.spin", state 260, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  66         line 394, ".input.spin", state 267, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  67         line 403, ".input.spin", state 299, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  68         line 407, ".input.spin", state 313, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  69         line 411, ".input.spin", state 332, "(1)"
  70         line 420, ".input.spin", state 362, "(1)"
  71         line 424, ".input.spin", state 375, "(1)"
  72         line 394, ".input.spin", state 396, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  73         line 403, ".input.spin", state 428, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  74         line 407, ".input.spin", state 442, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  75         line 411, ".input.spin", state 461, "(1)"
  76         line 420, ".input.spin", state 491, "(1)"
  77         line 424, ".input.spin", state 504, "(1)"
  78         line 394, ".input.spin", state 527, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  79         line 394, ".input.spin", state 529, "(1)"
  80         line 394, ".input.spin", state 530, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
  81         line 394, ".input.spin", state 530, "else"
  82         line 394, ".input.spin", state 533, "(1)"
  83         line 398, ".input.spin", state 541, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  84         line 398, ".input.spin", state 543, "(1)"
  85         line 398, ".input.spin", state 544, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
  86         line 398, ".input.spin", state 544, "else"
  87         line 398, ".input.spin", state 547, "(1)"
  88         line 398, ".input.spin", state 548, "(1)"
  89         line 398, ".input.spin", state 548, "(1)"
  90         line 396, ".input.spin", state 553, "((i<1))"
  91         line 396, ".input.spin", state 553, "((i>=1))"
  92         line 403, ".input.spin", state 559, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  93         line 403, ".input.spin", state 561, "(1)"
  94         line 403, ".input.spin", state 562, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
  95         line 403, ".input.spin", state 562, "else"
  96         line 403, ".input.spin", state 565, "(1)"
  97         line 403, ".input.spin", state 566, "(1)"
  98         line 403, ".input.spin", state 566, "(1)"
  99         line 407, ".input.spin", state 573, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 100         line 407, ".input.spin", state 575, "(1)"
 101         line 407, ".input.spin", state 576, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 102         line 407, ".input.spin", state 576, "else"
 103         line 407, ".input.spin", state 579, "(1)"
 104         line 407, ".input.spin", state 580, "(1)"
 105         line 407, ".input.spin", state 580, "(1)"
 106         line 405, ".input.spin", state 585, "((i<2))"
 107         line 405, ".input.spin", state 585, "((i>=2))"
 108         line 411, ".input.spin", state 592, "(1)"
 109         line 411, ".input.spin", state 593, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 110         line 411, ".input.spin", state 593, "else"
 111         line 411, ".input.spin", state 596, "(1)"
 112         line 411, ".input.spin", state 597, "(1)"
 113         line 411, ".input.spin", state 597, "(1)"
 114         line 415, ".input.spin", state 605, "(1)"
 115         line 415, ".input.spin", state 606, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 116         line 415, ".input.spin", state 606, "else"
 117         line 415, ".input.spin", state 609, "(1)"
 118         line 415, ".input.spin", state 610, "(1)"
 119         line 415, ".input.spin", state 610, "(1)"
 120         line 413, ".input.spin", state 615, "((i<1))"
 121         line 413, ".input.spin", state 615, "((i>=1))"
 122         line 420, ".input.spin", state 622, "(1)"
 123         line 420, ".input.spin", state 623, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 124         line 420, ".input.spin", state 623, "else"
 125         line 420, ".input.spin", state 626, "(1)"
 126         line 420, ".input.spin", state 627, "(1)"
 127         line 420, ".input.spin", state 627, "(1)"
 128         line 424, ".input.spin", state 635, "(1)"
 129         line 424, ".input.spin", state 636, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 130         line 424, ".input.spin", state 636, "else"
 131         line 424, ".input.spin", state 639, "(1)"
 132         line 424, ".input.spin", state 640, "(1)"
 133         line 424, ".input.spin", state 640, "(1)"
 134         line 422, ".input.spin", state 645, "((i<2))"
 135         line 422, ".input.spin", state 645, "((i>=2))"
 136         line 429, ".input.spin", state 649, "(1)"
 137         line 429, ".input.spin", state 649, "(1)"
 138         line 669, ".input.spin", state 652, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 139         line 669, ".input.spin", state 653, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 140         line 669, ".input.spin", state 654, "(1)"
 141         line 394, ".input.spin", state 661, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 142         line 403, ".input.spin", state 693, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 143         line 407, ".input.spin", state 707, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 144         line 411, ".input.spin", state 726, "(1)"
 145         line 420, ".input.spin", state 756, "(1)"
 146         line 424, ".input.spin", state 769, "(1)"
 147         line 394, ".input.spin", state 797, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 148         line 394, ".input.spin", state 799, "(1)"
 149         line 394, ".input.spin", state 800, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 150         line 394, ".input.spin", state 800, "else"
 151         line 394, ".input.spin", state 803, "(1)"
 152         line 398, ".input.spin", state 811, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 153         line 398, ".input.spin", state 813, "(1)"
 154         line 398, ".input.spin", state 814, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 155         line 398, ".input.spin", state 814, "else"
 156         line 398, ".input.spin", state 817, "(1)"
 157         line 398, ".input.spin", state 818, "(1)"
 158         line 398, ".input.spin", state 818, "(1)"
 159         line 396, ".input.spin", state 823, "((i<1))"
 160         line 396, ".input.spin", state 823, "((i>=1))"
 161         line 403, ".input.spin", state 829, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 162         line 403, ".input.spin", state 831, "(1)"
 163         line 403, ".input.spin", state 832, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 164         line 403, ".input.spin", state 832, "else"
 165         line 403, ".input.spin", state 835, "(1)"
 166         line 403, ".input.spin", state 836, "(1)"
 167         line 403, ".input.spin", state 836, "(1)"
 168         line 407, ".input.spin", state 843, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 169         line 407, ".input.spin", state 845, "(1)"
 170         line 407, ".input.spin", state 846, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 171         line 407, ".input.spin", state 846, "else"
 172         line 407, ".input.spin", state 849, "(1)"
 173         line 407, ".input.spin", state 850, "(1)"
 174         line 407, ".input.spin", state 850, "(1)"
 175         line 405, ".input.spin", state 855, "((i<2))"
 176         line 405, ".input.spin", state 855, "((i>=2))"
 177         line 411, ".input.spin", state 862, "(1)"
 178         line 411, ".input.spin", state 863, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 179         line 411, ".input.spin", state 863, "else"
 180         line 411, ".input.spin", state 866, "(1)"
 181         line 411, ".input.spin", state 867, "(1)"
 182         line 411, ".input.spin", state 867, "(1)"
 183         line 415, ".input.spin", state 875, "(1)"
 184         line 415, ".input.spin", state 876, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 185         line 415, ".input.spin", state 876, "else"
 186         line 415, ".input.spin", state 879, "(1)"
 187         line 415, ".input.spin", state 880, "(1)"
 188         line 415, ".input.spin", state 880, "(1)"
 189         line 413, ".input.spin", state 885, "((i<1))"
 190         line 413, ".input.spin", state 885, "((i>=1))"
 191         line 420, ".input.spin", state 892, "(1)"
 192         line 420, ".input.spin", state 893, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 193         line 420, ".input.spin", state 893, "else"
 194         line 420, ".input.spin", state 896, "(1)"
 195         line 420, ".input.spin", state 897, "(1)"
 196         line 420, ".input.spin", state 897, "(1)"
 197         line 424, ".input.spin", state 905, "(1)"
 198         line 424, ".input.spin", state 906, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 199         line 424, ".input.spin", state 906, "else"
 200         line 424, ".input.spin", state 909, "(1)"
 201         line 424, ".input.spin", state 910, "(1)"
 202         line 424, ".input.spin", state 910, "(1)"
 203         line 429, ".input.spin", state 919, "(1)"
 204         line 429, ".input.spin", state 919, "(1)"
 205         line 394, ".input.spin", state 926, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 206         line 394, ".input.spin", state 928, "(1)"
 207         line 394, ".input.spin", state 929, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 208         line 394, ".input.spin", state 929, "else"
 209         line 394, ".input.spin", state 932, "(1)"
 210         line 398, ".input.spin", state 940, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 211         line 398, ".input.spin", state 942, "(1)"
 212         line 398, ".input.spin", state 943, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 213         line 398, ".input.spin", state 943, "else"
 214         line 398, ".input.spin", state 946, "(1)"
 215         line 398, ".input.spin", state 947, "(1)"
 216         line 398, ".input.spin", state 947, "(1)"
 217         line 396, ".input.spin", state 952, "((i<1))"
 218         line 396, ".input.spin", state 952, "((i>=1))"
 219         line 403, ".input.spin", state 958, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 220         line 403, ".input.spin", state 960, "(1)"
 221         line 403, ".input.spin", state 961, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 222         line 403, ".input.spin", state 961, "else"
 223         line 403, ".input.spin", state 964, "(1)"
 224         line 403, ".input.spin", state 965, "(1)"
 225         line 403, ".input.spin", state 965, "(1)"
 226         line 407, ".input.spin", state 972, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 227         line 407, ".input.spin", state 974, "(1)"
 228         line 407, ".input.spin", state 975, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 229         line 407, ".input.spin", state 975, "else"
 230         line 407, ".input.spin", state 978, "(1)"
 231         line 407, ".input.spin", state 979, "(1)"
 232         line 407, ".input.spin", state 979, "(1)"
 233         line 405, ".input.spin", state 984, "((i<2))"
 234         line 405, ".input.spin", state 984, "((i>=2))"
 235         line 411, ".input.spin", state 991, "(1)"
 236         line 411, ".input.spin", state 992, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 237         line 411, ".input.spin", state 992, "else"
 238         line 411, ".input.spin", state 995, "(1)"
 239         line 411, ".input.spin", state 996, "(1)"
 240         line 411, ".input.spin", state 996, "(1)"
 241         line 415, ".input.spin", state 1004, "(1)"
 242         line 415, ".input.spin", state 1005, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 243         line 415, ".input.spin", state 1005, "else"
 244         line 415, ".input.spin", state 1008, "(1)"
 245         line 415, ".input.spin", state 1009, "(1)"
 246         line 415, ".input.spin", state 1009, "(1)"
 247         line 413, ".input.spin", state 1014, "((i<1))"
 248         line 413, ".input.spin", state 1014, "((i>=1))"
 249         line 420, ".input.spin", state 1021, "(1)"
 250         line 420, ".input.spin", state 1022, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 251         line 420, ".input.spin", state 1022, "else"
 252         line 420, ".input.spin", state 1025, "(1)"
 253         line 420, ".input.spin", state 1026, "(1)"
 254         line 420, ".input.spin", state 1026, "(1)"
 255         line 424, ".input.spin", state 1034, "(1)"
 256         line 424, ".input.spin", state 1035, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 257         line 424, ".input.spin", state 1035, "else"
 258         line 424, ".input.spin", state 1038, "(1)"
 259         line 424, ".input.spin", state 1039, "(1)"
 260         line 424, ".input.spin", state 1039, "(1)"
 261         line 422, ".input.spin", state 1044, "((i<2))"
 262         line 422, ".input.spin", state 1044, "((i>=2))"
 263         line 429, ".input.spin", state 1048, "(1)"
 264         line 429, ".input.spin", state 1048, "(1)"
 265         line 677, ".input.spin", state 1052, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
 266         line 394, ".input.spin", state 1057, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 267         line 403, ".input.spin", state 1089, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 268         line 407, ".input.spin", state 1103, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 269         line 411, ".input.spin", state 1122, "(1)"
 270         line 420, ".input.spin", state 1152, "(1)"
 271         line 424, ".input.spin", state 1165, "(1)"
 272         line 394, ".input.spin", state 1189, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 273         line 403, ".input.spin", state 1221, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 274         line 407, ".input.spin", state 1235, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 275         line 411, ".input.spin", state 1254, "(1)"
 276         line 420, ".input.spin", state 1284, "(1)"
 277         line 424, ".input.spin", state 1297, "(1)"
 278         line 394, ".input.spin", state 1322, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 279         line 403, ".input.spin", state 1354, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 280         line 407, ".input.spin", state 1368, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 281         line 411, ".input.spin", state 1387, "(1)"
 282         line 420, ".input.spin", state 1417, "(1)"
 283         line 424, ".input.spin", state 1430, "(1)"
 284         line 394, ".input.spin", state 1451, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 285         line 403, ".input.spin", state 1483, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 286         line 407, ".input.spin", state 1497, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 287         line 411, ".input.spin", state 1516, "(1)"
 288         line 420, ".input.spin", state 1546, "(1)"
 289         line 424, ".input.spin", state 1559, "(1)"
 290         line 394, ".input.spin", state 1585, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 291         line 403, ".input.spin", state 1617, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 292         line 407, ".input.spin", state 1631, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 293         line 411, ".input.spin", state 1650, "(1)"
 294         line 420, ".input.spin", state 1680, "(1)"
 295         line 424, ".input.spin", state 1693, "(1)"
 296         line 394, ".input.spin", state 1714, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 297         line 403, ".input.spin", state 1746, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 298         line 407, ".input.spin", state 1760, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 299         line 411, ".input.spin", state 1779, "(1)"
 300         line 420, ".input.spin", state 1809, "(1)"
 301         line 424, ".input.spin", state 1822, "(1)"
 302         line 394, ".input.spin", state 1846, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 303         line 403, ".input.spin", state 1878, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 304         line 407, ".input.spin", state 1892, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 305         line 411, ".input.spin", state 1911, "(1)"
 306         line 420, ".input.spin", state 1941, "(1)"
 307         line 424, ".input.spin", state 1954, "(1)"
 308         line 716, ".input.spin", state 1975, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
 309         line 394, ".input.spin", state 1982, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 310         line 403, ".input.spin", state 2014, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 311         line 407, ".input.spin", state 2028, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 312         line 411, ".input.spin", state 2047, "(1)"
 313         line 420, ".input.spin", state 2077, "(1)"
 314         line 424, ".input.spin", state 2090, "(1)"
 315         line 394, ".input.spin", state 2111, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 316         line 403, ".input.spin", state 2143, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 317         line 407, ".input.spin", state 2157, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 318         line 411, ".input.spin", state 2176, "(1)"
 319         line 420, ".input.spin", state 2206, "(1)"
 320         line 424, ".input.spin", state 2219, "(1)"
 321         line 394, ".input.spin", state 2242, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 322         line 394, ".input.spin", state 2244, "(1)"
 323         line 394, ".input.spin", state 2245, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 324         line 394, ".input.spin", state 2245, "else"
 325         line 394, ".input.spin", state 2248, "(1)"
 326         line 398, ".input.spin", state 2256, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 327         line 398, ".input.spin", state 2258, "(1)"
 328         line 398, ".input.spin", state 2259, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 329         line 398, ".input.spin", state 2259, "else"
 330         line 398, ".input.spin", state 2262, "(1)"
 331         line 398, ".input.spin", state 2263, "(1)"
 332         line 398, ".input.spin", state 2263, "(1)"
 333         line 396, ".input.spin", state 2268, "((i<1))"
 334         line 396, ".input.spin", state 2268, "((i>=1))"
 335         line 403, ".input.spin", state 2274, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 336         line 403, ".input.spin", state 2276, "(1)"
 337         line 403, ".input.spin", state 2277, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 338         line 403, ".input.spin", state 2277, "else"
 339         line 403, ".input.spin", state 2280, "(1)"
 340         line 403, ".input.spin", state 2281, "(1)"
 341         line 403, ".input.spin", state 2281, "(1)"
 342         line 407, ".input.spin", state 2288, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 343         line 407, ".input.spin", state 2290, "(1)"
 344         line 407, ".input.spin", state 2291, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 345         line 407, ".input.spin", state 2291, "else"
 346         line 407, ".input.spin", state 2294, "(1)"
 347         line 407, ".input.spin", state 2295, "(1)"
 348         line 407, ".input.spin", state 2295, "(1)"
 349         line 405, ".input.spin", state 2300, "((i<2))"
 350         line 405, ".input.spin", state 2300, "((i>=2))"
 351         line 411, ".input.spin", state 2307, "(1)"
 352         line 411, ".input.spin", state 2308, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 353         line 411, ".input.spin", state 2308, "else"
 354         line 411, ".input.spin", state 2311, "(1)"
 355         line 411, ".input.spin", state 2312, "(1)"
 356         line 411, ".input.spin", state 2312, "(1)"
 357         line 415, ".input.spin", state 2320, "(1)"
 358         line 415, ".input.spin", state 2321, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 359         line 415, ".input.spin", state 2321, "else"
 360         line 415, ".input.spin", state 2324, "(1)"
 361         line 415, ".input.spin", state 2325, "(1)"
 362         line 415, ".input.spin", state 2325, "(1)"
 363         line 413, ".input.spin", state 2330, "((i<1))"
 364         line 413, ".input.spin", state 2330, "((i>=1))"
 365         line 420, ".input.spin", state 2337, "(1)"
 366         line 420, ".input.spin", state 2338, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 367         line 420, ".input.spin", state 2338, "else"
 368         line 420, ".input.spin", state 2341, "(1)"
 369         line 420, ".input.spin", state 2342, "(1)"
 370         line 420, ".input.spin", state 2342, "(1)"
 371         line 424, ".input.spin", state 2350, "(1)"
 372         line 424, ".input.spin", state 2351, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 373         line 424, ".input.spin", state 2351, "else"
 374         line 424, ".input.spin", state 2354, "(1)"
 375         line 424, ".input.spin", state 2355, "(1)"
 376         line 424, ".input.spin", state 2355, "(1)"
 377         line 422, ".input.spin", state 2360, "((i<2))"
 378         line 422, ".input.spin", state 2360, "((i>=2))"
 379         line 429, ".input.spin", state 2364, "(1)"
 380         line 429, ".input.spin", state 2364, "(1)"
 381         line 716, ".input.spin", state 2367, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 382         line 716, ".input.spin", state 2368, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
 383         line 716, ".input.spin", state 2369, "(1)"
 384         line 394, ".input.spin", state 2376, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 385         line 403, ".input.spin", state 2408, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 386         line 407, ".input.spin", state 2422, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 387         line 411, ".input.spin", state 2441, "(1)"
 388         line 420, ".input.spin", state 2471, "(1)"
 389         line 424, ".input.spin", state 2484, "(1)"
 390         line 394, ".input.spin", state 2511, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 391         line 403, ".input.spin", state 2543, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 392         line 407, ".input.spin", state 2557, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 393         line 411, ".input.spin", state 2576, "(1)"
 394         line 420, ".input.spin", state 2606, "(1)"
 395         line 424, ".input.spin", state 2619, "(1)"
 396         line 394, ".input.spin", state 2640, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 397         line 403, ".input.spin", state 2672, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 398         line 407, ".input.spin", state 2686, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 399         line 411, ".input.spin", state 2705, "(1)"
 400         line 420, ".input.spin", state 2735, "(1)"
 401         line 424, ".input.spin", state 2748, "(1)"
 402         line 226, ".input.spin", state 2781, "(1)"
 403         line 234, ".input.spin", state 2801, "(1)"
 404         line 238, ".input.spin", state 2809, "(1)"
 405         line 226, ".input.spin", state 2824, "(1)"
 406         line 234, ".input.spin", state 2844, "(1)"
 407         line 238, ".input.spin", state 2852, "(1)"
 408         line 876, ".input.spin", state 2869, "-end-"
 409         (278 of 2869 states)
 410 unreached in proctype urcu_writer
 411         line 394, ".input.spin", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 412         line 398, ".input.spin", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 413         line 403, ".input.spin", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 414         line 411, ".input.spin", state 83, "(1)"
 415         line 415, ".input.spin", state 96, "(1)"
 416         line 420, ".input.spin", state 113, "(1)"
 417         line 249, ".input.spin", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 418         line 253, ".input.spin", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 419         line 257, ".input.spin", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 420         line 394, ".input.spin", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 421         line 398, ".input.spin", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 422         line 403, ".input.spin", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 423         line 407, ".input.spin", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 424         line 411, ".input.spin", state 276, "(1)"
 425         line 415, ".input.spin", state 289, "(1)"
 426         line 420, ".input.spin", state 306, "(1)"
 427         line 424, ".input.spin", state 319, "(1)"
 428         line 398, ".input.spin", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 429         line 403, ".input.spin", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 430         line 407, ".input.spin", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 431         line 415, ".input.spin", state 420, "(1)"
 432         line 420, ".input.spin", state 437, "(1)"
 433         line 424, ".input.spin", state 450, "(1)"
 434         line 398, ".input.spin", state 494, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 435         line 403, ".input.spin", state 512, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 436         line 407, ".input.spin", state 526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 437         line 415, ".input.spin", state 558, "(1)"
 438         line 420, ".input.spin", state 575, "(1)"
 439         line 424, ".input.spin", state 588, "(1)"
 440         line 398, ".input.spin", state 623, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 441         line 403, ".input.spin", state 641, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 442         line 407, ".input.spin", state 655, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 443         line 415, ".input.spin", state 687, "(1)"
 444         line 420, ".input.spin", state 704, "(1)"
 445         line 424, ".input.spin", state 717, "(1)"
 446         line 398, ".input.spin", state 754, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 447         line 403, ".input.spin", state 772, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 448         line 407, ".input.spin", state 786, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 449         line 415, ".input.spin", state 818, "(1)"
 450         line 420, ".input.spin", state 835, "(1)"
 451         line 424, ".input.spin", state 848, "(1)"
 452         line 249, ".input.spin", state 903, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 453         line 253, ".input.spin", state 912, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 454         line 257, ".input.spin", state 927, "(1)"
 455         line 261, ".input.spin", state 934, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 456         line 226, ".input.spin", state 950, "(1)"
 457         line 230, ".input.spin", state 958, "(1)"
 458         line 234, ".input.spin", state 970, "(1)"
 459         line 238, ".input.spin", state 978, "(1)"
 460         line 249, ".input.spin", state 1009, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 461         line 253, ".input.spin", state 1018, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 462         line 257, ".input.spin", state 1031, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 463         line 261, ".input.spin", state 1040, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 464         line 226, ".input.spin", state 1056, "(1)"
 465         line 230, ".input.spin", state 1064, "(1)"
 466         line 234, ".input.spin", state 1076, "(1)"
 467         line 238, ".input.spin", state 1084, "(1)"
 468         line 253, ".input.spin", state 1110, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 469         line 257, ".input.spin", state 1123, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 470         line 261, ".input.spin", state 1132, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 471         line 226, ".input.spin", state 1148, "(1)"
 472         line 230, ".input.spin", state 1156, "(1)"
 473         line 234, ".input.spin", state 1168, "(1)"
 474         line 238, ".input.spin", state 1176, "(1)"
 475         line 249, ".input.spin", state 1207, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 476         line 253, ".input.spin", state 1216, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 477         line 257, ".input.spin", state 1229, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 478         line 261, ".input.spin", state 1238, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 479         line 226, ".input.spin", state 1254, "(1)"
 480         line 230, ".input.spin", state 1262, "(1)"
 481         line 234, ".input.spin", state 1274, "(1)"
 482         line 238, ".input.spin", state 1282, "(1)"
 483         line 253, ".input.spin", state 1308, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 484         line 257, ".input.spin", state 1321, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 485         line 261, ".input.spin", state 1330, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 486         line 226, ".input.spin", state 1346, "(1)"
 487         line 230, ".input.spin", state 1354, "(1)"
 488         line 234, ".input.spin", state 1366, "(1)"
 489         line 238, ".input.spin", state 1374, "(1)"
 490         line 249, ".input.spin", state 1405, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 491         line 253, ".input.spin", state 1414, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 492         line 257, ".input.spin", state 1427, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 493         line 261, ".input.spin", state 1436, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 494         line 226, ".input.spin", state 1452, "(1)"
 495         line 230, ".input.spin", state 1460, "(1)"
 496         line 234, ".input.spin", state 1472, "(1)"
 497         line 238, ".input.spin", state 1480, "(1)"
 498         line 253, ".input.spin", state 1506, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 499         line 257, ".input.spin", state 1519, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 500         line 261, ".input.spin", state 1528, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 501         line 226, ".input.spin", state 1544, "(1)"
 502         line 230, ".input.spin", state 1552, "(1)"
 503         line 234, ".input.spin", state 1564, "(1)"
 504         line 238, ".input.spin", state 1572, "(1)"
 505         line 249, ".input.spin", state 1603, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 506         line 253, ".input.spin", state 1612, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 507         line 257, ".input.spin", state 1625, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 508         line 261, ".input.spin", state 1634, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 509         line 226, ".input.spin", state 1650, "(1)"
 510         line 230, ".input.spin", state 1658, "(1)"
 511         line 234, ".input.spin", state 1670, "(1)"
 512         line 238, ".input.spin", state 1678, "(1)"
 513         line 1203, ".input.spin", state 1694, "-end-"
 514         (103 of 1694 states)
 515 unreached in proctype :init:
 516         (0 of 78 states)
 517
 518 pan: elapsed time 4.43e+03 seconds
 519 pan: rate 3486.0658 states/second
 520 pan: avg transition delay 1.038e-06 usec
 521 cp .input.spin asserts.spin.input
 522 cp .input.spin.trail asserts.spin.input.trail