formal-model/urcu-controldataflow-alpha-ipi-progress-minimal/urcu_free_no_mb.log

   1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-min-progress'
   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_no_mb.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 -DCOLLAPSE -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 1179)
  19 pan: claim violated! (at depth 1246)
  20 pan: wrote .input.spin.trail
  21
  22 (Spin Version 5.1.7 -- 23 December 2008)
  23 Warning: Search not completed
  24         + Partial Order Reduction
  25         + Compression
  26
  27 Full statespace search for:
  28         never claim             +
  29         assertion violations    + (if within scope of claim)
  30         acceptance   cycles     + (fairness disabled)
  31         invalid end states      - (disabled by never claim)
  32
  33 State-vector 80 byte, depth reached 3190, errors: 1
  34    124498 states, stored
  35  15198533 states, matched
  36  15323031 transitions (= stored+matched)
  37  86866126 atomic steps
  38 hash conflicts:    473423 (resolved)
  39
  40 Stats on memory usage (in Megabytes):
  41    13.773       equivalent memory usage for states (stored*(State-vector + overhead))
  42     6.400       actual memory usage for states (compression: 46.47%)
  43                 state-vector as stored = 18 byte + 36 byte overhead
  44     8.000       memory used for hash table (-w20)
  45   457.764       memory used for DFS stack (-m10000000)
  46   472.111       total actual memory usage
  47
  48 nr of templates: [ globals chans procs ]
  49 collapse counts: [ 2572 1245 179 2 2 ]
  50 unreached in proctype urcu_reader
  51         line 713, "pan.___", state 12, "((i<1))"
  52         line 713, "pan.___", state 12, "((i>=1))"
  53         line 268, "pan.___", state 57, "cache_dirty_urcu_gp_ctr = 0"
  54         line 276, "pan.___", state 79, "cache_dirty_rcu_ptr = 0"
  55         line 280, "pan.___", state 88, "cache_dirty_rcu_data[i] = 0"
  56         line 245, "pan.___", state 104, "(1)"
  57         line 249, "pan.___", state 112, "(1)"
  58         line 253, "pan.___", state 124, "(1)"
  59         line 257, "pan.___", state 132, "(1)"
  60         line 404, "pan.___", state 158, "cache_dirty_urcu_gp_ctr = 0"
  61         line 413, "pan.___", state 190, "cache_dirty_rcu_ptr = 0"
  62         line 417, "pan.___", state 204, "cache_dirty_rcu_data[i] = 0"
  63         line 422, "pan.___", state 223, "(1)"
  64         line 431, "pan.___", state 253, "(1)"
  65         line 435, "pan.___", state 266, "(1)"
  66         line 614, "pan.___", state 287, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  67         line 404, "pan.___", state 294, "cache_dirty_urcu_gp_ctr = 0"
  68         line 413, "pan.___", state 326, "cache_dirty_rcu_ptr = 0"
  69         line 417, "pan.___", state 340, "cache_dirty_rcu_data[i] = 0"
  70         line 422, "pan.___", state 359, "(1)"
  71         line 431, "pan.___", state 389, "(1)"
  72         line 435, "pan.___", state 402, "(1)"
  73         line 404, "pan.___", state 423, "cache_dirty_urcu_gp_ctr = 0"
  74         line 413, "pan.___", state 455, "cache_dirty_rcu_ptr = 0"
  75         line 417, "pan.___", state 469, "cache_dirty_rcu_data[i] = 0"
  76         line 422, "pan.___", state 488, "(1)"
  77         line 431, "pan.___", state 518, "(1)"
  78         line 435, "pan.___", state 531, "(1)"
  79         line 404, "pan.___", state 554, "cache_dirty_urcu_gp_ctr = 0"
  80         line 404, "pan.___", state 556, "(1)"
  81         line 404, "pan.___", state 557, "(cache_dirty_urcu_gp_ctr)"
  82         line 404, "pan.___", state 557, "else"
  83         line 404, "pan.___", state 560, "(1)"
  84         line 408, "pan.___", state 568, "cache_dirty_urcu_active_readers = 0"
  85         line 408, "pan.___", state 570, "(1)"
  86         line 408, "pan.___", state 571, "(cache_dirty_urcu_active_readers)"
  87         line 408, "pan.___", state 571, "else"
  88         line 408, "pan.___", state 574, "(1)"
  89         line 408, "pan.___", state 575, "(1)"
  90         line 408, "pan.___", state 575, "(1)"
  91         line 406, "pan.___", state 580, "((i<1))"
  92         line 406, "pan.___", state 580, "((i>=1))"
  93         line 413, "pan.___", state 586, "cache_dirty_rcu_ptr = 0"
  94         line 413, "pan.___", state 588, "(1)"
  95         line 413, "pan.___", state 589, "(cache_dirty_rcu_ptr)"
  96         line 413, "pan.___", state 589, "else"
  97         line 413, "pan.___", state 592, "(1)"
  98         line 413, "pan.___", state 593, "(1)"
  99         line 413, "pan.___", state 593, "(1)"
 100         line 417, "pan.___", state 600, "cache_dirty_rcu_data[i] = 0"
 101         line 417, "pan.___", state 602, "(1)"
 102         line 417, "pan.___", state 603, "(cache_dirty_rcu_data[i])"
 103         line 417, "pan.___", state 603, "else"
 104         line 417, "pan.___", state 606, "(1)"
 105         line 417, "pan.___", state 607, "(1)"
 106         line 417, "pan.___", state 607, "(1)"
 107         line 415, "pan.___", state 612, "((i<2))"
 108         line 415, "pan.___", state 612, "((i>=2))"
 109         line 422, "pan.___", state 619, "(1)"
 110         line 422, "pan.___", state 620, "(!(cache_dirty_urcu_gp_ctr))"
 111         line 422, "pan.___", state 620, "else"
 112         line 422, "pan.___", state 623, "(1)"
 113         line 422, "pan.___", state 624, "(1)"
 114         line 422, "pan.___", state 624, "(1)"
 115         line 426, "pan.___", state 632, "(1)"
 116         line 426, "pan.___", state 633, "(!(cache_dirty_urcu_active_readers))"
 117         line 426, "pan.___", state 633, "else"
 118         line 426, "pan.___", state 636, "(1)"
 119         line 426, "pan.___", state 637, "(1)"
 120         line 426, "pan.___", state 637, "(1)"
 121         line 424, "pan.___", state 642, "((i<1))"
 122         line 424, "pan.___", state 642, "((i>=1))"
 123         line 431, "pan.___", state 649, "(1)"
 124         line 431, "pan.___", state 650, "(!(cache_dirty_rcu_ptr))"
 125         line 431, "pan.___", state 650, "else"
 126         line 431, "pan.___", state 653, "(1)"
 127         line 431, "pan.___", state 654, "(1)"
 128         line 431, "pan.___", state 654, "(1)"
 129         line 435, "pan.___", state 662, "(1)"
 130         line 435, "pan.___", state 663, "(!(cache_dirty_rcu_data[i]))"
 131         line 435, "pan.___", state 663, "else"
 132         line 435, "pan.___", state 666, "(1)"
 133         line 435, "pan.___", state 667, "(1)"
 134         line 435, "pan.___", state 667, "(1)"
 135         line 433, "pan.___", state 672, "((i<2))"
 136         line 433, "pan.___", state 672, "((i>=2))"
 137         line 443, "pan.___", state 676, "(1)"
 138         line 443, "pan.___", state 676, "(1)"
 139         line 614, "pan.___", state 679, "cached_urcu_active_readers = (tmp+1)"
 140         line 614, "pan.___", state 680, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 141         line 614, "pan.___", state 681, "(1)"
 142         line 404, "pan.___", state 688, "cache_dirty_urcu_gp_ctr = 0"
 143         line 413, "pan.___", state 720, "cache_dirty_rcu_ptr = 0"
 144         line 417, "pan.___", state 734, "cache_dirty_rcu_data[i] = 0"
 145         line 422, "pan.___", state 753, "(1)"
 146         line 431, "pan.___", state 783, "(1)"
 147         line 435, "pan.___", state 796, "(1)"
 148         line 404, "pan.___", state 823, "cache_dirty_urcu_gp_ctr = 0"
 149         line 413, "pan.___", state 855, "cache_dirty_rcu_ptr = 0"
 150         line 417, "pan.___", state 869, "cache_dirty_rcu_data[i] = 0"
 151         line 422, "pan.___", state 888, "(1)"
 152         line 431, "pan.___", state 918, "(1)"
 153         line 435, "pan.___", state 931, "(1)"
 154         line 404, "pan.___", state 952, "cache_dirty_urcu_gp_ctr = 0"
 155         line 413, "pan.___", state 984, "cache_dirty_rcu_ptr = 0"
 156         line 417, "pan.___", state 998, "cache_dirty_rcu_data[i] = 0"
 157         line 422, "pan.___", state 1017, "(1)"
 158         line 431, "pan.___", state 1047, "(1)"
 159         line 435, "pan.___", state 1060, "(1)"
 160         line 245, "pan.___", state 1093, "(1)"
 161         line 253, "pan.___", state 1113, "(1)"
 162         line 257, "pan.___", state 1121, "(1)"
 163         line 748, "pan.___", state 1138, "-end-"
 164         (92 of 1138 states)
 165 unreached in proctype urcu_writer
 166         line 837, "pan.___", state 12, "((i<1))"
 167         line 837, "pan.___", state 12, "((i>=1))"
 168         line 404, "pan.___", state 47, "cache_dirty_urcu_gp_ctr = 0"
 169         line 404, "pan.___", state 53, "(1)"
 170         line 408, "pan.___", state 61, "cache_dirty_urcu_active_readers = 0"
 171         line 408, "pan.___", state 67, "(1)"
 172         line 408, "pan.___", state 68, "(1)"
 173         line 408, "pan.___", state 68, "(1)"
 174         line 406, "pan.___", state 73, "((i<1))"
 175         line 406, "pan.___", state 73, "((i>=1))"
 176         line 413, "pan.___", state 79, "cache_dirty_rcu_ptr = 0"
 177         line 413, "pan.___", state 85, "(1)"
 178         line 413, "pan.___", state 86, "(1)"
 179         line 413, "pan.___", state 86, "(1)"
 180         line 417, "pan.___", state 99, "(1)"
 181         line 417, "pan.___", state 100, "(1)"
 182         line 417, "pan.___", state 100, "(1)"
 183         line 415, "pan.___", state 105, "((i<2))"
 184         line 415, "pan.___", state 105, "((i>=2))"
 185         line 422, "pan.___", state 112, "(1)"
 186         line 422, "pan.___", state 113, "(!(cache_dirty_urcu_gp_ctr))"
 187         line 422, "pan.___", state 113, "else"
 188         line 422, "pan.___", state 116, "(1)"
 189         line 422, "pan.___", state 117, "(1)"
 190         line 422, "pan.___", state 117, "(1)"
 191         line 426, "pan.___", state 125, "(1)"
 192         line 426, "pan.___", state 126, "(!(cache_dirty_urcu_active_readers))"
 193         line 426, "pan.___", state 126, "else"
 194         line 426, "pan.___", state 129, "(1)"
 195         line 426, "pan.___", state 130, "(1)"
 196         line 426, "pan.___", state 130, "(1)"
 197         line 424, "pan.___", state 135, "((i<1))"
 198         line 424, "pan.___", state 135, "((i>=1))"
 199         line 431, "pan.___", state 142, "(1)"
 200         line 431, "pan.___", state 143, "(!(cache_dirty_rcu_ptr))"
 201         line 431, "pan.___", state 143, "else"
 202         line 431, "pan.___", state 146, "(1)"
 203         line 431, "pan.___", state 147, "(1)"
 204         line 431, "pan.___", state 147, "(1)"
 205         line 435, "pan.___", state 155, "(1)"
 206         line 435, "pan.___", state 156, "(!(cache_dirty_rcu_data[i]))"
 207         line 435, "pan.___", state 156, "else"
 208         line 435, "pan.___", state 159, "(1)"
 209         line 435, "pan.___", state 160, "(1)"
 210         line 435, "pan.___", state 160, "(1)"
 211         line 433, "pan.___", state 165, "((i<2))"
 212         line 433, "pan.___", state 165, "((i>=2))"
 213         line 443, "pan.___", state 169, "(1)"
 214         line 443, "pan.___", state 169, "(1)"
 215         line 268, "pan.___", state 178, "cache_dirty_urcu_gp_ctr = 0"
 216         line 272, "pan.___", state 187, "cache_dirty_urcu_active_readers = 0"
 217         line 270, "pan.___", state 195, "((i<1))"
 218         line 270, "pan.___", state 195, "((i>=1))"
 219         line 276, "pan.___", state 200, "cache_dirty_rcu_ptr = 0"
 220         line 907, "pan.___", state 228, "old_data = cached_rcu_ptr"
 221         line 918, "pan.___", state 232, "_proc_urcu_writer = (_proc_urcu_writer|(1<<4))"
 222         line 404, "pan.___", state 240, "cache_dirty_urcu_gp_ctr = 0"
 223         line 404, "pan.___", state 246, "(1)"
 224         line 408, "pan.___", state 254, "cache_dirty_urcu_active_readers = 0"
 225         line 408, "pan.___", state 260, "(1)"
 226         line 408, "pan.___", state 261, "(1)"
 227         line 408, "pan.___", state 261, "(1)"
 228         line 406, "pan.___", state 266, "((i<1))"
 229         line 406, "pan.___", state 266, "((i>=1))"
 230         line 413, "pan.___", state 274, "(1)"
 231         line 413, "pan.___", state 275, "(cache_dirty_rcu_ptr)"
 232         line 413, "pan.___", state 275, "else"
 233         line 413, "pan.___", state 278, "(1)"
 234         line 413, "pan.___", state 279, "(1)"
 235         line 413, "pan.___", state 279, "(1)"
 236         line 417, "pan.___", state 286, "cache_dirty_rcu_data[i] = 0"
 237         line 417, "pan.___", state 292, "(1)"
 238         line 417, "pan.___", state 293, "(1)"
 239         line 417, "pan.___", state 293, "(1)"
 240         line 415, "pan.___", state 298, "((i<2))"
 241         line 415, "pan.___", state 298, "((i>=2))"
 242         line 422, "pan.___", state 305, "(1)"
 243         line 422, "pan.___", state 306, "(!(cache_dirty_urcu_gp_ctr))"
 244         line 422, "pan.___", state 306, "else"
 245         line 422, "pan.___", state 309, "(1)"
 246         line 422, "pan.___", state 310, "(1)"
 247         line 422, "pan.___", state 310, "(1)"
 248         line 426, "pan.___", state 318, "(1)"
 249         line 426, "pan.___", state 319, "(!(cache_dirty_urcu_active_readers))"
 250         line 426, "pan.___", state 319, "else"
 251         line 426, "pan.___", state 322, "(1)"
 252         line 426, "pan.___", state 323, "(1)"
 253         line 426, "pan.___", state 323, "(1)"
 254         line 424, "pan.___", state 328, "((i<1))"
 255         line 424, "pan.___", state 328, "((i>=1))"
 256         line 431, "pan.___", state 335, "(1)"
 257         line 431, "pan.___", state 336, "(!(cache_dirty_rcu_ptr))"
 258         line 431, "pan.___", state 336, "else"
 259         line 431, "pan.___", state 339, "(1)"
 260         line 431, "pan.___", state 340, "(1)"
 261         line 431, "pan.___", state 340, "(1)"
 262         line 435, "pan.___", state 348, "(1)"
 263         line 435, "pan.___", state 349, "(!(cache_dirty_rcu_data[i]))"
 264         line 435, "pan.___", state 349, "else"
 265         line 435, "pan.___", state 352, "(1)"
 266         line 435, "pan.___", state 353, "(1)"
 267         line 435, "pan.___", state 353, "(1)"
 268         line 433, "pan.___", state 358, "((i<2))"
 269         line 433, "pan.___", state 358, "((i>=2))"
 270         line 443, "pan.___", state 362, "(1)"
 271         line 443, "pan.___", state 362, "(1)"
 272         line 404, "pan.___", state 373, "(1)"
 273         line 404, "pan.___", state 374, "(cache_dirty_urcu_gp_ctr)"
 274         line 404, "pan.___", state 374, "else"
 275         line 404, "pan.___", state 377, "(1)"
 276         line 408, "pan.___", state 385, "cache_dirty_urcu_active_readers = 0"
 277         line 408, "pan.___", state 391, "(1)"
 278         line 408, "pan.___", state 392, "(1)"
 279         line 408, "pan.___", state 392, "(1)"
 280         line 406, "pan.___", state 397, "((i<1))"
 281         line 406, "pan.___", state 397, "((i>=1))"
 282         line 413, "pan.___", state 403, "cache_dirty_rcu_ptr = 0"
 283         line 413, "pan.___", state 409, "(1)"
 284         line 413, "pan.___", state 410, "(1)"
 285         line 413, "pan.___", state 410, "(1)"
 286         line 417, "pan.___", state 417, "cache_dirty_rcu_data[i] = 0"
 287         line 417, "pan.___", state 423, "(1)"
 288         line 417, "pan.___", state 424, "(1)"
 289         line 417, "pan.___", state 424, "(1)"
 290         line 415, "pan.___", state 429, "((i<2))"
 291         line 415, "pan.___", state 429, "((i>=2))"
 292         line 422, "pan.___", state 436, "(1)"
 293         line 422, "pan.___", state 437, "(!(cache_dirty_urcu_gp_ctr))"
 294         line 422, "pan.___", state 437, "else"
 295         line 422, "pan.___", state 440, "(1)"
 296         line 422, "pan.___", state 441, "(1)"
 297         line 422, "pan.___", state 441, "(1)"
 298         line 426, "pan.___", state 449, "(1)"
 299         line 426, "pan.___", state 450, "(!(cache_dirty_urcu_active_readers))"
 300         line 426, "pan.___", state 450, "else"
 301         line 426, "pan.___", state 453, "(1)"
 302         line 426, "pan.___", state 454, "(1)"
 303         line 426, "pan.___", state 454, "(1)"
 304         line 424, "pan.___", state 459, "((i<1))"
 305         line 424, "pan.___", state 459, "((i>=1))"
 306         line 431, "pan.___", state 466, "(1)"
 307         line 431, "pan.___", state 467, "(!(cache_dirty_rcu_ptr))"
 308         line 431, "pan.___", state 467, "else"
 309         line 431, "pan.___", state 470, "(1)"
 310         line 431, "pan.___", state 471, "(1)"
 311         line 431, "pan.___", state 471, "(1)"
 312         line 435, "pan.___", state 479, "(1)"
 313         line 435, "pan.___", state 480, "(!(cache_dirty_rcu_data[i]))"
 314         line 435, "pan.___", state 480, "else"
 315         line 435, "pan.___", state 483, "(1)"
 316         line 435, "pan.___", state 484, "(1)"
 317         line 435, "pan.___", state 484, "(1)"
 318         line 433, "pan.___", state 489, "((i<2))"
 319         line 433, "pan.___", state 489, "((i>=2))"
 320         line 443, "pan.___", state 493, "(1)"
 321         line 443, "pan.___", state 493, "(1)"
 322         line 972, "pan.___", state 504, "_proc_urcu_writer = (_proc_urcu_writer&~((1<<9)))"
 323         line 977, "pan.___", state 505, "_proc_urcu_writer = (_proc_urcu_writer&~(((1<<8)|(1<<7))))"
 324         line 404, "pan.___", state 510, "cache_dirty_urcu_gp_ctr = 0"
 325         line 404, "pan.___", state 516, "(1)"
 326         line 408, "pan.___", state 524, "cache_dirty_urcu_active_readers = 0"
 327         line 408, "pan.___", state 530, "(1)"
 328         line 408, "pan.___", state 531, "(1)"
 329         line 408, "pan.___", state 531, "(1)"
 330         line 406, "pan.___", state 536, "((i<1))"
 331         line 406, "pan.___", state 536, "((i>=1))"
 332         line 413, "pan.___", state 542, "cache_dirty_rcu_ptr = 0"
 333         line 413, "pan.___", state 548, "(1)"
 334         line 413, "pan.___", state 549, "(1)"
 335         line 413, "pan.___", state 549, "(1)"
 336         line 417, "pan.___", state 556, "cache_dirty_rcu_data[i] = 0"
 337         line 417, "pan.___", state 562, "(1)"
 338         line 417, "pan.___", state 563, "(1)"
 339         line 417, "pan.___", state 563, "(1)"
 340         line 415, "pan.___", state 568, "((i<2))"
 341         line 415, "pan.___", state 568, "((i>=2))"
 342         line 422, "pan.___", state 575, "(1)"
 343         line 422, "pan.___", state 576, "(!(cache_dirty_urcu_gp_ctr))"
 344         line 422, "pan.___", state 576, "else"
 345         line 422, "pan.___", state 579, "(1)"
 346         line 422, "pan.___", state 580, "(1)"
 347         line 422, "pan.___", state 580, "(1)"
 348         line 426, "pan.___", state 588, "(1)"
 349         line 426, "pan.___", state 589, "(!(cache_dirty_urcu_active_readers))"
 350         line 426, "pan.___", state 589, "else"
 351         line 426, "pan.___", state 592, "(1)"
 352         line 426, "pan.___", state 593, "(1)"
 353         line 426, "pan.___", state 593, "(1)"
 354         line 424, "pan.___", state 598, "((i<1))"
 355         line 424, "pan.___", state 598, "((i>=1))"
 356         line 431, "pan.___", state 605, "(1)"
 357         line 431, "pan.___", state 606, "(!(cache_dirty_rcu_ptr))"
 358         line 431, "pan.___", state 606, "else"
 359         line 431, "pan.___", state 609, "(1)"
 360         line 431, "pan.___", state 610, "(1)"
 361         line 431, "pan.___", state 610, "(1)"
 362         line 435, "pan.___", state 618, "(1)"
 363         line 435, "pan.___", state 619, "(!(cache_dirty_rcu_data[i]))"
 364         line 435, "pan.___", state 619, "else"
 365         line 435, "pan.___", state 622, "(1)"
 366         line 435, "pan.___", state 623, "(1)"
 367         line 435, "pan.___", state 623, "(1)"
 368         line 443, "pan.___", state 632, "(1)"
 369         line 443, "pan.___", state 632, "(1)"
 370         line 404, "pan.___", state 639, "cache_dirty_urcu_gp_ctr = 0"
 371         line 408, "pan.___", state 653, "cache_dirty_urcu_active_readers = 0"
 372         line 413, "pan.___", state 671, "cache_dirty_rcu_ptr = 0"
 373         line 422, "pan.___", state 704, "(1)"
 374         line 426, "pan.___", state 717, "(1)"
 375         line 431, "pan.___", state 734, "(1)"
 376         line 435, "pan.___", state 747, "(1)"
 377         line 408, "pan.___", state 784, "cache_dirty_urcu_active_readers = 0"
 378         line 413, "pan.___", state 802, "cache_dirty_rcu_ptr = 0"
 379         line 417, "pan.___", state 816, "cache_dirty_rcu_data[i] = 0"
 380         line 426, "pan.___", state 848, "(1)"
 381         line 431, "pan.___", state 865, "(1)"
 382         line 435, "pan.___", state 878, "(1)"
 383         line 1054, "pan.___", state 905, "_proc_urcu_writer = (_proc_urcu_writer|(1<<13))"
 384         line 268, "pan.___", state 933, "cache_dirty_urcu_gp_ctr = 0"
 385         line 268, "pan.___", state 935, "(1)"
 386         line 272, "pan.___", state 942, "cache_dirty_urcu_active_readers = 0"
 387         line 272, "pan.___", state 944, "(1)"
 388         line 272, "pan.___", state 945, "(cache_dirty_urcu_active_readers)"
 389         line 272, "pan.___", state 945, "else"
 390         line 270, "pan.___", state 950, "((i<1))"
 391         line 270, "pan.___", state 950, "((i>=1))"
 392         line 276, "pan.___", state 955, "cache_dirty_rcu_ptr = 0"
 393         line 276, "pan.___", state 957, "(1)"
 394         line 276, "pan.___", state 958, "(cache_dirty_rcu_ptr)"
 395         line 276, "pan.___", state 958, "else"
 396         line 280, "pan.___", state 964, "cache_dirty_rcu_data[i] = 0"
 397         line 280, "pan.___", state 966, "(1)"
 398         line 280, "pan.___", state 967, "(cache_dirty_rcu_data[i])"
 399         line 280, "pan.___", state 967, "else"
 400         line 278, "pan.___", state 972, "((i<2))"
 401         line 278, "pan.___", state 972, "((i>=2))"
 402         line 245, "pan.___", state 980, "(1)"
 403         line 249, "pan.___", state 988, "(1)"
 404         line 249, "pan.___", state 989, "(!(cache_dirty_urcu_active_readers))"
 405         line 249, "pan.___", state 989, "else"
 406         line 247, "pan.___", state 994, "((i<1))"
 407         line 247, "pan.___", state 994, "((i>=1))"
 408         line 253, "pan.___", state 1000, "(1)"
 409         line 253, "pan.___", state 1001, "(!(cache_dirty_rcu_ptr))"
 410         line 253, "pan.___", state 1001, "else"
 411         line 257, "pan.___", state 1008, "(1)"
 412         line 257, "pan.___", state 1009, "(!(cache_dirty_rcu_data[i]))"
 413         line 257, "pan.___", state 1009, "else"
 414         line 262, "pan.___", state 1018, "(!(cache_dirty_urcu_gp_ctr))"
 415         line 262, "pan.___", state 1018, "else"
 416         line 1108, "pan.___", state 1034, "((i<1))"
 417         line 1108, "pan.___", state 1034, "((i>=1))"
 418         line 268, "pan.___", state 1039, "cache_dirty_urcu_gp_ctr = 0"
 419         line 268, "pan.___", state 1041, "(1)"
 420         line 272, "pan.___", state 1048, "cache_dirty_urcu_active_readers = 0"
 421         line 272, "pan.___", state 1050, "(1)"
 422         line 272, "pan.___", state 1051, "(cache_dirty_urcu_active_readers)"
 423         line 272, "pan.___", state 1051, "else"
 424         line 270, "pan.___", state 1056, "((i<1))"
 425         line 270, "pan.___", state 1056, "((i>=1))"
 426         line 276, "pan.___", state 1061, "cache_dirty_rcu_ptr = 0"
 427         line 276, "pan.___", state 1063, "(1)"
 428         line 276, "pan.___", state 1064, "(cache_dirty_rcu_ptr)"
 429         line 276, "pan.___", state 1064, "else"
 430         line 280, "pan.___", state 1070, "cache_dirty_rcu_data[i] = 0"
 431         line 280, "pan.___", state 1072, "(1)"
 432         line 280, "pan.___", state 1073, "(cache_dirty_rcu_data[i])"
 433         line 280, "pan.___", state 1073, "else"
 434         line 278, "pan.___", state 1078, "((i<2))"
 435         line 278, "pan.___", state 1078, "((i>=2))"
 436         line 245, "pan.___", state 1086, "(1)"
 437         line 249, "pan.___", state 1094, "(1)"
 438         line 249, "pan.___", state 1095, "(!(cache_dirty_urcu_active_readers))"
 439         line 249, "pan.___", state 1095, "else"
 440         line 247, "pan.___", state 1100, "((i<1))"
 441         line 247, "pan.___", state 1100, "((i>=1))"
 442         line 253, "pan.___", state 1106, "(1)"
 443         line 253, "pan.___", state 1107, "(!(cache_dirty_rcu_ptr))"
 444         line 253, "pan.___", state 1107, "else"
 445         line 257, "pan.___", state 1114, "(1)"
 446         line 257, "pan.___", state 1115, "(!(cache_dirty_rcu_data[i]))"
 447         line 257, "pan.___", state 1115, "else"
 448         line 262, "pan.___", state 1124, "(!(cache_dirty_urcu_gp_ctr))"
 449         line 262, "pan.___", state 1124, "else"
 450         line 295, "pan.___", state 1126, "(cache_dirty_urcu_gp_ctr)"
 451         line 295, "pan.___", state 1126, "else"
 452         line 1108, "pan.___", state 1127, "(cache_dirty_urcu_gp_ctr)"
 453         line 1108, "pan.___", state 1127, "else"
 454         line 268, "pan.___", state 1131, "cache_dirty_urcu_gp_ctr = 0"
 455         line 268, "pan.___", state 1133, "(1)"
 456         line 272, "pan.___", state 1140, "cache_dirty_urcu_active_readers = 0"
 457         line 272, "pan.___", state 1142, "(1)"
 458         line 272, "pan.___", state 1143, "(cache_dirty_urcu_active_readers)"
 459         line 272, "pan.___", state 1143, "else"
 460         line 270, "pan.___", state 1148, "((i<1))"
 461         line 270, "pan.___", state 1148, "((i>=1))"
 462         line 276, "pan.___", state 1153, "cache_dirty_rcu_ptr = 0"
 463         line 276, "pan.___", state 1155, "(1)"
 464         line 276, "pan.___", state 1156, "(cache_dirty_rcu_ptr)"
 465         line 276, "pan.___", state 1156, "else"
 466         line 280, "pan.___", state 1162, "cache_dirty_rcu_data[i] = 0"
 467         line 280, "pan.___", state 1164, "(1)"
 468         line 280, "pan.___", state 1165, "(cache_dirty_rcu_data[i])"
 469         line 280, "pan.___", state 1165, "else"
 470         line 278, "pan.___", state 1170, "((i<2))"
 471         line 278, "pan.___", state 1170, "((i>=2))"
 472         line 245, "pan.___", state 1178, "(1)"
 473         line 249, "pan.___", state 1186, "(1)"
 474         line 249, "pan.___", state 1187, "(!(cache_dirty_urcu_active_readers))"
 475         line 249, "pan.___", state 1187, "else"
 476         line 247, "pan.___", state 1192, "((i<1))"
 477         line 247, "pan.___", state 1192, "((i>=1))"
 478         line 253, "pan.___", state 1198, "(1)"
 479         line 253, "pan.___", state 1199, "(!(cache_dirty_rcu_ptr))"
 480         line 253, "pan.___", state 1199, "else"
 481         line 257, "pan.___", state 1206, "(1)"
 482         line 257, "pan.___", state 1207, "(!(cache_dirty_rcu_data[i]))"
 483         line 257, "pan.___", state 1207, "else"
 484         line 262, "pan.___", state 1216, "(!(cache_dirty_urcu_gp_ctr))"
 485         line 262, "pan.___", state 1216, "else"
 486         line 1112, "pan.___", state 1219, "i = 0"
 487         line 1112, "pan.___", state 1221, "reader_barrier = 1"
 488         line 1112, "pan.___", state 1232, "((i<1))"
 489         line 1112, "pan.___", state 1232, "((i>=1))"
 490         line 268, "pan.___", state 1237, "cache_dirty_urcu_gp_ctr = 0"
 491         line 268, "pan.___", state 1239, "(1)"
 492         line 272, "pan.___", state 1246, "cache_dirty_urcu_active_readers = 0"
 493         line 272, "pan.___", state 1248, "(1)"
 494         line 272, "pan.___", state 1249, "(cache_dirty_urcu_active_readers)"
 495         line 272, "pan.___", state 1249, "else"
 496         line 270, "pan.___", state 1254, "((i<1))"
 497         line 270, "pan.___", state 1254, "((i>=1))"
 498         line 276, "pan.___", state 1259, "cache_dirty_rcu_ptr = 0"
 499         line 276, "pan.___", state 1261, "(1)"
 500         line 276, "pan.___", state 1262, "(cache_dirty_rcu_ptr)"
 501         line 276, "pan.___", state 1262, "else"
 502         line 280, "pan.___", state 1268, "cache_dirty_rcu_data[i] = 0"
 503         line 280, "pan.___", state 1270, "(1)"
 504         line 280, "pan.___", state 1271, "(cache_dirty_rcu_data[i])"
 505         line 280, "pan.___", state 1271, "else"
 506         line 278, "pan.___", state 1276, "((i<2))"
 507         line 278, "pan.___", state 1276, "((i>=2))"
 508         line 245, "pan.___", state 1284, "(1)"
 509         line 249, "pan.___", state 1292, "(1)"
 510         line 249, "pan.___", state 1293, "(!(cache_dirty_urcu_active_readers))"
 511         line 249, "pan.___", state 1293, "else"
 512         line 247, "pan.___", state 1298, "((i<1))"
 513         line 247, "pan.___", state 1298, "((i>=1))"
 514         line 253, "pan.___", state 1304, "(1)"
 515         line 253, "pan.___", state 1305, "(!(cache_dirty_rcu_ptr))"
 516         line 253, "pan.___", state 1305, "else"
 517         line 257, "pan.___", state 1312, "(1)"
 518         line 257, "pan.___", state 1313, "(!(cache_dirty_rcu_data[i]))"
 519         line 257, "pan.___", state 1313, "else"
 520         line 262, "pan.___", state 1322, "(!(cache_dirty_urcu_gp_ctr))"
 521         line 262, "pan.___", state 1322, "else"
 522         line 295, "pan.___", state 1324, "(cache_dirty_urcu_gp_ctr)"
 523         line 295, "pan.___", state 1324, "else"
 524         line 1112, "pan.___", state 1325, "(cache_dirty_urcu_gp_ctr)"
 525         line 1112, "pan.___", state 1325, "else"
 526         line 272, "pan.___", state 1338, "cache_dirty_urcu_active_readers = 0"
 527         line 276, "pan.___", state 1351, "cache_dirty_rcu_ptr = 0"
 528         line 280, "pan.___", state 1360, "cache_dirty_rcu_data[i] = 0"
 529         line 245, "pan.___", state 1376, "(1)"
 530         line 249, "pan.___", state 1384, "(1)"
 531         line 253, "pan.___", state 1396, "(1)"
 532         line 257, "pan.___", state 1404, "(1)"
 533         line 268, "pan.___", state 1435, "cache_dirty_urcu_gp_ctr = 0"
 534         line 272, "pan.___", state 1444, "cache_dirty_urcu_active_readers = 0"
 535         line 276, "pan.___", state 1457, "cache_dirty_rcu_ptr = 0"
 536         line 280, "pan.___", state 1466, "cache_dirty_rcu_data[i] = 0"
 537         line 245, "pan.___", state 1482, "(1)"
 538         line 249, "pan.___", state 1490, "(1)"
 539         line 253, "pan.___", state 1502, "(1)"
 540         line 257, "pan.___", state 1510, "(1)"
 541         line 268, "pan.___", state 1527, "cache_dirty_urcu_gp_ctr = 0"
 542         line 268, "pan.___", state 1529, "(1)"
 543         line 272, "pan.___", state 1536, "cache_dirty_urcu_active_readers = 0"
 544         line 272, "pan.___", state 1538, "(1)"
 545         line 272, "pan.___", state 1539, "(cache_dirty_urcu_active_readers)"
 546         line 272, "pan.___", state 1539, "else"
 547         line 270, "pan.___", state 1544, "((i<1))"
 548         line 270, "pan.___", state 1544, "((i>=1))"
 549         line 276, "pan.___", state 1549, "cache_dirty_rcu_ptr = 0"
 550         line 276, "pan.___", state 1551, "(1)"
 551         line 276, "pan.___", state 1552, "(cache_dirty_rcu_ptr)"
 552         line 276, "pan.___", state 1552, "else"
 553         line 280, "pan.___", state 1558, "cache_dirty_rcu_data[i] = 0"
 554         line 280, "pan.___", state 1560, "(1)"
 555         line 280, "pan.___", state 1561, "(cache_dirty_rcu_data[i])"
 556         line 280, "pan.___", state 1561, "else"
 557         line 278, "pan.___", state 1566, "((i<2))"
 558         line 278, "pan.___", state 1566, "((i>=2))"
 559         line 245, "pan.___", state 1574, "(1)"
 560         line 249, "pan.___", state 1582, "(1)"
 561         line 249, "pan.___", state 1583, "(!(cache_dirty_urcu_active_readers))"
 562         line 249, "pan.___", state 1583, "else"
 563         line 247, "pan.___", state 1588, "((i<1))"
 564         line 247, "pan.___", state 1588, "((i>=1))"
 565         line 253, "pan.___", state 1594, "(1)"
 566         line 253, "pan.___", state 1595, "(!(cache_dirty_rcu_ptr))"
 567         line 253, "pan.___", state 1595, "else"
 568         line 257, "pan.___", state 1602, "(1)"
 569         line 257, "pan.___", state 1603, "(!(cache_dirty_rcu_data[i]))"
 570         line 257, "pan.___", state 1603, "else"
 571         line 262, "pan.___", state 1612, "(!(cache_dirty_urcu_gp_ctr))"
 572         line 262, "pan.___", state 1612, "else"
 573         line 1119, "pan.___", state 1615, "i = 0"
 574         line 1119, "pan.___", state 1617, "reader_barrier = 1"
 575         line 1119, "pan.___", state 1628, "((i<1))"
 576         line 1119, "pan.___", state 1628, "((i>=1))"
 577         line 268, "pan.___", state 1633, "cache_dirty_urcu_gp_ctr = 0"
 578         line 268, "pan.___", state 1635, "(1)"
 579         line 272, "pan.___", state 1642, "cache_dirty_urcu_active_readers = 0"
 580         line 272, "pan.___", state 1644, "(1)"
 581         line 272, "pan.___", state 1645, "(cache_dirty_urcu_active_readers)"
 582         line 272, "pan.___", state 1645, "else"
 583         line 270, "pan.___", state 1650, "((i<1))"
 584         line 270, "pan.___", state 1650, "((i>=1))"
 585         line 276, "pan.___", state 1655, "cache_dirty_rcu_ptr = 0"
 586         line 276, "pan.___", state 1657, "(1)"
 587         line 276, "pan.___", state 1658, "(cache_dirty_rcu_ptr)"
 588         line 276, "pan.___", state 1658, "else"
 589         line 280, "pan.___", state 1664, "cache_dirty_rcu_data[i] = 0"
 590         line 280, "pan.___", state 1666, "(1)"
 591         line 280, "pan.___", state 1667, "(cache_dirty_rcu_data[i])"
 592         line 280, "pan.___", state 1667, "else"
 593         line 278, "pan.___", state 1672, "((i<2))"
 594         line 278, "pan.___", state 1672, "((i>=2))"
 595         line 245, "pan.___", state 1680, "(1)"
 596         line 249, "pan.___", state 1688, "(1)"
 597         line 249, "pan.___", state 1689, "(!(cache_dirty_urcu_active_readers))"
 598         line 249, "pan.___", state 1689, "else"
 599         line 247, "pan.___", state 1694, "((i<1))"
 600         line 247, "pan.___", state 1694, "((i>=1))"
 601         line 253, "pan.___", state 1700, "(1)"
 602         line 253, "pan.___", state 1701, "(!(cache_dirty_rcu_ptr))"
 603         line 253, "pan.___", state 1701, "else"
 604         line 257, "pan.___", state 1708, "(1)"
 605         line 257, "pan.___", state 1709, "(!(cache_dirty_rcu_data[i]))"
 606         line 257, "pan.___", state 1709, "else"
 607         line 262, "pan.___", state 1718, "(!(cache_dirty_urcu_gp_ctr))"
 608         line 262, "pan.___", state 1718, "else"
 609         line 295, "pan.___", state 1720, "(cache_dirty_urcu_gp_ctr)"
 610         line 295, "pan.___", state 1720, "else"
 611         line 1119, "pan.___", state 1721, "(cache_dirty_urcu_gp_ctr)"
 612         line 1119, "pan.___", state 1721, "else"
 613         line 1123, "pan.___", state 1724, "-end-"
 614         (312 of 1724 states)
 615 unreached in proctype :init:
 616         line 1138, "pan.___", state 11, "((i<1))"
 617         line 1138, "pan.___", state 11, "((i>=1))"
 618         (1 of 26 states)
 619 unreached in proctype :never:
 620         line 1184, "pan.___", state 8, "-end-"
 621         (1 of 8 states)
 622
 623 pan: elapsed time 23.7 seconds
 624 pan: rate 5259.7381 states/second
 625 pan: avg transition delay 1.5447e-06 usec
 626 cp .input.spin urcu_free_no_mb.spin.input
 627 cp .input.spin.trail urcu_free_no_mb.spin.input.trail
 628 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-min-progress'