formal-model/results/urcu-controldataflow-no-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=    4311 States=    1e+06 Transitions= 4.65e+08 Memory=   542.717 t=    480 R=   2e+03
  10
  11 (Spin Version 5.1.7 -- 23 December 2008)
  12         + Partial Order Reduction
  13
  14 Full statespace search for:
  15         never claim             - (none specified)
  16         assertion violations    +
  17         cycle checks            - (disabled by -DSAFETY)
  18         invalid end states      +
  19
  20 State-vector 72 byte, depth reached 4311, errors: 0
  21   1884295 states, stored
  22 9.0500014e+08 states, matched
  23 9.0688444e+08 transitions (= stored+matched)
  24 5.3819272e+09 atomic steps
  25 hash conflicts: 4.4436974e+08 (resolved)
  26
  27 Stats on memory usage (in Megabytes):
  28   179.700       equivalent memory usage for states (stored*(State-vector + overhead))
  29   144.496       actual memory usage for states (compression: 80.41%)
  30                 state-vector as stored = 52 byte + 28 byte overhead
  31     8.000       memory used for hash table (-w20)
  32   457.764       memory used for DFS stack (-m10000000)
  33   610.197       total actual memory usage
  34
  35 unreached in proctype urcu_reader
  36         line 394, ".input.spin", state 17, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  37         line 403, ".input.spin", state 49, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  38         line 407, ".input.spin", state 63, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  39         line 411, ".input.spin", state 82, "(1)"
  40         line 420, ".input.spin", state 112, "(1)"
  41         line 424, ".input.spin", state 125, "(1)"
  42         line 575, ".input.spin", state 146, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  43         line 394, ".input.spin", state 153, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  44         line 403, ".input.spin", state 185, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  45         line 407, ".input.spin", state 199, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  46         line 411, ".input.spin", state 218, "(1)"
  47         line 420, ".input.spin", state 248, "(1)"
  48         line 424, ".input.spin", state 261, "(1)"
  49         line 394, ".input.spin", state 282, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  50         line 403, ".input.spin", state 314, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  51         line 407, ".input.spin", state 328, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  52         line 411, ".input.spin", state 347, "(1)"
  53         line 420, ".input.spin", state 377, "(1)"
  54         line 424, ".input.spin", state 390, "(1)"
  55         line 394, ".input.spin", state 413, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  56         line 394, ".input.spin", state 415, "(1)"
  57         line 394, ".input.spin", state 416, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
  58         line 394, ".input.spin", state 416, "else"
  59         line 394, ".input.spin", state 419, "(1)"
  60         line 398, ".input.spin", state 427, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  61         line 398, ".input.spin", state 429, "(1)"
  62         line 398, ".input.spin", state 430, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
  63         line 398, ".input.spin", state 430, "else"
  64         line 398, ".input.spin", state 433, "(1)"
  65         line 398, ".input.spin", state 434, "(1)"
  66         line 398, ".input.spin", state 434, "(1)"
  67         line 396, ".input.spin", state 439, "((i<1))"
  68         line 396, ".input.spin", state 439, "((i>=1))"
  69         line 403, ".input.spin", state 445, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  70         line 403, ".input.spin", state 447, "(1)"
  71         line 403, ".input.spin", state 448, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
  72         line 403, ".input.spin", state 448, "else"
  73         line 403, ".input.spin", state 451, "(1)"
  74         line 403, ".input.spin", state 452, "(1)"
  75         line 403, ".input.spin", state 452, "(1)"
  76         line 407, ".input.spin", state 459, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  77         line 407, ".input.spin", state 461, "(1)"
  78         line 407, ".input.spin", state 462, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
  79         line 407, ".input.spin", state 462, "else"
  80         line 407, ".input.spin", state 465, "(1)"
  81         line 407, ".input.spin", state 466, "(1)"
  82         line 407, ".input.spin", state 466, "(1)"
  83         line 405, ".input.spin", state 471, "((i<2))"
  84         line 405, ".input.spin", state 471, "((i>=2))"
  85         line 411, ".input.spin", state 478, "(1)"
  86         line 411, ".input.spin", state 479, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
  87         line 411, ".input.spin", state 479, "else"
  88         line 411, ".input.spin", state 482, "(1)"
  89         line 411, ".input.spin", state 483, "(1)"
  90         line 411, ".input.spin", state 483, "(1)"
  91         line 415, ".input.spin", state 491, "(1)"
  92         line 415, ".input.spin", state 492, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
  93         line 415, ".input.spin", state 492, "else"
  94         line 415, ".input.spin", state 495, "(1)"
  95         line 415, ".input.spin", state 496, "(1)"
  96         line 415, ".input.spin", state 496, "(1)"
  97         line 413, ".input.spin", state 501, "((i<1))"
  98         line 413, ".input.spin", state 501, "((i>=1))"
  99         line 420, ".input.spin", state 508, "(1)"
 100         line 420, ".input.spin", state 509, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 101         line 420, ".input.spin", state 509, "else"
 102         line 420, ".input.spin", state 512, "(1)"
 103         line 420, ".input.spin", state 513, "(1)"
 104         line 420, ".input.spin", state 513, "(1)"
 105         line 424, ".input.spin", state 521, "(1)"
 106         line 424, ".input.spin", state 522, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 107         line 424, ".input.spin", state 522, "else"
 108         line 424, ".input.spin", state 525, "(1)"
 109         line 424, ".input.spin", state 526, "(1)"
 110         line 424, ".input.spin", state 526, "(1)"
 111         line 422, ".input.spin", state 531, "((i<2))"
 112         line 422, ".input.spin", state 531, "((i>=2))"
 113         line 429, ".input.spin", state 535, "(1)"
 114         line 429, ".input.spin", state 535, "(1)"
 115         line 575, ".input.spin", state 538, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 116         line 575, ".input.spin", state 539, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 117         line 575, ".input.spin", state 540, "(1)"
 118         line 249, ".input.spin", state 544, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 119         line 253, ".input.spin", state 555, "(1)"
 120         line 257, ".input.spin", state 566, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 121         line 261, ".input.spin", state 575, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 122         line 226, ".input.spin", state 591, "(1)"
 123         line 230, ".input.spin", state 599, "(1)"
 124         line 234, ".input.spin", state 611, "(1)"
 125         line 238, ".input.spin", state 619, "(1)"
 126         line 394, ".input.spin", state 637, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 127         line 398, ".input.spin", state 651, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 128         line 403, ".input.spin", state 669, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 129         line 407, ".input.spin", state 683, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 130         line 411, ".input.spin", state 702, "(1)"
 131         line 415, ".input.spin", state 715, "(1)"
 132         line 420, ".input.spin", state 732, "(1)"
 133         line 424, ".input.spin", state 745, "(1)"
 134         line 394, ".input.spin", state 773, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 135         line 394, ".input.spin", state 775, "(1)"
 136         line 394, ".input.spin", state 776, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 137         line 394, ".input.spin", state 776, "else"
 138         line 394, ".input.spin", state 779, "(1)"
 139         line 398, ".input.spin", state 787, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 140         line 398, ".input.spin", state 789, "(1)"
 141         line 398, ".input.spin", state 790, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 142         line 398, ".input.spin", state 790, "else"
 143         line 398, ".input.spin", state 793, "(1)"
 144         line 398, ".input.spin", state 794, "(1)"
 145         line 398, ".input.spin", state 794, "(1)"
 146         line 396, ".input.spin", state 799, "((i<1))"
 147         line 396, ".input.spin", state 799, "((i>=1))"
 148         line 403, ".input.spin", state 805, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 149         line 403, ".input.spin", state 807, "(1)"
 150         line 403, ".input.spin", state 808, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 151         line 403, ".input.spin", state 808, "else"
 152         line 403, ".input.spin", state 811, "(1)"
 153         line 403, ".input.spin", state 812, "(1)"
 154         line 403, ".input.spin", state 812, "(1)"
 155         line 407, ".input.spin", state 819, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 156         line 407, ".input.spin", state 821, "(1)"
 157         line 407, ".input.spin", state 822, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 158         line 407, ".input.spin", state 822, "else"
 159         line 407, ".input.spin", state 825, "(1)"
 160         line 407, ".input.spin", state 826, "(1)"
 161         line 407, ".input.spin", state 826, "(1)"
 162         line 405, ".input.spin", state 831, "((i<2))"
 163         line 405, ".input.spin", state 831, "((i>=2))"
 164         line 411, ".input.spin", state 838, "(1)"
 165         line 411, ".input.spin", state 839, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 166         line 411, ".input.spin", state 839, "else"
 167         line 411, ".input.spin", state 842, "(1)"
 168         line 411, ".input.spin", state 843, "(1)"
 169         line 411, ".input.spin", state 843, "(1)"
 170         line 415, ".input.spin", state 851, "(1)"
 171         line 415, ".input.spin", state 852, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 172         line 415, ".input.spin", state 852, "else"
 173         line 415, ".input.spin", state 855, "(1)"
 174         line 415, ".input.spin", state 856, "(1)"
 175         line 415, ".input.spin", state 856, "(1)"
 176         line 413, ".input.spin", state 861, "((i<1))"
 177         line 413, ".input.spin", state 861, "((i>=1))"
 178         line 420, ".input.spin", state 868, "(1)"
 179         line 420, ".input.spin", state 869, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 180         line 420, ".input.spin", state 869, "else"
 181         line 420, ".input.spin", state 872, "(1)"
 182         line 420, ".input.spin", state 873, "(1)"
 183         line 420, ".input.spin", state 873, "(1)"
 184         line 424, ".input.spin", state 881, "(1)"
 185         line 424, ".input.spin", state 882, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 186         line 424, ".input.spin", state 882, "else"
 187         line 424, ".input.spin", state 885, "(1)"
 188         line 424, ".input.spin", state 886, "(1)"
 189         line 424, ".input.spin", state 886, "(1)"
 190         line 429, ".input.spin", state 895, "(1)"
 191         line 429, ".input.spin", state 895, "(1)"
 192         line 394, ".input.spin", state 902, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 193         line 394, ".input.spin", state 904, "(1)"
 194         line 394, ".input.spin", state 905, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 195         line 394, ".input.spin", state 905, "else"
 196         line 394, ".input.spin", state 908, "(1)"
 197         line 398, ".input.spin", state 916, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 198         line 398, ".input.spin", state 918, "(1)"
 199         line 398, ".input.spin", state 919, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 200         line 398, ".input.spin", state 919, "else"
 201         line 398, ".input.spin", state 922, "(1)"
 202         line 398, ".input.spin", state 923, "(1)"
 203         line 398, ".input.spin", state 923, "(1)"
 204         line 396, ".input.spin", state 928, "((i<1))"
 205         line 396, ".input.spin", state 928, "((i>=1))"
 206         line 403, ".input.spin", state 934, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 207         line 403, ".input.spin", state 936, "(1)"
 208         line 403, ".input.spin", state 937, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 209         line 403, ".input.spin", state 937, "else"
 210         line 403, ".input.spin", state 940, "(1)"
 211         line 403, ".input.spin", state 941, "(1)"
 212         line 403, ".input.spin", state 941, "(1)"
 213         line 407, ".input.spin", state 948, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 214         line 407, ".input.spin", state 950, "(1)"
 215         line 407, ".input.spin", state 951, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 216         line 407, ".input.spin", state 951, "else"
 217         line 407, ".input.spin", state 954, "(1)"
 218         line 407, ".input.spin", state 955, "(1)"
 219         line 407, ".input.spin", state 955, "(1)"
 220         line 405, ".input.spin", state 960, "((i<2))"
 221         line 405, ".input.spin", state 960, "((i>=2))"
 222         line 411, ".input.spin", state 967, "(1)"
 223         line 411, ".input.spin", state 968, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 224         line 411, ".input.spin", state 968, "else"
 225         line 411, ".input.spin", state 971, "(1)"
 226         line 411, ".input.spin", state 972, "(1)"
 227         line 411, ".input.spin", state 972, "(1)"
 228         line 415, ".input.spin", state 980, "(1)"
 229         line 415, ".input.spin", state 981, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 230         line 415, ".input.spin", state 981, "else"
 231         line 415, ".input.spin", state 984, "(1)"
 232         line 415, ".input.spin", state 985, "(1)"
 233         line 415, ".input.spin", state 985, "(1)"
 234         line 413, ".input.spin", state 990, "((i<1))"
 235         line 413, ".input.spin", state 990, "((i>=1))"
 236         line 420, ".input.spin", state 997, "(1)"
 237         line 420, ".input.spin", state 998, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 238         line 420, ".input.spin", state 998, "else"
 239         line 420, ".input.spin", state 1001, "(1)"
 240         line 420, ".input.spin", state 1002, "(1)"
 241         line 420, ".input.spin", state 1002, "(1)"
 242         line 424, ".input.spin", state 1010, "(1)"
 243         line 424, ".input.spin", state 1011, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 244         line 424, ".input.spin", state 1011, "else"
 245         line 424, ".input.spin", state 1014, "(1)"
 246         line 424, ".input.spin", state 1015, "(1)"
 247         line 424, ".input.spin", state 1015, "(1)"
 248         line 422, ".input.spin", state 1020, "((i<2))"
 249         line 422, ".input.spin", state 1020, "((i>=2))"
 250         line 429, ".input.spin", state 1024, "(1)"
 251         line 429, ".input.spin", state 1024, "(1)"
 252         line 583, ".input.spin", state 1028, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
 253         line 394, ".input.spin", state 1033, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 254         line 398, ".input.spin", state 1047, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 255         line 403, ".input.spin", state 1065, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 256         line 407, ".input.spin", state 1079, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 257         line 411, ".input.spin", state 1098, "(1)"
 258         line 415, ".input.spin", state 1111, "(1)"
 259         line 420, ".input.spin", state 1128, "(1)"
 260         line 424, ".input.spin", state 1141, "(1)"
 261         line 394, ".input.spin", state 1165, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 262         line 403, ".input.spin", state 1197, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 263         line 407, ".input.spin", state 1211, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 264         line 411, ".input.spin", state 1230, "(1)"
 265         line 420, ".input.spin", state 1260, "(1)"
 266         line 424, ".input.spin", state 1273, "(1)"
 267         line 394, ".input.spin", state 1298, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 268         line 403, ".input.spin", state 1330, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 269         line 407, ".input.spin", state 1344, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 270         line 411, ".input.spin", state 1363, "(1)"
 271         line 420, ".input.spin", state 1393, "(1)"
 272         line 424, ".input.spin", state 1406, "(1)"
 273         line 394, ".input.spin", state 1427, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 274         line 403, ".input.spin", state 1459, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 275         line 407, ".input.spin", state 1473, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 276         line 411, ".input.spin", state 1492, "(1)"
 277         line 420, ".input.spin", state 1522, "(1)"
 278         line 424, ".input.spin", state 1535, "(1)"
 279         line 249, ".input.spin", state 1558, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 280         line 257, ".input.spin", state 1580, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 281         line 261, ".input.spin", state 1589, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 282         line 226, ".input.spin", state 1605, "(1)"
 283         line 230, ".input.spin", state 1613, "(1)"
 284         line 234, ".input.spin", state 1625, "(1)"
 285         line 238, ".input.spin", state 1633, "(1)"
 286         line 394, ".input.spin", state 1651, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 287         line 398, ".input.spin", state 1665, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 288         line 403, ".input.spin", state 1683, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 289         line 407, ".input.spin", state 1697, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 290         line 411, ".input.spin", state 1716, "(1)"
 291         line 415, ".input.spin", state 1729, "(1)"
 292         line 420, ".input.spin", state 1746, "(1)"
 293         line 424, ".input.spin", state 1759, "(1)"
 294         line 394, ".input.spin", state 1780, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 295         line 398, ".input.spin", state 1794, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 296         line 403, ".input.spin", state 1812, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 297         line 407, ".input.spin", state 1826, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 298         line 411, ".input.spin", state 1845, "(1)"
 299         line 415, ".input.spin", state 1858, "(1)"
 300         line 420, ".input.spin", state 1875, "(1)"
 301         line 424, ".input.spin", state 1888, "(1)"
 302         line 394, ".input.spin", state 1912, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 303         line 398, ".input.spin", state 1928, "(1)"
 304         line 403, ".input.spin", state 1944, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 305         line 407, ".input.spin", state 1958, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 306         line 411, ".input.spin", state 1977, "(1)"
 307         line 420, ".input.spin", state 2007, "(1)"
 308         line 424, ".input.spin", state 2020, "(1)"
 309         line 622, ".input.spin", state 2041, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
 310         line 394, ".input.spin", state 2048, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 311         line 403, ".input.spin", state 2080, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 312         line 407, ".input.spin", state 2094, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 313         line 411, ".input.spin", state 2113, "(1)"
 314         line 420, ".input.spin", state 2143, "(1)"
 315         line 424, ".input.spin", state 2156, "(1)"
 316         line 394, ".input.spin", state 2177, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 317         line 403, ".input.spin", state 2209, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 318         line 407, ".input.spin", state 2223, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 319         line 411, ".input.spin", state 2242, "(1)"
 320         line 420, ".input.spin", state 2272, "(1)"
 321         line 424, ".input.spin", state 2285, "(1)"
 322         line 394, ".input.spin", state 2308, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 323         line 394, ".input.spin", state 2310, "(1)"
 324         line 394, ".input.spin", state 2311, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 325         line 394, ".input.spin", state 2311, "else"
 326         line 394, ".input.spin", state 2314, "(1)"
 327         line 398, ".input.spin", state 2322, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 328         line 398, ".input.spin", state 2324, "(1)"
 329         line 398, ".input.spin", state 2325, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 330         line 398, ".input.spin", state 2325, "else"
 331         line 398, ".input.spin", state 2328, "(1)"
 332         line 398, ".input.spin", state 2329, "(1)"
 333         line 398, ".input.spin", state 2329, "(1)"
 334         line 396, ".input.spin", state 2334, "((i<1))"
 335         line 396, ".input.spin", state 2334, "((i>=1))"
 336         line 403, ".input.spin", state 2340, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 337         line 403, ".input.spin", state 2342, "(1)"
 338         line 403, ".input.spin", state 2343, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 339         line 403, ".input.spin", state 2343, "else"
 340         line 403, ".input.spin", state 2346, "(1)"
 341         line 403, ".input.spin", state 2347, "(1)"
 342         line 403, ".input.spin", state 2347, "(1)"
 343         line 407, ".input.spin", state 2354, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 344         line 407, ".input.spin", state 2356, "(1)"
 345         line 407, ".input.spin", state 2357, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 346         line 407, ".input.spin", state 2357, "else"
 347         line 407, ".input.spin", state 2360, "(1)"
 348         line 407, ".input.spin", state 2361, "(1)"
 349         line 407, ".input.spin", state 2361, "(1)"
 350         line 405, ".input.spin", state 2366, "((i<2))"
 351         line 405, ".input.spin", state 2366, "((i>=2))"
 352         line 411, ".input.spin", state 2373, "(1)"
 353         line 411, ".input.spin", state 2374, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 354         line 411, ".input.spin", state 2374, "else"
 355         line 411, ".input.spin", state 2377, "(1)"
 356         line 411, ".input.spin", state 2378, "(1)"
 357         line 411, ".input.spin", state 2378, "(1)"
 358         line 415, ".input.spin", state 2386, "(1)"
 359         line 415, ".input.spin", state 2387, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 360         line 415, ".input.spin", state 2387, "else"
 361         line 415, ".input.spin", state 2390, "(1)"
 362         line 415, ".input.spin", state 2391, "(1)"
 363         line 415, ".input.spin", state 2391, "(1)"
 364         line 413, ".input.spin", state 2396, "((i<1))"
 365         line 413, ".input.spin", state 2396, "((i>=1))"
 366         line 420, ".input.spin", state 2403, "(1)"
 367         line 420, ".input.spin", state 2404, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 368         line 420, ".input.spin", state 2404, "else"
 369         line 420, ".input.spin", state 2407, "(1)"
 370         line 420, ".input.spin", state 2408, "(1)"
 371         line 420, ".input.spin", state 2408, "(1)"
 372         line 424, ".input.spin", state 2416, "(1)"
 373         line 424, ".input.spin", state 2417, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 374         line 424, ".input.spin", state 2417, "else"
 375         line 424, ".input.spin", state 2420, "(1)"
 376         line 424, ".input.spin", state 2421, "(1)"
 377         line 424, ".input.spin", state 2421, "(1)"
 378         line 422, ".input.spin", state 2426, "((i<2))"
 379         line 422, ".input.spin", state 2426, "((i>=2))"
 380         line 429, ".input.spin", state 2430, "(1)"
 381         line 429, ".input.spin", state 2430, "(1)"
 382         line 622, ".input.spin", state 2433, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 383         line 622, ".input.spin", state 2434, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
 384         line 622, ".input.spin", state 2435, "(1)"
 385         line 249, ".input.spin", state 2439, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 386         line 253, ".input.spin", state 2450, "(1)"
 387         line 257, ".input.spin", state 2461, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 388         line 261, ".input.spin", state 2470, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 389         line 226, ".input.spin", state 2486, "(1)"
 390         line 230, ".input.spin", state 2494, "(1)"
 391         line 234, ".input.spin", state 2506, "(1)"
 392         line 238, ".input.spin", state 2514, "(1)"
 393         line 394, ".input.spin", state 2532, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 394         line 398, ".input.spin", state 2546, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 395         line 403, ".input.spin", state 2564, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 396         line 407, ".input.spin", state 2578, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 397         line 411, ".input.spin", state 2597, "(1)"
 398         line 415, ".input.spin", state 2610, "(1)"
 399         line 420, ".input.spin", state 2627, "(1)"
 400         line 424, ".input.spin", state 2640, "(1)"
 401         line 249, ".input.spin", state 2664, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 402         line 253, ".input.spin", state 2673, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 403         line 257, ".input.spin", state 2686, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 404         line 261, ".input.spin", state 2695, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 405         line 226, ".input.spin", state 2711, "(1)"
 406         line 230, ".input.spin", state 2719, "(1)"
 407         line 234, ".input.spin", state 2731, "(1)"
 408         line 238, ".input.spin", state 2739, "(1)"
 409         line 394, ".input.spin", state 2757, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 410         line 398, ".input.spin", state 2771, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 411         line 403, ".input.spin", state 2789, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 412         line 407, ".input.spin", state 2803, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 413         line 411, ".input.spin", state 2822, "(1)"
 414         line 415, ".input.spin", state 2835, "(1)"
 415         line 420, ".input.spin", state 2852, "(1)"
 416         line 424, ".input.spin", state 2865, "(1)"
 417         line 394, ".input.spin", state 2886, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 418         line 398, ".input.spin", state 2900, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 419         line 403, ".input.spin", state 2918, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 420         line 407, ".input.spin", state 2932, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 421         line 411, ".input.spin", state 2951, "(1)"
 422         line 415, ".input.spin", state 2964, "(1)"
 423         line 420, ".input.spin", state 2981, "(1)"
 424         line 424, ".input.spin", state 2994, "(1)"
 425         line 226, ".input.spin", state 3027, "(1)"
 426         line 234, ".input.spin", state 3047, "(1)"
 427         line 238, ".input.spin", state 3055, "(1)"
 428         line 226, ".input.spin", state 3070, "(1)"
 429         line 230, ".input.spin", state 3078, "(1)"
 430         line 234, ".input.spin", state 3090, "(1)"
 431         line 238, ".input.spin", state 3098, "(1)"
 432         line 876, ".input.spin", state 3115, "-end-"
 433         (318 of 3115 states)
 434 unreached in proctype urcu_writer
 435         line 394, ".input.spin", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 436         line 398, ".input.spin", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 437         line 403, ".input.spin", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 438         line 411, ".input.spin", state 83, "(1)"
 439         line 415, ".input.spin", state 96, "(1)"
 440         line 420, ".input.spin", state 113, "(1)"
 441         line 249, ".input.spin", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 442         line 253, ".input.spin", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 443         line 257, ".input.spin", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 444         line 394, ".input.spin", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 445         line 398, ".input.spin", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 446         line 403, ".input.spin", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 447         line 407, ".input.spin", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 448         line 411, ".input.spin", state 276, "(1)"
 449         line 415, ".input.spin", state 289, "(1)"
 450         line 420, ".input.spin", state 306, "(1)"
 451         line 424, ".input.spin", state 319, "(1)"
 452         line 398, ".input.spin", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 453         line 403, ".input.spin", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 454         line 407, ".input.spin", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 455         line 415, ".input.spin", state 420, "(1)"
 456         line 420, ".input.spin", state 437, "(1)"
 457         line 424, ".input.spin", state 450, "(1)"
 458         line 398, ".input.spin", state 494, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 459         line 403, ".input.spin", state 512, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 460         line 407, ".input.spin", state 526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 461         line 415, ".input.spin", state 558, "(1)"
 462         line 420, ".input.spin", state 575, "(1)"
 463         line 424, ".input.spin", state 588, "(1)"
 464         line 398, ".input.spin", state 623, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 465         line 403, ".input.spin", state 641, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 466         line 407, ".input.spin", state 655, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 467         line 415, ".input.spin", state 687, "(1)"
 468         line 420, ".input.spin", state 704, "(1)"
 469         line 424, ".input.spin", state 717, "(1)"
 470         line 398, ".input.spin", state 754, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 471         line 403, ".input.spin", state 772, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 472         line 407, ".input.spin", state 786, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 473         line 415, ".input.spin", state 818, "(1)"
 474         line 420, ".input.spin", state 835, "(1)"
 475         line 424, ".input.spin", state 848, "(1)"
 476         line 249, ".input.spin", state 903, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 477         line 253, ".input.spin", state 912, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 478         line 257, ".input.spin", state 927, "(1)"
 479         line 261, ".input.spin", state 934, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 480         line 226, ".input.spin", state 950, "(1)"
 481         line 230, ".input.spin", state 958, "(1)"
 482         line 234, ".input.spin", state 970, "(1)"
 483         line 238, ".input.spin", state 978, "(1)"
 484         line 253, ".input.spin", state 1003, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 485         line 257, ".input.spin", state 1016, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 486         line 261, ".input.spin", state 1025, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 487         line 226, ".input.spin", state 1041, "(1)"
 488         line 230, ".input.spin", state 1049, "(1)"
 489         line 234, ".input.spin", state 1061, "(1)"
 490         line 238, ".input.spin", state 1069, "(1)"
 491         line 253, ".input.spin", state 1094, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 492         line 257, ".input.spin", state 1107, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 493         line 261, ".input.spin", state 1116, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 494         line 226, ".input.spin", state 1132, "(1)"
 495         line 230, ".input.spin", state 1140, "(1)"
 496         line 234, ".input.spin", state 1152, "(1)"
 497         line 238, ".input.spin", state 1160, "(1)"
 498         line 253, ".input.spin", state 1185, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 499         line 257, ".input.spin", state 1198, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 500         line 261, ".input.spin", state 1207, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 501         line 226, ".input.spin", state 1223, "(1)"
 502         line 230, ".input.spin", state 1231, "(1)"
 503         line 234, ".input.spin", state 1243, "(1)"
 504         line 238, ".input.spin", state 1251, "(1)"
 505         line 1203, ".input.spin", state 1266, "-end-"
 506         (71 of 1266 states)
 507 unreached in proctype :init:
 508         (0 of 78 states)
 509
 510 pan: elapsed time 944 seconds
 511 pan: rate 1995.0819 states/second
 512 pan: avg transition delay 1.0414e-06 usec
 513 cp .input.spin asserts.spin.input
 514 cp .input.spin.trail asserts.spin.input.trail