formal-model/urcu-controldataflow-alpha-ipi-progress-minimal/urcu_free_single_flip.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_single_flip.define .input.define
   8 cat .input.define > .input.spin
   9 cat DEFINES >> .input.spin
  10 cat urcu.spin >> .input.spin
  11 rm -f .input.spin.trail
  12 spin -a -X -N pan.ltl .input.spin
  13 Exit-Status 0
  14 gcc -O2 -w -DHASH64 -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 Depth=    4014 States=    1e+06 Transitions= 1.62e+08 Memory=   512.736 t=    256 R=   4e+03
  20 pan: claim violated! (at depth 1235)
  21 pan: wrote .input.spin.trail
  22
  23 (Spin Version 5.1.7 -- 23 December 2008)
  24 Warning: Search not completed
  25         + Partial Order Reduction
  26         + Compression
  27
  28 Full statespace search for:
  29         never claim             +
  30         assertion violations    + (if within scope of claim)
  31         acceptance   cycles     + (fairness disabled)
  32         invalid end states      - (disabled by never claim)
  33
  34 State-vector 80 byte, depth reached 4014, errors: 1
  35   1411681 states, stored
  36 2.3165948e+08 states, matched
  37 2.3307116e+08 transitions (= stored+matched)
  38 1.3076596e+09 atomic steps
  39 hash conflicts:  78416855 (resolved)
  40
  41 Stats on memory usage (in Megabytes):
  42   156.169       equivalent memory usage for states (stored*(State-vector + overhead))
  43    66.078       actual memory usage for states (compression: 42.31%)
  44                 state-vector as stored = 13 byte + 36 byte overhead
  45     8.000       memory used for hash table (-w20)
  46   457.764       memory used for DFS stack (-m10000000)
  47   531.779       total actual memory usage
  48
  49 nr of templates: [ globals chans procs ]
  50 collapse counts: [ 14645 1835 1567 2 2 ]
  51 unreached in proctype urcu_reader
  52         line 713, "pan.___", state 12, "((i<1))"
  53         line 713, "pan.___", state 12, "((i>=1))"
  54         line 268, "pan.___", state 55, "cache_dirty_urcu_gp_ctr = 0"
  55         line 276, "pan.___", state 77, "cache_dirty_rcu_ptr = 0"
  56         line 280, "pan.___", state 86, "cache_dirty_rcu_data[i] = 0"
  57         line 245, "pan.___", state 102, "(1)"
  58         line 249, "pan.___", state 110, "(1)"
  59         line 253, "pan.___", state 122, "(1)"
  60         line 257, "pan.___", state 130, "(1)"
  61         line 404, "pan.___", state 156, "cache_dirty_urcu_gp_ctr = 0"
  62         line 413, "pan.___", state 188, "cache_dirty_rcu_ptr = 0"
  63         line 417, "pan.___", state 202, "cache_dirty_rcu_data[i] = 0"
  64         line 422, "pan.___", state 221, "(1)"
  65         line 431, "pan.___", state 251, "(1)"
  66         line 435, "pan.___", state 264, "(1)"
  67         line 614, "pan.___", state 285, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  68         line 404, "pan.___", state 292, "cache_dirty_urcu_gp_ctr = 0"
  69         line 413, "pan.___", state 324, "cache_dirty_rcu_ptr = 0"
  70         line 417, "pan.___", state 338, "cache_dirty_rcu_data[i] = 0"
  71         line 422, "pan.___", state 357, "(1)"
  72         line 431, "pan.___", state 387, "(1)"
  73         line 435, "pan.___", state 400, "(1)"
  74         line 404, "pan.___", state 421, "cache_dirty_urcu_gp_ctr = 0"
  75         line 413, "pan.___", state 453, "cache_dirty_rcu_ptr = 0"
  76         line 417, "pan.___", state 467, "cache_dirty_rcu_data[i] = 0"
  77         line 422, "pan.___", state 486, "(1)"
  78         line 431, "pan.___", state 516, "(1)"
  79         line 435, "pan.___", state 529, "(1)"
  80         line 404, "pan.___", state 552, "cache_dirty_urcu_gp_ctr = 0"
  81         line 404, "pan.___", state 554, "(1)"
  82         line 404, "pan.___", state 555, "(cache_dirty_urcu_gp_ctr)"
  83         line 404, "pan.___", state 555, "else"
  84         line 404, "pan.___", state 558, "(1)"
  85         line 408, "pan.___", state 566, "cache_dirty_urcu_active_readers = 0"
  86         line 408, "pan.___", state 568, "(1)"
  87         line 408, "pan.___", state 569, "(cache_dirty_urcu_active_readers)"
  88         line 408, "pan.___", state 569, "else"
  89         line 408, "pan.___", state 572, "(1)"
  90         line 408, "pan.___", state 573, "(1)"
  91         line 408, "pan.___", state 573, "(1)"
  92         line 406, "pan.___", state 578, "((i<1))"
  93         line 406, "pan.___", state 578, "((i>=1))"
  94         line 413, "pan.___", state 584, "cache_dirty_rcu_ptr = 0"
  95         line 413, "pan.___", state 586, "(1)"
  96         line 413, "pan.___", state 587, "(cache_dirty_rcu_ptr)"
  97         line 413, "pan.___", state 587, "else"
  98         line 413, "pan.___", state 590, "(1)"
  99         line 413, "pan.___", state 591, "(1)"
 100         line 413, "pan.___", state 591, "(1)"
 101         line 417, "pan.___", state 598, "cache_dirty_rcu_data[i] = 0"
 102         line 417, "pan.___", state 600, "(1)"
 103         line 417, "pan.___", state 601, "(cache_dirty_rcu_data[i])"
 104         line 417, "pan.___", state 601, "else"
 105         line 417, "pan.___", state 604, "(1)"
 106         line 417, "pan.___", state 605, "(1)"
 107         line 417, "pan.___", state 605, "(1)"
 108         line 415, "pan.___", state 610, "((i<2))"
 109         line 415, "pan.___", state 610, "((i>=2))"
 110         line 422, "pan.___", state 617, "(1)"
 111         line 422, "pan.___", state 618, "(!(cache_dirty_urcu_gp_ctr))"
 112         line 422, "pan.___", state 618, "else"
 113         line 422, "pan.___", state 621, "(1)"
 114         line 422, "pan.___", state 622, "(1)"
 115         line 422, "pan.___", state 622, "(1)"
 116         line 426, "pan.___", state 630, "(1)"
 117         line 426, "pan.___", state 631, "(!(cache_dirty_urcu_active_readers))"
 118         line 426, "pan.___", state 631, "else"
 119         line 426, "pan.___", state 634, "(1)"
 120         line 426, "pan.___", state 635, "(1)"
 121         line 426, "pan.___", state 635, "(1)"
 122         line 424, "pan.___", state 640, "((i<1))"
 123         line 424, "pan.___", state 640, "((i>=1))"
 124         line 431, "pan.___", state 647, "(1)"
 125         line 431, "pan.___", state 648, "(!(cache_dirty_rcu_ptr))"
 126         line 431, "pan.___", state 648, "else"
 127         line 431, "pan.___", state 651, "(1)"
 128         line 431, "pan.___", state 652, "(1)"
 129         line 431, "pan.___", state 652, "(1)"
 130         line 435, "pan.___", state 660, "(1)"
 131         line 435, "pan.___", state 661, "(!(cache_dirty_rcu_data[i]))"
 132         line 435, "pan.___", state 661, "else"
 133         line 435, "pan.___", state 664, "(1)"
 134         line 435, "pan.___", state 665, "(1)"
 135         line 435, "pan.___", state 665, "(1)"
 136         line 433, "pan.___", state 670, "((i<2))"
 137         line 433, "pan.___", state 670, "((i>=2))"
 138         line 443, "pan.___", state 674, "(1)"
 139         line 443, "pan.___", state 674, "(1)"
 140         line 614, "pan.___", state 677, "cached_urcu_active_readers = (tmp+1)"
 141         line 614, "pan.___", state 678, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 142         line 614, "pan.___", state 679, "(1)"
 143         line 404, "pan.___", state 686, "cache_dirty_urcu_gp_ctr = 0"
 144         line 413, "pan.___", state 718, "cache_dirty_rcu_ptr = 0"
 145         line 417, "pan.___", state 732, "cache_dirty_rcu_data[i] = 0"
 146         line 422, "pan.___", state 751, "(1)"
 147         line 431, "pan.___", state 781, "(1)"
 148         line 435, "pan.___", state 794, "(1)"
 149         line 404, "pan.___", state 821, "cache_dirty_urcu_gp_ctr = 0"
 150         line 413, "pan.___", state 853, "cache_dirty_rcu_ptr = 0"
 151         line 417, "pan.___", state 867, "cache_dirty_rcu_data[i] = 0"
 152         line 422, "pan.___", state 886, "(1)"
 153         line 431, "pan.___", state 916, "(1)"
 154         line 435, "pan.___", state 929, "(1)"
 155         line 404, "pan.___", state 950, "cache_dirty_urcu_gp_ctr = 0"
 156         line 413, "pan.___", state 982, "cache_dirty_rcu_ptr = 0"
 157         line 417, "pan.___", state 996, "cache_dirty_rcu_data[i] = 0"
 158         line 422, "pan.___", state 1015, "(1)"
 159         line 431, "pan.___", state 1045, "(1)"
 160         line 435, "pan.___", state 1058, "(1)"
 161         line 245, "pan.___", state 1091, "(1)"
 162         line 253, "pan.___", state 1111, "(1)"
 163         line 257, "pan.___", state 1119, "(1)"
 164         line 748, "pan.___", state 1136, "-end-"
 165         (92 of 1136 states)
 166 unreached in proctype urcu_writer
 167         line 837, "pan.___", state 12, "((i<1))"
 168         line 837, "pan.___", state 12, "((i>=1))"
 169         line 404, "pan.___", state 49, "cache_dirty_urcu_gp_ctr = 0"
 170         line 408, "pan.___", state 63, "cache_dirty_urcu_active_readers = 0"
 171         line 413, "pan.___", state 81, "cache_dirty_rcu_ptr = 0"
 172         line 422, "pan.___", state 114, "(1)"
 173         line 426, "pan.___", state 127, "(1)"
 174         line 431, "pan.___", state 144, "(1)"
 175         line 268, "pan.___", state 180, "cache_dirty_urcu_gp_ctr = 0"
 176         line 272, "pan.___", state 189, "cache_dirty_urcu_active_readers = 0"
 177         line 276, "pan.___", state 202, "cache_dirty_rcu_ptr = 0"
 178         line 404, "pan.___", state 242, "cache_dirty_urcu_gp_ctr = 0"
 179         line 408, "pan.___", state 256, "cache_dirty_urcu_active_readers = 0"
 180         line 413, "pan.___", state 274, "cache_dirty_rcu_ptr = 0"
 181         line 417, "pan.___", state 288, "cache_dirty_rcu_data[i] = 0"
 182         line 422, "pan.___", state 307, "(1)"
 183         line 426, "pan.___", state 320, "(1)"
 184         line 431, "pan.___", state 337, "(1)"
 185         line 435, "pan.___", state 350, "(1)"
 186         line 408, "pan.___", state 387, "cache_dirty_urcu_active_readers = 0"
 187         line 413, "pan.___", state 405, "cache_dirty_rcu_ptr = 0"
 188         line 417, "pan.___", state 419, "cache_dirty_rcu_data[i] = 0"
 189         line 426, "pan.___", state 451, "(1)"
 190         line 431, "pan.___", state 468, "(1)"
 191         line 435, "pan.___", state 481, "(1)"
 192         line 404, "pan.___", state 511, "cache_dirty_urcu_gp_ctr = 0"
 193         line 408, "pan.___", state 525, "cache_dirty_urcu_active_readers = 0"
 194         line 413, "pan.___", state 543, "cache_dirty_rcu_ptr = 0"
 195         line 417, "pan.___", state 557, "cache_dirty_rcu_data[i] = 0"
 196         line 422, "pan.___", state 576, "(1)"
 197         line 426, "pan.___", state 589, "(1)"
 198         line 431, "pan.___", state 606, "(1)"
 199         line 435, "pan.___", state 619, "(1)"
 200         line 404, "pan.___", state 640, "cache_dirty_urcu_gp_ctr = 0"
 201         line 404, "pan.___", state 642, "(1)"
 202         line 404, "pan.___", state 643, "(cache_dirty_urcu_gp_ctr)"
 203         line 404, "pan.___", state 643, "else"
 204         line 404, "pan.___", state 646, "(1)"
 205         line 408, "pan.___", state 654, "cache_dirty_urcu_active_readers = 0"
 206         line 408, "pan.___", state 656, "(1)"
 207         line 408, "pan.___", state 657, "(cache_dirty_urcu_active_readers)"
 208         line 408, "pan.___", state 657, "else"
 209         line 408, "pan.___", state 660, "(1)"
 210         line 408, "pan.___", state 661, "(1)"
 211         line 408, "pan.___", state 661, "(1)"
 212         line 406, "pan.___", state 666, "((i<1))"
 213         line 406, "pan.___", state 666, "((i>=1))"
 214         line 413, "pan.___", state 672, "cache_dirty_rcu_ptr = 0"
 215         line 413, "pan.___", state 674, "(1)"
 216         line 413, "pan.___", state 675, "(cache_dirty_rcu_ptr)"
 217         line 413, "pan.___", state 675, "else"
 218         line 413, "pan.___", state 678, "(1)"
 219         line 413, "pan.___", state 679, "(1)"
 220         line 413, "pan.___", state 679, "(1)"
 221         line 417, "pan.___", state 686, "cache_dirty_rcu_data[i] = 0"
 222         line 417, "pan.___", state 688, "(1)"
 223         line 417, "pan.___", state 689, "(cache_dirty_rcu_data[i])"
 224         line 417, "pan.___", state 689, "else"
 225         line 417, "pan.___", state 692, "(1)"
 226         line 417, "pan.___", state 693, "(1)"
 227         line 417, "pan.___", state 693, "(1)"
 228         line 415, "pan.___", state 698, "((i<2))"
 229         line 415, "pan.___", state 698, "((i>=2))"
 230         line 422, "pan.___", state 705, "(1)"
 231         line 422, "pan.___", state 706, "(!(cache_dirty_urcu_gp_ctr))"
 232         line 422, "pan.___", state 706, "else"
 233         line 422, "pan.___", state 709, "(1)"
 234         line 422, "pan.___", state 710, "(1)"
 235         line 422, "pan.___", state 710, "(1)"
 236         line 426, "pan.___", state 718, "(1)"
 237         line 426, "pan.___", state 719, "(!(cache_dirty_urcu_active_readers))"
 238         line 426, "pan.___", state 719, "else"
 239         line 426, "pan.___", state 722, "(1)"
 240         line 426, "pan.___", state 723, "(1)"
 241         line 426, "pan.___", state 723, "(1)"
 242         line 424, "pan.___", state 728, "((i<1))"
 243         line 424, "pan.___", state 728, "((i>=1))"
 244         line 431, "pan.___", state 735, "(1)"
 245         line 431, "pan.___", state 736, "(!(cache_dirty_rcu_ptr))"
 246         line 431, "pan.___", state 736, "else"
 247         line 431, "pan.___", state 739, "(1)"
 248         line 431, "pan.___", state 740, "(1)"
 249         line 431, "pan.___", state 740, "(1)"
 250         line 435, "pan.___", state 748, "(1)"
 251         line 435, "pan.___", state 749, "(!(cache_dirty_rcu_data[i]))"
 252         line 435, "pan.___", state 749, "else"
 253         line 435, "pan.___", state 752, "(1)"
 254         line 435, "pan.___", state 753, "(1)"
 255         line 435, "pan.___", state 753, "(1)"
 256         line 433, "pan.___", state 758, "((i<2))"
 257         line 433, "pan.___", state 758, "((i>=2))"
 258         line 443, "pan.___", state 762, "(1)"
 259         line 443, "pan.___", state 762, "(1)"
 260         line 1003, "pan.___", state 766, "_proc_urcu_writer = (_proc_urcu_writer|(1<<10))"
 261         line 404, "pan.___", state 771, "cache_dirty_urcu_gp_ctr = 0"
 262         line 404, "pan.___", state 773, "(1)"
 263         line 404, "pan.___", state 774, "(cache_dirty_urcu_gp_ctr)"
 264         line 404, "pan.___", state 774, "else"
 265         line 404, "pan.___", state 777, "(1)"
 266         line 408, "pan.___", state 785, "cache_dirty_urcu_active_readers = 0"
 267         line 408, "pan.___", state 787, "(1)"
 268         line 408, "pan.___", state 788, "(cache_dirty_urcu_active_readers)"
 269         line 408, "pan.___", state 788, "else"
 270         line 408, "pan.___", state 791, "(1)"
 271         line 408, "pan.___", state 792, "(1)"
 272         line 408, "pan.___", state 792, "(1)"
 273         line 406, "pan.___", state 797, "((i<1))"
 274         line 406, "pan.___", state 797, "((i>=1))"
 275         line 413, "pan.___", state 803, "cache_dirty_rcu_ptr = 0"
 276         line 413, "pan.___", state 805, "(1)"
 277         line 413, "pan.___", state 806, "(cache_dirty_rcu_ptr)"
 278         line 413, "pan.___", state 806, "else"
 279         line 413, "pan.___", state 809, "(1)"
 280         line 413, "pan.___", state 810, "(1)"
 281         line 413, "pan.___", state 810, "(1)"
 282         line 417, "pan.___", state 817, "cache_dirty_rcu_data[i] = 0"
 283         line 417, "pan.___", state 819, "(1)"
 284         line 417, "pan.___", state 820, "(cache_dirty_rcu_data[i])"
 285         line 417, "pan.___", state 820, "else"
 286         line 417, "pan.___", state 823, "(1)"
 287         line 417, "pan.___", state 824, "(1)"
 288         line 417, "pan.___", state 824, "(1)"
 289         line 415, "pan.___", state 829, "((i<2))"
 290         line 415, "pan.___", state 829, "((i>=2))"
 291         line 422, "pan.___", state 836, "(1)"
 292         line 422, "pan.___", state 837, "(!(cache_dirty_urcu_gp_ctr))"
 293         line 422, "pan.___", state 837, "else"
 294         line 422, "pan.___", state 840, "(1)"
 295         line 422, "pan.___", state 841, "(1)"
 296         line 422, "pan.___", state 841, "(1)"
 297         line 426, "pan.___", state 849, "(1)"
 298         line 426, "pan.___", state 850, "(!(cache_dirty_urcu_active_readers))"
 299         line 426, "pan.___", state 850, "else"
 300         line 426, "pan.___", state 853, "(1)"
 301         line 426, "pan.___", state 854, "(1)"
 302         line 426, "pan.___", state 854, "(1)"
 303         line 424, "pan.___", state 859, "((i<1))"
 304         line 424, "pan.___", state 859, "((i>=1))"
 305         line 431, "pan.___", state 866, "(1)"
 306         line 431, "pan.___", state 867, "(!(cache_dirty_rcu_ptr))"
 307         line 431, "pan.___", state 867, "else"
 308         line 431, "pan.___", state 870, "(1)"
 309         line 431, "pan.___", state 871, "(1)"
 310         line 431, "pan.___", state 871, "(1)"
 311         line 435, "pan.___", state 879, "(1)"
 312         line 435, "pan.___", state 880, "(!(cache_dirty_rcu_data[i]))"
 313         line 435, "pan.___", state 880, "else"
 314         line 435, "pan.___", state 883, "(1)"
 315         line 435, "pan.___", state 884, "(1)"
 316         line 435, "pan.___", state 884, "(1)"
 317         line 433, "pan.___", state 889, "((i<2))"
 318         line 433, "pan.___", state 889, "((i>=2))"
 319         line 443, "pan.___", state 893, "(1)"
 320         line 443, "pan.___", state 893, "(1)"
 321         line 1019, "pan.___", state 898, "_proc_urcu_writer = (_proc_urcu_writer|(1<<11))"
 322         line 1014, "pan.___", state 899, "(((tmp2&((1<<7)-1))&&((tmp2^0)&(1<<7))))"
 323         line 1014, "pan.___", state 899, "else"
 324         line 1039, "pan.___", state 903, "_proc_urcu_writer = (_proc_urcu_writer&~(((1<<12)|(1<<11))))"
 325         line 268, "pan.___", state 934, "cache_dirty_urcu_gp_ctr = 0"
 326         line 272, "pan.___", state 943, "cache_dirty_urcu_active_readers = 0"
 327         line 276, "pan.___", state 958, "(1)"
 328         line 280, "pan.___", state 965, "cache_dirty_rcu_data[i] = 0"
 329         line 245, "pan.___", state 981, "(1)"
 330         line 249, "pan.___", state 989, "(1)"
 331         line 253, "pan.___", state 1001, "(1)"
 332         line 257, "pan.___", state 1009, "(1)"
 333         line 268, "pan.___", state 1040, "cache_dirty_urcu_gp_ctr = 0"
 334         line 272, "pan.___", state 1049, "cache_dirty_urcu_active_readers = 0"
 335         line 276, "pan.___", state 1062, "cache_dirty_rcu_ptr = 0"
 336         line 280, "pan.___", state 1071, "cache_dirty_rcu_data[i] = 0"
 337         line 245, "pan.___", state 1087, "(1)"
 338         line 249, "pan.___", state 1095, "(1)"
 339         line 253, "pan.___", state 1107, "(1)"
 340         line 257, "pan.___", state 1115, "(1)"
 341         line 272, "pan.___", state 1141, "cache_dirty_urcu_active_readers = 0"
 342         line 276, "pan.___", state 1154, "cache_dirty_rcu_ptr = 0"
 343         line 280, "pan.___", state 1163, "cache_dirty_rcu_data[i] = 0"
 344         line 245, "pan.___", state 1179, "(1)"
 345         line 249, "pan.___", state 1187, "(1)"
 346         line 253, "pan.___", state 1199, "(1)"
 347         line 257, "pan.___", state 1207, "(1)"
 348         line 268, "pan.___", state 1238, "cache_dirty_urcu_gp_ctr = 0"
 349         line 272, "pan.___", state 1247, "cache_dirty_urcu_active_readers = 0"
 350         line 276, "pan.___", state 1260, "cache_dirty_rcu_ptr = 0"
 351         line 280, "pan.___", state 1269, "cache_dirty_rcu_data[i] = 0"
 352         line 245, "pan.___", state 1285, "(1)"
 353         line 249, "pan.___", state 1293, "(1)"
 354         line 253, "pan.___", state 1305, "(1)"
 355         line 257, "pan.___", state 1313, "(1)"
 356         line 268, "pan.___", state 1330, "cache_dirty_urcu_gp_ctr = 0"
 357         line 268, "pan.___", state 1332, "(1)"
 358         line 272, "pan.___", state 1339, "cache_dirty_urcu_active_readers = 0"
 359         line 272, "pan.___", state 1341, "(1)"
 360         line 272, "pan.___", state 1342, "(cache_dirty_urcu_active_readers)"
 361         line 272, "pan.___", state 1342, "else"
 362         line 270, "pan.___", state 1347, "((i<1))"
 363         line 270, "pan.___", state 1347, "((i>=1))"
 364         line 276, "pan.___", state 1352, "cache_dirty_rcu_ptr = 0"
 365         line 276, "pan.___", state 1354, "(1)"
 366         line 276, "pan.___", state 1355, "(cache_dirty_rcu_ptr)"
 367         line 276, "pan.___", state 1355, "else"
 368         line 280, "pan.___", state 1361, "cache_dirty_rcu_data[i] = 0"
 369         line 280, "pan.___", state 1363, "(1)"
 370         line 280, "pan.___", state 1364, "(cache_dirty_rcu_data[i])"
 371         line 280, "pan.___", state 1364, "else"
 372         line 278, "pan.___", state 1369, "((i<2))"
 373         line 278, "pan.___", state 1369, "((i>=2))"
 374         line 245, "pan.___", state 1377, "(1)"
 375         line 249, "pan.___", state 1385, "(1)"
 376         line 249, "pan.___", state 1386, "(!(cache_dirty_urcu_active_readers))"
 377         line 249, "pan.___", state 1386, "else"
 378         line 247, "pan.___", state 1391, "((i<1))"
 379         line 247, "pan.___", state 1391, "((i>=1))"
 380         line 253, "pan.___", state 1397, "(1)"
 381         line 253, "pan.___", state 1398, "(!(cache_dirty_rcu_ptr))"
 382         line 253, "pan.___", state 1398, "else"
 383         line 257, "pan.___", state 1405, "(1)"
 384         line 257, "pan.___", state 1406, "(!(cache_dirty_rcu_data[i]))"
 385         line 257, "pan.___", state 1406, "else"
 386         line 262, "pan.___", state 1415, "(!(cache_dirty_urcu_gp_ctr))"
 387         line 262, "pan.___", state 1415, "else"
 388         line 1115, "pan.___", state 1418, "i = 0"
 389         line 1115, "pan.___", state 1420, "reader_barrier = 1"
 390         line 1115, "pan.___", state 1431, "((i<1))"
 391         line 1115, "pan.___", state 1431, "((i>=1))"
 392         line 268, "pan.___", state 1436, "cache_dirty_urcu_gp_ctr = 0"
 393         line 268, "pan.___", state 1438, "(1)"
 394         line 272, "pan.___", state 1445, "cache_dirty_urcu_active_readers = 0"
 395         line 272, "pan.___", state 1447, "(1)"
 396         line 272, "pan.___", state 1448, "(cache_dirty_urcu_active_readers)"
 397         line 272, "pan.___", state 1448, "else"
 398         line 270, "pan.___", state 1453, "((i<1))"
 399         line 270, "pan.___", state 1453, "((i>=1))"
 400         line 276, "pan.___", state 1458, "cache_dirty_rcu_ptr = 0"
 401         line 276, "pan.___", state 1460, "(1)"
 402         line 276, "pan.___", state 1461, "(cache_dirty_rcu_ptr)"
 403         line 276, "pan.___", state 1461, "else"
 404         line 280, "pan.___", state 1467, "cache_dirty_rcu_data[i] = 0"
 405         line 280, "pan.___", state 1469, "(1)"
 406         line 280, "pan.___", state 1470, "(cache_dirty_rcu_data[i])"
 407         line 280, "pan.___", state 1470, "else"
 408         line 278, "pan.___", state 1475, "((i<2))"
 409         line 278, "pan.___", state 1475, "((i>=2))"
 410         line 245, "pan.___", state 1483, "(1)"
 411         line 249, "pan.___", state 1491, "(1)"
 412         line 249, "pan.___", state 1492, "(!(cache_dirty_urcu_active_readers))"
 413         line 249, "pan.___", state 1492, "else"
 414         line 247, "pan.___", state 1497, "((i<1))"
 415         line 247, "pan.___", state 1497, "((i>=1))"
 416         line 253, "pan.___", state 1503, "(1)"
 417         line 253, "pan.___", state 1504, "(!(cache_dirty_rcu_ptr))"
 418         line 253, "pan.___", state 1504, "else"
 419         line 257, "pan.___", state 1511, "(1)"
 420         line 257, "pan.___", state 1512, "(!(cache_dirty_rcu_data[i]))"
 421         line 257, "pan.___", state 1512, "else"
 422         line 262, "pan.___", state 1521, "(!(cache_dirty_urcu_gp_ctr))"
 423         line 262, "pan.___", state 1521, "else"
 424         line 295, "pan.___", state 1523, "(cache_dirty_urcu_gp_ctr)"
 425         line 295, "pan.___", state 1523, "else"
 426         line 1115, "pan.___", state 1524, "(cache_dirty_urcu_gp_ctr)"
 427         line 1115, "pan.___", state 1524, "else"
 428         line 272, "pan.___", state 1537, "cache_dirty_urcu_active_readers = 0"
 429         line 276, "pan.___", state 1550, "cache_dirty_rcu_ptr = 0"
 430         line 280, "pan.___", state 1559, "cache_dirty_rcu_data[i] = 0"
 431         line 245, "pan.___", state 1575, "(1)"
 432         line 249, "pan.___", state 1583, "(1)"
 433         line 253, "pan.___", state 1595, "(1)"
 434         line 257, "pan.___", state 1603, "(1)"
 435         line 268, "pan.___", state 1634, "cache_dirty_urcu_gp_ctr = 0"
 436         line 272, "pan.___", state 1643, "cache_dirty_urcu_active_readers = 0"
 437         line 276, "pan.___", state 1656, "cache_dirty_rcu_ptr = 0"
 438         line 280, "pan.___", state 1665, "cache_dirty_rcu_data[i] = 0"
 439         line 245, "pan.___", state 1681, "(1)"
 440         line 249, "pan.___", state 1689, "(1)"
 441         line 253, "pan.___", state 1701, "(1)"
 442         line 257, "pan.___", state 1709, "(1)"
 443         line 1123, "pan.___", state 1725, "-end-"
 444         (212 of 1725 states)
 445 unreached in proctype :init:
 446         line 1138, "pan.___", state 11, "((i<1))"
 447         line 1138, "pan.___", state 11, "((i>=1))"
 448         (1 of 26 states)
 449 unreached in proctype :never:
 450         line 1184, "pan.___", state 8, "-end-"
 451         (1 of 8 states)
 452
 453 pan: elapsed time 372 seconds
 454 pan: rate 3796.6785 states/second
 455 pan: avg transition delay 1.5953e-06 usec
 456 cp .input.spin urcu_free_single_flip.spin.input
 457 cp .input.spin.trail urcu_free_single_flip.spin.input.trail
 458 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-min-progress'