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

   1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-alpha-ipi'
   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 1362)
  19 Depth=    9193 States=    1e+06 Transitions= 2.02e+08 Memory=   513.615 t=    308 R=   3e+03
  20 Depth=    9193 States=    2e+06 Transitions= 4.02e+08 Memory=   560.100 t=    617 R=   3e+03
  21 pan: claim violated! (at depth 1482)
  22 pan: wrote .input.spin.trail
  23
  24 (Spin Version 5.1.7 -- 23 December 2008)
  25 Warning: Search not completed
  26         + Partial Order Reduction
  27         + Compression
  28
  29 Full statespace search for:
  30         never claim             +
  31         assertion violations    + (if within scope of claim)
  32         acceptance   cycles     + (fairness disabled)
  33         invalid end states      - (disabled by never claim)
  34
  35 State-vector 80 byte, depth reached 9193, errors: 1
  36   2638623 states, stored
  37 5.0906949e+08 states, matched
  38 5.1170812e+08 transitions (= stored+matched)
  39 2.7495835e+09 atomic steps
  40 hash conflicts: 3.3187407e+08 (resolved)
  41
  42 Stats on memory usage (in Megabytes):
  43   291.901       equivalent memory usage for states (stored*(State-vector + overhead))
  44   123.793       actual memory usage for states (compression: 42.41%)
  45                 state-vector as stored = 13 byte + 36 byte overhead
  46     8.000       memory used for hash table (-w20)
  47   457.764       memory used for DFS stack (-m10000000)
  48   589.494       total actual memory usage
  49
  50 nr of templates: [ globals chans procs ]
  51 collapse counts: [ 39337 2870 221 2 2 ]
  52 unreached in proctype urcu_reader
  53         line 894, "pan.___", state 12, "((i<1))"
  54         line 894, "pan.___", state 12, "((i>=1))"
  55         line 268, "pan.___", state 61, "cache_dirty_urcu_gp_ctr = 0"
  56         line 276, "pan.___", state 83, "cache_dirty_rcu_ptr = 0"
  57         line 280, "pan.___", state 92, "cache_dirty_rcu_data[i] = 0"
  58         line 245, "pan.___", state 108, "(1)"
  59         line 249, "pan.___", state 116, "(1)"
  60         line 253, "pan.___", state 128, "(1)"
  61         line 257, "pan.___", state 136, "(1)"
  62         line 407, "pan.___", state 162, "cache_dirty_urcu_gp_ctr = 0"
  63         line 416, "pan.___", state 194, "cache_dirty_rcu_ptr = 0"
  64         line 420, "pan.___", state 208, "cache_dirty_rcu_data[i] = 0"
  65         line 425, "pan.___", state 227, "(1)"
  66         line 434, "pan.___", state 257, "(1)"
  67         line 438, "pan.___", state 270, "(1)"
  68         line 696, "pan.___", state 291, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  69         line 407, "pan.___", state 298, "cache_dirty_urcu_gp_ctr = 0"
  70         line 416, "pan.___", state 330, "cache_dirty_rcu_ptr = 0"
  71         line 420, "pan.___", state 344, "cache_dirty_rcu_data[i] = 0"
  72         line 425, "pan.___", state 363, "(1)"
  73         line 434, "pan.___", state 393, "(1)"
  74         line 438, "pan.___", state 406, "(1)"
  75         line 407, "pan.___", state 427, "cache_dirty_urcu_gp_ctr = 0"
  76         line 416, "pan.___", state 459, "cache_dirty_rcu_ptr = 0"
  77         line 420, "pan.___", state 473, "cache_dirty_rcu_data[i] = 0"
  78         line 425, "pan.___", state 492, "(1)"
  79         line 434, "pan.___", state 522, "(1)"
  80         line 438, "pan.___", state 535, "(1)"
  81         line 407, "pan.___", state 558, "cache_dirty_urcu_gp_ctr = 0"
  82         line 407, "pan.___", state 560, "(1)"
  83         line 407, "pan.___", state 561, "(cache_dirty_urcu_gp_ctr)"
  84         line 407, "pan.___", state 561, "else"
  85         line 407, "pan.___", state 564, "(1)"
  86         line 411, "pan.___", state 572, "cache_dirty_urcu_active_readers = 0"
  87         line 411, "pan.___", state 574, "(1)"
  88         line 411, "pan.___", state 575, "(cache_dirty_urcu_active_readers)"
  89         line 411, "pan.___", state 575, "else"
  90         line 411, "pan.___", state 578, "(1)"
  91         line 411, "pan.___", state 579, "(1)"
  92         line 411, "pan.___", state 579, "(1)"
  93         line 409, "pan.___", state 584, "((i<1))"
  94         line 409, "pan.___", state 584, "((i>=1))"
  95         line 416, "pan.___", state 590, "cache_dirty_rcu_ptr = 0"
  96         line 416, "pan.___", state 592, "(1)"
  97         line 416, "pan.___", state 593, "(cache_dirty_rcu_ptr)"
  98         line 416, "pan.___", state 593, "else"
  99         line 416, "pan.___", state 596, "(1)"
 100         line 416, "pan.___", state 597, "(1)"
 101         line 416, "pan.___", state 597, "(1)"
 102         line 420, "pan.___", state 604, "cache_dirty_rcu_data[i] = 0"
 103         line 420, "pan.___", state 606, "(1)"
 104         line 420, "pan.___", state 607, "(cache_dirty_rcu_data[i])"
 105         line 420, "pan.___", state 607, "else"
 106         line 420, "pan.___", state 610, "(1)"
 107         line 420, "pan.___", state 611, "(1)"
 108         line 420, "pan.___", state 611, "(1)"
 109         line 418, "pan.___", state 616, "((i<2))"
 110         line 418, "pan.___", state 616, "((i>=2))"
 111         line 425, "pan.___", state 623, "(1)"
 112         line 425, "pan.___", state 624, "(!(cache_dirty_urcu_gp_ctr))"
 113         line 425, "pan.___", state 624, "else"
 114         line 425, "pan.___", state 627, "(1)"
 115         line 425, "pan.___", state 628, "(1)"
 116         line 425, "pan.___", state 628, "(1)"
 117         line 429, "pan.___", state 636, "(1)"
 118         line 429, "pan.___", state 637, "(!(cache_dirty_urcu_active_readers))"
 119         line 429, "pan.___", state 637, "else"
 120         line 429, "pan.___", state 640, "(1)"
 121         line 429, "pan.___", state 641, "(1)"
 122         line 429, "pan.___", state 641, "(1)"
 123         line 427, "pan.___", state 646, "((i<1))"
 124         line 427, "pan.___", state 646, "((i>=1))"
 125         line 434, "pan.___", state 653, "(1)"
 126         line 434, "pan.___", state 654, "(!(cache_dirty_rcu_ptr))"
 127         line 434, "pan.___", state 654, "else"
 128         line 434, "pan.___", state 657, "(1)"
 129         line 434, "pan.___", state 658, "(1)"
 130         line 434, "pan.___", state 658, "(1)"
 131         line 438, "pan.___", state 666, "(1)"
 132         line 438, "pan.___", state 667, "(!(cache_dirty_rcu_data[i]))"
 133         line 438, "pan.___", state 667, "else"
 134         line 438, "pan.___", state 670, "(1)"
 135         line 438, "pan.___", state 671, "(1)"
 136         line 438, "pan.___", state 671, "(1)"
 137         line 436, "pan.___", state 676, "((i<2))"
 138         line 436, "pan.___", state 676, "((i>=2))"
 139         line 446, "pan.___", state 680, "(1)"
 140         line 446, "pan.___", state 680, "(1)"
 141         line 696, "pan.___", state 683, "cached_urcu_active_readers = (tmp+1)"
 142         line 696, "pan.___", state 684, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 143         line 696, "pan.___", state 685, "(1)"
 144         line 407, "pan.___", state 692, "cache_dirty_urcu_gp_ctr = 0"
 145         line 416, "pan.___", state 724, "cache_dirty_rcu_ptr = 0"
 146         line 420, "pan.___", state 738, "cache_dirty_rcu_data[i] = 0"
 147         line 425, "pan.___", state 757, "(1)"
 148         line 434, "pan.___", state 787, "(1)"
 149         line 438, "pan.___", state 800, "(1)"
 150         line 407, "pan.___", state 828, "cache_dirty_urcu_gp_ctr = 0"
 151         line 416, "pan.___", state 860, "cache_dirty_rcu_ptr = 0"
 152         line 420, "pan.___", state 874, "cache_dirty_rcu_data[i] = 0"
 153         line 425, "pan.___", state 893, "(1)"
 154         line 434, "pan.___", state 923, "(1)"
 155         line 438, "pan.___", state 936, "(1)"
 156         line 407, "pan.___", state 957, "cache_dirty_urcu_gp_ctr = 0"
 157         line 407, "pan.___", state 959, "(1)"
 158         line 407, "pan.___", state 960, "(cache_dirty_urcu_gp_ctr)"
 159         line 407, "pan.___", state 960, "else"
 160         line 407, "pan.___", state 963, "(1)"
 161         line 411, "pan.___", state 971, "cache_dirty_urcu_active_readers = 0"
 162         line 411, "pan.___", state 973, "(1)"
 163         line 411, "pan.___", state 974, "(cache_dirty_urcu_active_readers)"
 164         line 411, "pan.___", state 974, "else"
 165         line 411, "pan.___", state 977, "(1)"
 166         line 411, "pan.___", state 978, "(1)"
 167         line 411, "pan.___", state 978, "(1)"
 168         line 409, "pan.___", state 983, "((i<1))"
 169         line 409, "pan.___", state 983, "((i>=1))"
 170         line 416, "pan.___", state 989, "cache_dirty_rcu_ptr = 0"
 171         line 416, "pan.___", state 991, "(1)"
 172         line 416, "pan.___", state 992, "(cache_dirty_rcu_ptr)"
 173         line 416, "pan.___", state 992, "else"
 174         line 416, "pan.___", state 995, "(1)"
 175         line 416, "pan.___", state 996, "(1)"
 176         line 416, "pan.___", state 996, "(1)"
 177         line 420, "pan.___", state 1003, "cache_dirty_rcu_data[i] = 0"
 178         line 420, "pan.___", state 1005, "(1)"
 179         line 420, "pan.___", state 1006, "(cache_dirty_rcu_data[i])"
 180         line 420, "pan.___", state 1006, "else"
 181         line 420, "pan.___", state 1009, "(1)"
 182         line 420, "pan.___", state 1010, "(1)"
 183         line 420, "pan.___", state 1010, "(1)"
 184         line 418, "pan.___", state 1015, "((i<2))"
 185         line 418, "pan.___", state 1015, "((i>=2))"
 186         line 425, "pan.___", state 1022, "(1)"
 187         line 425, "pan.___", state 1023, "(!(cache_dirty_urcu_gp_ctr))"
 188         line 425, "pan.___", state 1023, "else"
 189         line 425, "pan.___", state 1026, "(1)"
 190         line 425, "pan.___", state 1027, "(1)"
 191         line 425, "pan.___", state 1027, "(1)"
 192         line 429, "pan.___", state 1035, "(1)"
 193         line 429, "pan.___", state 1036, "(!(cache_dirty_urcu_active_readers))"
 194         line 429, "pan.___", state 1036, "else"
 195         line 429, "pan.___", state 1039, "(1)"
 196         line 429, "pan.___", state 1040, "(1)"
 197         line 429, "pan.___", state 1040, "(1)"
 198         line 427, "pan.___", state 1045, "((i<1))"
 199         line 427, "pan.___", state 1045, "((i>=1))"
 200         line 434, "pan.___", state 1052, "(1)"
 201         line 434, "pan.___", state 1053, "(!(cache_dirty_rcu_ptr))"
 202         line 434, "pan.___", state 1053, "else"
 203         line 434, "pan.___", state 1056, "(1)"
 204         line 434, "pan.___", state 1057, "(1)"
 205         line 434, "pan.___", state 1057, "(1)"
 206         line 438, "pan.___", state 1065, "(1)"
 207         line 438, "pan.___", state 1066, "(!(cache_dirty_rcu_data[i]))"
 208         line 438, "pan.___", state 1066, "else"
 209         line 438, "pan.___", state 1069, "(1)"
 210         line 438, "pan.___", state 1070, "(1)"
 211         line 438, "pan.___", state 1070, "(1)"
 212         line 436, "pan.___", state 1075, "((i<2))"
 213         line 436, "pan.___", state 1075, "((i>=2))"
 214         line 446, "pan.___", state 1079, "(1)"
 215         line 446, "pan.___", state 1079, "(1)"
 216         line 704, "pan.___", state 1083, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
 217         line 407, "pan.___", state 1088, "cache_dirty_urcu_gp_ctr = 0"
 218         line 416, "pan.___", state 1120, "cache_dirty_rcu_ptr = 0"
 219         line 420, "pan.___", state 1134, "cache_dirty_rcu_data[i] = 0"
 220         line 425, "pan.___", state 1153, "(1)"
 221         line 434, "pan.___", state 1183, "(1)"
 222         line 438, "pan.___", state 1196, "(1)"
 223         line 407, "pan.___", state 1220, "cache_dirty_urcu_gp_ctr = 0"
 224         line 416, "pan.___", state 1252, "cache_dirty_rcu_ptr = 0"
 225         line 420, "pan.___", state 1266, "cache_dirty_rcu_data[i] = 0"
 226         line 425, "pan.___", state 1285, "(1)"
 227         line 434, "pan.___", state 1315, "(1)"
 228         line 438, "pan.___", state 1328, "(1)"
 229         line 407, "pan.___", state 1353, "cache_dirty_urcu_gp_ctr = 0"
 230         line 416, "pan.___", state 1385, "cache_dirty_rcu_ptr = 0"
 231         line 420, "pan.___", state 1399, "cache_dirty_rcu_data[i] = 0"
 232         line 425, "pan.___", state 1418, "(1)"
 233         line 434, "pan.___", state 1448, "(1)"
 234         line 438, "pan.___", state 1461, "(1)"
 235         line 407, "pan.___", state 1482, "cache_dirty_urcu_gp_ctr = 0"
 236         line 416, "pan.___", state 1514, "cache_dirty_rcu_ptr = 0"
 237         line 420, "pan.___", state 1528, "cache_dirty_rcu_data[i] = 0"
 238         line 425, "pan.___", state 1547, "(1)"
 239         line 434, "pan.___", state 1577, "(1)"
 240         line 438, "pan.___", state 1590, "(1)"
 241         line 407, "pan.___", state 1616, "cache_dirty_urcu_gp_ctr = 0"
 242         line 416, "pan.___", state 1648, "cache_dirty_rcu_ptr = 0"
 243         line 420, "pan.___", state 1662, "cache_dirty_rcu_data[i] = 0"
 244         line 425, "pan.___", state 1681, "(1)"
 245         line 434, "pan.___", state 1711, "(1)"
 246         line 438, "pan.___", state 1724, "(1)"
 247         line 407, "pan.___", state 1745, "cache_dirty_urcu_gp_ctr = 0"
 248         line 416, "pan.___", state 1777, "cache_dirty_rcu_ptr = 0"
 249         line 420, "pan.___", state 1791, "cache_dirty_rcu_data[i] = 0"
 250         line 425, "pan.___", state 1810, "(1)"
 251         line 434, "pan.___", state 1840, "(1)"
 252         line 438, "pan.___", state 1853, "(1)"
 253         line 407, "pan.___", state 1877, "cache_dirty_urcu_gp_ctr = 0"
 254         line 416, "pan.___", state 1909, "cache_dirty_rcu_ptr = 0"
 255         line 420, "pan.___", state 1923, "cache_dirty_rcu_data[i] = 0"
 256         line 425, "pan.___", state 1942, "(1)"
 257         line 434, "pan.___", state 1972, "(1)"
 258         line 438, "pan.___", state 1985, "(1)"
 259         line 743, "pan.___", state 2006, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
 260         line 407, "pan.___", state 2013, "cache_dirty_urcu_gp_ctr = 0"
 261         line 416, "pan.___", state 2045, "cache_dirty_rcu_ptr = 0"
 262         line 420, "pan.___", state 2059, "cache_dirty_rcu_data[i] = 0"
 263         line 425, "pan.___", state 2078, "(1)"
 264         line 434, "pan.___", state 2108, "(1)"
 265         line 438, "pan.___", state 2121, "(1)"
 266         line 407, "pan.___", state 2142, "cache_dirty_urcu_gp_ctr = 0"
 267         line 416, "pan.___", state 2174, "cache_dirty_rcu_ptr = 0"
 268         line 420, "pan.___", state 2188, "cache_dirty_rcu_data[i] = 0"
 269         line 425, "pan.___", state 2207, "(1)"
 270         line 434, "pan.___", state 2237, "(1)"
 271         line 438, "pan.___", state 2250, "(1)"
 272         line 407, "pan.___", state 2273, "cache_dirty_urcu_gp_ctr = 0"
 273         line 407, "pan.___", state 2275, "(1)"
 274         line 407, "pan.___", state 2276, "(cache_dirty_urcu_gp_ctr)"
 275         line 407, "pan.___", state 2276, "else"
 276         line 407, "pan.___", state 2279, "(1)"
 277         line 411, "pan.___", state 2287, "cache_dirty_urcu_active_readers = 0"
 278         line 411, "pan.___", state 2289, "(1)"
 279         line 411, "pan.___", state 2290, "(cache_dirty_urcu_active_readers)"
 280         line 411, "pan.___", state 2290, "else"
 281         line 411, "pan.___", state 2293, "(1)"
 282         line 411, "pan.___", state 2294, "(1)"
 283         line 411, "pan.___", state 2294, "(1)"
 284         line 409, "pan.___", state 2299, "((i<1))"
 285         line 409, "pan.___", state 2299, "((i>=1))"
 286         line 416, "pan.___", state 2305, "cache_dirty_rcu_ptr = 0"
 287         line 416, "pan.___", state 2307, "(1)"
 288         line 416, "pan.___", state 2308, "(cache_dirty_rcu_ptr)"
 289         line 416, "pan.___", state 2308, "else"
 290         line 416, "pan.___", state 2311, "(1)"
 291         line 416, "pan.___", state 2312, "(1)"
 292         line 416, "pan.___", state 2312, "(1)"
 293         line 420, "pan.___", state 2319, "cache_dirty_rcu_data[i] = 0"
 294         line 420, "pan.___", state 2321, "(1)"
 295         line 420, "pan.___", state 2322, "(cache_dirty_rcu_data[i])"
 296         line 420, "pan.___", state 2322, "else"
 297         line 420, "pan.___", state 2325, "(1)"
 298         line 420, "pan.___", state 2326, "(1)"
 299         line 420, "pan.___", state 2326, "(1)"
 300         line 418, "pan.___", state 2331, "((i<2))"
 301         line 418, "pan.___", state 2331, "((i>=2))"
 302         line 425, "pan.___", state 2338, "(1)"
 303         line 425, "pan.___", state 2339, "(!(cache_dirty_urcu_gp_ctr))"
 304         line 425, "pan.___", state 2339, "else"
 305         line 425, "pan.___", state 2342, "(1)"
 306         line 425, "pan.___", state 2343, "(1)"
 307         line 425, "pan.___", state 2343, "(1)"
 308         line 429, "pan.___", state 2351, "(1)"
 309         line 429, "pan.___", state 2352, "(!(cache_dirty_urcu_active_readers))"
 310         line 429, "pan.___", state 2352, "else"
 311         line 429, "pan.___", state 2355, "(1)"
 312         line 429, "pan.___", state 2356, "(1)"
 313         line 429, "pan.___", state 2356, "(1)"
 314         line 427, "pan.___", state 2361, "((i<1))"
 315         line 427, "pan.___", state 2361, "((i>=1))"
 316         line 434, "pan.___", state 2368, "(1)"
 317         line 434, "pan.___", state 2369, "(!(cache_dirty_rcu_ptr))"
 318         line 434, "pan.___", state 2369, "else"
 319         line 434, "pan.___", state 2372, "(1)"
 320         line 434, "pan.___", state 2373, "(1)"
 321         line 434, "pan.___", state 2373, "(1)"
 322         line 438, "pan.___", state 2381, "(1)"
 323         line 438, "pan.___", state 2382, "(!(cache_dirty_rcu_data[i]))"
 324         line 438, "pan.___", state 2382, "else"
 325         line 438, "pan.___", state 2385, "(1)"
 326         line 438, "pan.___", state 2386, "(1)"
 327         line 438, "pan.___", state 2386, "(1)"
 328         line 436, "pan.___", state 2391, "((i<2))"
 329         line 436, "pan.___", state 2391, "((i>=2))"
 330         line 446, "pan.___", state 2395, "(1)"
 331         line 446, "pan.___", state 2395, "(1)"
 332         line 743, "pan.___", state 2398, "cached_urcu_active_readers = (tmp+1)"
 333         line 743, "pan.___", state 2399, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
 334         line 743, "pan.___", state 2400, "(1)"
 335         line 407, "pan.___", state 2407, "cache_dirty_urcu_gp_ctr = 0"
 336         line 416, "pan.___", state 2439, "cache_dirty_rcu_ptr = 0"
 337         line 420, "pan.___", state 2453, "cache_dirty_rcu_data[i] = 0"
 338         line 425, "pan.___", state 2472, "(1)"
 339         line 434, "pan.___", state 2502, "(1)"
 340         line 438, "pan.___", state 2515, "(1)"
 341         line 407, "pan.___", state 2542, "cache_dirty_urcu_gp_ctr = 0"
 342         line 416, "pan.___", state 2574, "cache_dirty_rcu_ptr = 0"
 343         line 420, "pan.___", state 2588, "cache_dirty_rcu_data[i] = 0"
 344         line 425, "pan.___", state 2607, "(1)"
 345         line 434, "pan.___", state 2637, "(1)"
 346         line 438, "pan.___", state 2650, "(1)"
 347         line 407, "pan.___", state 2671, "cache_dirty_urcu_gp_ctr = 0"
 348         line 416, "pan.___", state 2703, "cache_dirty_rcu_ptr = 0"
 349         line 420, "pan.___", state 2717, "cache_dirty_rcu_data[i] = 0"
 350         line 425, "pan.___", state 2736, "(1)"
 351         line 434, "pan.___", state 2766, "(1)"
 352         line 438, "pan.___", state 2779, "(1)"
 353         line 245, "pan.___", state 2812, "(1)"
 354         line 253, "pan.___", state 2832, "(1)"
 355         line 257, "pan.___", state 2840, "(1)"
 356         line 245, "pan.___", state 2855, "(1)"
 357         line 253, "pan.___", state 2875, "(1)"
 358         line 257, "pan.___", state 2883, "(1)"
 359         line 929, "pan.___", state 2900, "-end-"
 360         (246 of 2900 states)
 361 unreached in proctype urcu_writer
 362         line 1018, "pan.___", state 12, "((i<1))"
 363         line 1018, "pan.___", state 12, "((i>=1))"
 364         line 407, "pan.___", state 47, "cache_dirty_urcu_gp_ctr = 0"
 365         line 407, "pan.___", state 53, "(1)"
 366         line 411, "pan.___", state 61, "cache_dirty_urcu_active_readers = 0"
 367         line 411, "pan.___", state 67, "(1)"
 368         line 411, "pan.___", state 68, "(1)"
 369         line 411, "pan.___", state 68, "(1)"
 370         line 409, "pan.___", state 73, "((i<1))"
 371         line 409, "pan.___", state 73, "((i>=1))"
 372         line 416, "pan.___", state 79, "cache_dirty_rcu_ptr = 0"
 373         line 416, "pan.___", state 85, "(1)"
 374         line 416, "pan.___", state 86, "(1)"
 375         line 416, "pan.___", state 86, "(1)"
 376         line 420, "pan.___", state 99, "(1)"
 377         line 420, "pan.___", state 100, "(1)"
 378         line 420, "pan.___", state 100, "(1)"
 379         line 418, "pan.___", state 105, "((i<2))"
 380         line 418, "pan.___", state 105, "((i>=2))"
 381         line 425, "pan.___", state 112, "(1)"
 382         line 425, "pan.___", state 113, "(!(cache_dirty_urcu_gp_ctr))"
 383         line 425, "pan.___", state 113, "else"
 384         line 425, "pan.___", state 116, "(1)"
 385         line 425, "pan.___", state 117, "(1)"
 386         line 425, "pan.___", state 117, "(1)"
 387         line 429, "pan.___", state 125, "(1)"
 388         line 429, "pan.___", state 126, "(!(cache_dirty_urcu_active_readers))"
 389         line 429, "pan.___", state 126, "else"
 390         line 429, "pan.___", state 129, "(1)"
 391         line 429, "pan.___", state 130, "(1)"
 392         line 429, "pan.___", state 130, "(1)"
 393         line 427, "pan.___", state 135, "((i<1))"
 394         line 427, "pan.___", state 135, "((i>=1))"
 395         line 434, "pan.___", state 142, "(1)"
 396         line 434, "pan.___", state 143, "(!(cache_dirty_rcu_ptr))"
 397         line 434, "pan.___", state 143, "else"
 398         line 434, "pan.___", state 146, "(1)"
 399         line 434, "pan.___", state 147, "(1)"
 400         line 434, "pan.___", state 147, "(1)"
 401         line 438, "pan.___", state 155, "(1)"
 402         line 438, "pan.___", state 156, "(!(cache_dirty_rcu_data[i]))"
 403         line 438, "pan.___", state 156, "else"
 404         line 438, "pan.___", state 159, "(1)"
 405         line 438, "pan.___", state 160, "(1)"
 406         line 438, "pan.___", state 160, "(1)"
 407         line 436, "pan.___", state 165, "((i<2))"
 408         line 436, "pan.___", state 165, "((i>=2))"
 409         line 446, "pan.___", state 169, "(1)"
 410         line 446, "pan.___", state 169, "(1)"
 411         line 268, "pan.___", state 178, "cache_dirty_urcu_gp_ctr = 0"
 412         line 272, "pan.___", state 187, "cache_dirty_urcu_active_readers = 0"
 413         line 270, "pan.___", state 195, "((i<1))"
 414         line 270, "pan.___", state 195, "((i>=1))"
 415         line 276, "pan.___", state 200, "cache_dirty_rcu_ptr = 0"
 416         line 1088, "pan.___", state 228, "old_data = cached_rcu_ptr"
 417         line 1099, "pan.___", state 232, "_proc_urcu_writer = (_proc_urcu_writer|(1<<4))"
 418         line 407, "pan.___", state 240, "cache_dirty_urcu_gp_ctr = 0"
 419         line 407, "pan.___", state 246, "(1)"
 420         line 411, "pan.___", state 254, "cache_dirty_urcu_active_readers = 0"
 421         line 411, "pan.___", state 260, "(1)"
 422         line 411, "pan.___", state 261, "(1)"
 423         line 411, "pan.___", state 261, "(1)"
 424         line 409, "pan.___", state 266, "((i<1))"
 425         line 409, "pan.___", state 266, "((i>=1))"
 426         line 416, "pan.___", state 274, "(1)"
 427         line 416, "pan.___", state 275, "(cache_dirty_rcu_ptr)"
 428         line 416, "pan.___", state 275, "else"
 429         line 416, "pan.___", state 278, "(1)"
 430         line 416, "pan.___", state 279, "(1)"
 431         line 416, "pan.___", state 279, "(1)"
 432         line 420, "pan.___", state 286, "cache_dirty_rcu_data[i] = 0"
 433         line 420, "pan.___", state 292, "(1)"
 434         line 420, "pan.___", state 293, "(1)"
 435         line 420, "pan.___", state 293, "(1)"
 436         line 418, "pan.___", state 298, "((i<2))"
 437         line 418, "pan.___", state 298, "((i>=2))"
 438         line 425, "pan.___", state 305, "(1)"
 439         line 425, "pan.___", state 306, "(!(cache_dirty_urcu_gp_ctr))"
 440         line 425, "pan.___", state 306, "else"
 441         line 425, "pan.___", state 309, "(1)"
 442         line 425, "pan.___", state 310, "(1)"
 443         line 425, "pan.___", state 310, "(1)"
 444         line 429, "pan.___", state 318, "(1)"
 445         line 429, "pan.___", state 319, "(!(cache_dirty_urcu_active_readers))"
 446         line 429, "pan.___", state 319, "else"
 447         line 429, "pan.___", state 322, "(1)"
 448         line 429, "pan.___", state 323, "(1)"
 449         line 429, "pan.___", state 323, "(1)"
 450         line 427, "pan.___", state 328, "((i<1))"
 451         line 427, "pan.___", state 328, "((i>=1))"
 452         line 434, "pan.___", state 335, "(1)"
 453         line 434, "pan.___", state 336, "(!(cache_dirty_rcu_ptr))"
 454         line 434, "pan.___", state 336, "else"
 455         line 434, "pan.___", state 339, "(1)"
 456         line 434, "pan.___", state 340, "(1)"
 457         line 434, "pan.___", state 340, "(1)"
 458         line 438, "pan.___", state 348, "(1)"
 459         line 438, "pan.___", state 349, "(!(cache_dirty_rcu_data[i]))"
 460         line 438, "pan.___", state 349, "else"
 461         line 438, "pan.___", state 352, "(1)"
 462         line 438, "pan.___", state 353, "(1)"
 463         line 438, "pan.___", state 353, "(1)"
 464         line 436, "pan.___", state 358, "((i<2))"
 465         line 436, "pan.___", state 358, "((i>=2))"
 466         line 446, "pan.___", state 362, "(1)"
 467         line 446, "pan.___", state 362, "(1)"
 468         line 407, "pan.___", state 373, "(1)"
 469         line 407, "pan.___", state 374, "(cache_dirty_urcu_gp_ctr)"
 470         line 407, "pan.___", state 374, "else"
 471         line 407, "pan.___", state 377, "(1)"
 472         line 411, "pan.___", state 385, "cache_dirty_urcu_active_readers = 0"
 473         line 411, "pan.___", state 391, "(1)"
 474         line 411, "pan.___", state 392, "(1)"
 475         line 411, "pan.___", state 392, "(1)"
 476         line 409, "pan.___", state 397, "((i<1))"
 477         line 409, "pan.___", state 397, "((i>=1))"
 478         line 416, "pan.___", state 403, "cache_dirty_rcu_ptr = 0"
 479         line 416, "pan.___", state 409, "(1)"
 480         line 416, "pan.___", state 410, "(1)"
 481         line 416, "pan.___", state 410, "(1)"
 482         line 420, "pan.___", state 417, "cache_dirty_rcu_data[i] = 0"
 483         line 420, "pan.___", state 423, "(1)"
 484         line 420, "pan.___", state 424, "(1)"
 485         line 420, "pan.___", state 424, "(1)"
 486         line 418, "pan.___", state 429, "((i<2))"
 487         line 418, "pan.___", state 429, "((i>=2))"
 488         line 425, "pan.___", state 436, "(1)"
 489         line 425, "pan.___", state 437, "(!(cache_dirty_urcu_gp_ctr))"
 490         line 425, "pan.___", state 437, "else"
 491         line 425, "pan.___", state 440, "(1)"
 492         line 425, "pan.___", state 441, "(1)"
 493         line 425, "pan.___", state 441, "(1)"
 494         line 429, "pan.___", state 449, "(1)"
 495         line 429, "pan.___", state 450, "(!(cache_dirty_urcu_active_readers))"
 496         line 429, "pan.___", state 450, "else"
 497         line 429, "pan.___", state 453, "(1)"
 498         line 429, "pan.___", state 454, "(1)"
 499         line 429, "pan.___", state 454, "(1)"
 500         line 427, "pan.___", state 459, "((i<1))"
 501         line 427, "pan.___", state 459, "((i>=1))"
 502         line 434, "pan.___", state 466, "(1)"
 503         line 434, "pan.___", state 467, "(!(cache_dirty_rcu_ptr))"
 504         line 434, "pan.___", state 467, "else"
 505         line 434, "pan.___", state 470, "(1)"
 506         line 434, "pan.___", state 471, "(1)"
 507         line 434, "pan.___", state 471, "(1)"
 508         line 438, "pan.___", state 479, "(1)"
 509         line 438, "pan.___", state 480, "(!(cache_dirty_rcu_data[i]))"
 510         line 438, "pan.___", state 480, "else"
 511         line 438, "pan.___", state 483, "(1)"
 512         line 438, "pan.___", state 484, "(1)"
 513         line 438, "pan.___", state 484, "(1)"
 514         line 436, "pan.___", state 489, "((i<2))"
 515         line 436, "pan.___", state 489, "((i>=2))"
 516         line 446, "pan.___", state 493, "(1)"
 517         line 446, "pan.___", state 493, "(1)"
 518         line 1153, "pan.___", state 504, "_proc_urcu_writer = (_proc_urcu_writer&~((1<<9)))"
 519         line 1158, "pan.___", state 505, "_proc_urcu_writer = (_proc_urcu_writer&~(((1<<8)|(1<<7))))"
 520         line 407, "pan.___", state 510, "cache_dirty_urcu_gp_ctr = 0"
 521         line 407, "pan.___", state 516, "(1)"
 522         line 411, "pan.___", state 524, "cache_dirty_urcu_active_readers = 0"
 523         line 411, "pan.___", state 530, "(1)"
 524         line 411, "pan.___", state 531, "(1)"
 525         line 411, "pan.___", state 531, "(1)"
 526         line 409, "pan.___", state 536, "((i<1))"
 527         line 409, "pan.___", state 536, "((i>=1))"
 528         line 416, "pan.___", state 542, "cache_dirty_rcu_ptr = 0"
 529         line 416, "pan.___", state 548, "(1)"
 530         line 416, "pan.___", state 549, "(1)"
 531         line 416, "pan.___", state 549, "(1)"
 532         line 420, "pan.___", state 556, "cache_dirty_rcu_data[i] = 0"
 533         line 420, "pan.___", state 562, "(1)"
 534         line 420, "pan.___", state 563, "(1)"
 535         line 420, "pan.___", state 563, "(1)"
 536         line 418, "pan.___", state 568, "((i<2))"
 537         line 418, "pan.___", state 568, "((i>=2))"
 538         line 425, "pan.___", state 575, "(1)"
 539         line 425, "pan.___", state 576, "(!(cache_dirty_urcu_gp_ctr))"
 540         line 425, "pan.___", state 576, "else"
 541         line 425, "pan.___", state 579, "(1)"
 542         line 425, "pan.___", state 580, "(1)"
 543         line 425, "pan.___", state 580, "(1)"
 544         line 429, "pan.___", state 588, "(1)"
 545         line 429, "pan.___", state 589, "(!(cache_dirty_urcu_active_readers))"
 546         line 429, "pan.___", state 589, "else"
 547         line 429, "pan.___", state 592, "(1)"
 548         line 429, "pan.___", state 593, "(1)"
 549         line 429, "pan.___", state 593, "(1)"
 550         line 427, "pan.___", state 598, "((i<1))"
 551         line 427, "pan.___", state 598, "((i>=1))"
 552         line 434, "pan.___", state 605, "(1)"
 553         line 434, "pan.___", state 606, "(!(cache_dirty_rcu_ptr))"
 554         line 434, "pan.___", state 606, "else"
 555         line 434, "pan.___", state 609, "(1)"
 556         line 434, "pan.___", state 610, "(1)"
 557         line 434, "pan.___", state 610, "(1)"
 558         line 438, "pan.___", state 618, "(1)"
 559         line 438, "pan.___", state 619, "(!(cache_dirty_rcu_data[i]))"
 560         line 438, "pan.___", state 619, "else"
 561         line 438, "pan.___", state 622, "(1)"
 562         line 438, "pan.___", state 623, "(1)"
 563         line 438, "pan.___", state 623, "(1)"
 564         line 446, "pan.___", state 632, "(1)"
 565         line 446, "pan.___", state 632, "(1)"
 566         line 407, "pan.___", state 639, "cache_dirty_urcu_gp_ctr = 0"
 567         line 411, "pan.___", state 653, "cache_dirty_urcu_active_readers = 0"
 568         line 416, "pan.___", state 671, "cache_dirty_rcu_ptr = 0"
 569         line 425, "pan.___", state 704, "(1)"
 570         line 429, "pan.___", state 717, "(1)"
 571         line 434, "pan.___", state 734, "(1)"
 572         line 438, "pan.___", state 747, "(1)"
 573         line 411, "pan.___", state 784, "cache_dirty_urcu_active_readers = 0"
 574         line 416, "pan.___", state 802, "cache_dirty_rcu_ptr = 0"
 575         line 420, "pan.___", state 816, "cache_dirty_rcu_data[i] = 0"
 576         line 429, "pan.___", state 848, "(1)"
 577         line 434, "pan.___", state 865, "(1)"
 578         line 438, "pan.___", state 878, "(1)"
 579         line 1235, "pan.___", state 905, "_proc_urcu_writer = (_proc_urcu_writer|(1<<13))"
 580         line 268, "pan.___", state 933, "cache_dirty_urcu_gp_ctr = 0"
 581         line 268, "pan.___", state 935, "(1)"
 582         line 272, "pan.___", state 942, "cache_dirty_urcu_active_readers = 0"
 583         line 272, "pan.___", state 944, "(1)"
 584         line 272, "pan.___", state 945, "(cache_dirty_urcu_active_readers)"
 585         line 272, "pan.___", state 945, "else"
 586         line 270, "pan.___", state 950, "((i<1))"
 587         line 270, "pan.___", state 950, "((i>=1))"
 588         line 276, "pan.___", state 955, "cache_dirty_rcu_ptr = 0"
 589         line 276, "pan.___", state 957, "(1)"
 590         line 276, "pan.___", state 958, "(cache_dirty_rcu_ptr)"
 591         line 276, "pan.___", state 958, "else"
 592         line 280, "pan.___", state 964, "cache_dirty_rcu_data[i] = 0"
 593         line 280, "pan.___", state 966, "(1)"
 594         line 280, "pan.___", state 967, "(cache_dirty_rcu_data[i])"
 595         line 280, "pan.___", state 967, "else"
 596         line 278, "pan.___", state 972, "((i<2))"
 597         line 278, "pan.___", state 972, "((i>=2))"
 598         line 245, "pan.___", state 980, "(1)"
 599         line 249, "pan.___", state 988, "(1)"
 600         line 249, "pan.___", state 989, "(!(cache_dirty_urcu_active_readers))"
 601         line 249, "pan.___", state 989, "else"
 602         line 247, "pan.___", state 994, "((i<1))"
 603         line 247, "pan.___", state 994, "((i>=1))"
 604         line 253, "pan.___", state 1000, "(1)"
 605         line 253, "pan.___", state 1001, "(!(cache_dirty_rcu_ptr))"
 606         line 253, "pan.___", state 1001, "else"
 607         line 257, "pan.___", state 1008, "(1)"
 608         line 257, "pan.___", state 1009, "(!(cache_dirty_rcu_data[i]))"
 609         line 257, "pan.___", state 1009, "else"
 610         line 262, "pan.___", state 1018, "(!(cache_dirty_urcu_gp_ctr))"
 611         line 262, "pan.___", state 1018, "else"
 612         line 1289, "pan.___", state 1034, "((i<1))"
 613         line 1289, "pan.___", state 1034, "((i>=1))"
 614         line 268, "pan.___", state 1039, "cache_dirty_urcu_gp_ctr = 0"
 615         line 268, "pan.___", state 1041, "(1)"
 616         line 272, "pan.___", state 1048, "cache_dirty_urcu_active_readers = 0"
 617         line 272, "pan.___", state 1050, "(1)"
 618         line 272, "pan.___", state 1051, "(cache_dirty_urcu_active_readers)"
 619         line 272, "pan.___", state 1051, "else"
 620         line 270, "pan.___", state 1056, "((i<1))"
 621         line 270, "pan.___", state 1056, "((i>=1))"
 622         line 276, "pan.___", state 1061, "cache_dirty_rcu_ptr = 0"
 623         line 276, "pan.___", state 1063, "(1)"
 624         line 276, "pan.___", state 1064, "(cache_dirty_rcu_ptr)"
 625         line 276, "pan.___", state 1064, "else"
 626         line 280, "pan.___", state 1070, "cache_dirty_rcu_data[i] = 0"
 627         line 280, "pan.___", state 1072, "(1)"
 628         line 280, "pan.___", state 1073, "(cache_dirty_rcu_data[i])"
 629         line 280, "pan.___", state 1073, "else"
 630         line 278, "pan.___", state 1078, "((i<2))"
 631         line 278, "pan.___", state 1078, "((i>=2))"
 632         line 245, "pan.___", state 1086, "(1)"
 633         line 249, "pan.___", state 1094, "(1)"
 634         line 249, "pan.___", state 1095, "(!(cache_dirty_urcu_active_readers))"
 635         line 249, "pan.___", state 1095, "else"
 636         line 247, "pan.___", state 1100, "((i<1))"
 637         line 247, "pan.___", state 1100, "((i>=1))"
 638         line 253, "pan.___", state 1106, "(1)"
 639         line 253, "pan.___", state 1107, "(!(cache_dirty_rcu_ptr))"
 640         line 253, "pan.___", state 1107, "else"
 641         line 257, "pan.___", state 1114, "(1)"
 642         line 257, "pan.___", state 1115, "(!(cache_dirty_rcu_data[i]))"
 643         line 257, "pan.___", state 1115, "else"
 644         line 262, "pan.___", state 1124, "(!(cache_dirty_urcu_gp_ctr))"
 645         line 262, "pan.___", state 1124, "else"
 646         line 295, "pan.___", state 1126, "(cache_dirty_urcu_gp_ctr)"
 647         line 295, "pan.___", state 1126, "else"
 648         line 1289, "pan.___", state 1127, "(cache_dirty_urcu_gp_ctr)"
 649         line 1289, "pan.___", state 1127, "else"
 650         line 268, "pan.___", state 1131, "cache_dirty_urcu_gp_ctr = 0"
 651         line 268, "pan.___", state 1133, "(1)"
 652         line 272, "pan.___", state 1140, "cache_dirty_urcu_active_readers = 0"
 653         line 272, "pan.___", state 1142, "(1)"
 654         line 272, "pan.___", state 1143, "(cache_dirty_urcu_active_readers)"
 655         line 272, "pan.___", state 1143, "else"
 656         line 270, "pan.___", state 1148, "((i<1))"
 657         line 270, "pan.___", state 1148, "((i>=1))"
 658         line 276, "pan.___", state 1153, "cache_dirty_rcu_ptr = 0"
 659         line 276, "pan.___", state 1155, "(1)"
 660         line 276, "pan.___", state 1156, "(cache_dirty_rcu_ptr)"
 661         line 276, "pan.___", state 1156, "else"
 662         line 280, "pan.___", state 1162, "cache_dirty_rcu_data[i] = 0"
 663         line 280, "pan.___", state 1164, "(1)"
 664         line 280, "pan.___", state 1165, "(cache_dirty_rcu_data[i])"
 665         line 280, "pan.___", state 1165, "else"
 666         line 278, "pan.___", state 1170, "((i<2))"
 667         line 278, "pan.___", state 1170, "((i>=2))"
 668         line 245, "pan.___", state 1178, "(1)"
 669         line 249, "pan.___", state 1186, "(1)"
 670         line 249, "pan.___", state 1187, "(!(cache_dirty_urcu_active_readers))"
 671         line 249, "pan.___", state 1187, "else"
 672         line 247, "pan.___", state 1192, "((i<1))"
 673         line 247, "pan.___", state 1192, "((i>=1))"
 674         line 253, "pan.___", state 1198, "(1)"
 675         line 253, "pan.___", state 1199, "(!(cache_dirty_rcu_ptr))"
 676         line 253, "pan.___", state 1199, "else"
 677         line 257, "pan.___", state 1206, "(1)"
 678         line 257, "pan.___", state 1207, "(!(cache_dirty_rcu_data[i]))"
 679         line 257, "pan.___", state 1207, "else"
 680         line 262, "pan.___", state 1216, "(!(cache_dirty_urcu_gp_ctr))"
 681         line 262, "pan.___", state 1216, "else"
 682         line 1293, "pan.___", state 1219, "i = 0"
 683         line 1293, "pan.___", state 1221, "reader_barrier = 1"
 684         line 1293, "pan.___", state 1232, "((i<1))"
 685         line 1293, "pan.___", state 1232, "((i>=1))"
 686         line 268, "pan.___", state 1237, "cache_dirty_urcu_gp_ctr = 0"
 687         line 268, "pan.___", state 1239, "(1)"
 688         line 272, "pan.___", state 1246, "cache_dirty_urcu_active_readers = 0"
 689         line 272, "pan.___", state 1248, "(1)"
 690         line 272, "pan.___", state 1249, "(cache_dirty_urcu_active_readers)"
 691         line 272, "pan.___", state 1249, "else"
 692         line 270, "pan.___", state 1254, "((i<1))"
 693         line 270, "pan.___", state 1254, "((i>=1))"
 694         line 276, "pan.___", state 1259, "cache_dirty_rcu_ptr = 0"
 695         line 276, "pan.___", state 1261, "(1)"
 696         line 276, "pan.___", state 1262, "(cache_dirty_rcu_ptr)"
 697         line 276, "pan.___", state 1262, "else"
 698         line 280, "pan.___", state 1268, "cache_dirty_rcu_data[i] = 0"
 699         line 280, "pan.___", state 1270, "(1)"
 700         line 280, "pan.___", state 1271, "(cache_dirty_rcu_data[i])"
 701         line 280, "pan.___", state 1271, "else"
 702         line 278, "pan.___", state 1276, "((i<2))"
 703         line 278, "pan.___", state 1276, "((i>=2))"
 704         line 245, "pan.___", state 1284, "(1)"
 705         line 249, "pan.___", state 1292, "(1)"
 706         line 249, "pan.___", state 1293, "(!(cache_dirty_urcu_active_readers))"
 707         line 249, "pan.___", state 1293, "else"
 708         line 247, "pan.___", state 1298, "((i<1))"
 709         line 247, "pan.___", state 1298, "((i>=1))"
 710         line 253, "pan.___", state 1304, "(1)"
 711         line 253, "pan.___", state 1305, "(!(cache_dirty_rcu_ptr))"
 712         line 253, "pan.___", state 1305, "else"
 713         line 257, "pan.___", state 1312, "(1)"
 714         line 257, "pan.___", state 1313, "(!(cache_dirty_rcu_data[i]))"
 715         line 257, "pan.___", state 1313, "else"
 716         line 262, "pan.___", state 1322, "(!(cache_dirty_urcu_gp_ctr))"
 717         line 262, "pan.___", state 1322, "else"
 718         line 295, "pan.___", state 1324, "(cache_dirty_urcu_gp_ctr)"
 719         line 295, "pan.___", state 1324, "else"
 720         line 1293, "pan.___", state 1325, "(cache_dirty_urcu_gp_ctr)"
 721         line 1293, "pan.___", state 1325, "else"
 722         line 272, "pan.___", state 1338, "cache_dirty_urcu_active_readers = 0"
 723         line 276, "pan.___", state 1351, "cache_dirty_rcu_ptr = 0"
 724         line 280, "pan.___", state 1360, "cache_dirty_rcu_data[i] = 0"
 725         line 245, "pan.___", state 1376, "(1)"
 726         line 249, "pan.___", state 1384, "(1)"
 727         line 253, "pan.___", state 1396, "(1)"
 728         line 257, "pan.___", state 1404, "(1)"
 729         line 268, "pan.___", state 1435, "cache_dirty_urcu_gp_ctr = 0"
 730         line 272, "pan.___", state 1444, "cache_dirty_urcu_active_readers = 0"
 731         line 276, "pan.___", state 1457, "cache_dirty_rcu_ptr = 0"
 732         line 280, "pan.___", state 1466, "cache_dirty_rcu_data[i] = 0"
 733         line 245, "pan.___", state 1482, "(1)"
 734         line 249, "pan.___", state 1490, "(1)"
 735         line 253, "pan.___", state 1502, "(1)"
 736         line 257, "pan.___", state 1510, "(1)"
 737         line 268, "pan.___", state 1527, "cache_dirty_urcu_gp_ctr = 0"
 738         line 268, "pan.___", state 1529, "(1)"
 739         line 272, "pan.___", state 1536, "cache_dirty_urcu_active_readers = 0"
 740         line 272, "pan.___", state 1538, "(1)"
 741         line 272, "pan.___", state 1539, "(cache_dirty_urcu_active_readers)"
 742         line 272, "pan.___", state 1539, "else"
 743         line 270, "pan.___", state 1544, "((i<1))"
 744         line 270, "pan.___", state 1544, "((i>=1))"
 745         line 276, "pan.___", state 1549, "cache_dirty_rcu_ptr = 0"
 746         line 276, "pan.___", state 1551, "(1)"
 747         line 276, "pan.___", state 1552, "(cache_dirty_rcu_ptr)"
 748         line 276, "pan.___", state 1552, "else"
 749         line 280, "pan.___", state 1558, "cache_dirty_rcu_data[i] = 0"
 750         line 280, "pan.___", state 1560, "(1)"
 751         line 280, "pan.___", state 1561, "(cache_dirty_rcu_data[i])"
 752         line 280, "pan.___", state 1561, "else"
 753         line 278, "pan.___", state 1566, "((i<2))"
 754         line 278, "pan.___", state 1566, "((i>=2))"
 755         line 245, "pan.___", state 1574, "(1)"
 756         line 249, "pan.___", state 1582, "(1)"
 757         line 249, "pan.___", state 1583, "(!(cache_dirty_urcu_active_readers))"
 758         line 249, "pan.___", state 1583, "else"
 759         line 247, "pan.___", state 1588, "((i<1))"
 760         line 247, "pan.___", state 1588, "((i>=1))"
 761         line 253, "pan.___", state 1594, "(1)"
 762         line 253, "pan.___", state 1595, "(!(cache_dirty_rcu_ptr))"
 763         line 253, "pan.___", state 1595, "else"
 764         line 257, "pan.___", state 1602, "(1)"
 765         line 257, "pan.___", state 1603, "(!(cache_dirty_rcu_data[i]))"
 766         line 257, "pan.___", state 1603, "else"
 767         line 262, "pan.___", state 1612, "(!(cache_dirty_urcu_gp_ctr))"
 768         line 262, "pan.___", state 1612, "else"
 769         line 1300, "pan.___", state 1615, "i = 0"
 770         line 1300, "pan.___", state 1617, "reader_barrier = 1"
 771         line 1300, "pan.___", state 1628, "((i<1))"
 772         line 1300, "pan.___", state 1628, "((i>=1))"
 773         line 268, "pan.___", state 1633, "cache_dirty_urcu_gp_ctr = 0"
 774         line 268, "pan.___", state 1635, "(1)"
 775         line 272, "pan.___", state 1642, "cache_dirty_urcu_active_readers = 0"
 776         line 272, "pan.___", state 1644, "(1)"
 777         line 272, "pan.___", state 1645, "(cache_dirty_urcu_active_readers)"
 778         line 272, "pan.___", state 1645, "else"
 779         line 270, "pan.___", state 1650, "((i<1))"
 780         line 270, "pan.___", state 1650, "((i>=1))"
 781         line 276, "pan.___", state 1655, "cache_dirty_rcu_ptr = 0"
 782         line 276, "pan.___", state 1657, "(1)"
 783         line 276, "pan.___", state 1658, "(cache_dirty_rcu_ptr)"
 784         line 276, "pan.___", state 1658, "else"
 785         line 280, "pan.___", state 1664, "cache_dirty_rcu_data[i] = 0"
 786         line 280, "pan.___", state 1666, "(1)"
 787         line 280, "pan.___", state 1667, "(cache_dirty_rcu_data[i])"
 788         line 280, "pan.___", state 1667, "else"
 789         line 278, "pan.___", state 1672, "((i<2))"
 790         line 278, "pan.___", state 1672, "((i>=2))"
 791         line 245, "pan.___", state 1680, "(1)"
 792         line 249, "pan.___", state 1688, "(1)"
 793         line 249, "pan.___", state 1689, "(!(cache_dirty_urcu_active_readers))"
 794         line 249, "pan.___", state 1689, "else"
 795         line 247, "pan.___", state 1694, "((i<1))"
 796         line 247, "pan.___", state 1694, "((i>=1))"
 797         line 253, "pan.___", state 1700, "(1)"
 798         line 253, "pan.___", state 1701, "(!(cache_dirty_rcu_ptr))"
 799         line 253, "pan.___", state 1701, "else"
 800         line 257, "pan.___", state 1708, "(1)"
 801         line 257, "pan.___", state 1709, "(!(cache_dirty_rcu_data[i]))"
 802         line 257, "pan.___", state 1709, "else"
 803         line 262, "pan.___", state 1718, "(!(cache_dirty_urcu_gp_ctr))"
 804         line 262, "pan.___", state 1718, "else"
 805         line 295, "pan.___", state 1720, "(cache_dirty_urcu_gp_ctr)"
 806         line 295, "pan.___", state 1720, "else"
 807         line 1300, "pan.___", state 1721, "(cache_dirty_urcu_gp_ctr)"
 808         line 1300, "pan.___", state 1721, "else"
 809         line 1304, "pan.___", state 1724, "-end-"
 810         (312 of 1724 states)
 811 unreached in proctype :init:
 812         line 1319, "pan.___", state 13, "((i<1))"
 813         line 1319, "pan.___", state 13, "((i>=1))"
 814         (1 of 28 states)
 815 unreached in proctype :never:
 816         line 1367, "pan.___", state 8, "-end-"
 817         (1 of 8 states)
 818
 819 pan: elapsed time 792 seconds
 820 pan: rate 3330.8797 states/second
 821 pan: avg transition delay 1.5481e-06 usec
 822 cp .input.spin urcu_free_no_mb.spin.input
 823 cp .input.spin.trail urcu_free_no_mb.spin.input.trail
 824 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-alpha-ipi'