formal-model/urcu-controldataflow-intel-ipi-compress/urcu_progress_writer_error.log

   1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-intel-ipi-compress'
   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_progress.ltl | grep -v ^//`)" >> pan.ltl
   7 cp urcu_progress_writer_error.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 -f -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 1363)
  19 depth 7: Claim reached state 9 (line 1368)
  20 depth 50: Claim reached state 9 (line 1367)
  21 Depth=    7070 States=    1e+06 Transitions= 1.16e+07 Memory=   492.912 t=   33.7 R=   3e+04
  22 Depth=    7070 States=    2e+06 Transitions= 2.31e+07 Memory=   521.233 t=     68 R=   3e+04
  23 Depth=    7070 States=    3e+06 Transitions= 3.43e+07 Memory=   549.358 t=    102 R=   3e+04
  24 pan: resizing hashtable to -w22..  done
  25 pan: acceptance cycle (at depth 1558)
  26 pan: wrote .input.spin.trail
  27
  28 (Spin Version 5.1.7 -- 23 December 2008)
  29 Warning: Search not completed
  30         + Partial Order Reduction
  31         + Compression
  32
  33 Full statespace search for:
  34         never claim             +
  35         assertion violations    + (if within scope of claim)
  36         acceptance   cycles     + (fairness enabled)
  37         invalid end states      - (disabled by never claim)
  38
  39 State-vector 80 byte, depth reached 7070, errors: 1
  40   1856640 states, stored (3.13554e+06 visited)
  41  32657997 states, matched
  42  35793542 transitions (= visited+matched)
  43 5.1088012e+08 atomic steps
  44 hash conflicts:  10885217 (resolved)
  45
  46 Stats on memory usage (in Megabytes):
  47   205.393       equivalent memory usage for states (stored*(State-vector + overhead))
  48    93.456       actual memory usage for states (compression: 45.50%)
  49                 state-vector as stored = 17 byte + 36 byte overhead
  50    32.000       memory used for hash table (-w22)
  51   457.764       memory used for DFS stack (-m10000000)
  52   583.115       total actual memory usage
  53
  54 nr of templates: [ globals chans procs ]
  55 collapse counts: [ 12368 744 254 2 2 ]
  56 unreached in proctype urcu_reader
  57         line 269, "pan.___", state 57, "cache_dirty_urcu_gp_ctr = 0"
  58         line 277, "pan.___", state 79, "cache_dirty_rcu_ptr = 0"
  59         line 281, "pan.___", state 88, "cache_dirty_rcu_data[i] = 0"
  60         line 246, "pan.___", state 104, "(1)"
  61         line 250, "pan.___", state 112, "(1)"
  62         line 254, "pan.___", state 124, "(1)"
  63         line 258, "pan.___", state 132, "(1)"
  64         line 408, "pan.___", state 158, "cache_dirty_urcu_gp_ctr = 0"
  65         line 417, "pan.___", state 190, "cache_dirty_rcu_ptr = 0"
  66         line 421, "pan.___", state 204, "cache_dirty_rcu_data[i] = 0"
  67         line 246, "pan.___", state 222, "(1)"
  68         line 254, "pan.___", state 242, "(1)"
  69         line 258, "pan.___", state 250, "(1)"
  70         line 688, "pan.___", state 269, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  71         line 408, "pan.___", state 276, "cache_dirty_urcu_gp_ctr = 0"
  72         line 417, "pan.___", state 308, "cache_dirty_rcu_ptr = 0"
  73         line 421, "pan.___", state 322, "cache_dirty_rcu_data[i] = 0"
  74         line 246, "pan.___", state 340, "(1)"
  75         line 254, "pan.___", state 360, "(1)"
  76         line 258, "pan.___", state 368, "(1)"
  77         line 408, "pan.___", state 387, "cache_dirty_urcu_gp_ctr = 0"
  78         line 417, "pan.___", state 419, "cache_dirty_rcu_ptr = 0"
  79         line 421, "pan.___", state 433, "cache_dirty_rcu_data[i] = 0"
  80         line 246, "pan.___", state 451, "(1)"
  81         line 254, "pan.___", state 471, "(1)"
  82         line 258, "pan.___", state 479, "(1)"
  83         line 408, "pan.___", state 500, "cache_dirty_urcu_gp_ctr = 0"
  84         line 408, "pan.___", state 502, "(1)"
  85         line 408, "pan.___", state 503, "(cache_dirty_urcu_gp_ctr)"
  86         line 408, "pan.___", state 503, "else"
  87         line 408, "pan.___", state 506, "(1)"
  88         line 412, "pan.___", state 514, "cache_dirty_urcu_active_readers = 0"
  89         line 412, "pan.___", state 516, "(1)"
  90         line 412, "pan.___", state 517, "(cache_dirty_urcu_active_readers)"
  91         line 412, "pan.___", state 517, "else"
  92         line 412, "pan.___", state 520, "(1)"
  93         line 412, "pan.___", state 521, "(1)"
  94         line 412, "pan.___", state 521, "(1)"
  95         line 410, "pan.___", state 526, "((i<1))"
  96         line 410, "pan.___", state 526, "((i>=1))"
  97         line 417, "pan.___", state 532, "cache_dirty_rcu_ptr = 0"
  98         line 417, "pan.___", state 534, "(1)"
  99         line 417, "pan.___", state 535, "(cache_dirty_rcu_ptr)"
 100         line 417, "pan.___", state 535, "else"
 101         line 417, "pan.___", state 538, "(1)"
 102         line 417, "pan.___", state 539, "(1)"
 103         line 417, "pan.___", state 539, "(1)"
 104         line 421, "pan.___", state 546, "cache_dirty_rcu_data[i] = 0"
 105         line 421, "pan.___", state 548, "(1)"
 106         line 421, "pan.___", state 549, "(cache_dirty_rcu_data[i])"
 107         line 421, "pan.___", state 549, "else"
 108         line 421, "pan.___", state 552, "(1)"
 109         line 421, "pan.___", state 553, "(1)"
 110         line 421, "pan.___", state 553, "(1)"
 111         line 419, "pan.___", state 558, "((i<2))"
 112         line 419, "pan.___", state 558, "((i>=2))"
 113         line 246, "pan.___", state 564, "(1)"
 114         line 250, "pan.___", state 572, "(1)"
 115         line 250, "pan.___", state 573, "(!(cache_dirty_urcu_active_readers))"
 116         line 250, "pan.___", state 573, "else"
 117         line 248, "pan.___", state 578, "((i<1))"
 118         line 248, "pan.___", state 578, "((i>=1))"
 119         line 254, "pan.___", state 584, "(1)"
 120         line 254, "pan.___", state 585, "(!(cache_dirty_rcu_ptr))"
 121         line 254, "pan.___", state 585, "else"
 122         line 258, "pan.___", state 592, "(1)"
 123         line 258, "pan.___", state 593, "(!(cache_dirty_rcu_data[i]))"
 124         line 258, "pan.___", state 593, "else"
 125         line 256, "pan.___", state 598, "((i<2))"
 126         line 256, "pan.___", state 598, "((i>=2))"
 127         line 263, "pan.___", state 602, "(!(cache_dirty_urcu_gp_ctr))"
 128         line 263, "pan.___", state 602, "else"
 129         line 428, "pan.___", state 604, "(1)"
 130         line 428, "pan.___", state 604, "(1)"
 131         line 688, "pan.___", state 607, "cached_urcu_active_readers = (tmp+1)"
 132         line 688, "pan.___", state 608, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 133         line 688, "pan.___", state 609, "(1)"
 134         line 408, "pan.___", state 616, "cache_dirty_urcu_gp_ctr = 0"
 135         line 417, "pan.___", state 648, "cache_dirty_rcu_ptr = 0"
 136         line 421, "pan.___", state 662, "cache_dirty_rcu_data[i] = 0"
 137         line 246, "pan.___", state 680, "(1)"
 138         line 254, "pan.___", state 700, "(1)"
 139         line 258, "pan.___", state 708, "(1)"
 140         line 408, "pan.___", state 734, "cache_dirty_urcu_gp_ctr = 0"
 141         line 417, "pan.___", state 766, "cache_dirty_rcu_ptr = 0"
 142         line 421, "pan.___", state 780, "cache_dirty_rcu_data[i] = 0"
 143         line 246, "pan.___", state 798, "(1)"
 144         line 254, "pan.___", state 818, "(1)"
 145         line 258, "pan.___", state 826, "(1)"
 146         line 408, "pan.___", state 845, "cache_dirty_urcu_gp_ctr = 0"
 147         line 408, "pan.___", state 847, "(1)"
 148         line 408, "pan.___", state 848, "(cache_dirty_urcu_gp_ctr)"
 149         line 408, "pan.___", state 848, "else"
 150         line 408, "pan.___", state 851, "(1)"
 151         line 412, "pan.___", state 859, "cache_dirty_urcu_active_readers = 0"
 152         line 412, "pan.___", state 861, "(1)"
 153         line 412, "pan.___", state 862, "(cache_dirty_urcu_active_readers)"
 154         line 412, "pan.___", state 862, "else"
 155         line 412, "pan.___", state 865, "(1)"
 156         line 412, "pan.___", state 866, "(1)"
 157         line 412, "pan.___", state 866, "(1)"
 158         line 410, "pan.___", state 871, "((i<1))"
 159         line 410, "pan.___", state 871, "((i>=1))"
 160         line 417, "pan.___", state 877, "cache_dirty_rcu_ptr = 0"
 161         line 417, "pan.___", state 879, "(1)"
 162         line 417, "pan.___", state 880, "(cache_dirty_rcu_ptr)"
 163         line 417, "pan.___", state 880, "else"
 164         line 417, "pan.___", state 883, "(1)"
 165         line 417, "pan.___", state 884, "(1)"
 166         line 417, "pan.___", state 884, "(1)"
 167         line 421, "pan.___", state 891, "cache_dirty_rcu_data[i] = 0"
 168         line 421, "pan.___", state 893, "(1)"
 169         line 421, "pan.___", state 894, "(cache_dirty_rcu_data[i])"
 170         line 421, "pan.___", state 894, "else"
 171         line 421, "pan.___", state 897, "(1)"
 172         line 421, "pan.___", state 898, "(1)"
 173         line 421, "pan.___", state 898, "(1)"
 174         line 419, "pan.___", state 903, "((i<2))"
 175         line 419, "pan.___", state 903, "((i>=2))"
 176         line 246, "pan.___", state 909, "(1)"
 177         line 250, "pan.___", state 917, "(1)"
 178         line 250, "pan.___", state 918, "(!(cache_dirty_urcu_active_readers))"
 179         line 250, "pan.___", state 918, "else"
 180         line 248, "pan.___", state 923, "((i<1))"
 181         line 248, "pan.___", state 923, "((i>=1))"
 182         line 254, "pan.___", state 929, "(1)"
 183         line 254, "pan.___", state 930, "(!(cache_dirty_rcu_ptr))"
 184         line 254, "pan.___", state 930, "else"
 185         line 258, "pan.___", state 937, "(1)"
 186         line 258, "pan.___", state 938, "(!(cache_dirty_rcu_data[i]))"
 187         line 258, "pan.___", state 938, "else"
 188         line 256, "pan.___", state 943, "((i<2))"
 189         line 256, "pan.___", state 943, "((i>=2))"
 190         line 263, "pan.___", state 947, "(!(cache_dirty_urcu_gp_ctr))"
 191         line 263, "pan.___", state 947, "else"
 192         line 428, "pan.___", state 949, "(1)"
 193         line 428, "pan.___", state 949, "(1)"
 194         line 696, "pan.___", state 953, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
 195         line 408, "pan.___", state 958, "cache_dirty_urcu_gp_ctr = 0"
 196         line 417, "pan.___", state 990, "cache_dirty_rcu_ptr = 0"
 197         line 421, "pan.___", state 1004, "cache_dirty_rcu_data[i] = 0"
 198         line 246, "pan.___", state 1022, "(1)"
 199         line 254, "pan.___", state 1042, "(1)"
 200         line 258, "pan.___", state 1050, "(1)"
 201         line 408, "pan.___", state 1072, "cache_dirty_urcu_gp_ctr = 0"
 202         line 417, "pan.___", state 1104, "cache_dirty_rcu_ptr = 0"
 203         line 421, "pan.___", state 1118, "cache_dirty_rcu_data[i] = 0"
 204         line 246, "pan.___", state 1136, "(1)"
 205         line 254, "pan.___", state 1156, "(1)"
 206         line 258, "pan.___", state 1164, "(1)"
 207         line 408, "pan.___", state 1187, "cache_dirty_urcu_gp_ctr = 0"
 208         line 417, "pan.___", state 1219, "cache_dirty_rcu_ptr = 0"
 209         line 421, "pan.___", state 1233, "cache_dirty_rcu_data[i] = 0"
 210         line 246, "pan.___", state 1251, "(1)"
 211         line 254, "pan.___", state 1271, "(1)"
 212         line 258, "pan.___", state 1279, "(1)"
 213         line 408, "pan.___", state 1298, "cache_dirty_urcu_gp_ctr = 0"
 214         line 417, "pan.___", state 1330, "cache_dirty_rcu_ptr = 0"
 215         line 421, "pan.___", state 1344, "cache_dirty_rcu_data[i] = 0"
 216         line 246, "pan.___", state 1362, "(1)"
 217         line 254, "pan.___", state 1382, "(1)"
 218         line 258, "pan.___", state 1390, "(1)"
 219         line 408, "pan.___", state 1414, "cache_dirty_urcu_gp_ctr = 0"
 220         line 417, "pan.___", state 1446, "cache_dirty_rcu_ptr = 0"
 221         line 421, "pan.___", state 1460, "cache_dirty_rcu_data[i] = 0"
 222         line 246, "pan.___", state 1478, "(1)"
 223         line 254, "pan.___", state 1498, "(1)"
 224         line 258, "pan.___", state 1506, "(1)"
 225         line 408, "pan.___", state 1525, "cache_dirty_urcu_gp_ctr = 0"
 226         line 417, "pan.___", state 1557, "cache_dirty_rcu_ptr = 0"
 227         line 421, "pan.___", state 1571, "cache_dirty_rcu_data[i] = 0"
 228         line 246, "pan.___", state 1589, "(1)"
 229         line 254, "pan.___", state 1609, "(1)"
 230         line 258, "pan.___", state 1617, "(1)"
 231         line 408, "pan.___", state 1639, "cache_dirty_urcu_gp_ctr = 0"
 232         line 417, "pan.___", state 1671, "cache_dirty_rcu_ptr = 0"
 233         line 421, "pan.___", state 1685, "cache_dirty_rcu_data[i] = 0"
 234         line 246, "pan.___", state 1703, "(1)"
 235         line 254, "pan.___", state 1723, "(1)"
 236         line 258, "pan.___", state 1731, "(1)"
 237         line 735, "pan.___", state 1750, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
 238         line 408, "pan.___", state 1757, "cache_dirty_urcu_gp_ctr = 0"
 239         line 417, "pan.___", state 1789, "cache_dirty_rcu_ptr = 0"
 240         line 421, "pan.___", state 1803, "cache_dirty_rcu_data[i] = 0"
 241         line 246, "pan.___", state 1821, "(1)"
 242         line 254, "pan.___", state 1841, "(1)"
 243         line 258, "pan.___", state 1849, "(1)"
 244         line 408, "pan.___", state 1868, "cache_dirty_urcu_gp_ctr = 0"
 245         line 417, "pan.___", state 1900, "cache_dirty_rcu_ptr = 0"
 246         line 421, "pan.___", state 1914, "cache_dirty_rcu_data[i] = 0"
 247         line 246, "pan.___", state 1932, "(1)"
 248         line 254, "pan.___", state 1952, "(1)"
 249         line 258, "pan.___", state 1960, "(1)"
 250         line 408, "pan.___", state 1981, "cache_dirty_urcu_gp_ctr = 0"
 251         line 408, "pan.___", state 1983, "(1)"
 252         line 408, "pan.___", state 1984, "(cache_dirty_urcu_gp_ctr)"
 253         line 408, "pan.___", state 1984, "else"
 254         line 408, "pan.___", state 1987, "(1)"
 255         line 412, "pan.___", state 1995, "cache_dirty_urcu_active_readers = 0"
 256         line 412, "pan.___", state 1997, "(1)"
 257         line 412, "pan.___", state 1998, "(cache_dirty_urcu_active_readers)"
 258         line 412, "pan.___", state 1998, "else"
 259         line 412, "pan.___", state 2001, "(1)"
 260         line 412, "pan.___", state 2002, "(1)"
 261         line 412, "pan.___", state 2002, "(1)"
 262         line 410, "pan.___", state 2007, "((i<1))"
 263         line 410, "pan.___", state 2007, "((i>=1))"
 264         line 417, "pan.___", state 2013, "cache_dirty_rcu_ptr = 0"
 265         line 417, "pan.___", state 2015, "(1)"
 266         line 417, "pan.___", state 2016, "(cache_dirty_rcu_ptr)"
 267         line 417, "pan.___", state 2016, "else"
 268         line 417, "pan.___", state 2019, "(1)"
 269         line 417, "pan.___", state 2020, "(1)"
 270         line 417, "pan.___", state 2020, "(1)"
 271         line 421, "pan.___", state 2027, "cache_dirty_rcu_data[i] = 0"
 272         line 421, "pan.___", state 2029, "(1)"
 273         line 421, "pan.___", state 2030, "(cache_dirty_rcu_data[i])"
 274         line 421, "pan.___", state 2030, "else"
 275         line 421, "pan.___", state 2033, "(1)"
 276         line 421, "pan.___", state 2034, "(1)"
 277         line 421, "pan.___", state 2034, "(1)"
 278         line 419, "pan.___", state 2039, "((i<2))"
 279         line 419, "pan.___", state 2039, "((i>=2))"
 280         line 246, "pan.___", state 2045, "(1)"
 281         line 250, "pan.___", state 2053, "(1)"
 282         line 250, "pan.___", state 2054, "(!(cache_dirty_urcu_active_readers))"
 283         line 250, "pan.___", state 2054, "else"
 284         line 248, "pan.___", state 2059, "((i<1))"
 285         line 248, "pan.___", state 2059, "((i>=1))"
 286         line 254, "pan.___", state 2065, "(1)"
 287         line 254, "pan.___", state 2066, "(!(cache_dirty_rcu_ptr))"
 288         line 254, "pan.___", state 2066, "else"
 289         line 258, "pan.___", state 2073, "(1)"
 290         line 258, "pan.___", state 2074, "(!(cache_dirty_rcu_data[i]))"
 291         line 258, "pan.___", state 2074, "else"
 292         line 256, "pan.___", state 2079, "((i<2))"
 293         line 256, "pan.___", state 2079, "((i>=2))"
 294         line 263, "pan.___", state 2083, "(!(cache_dirty_urcu_gp_ctr))"
 295         line 263, "pan.___", state 2083, "else"
 296         line 428, "pan.___", state 2085, "(1)"
 297         line 428, "pan.___", state 2085, "(1)"
 298         line 735, "pan.___", state 2088, "cached_urcu_active_readers = (tmp+1)"
 299         line 735, "pan.___", state 2089, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
 300         line 735, "pan.___", state 2090, "(1)"
 301         line 408, "pan.___", state 2097, "cache_dirty_urcu_gp_ctr = 0"
 302         line 417, "pan.___", state 2129, "cache_dirty_rcu_ptr = 0"
 303         line 421, "pan.___", state 2143, "cache_dirty_rcu_data[i] = 0"
 304         line 246, "pan.___", state 2161, "(1)"
 305         line 254, "pan.___", state 2181, "(1)"
 306         line 258, "pan.___", state 2189, "(1)"
 307         line 408, "pan.___", state 2214, "cache_dirty_urcu_gp_ctr = 0"
 308         line 417, "pan.___", state 2246, "cache_dirty_rcu_ptr = 0"
 309         line 421, "pan.___", state 2260, "cache_dirty_rcu_data[i] = 0"
 310         line 246, "pan.___", state 2278, "(1)"
 311         line 254, "pan.___", state 2298, "(1)"
 312         line 258, "pan.___", state 2306, "(1)"
 313         line 408, "pan.___", state 2325, "cache_dirty_urcu_gp_ctr = 0"
 314         line 417, "pan.___", state 2357, "cache_dirty_rcu_ptr = 0"
 315         line 421, "pan.___", state 2371, "cache_dirty_rcu_data[i] = 0"
 316         line 246, "pan.___", state 2389, "(1)"
 317         line 254, "pan.___", state 2409, "(1)"
 318         line 258, "pan.___", state 2417, "(1)"
 319         line 246, "pan.___", state 2448, "(1)"
 320         line 254, "pan.___", state 2468, "(1)"
 321         line 258, "pan.___", state 2476, "(1)"
 322         line 246, "pan.___", state 2491, "(1)"
 323         line 254, "pan.___", state 2511, "(1)"
 324         line 258, "pan.___", state 2519, "(1)"
 325         line 930, "pan.___", state 2536, "-end-"
 326         (221 of 2536 states)
 327 unreached in proctype urcu_writer
 328         line 408, "pan.___", state 45, "cache_dirty_urcu_gp_ctr = 0"
 329         line 412, "pan.___", state 59, "cache_dirty_urcu_active_readers = 0"
 330         line 417, "pan.___", state 77, "cache_dirty_rcu_ptr = 0"
 331         line 246, "pan.___", state 109, "(1)"
 332         line 250, "pan.___", state 117, "(1)"
 333         line 254, "pan.___", state 129, "(1)"
 334         line 269, "pan.___", state 158, "cache_dirty_urcu_gp_ctr = 0"
 335         line 273, "pan.___", state 167, "cache_dirty_urcu_active_readers = 0"
 336         line 277, "pan.___", state 180, "cache_dirty_rcu_ptr = 0"
 337         line 408, "pan.___", state 220, "cache_dirty_urcu_gp_ctr = 0"
 338         line 412, "pan.___", state 234, "cache_dirty_urcu_active_readers = 0"
 339         line 417, "pan.___", state 252, "cache_dirty_rcu_ptr = 0"
 340         line 421, "pan.___", state 266, "cache_dirty_rcu_data[i] = 0"
 341         line 246, "pan.___", state 284, "(1)"
 342         line 250, "pan.___", state 292, "(1)"
 343         line 254, "pan.___", state 304, "(1)"
 344         line 258, "pan.___", state 312, "(1)"
 345         line 412, "pan.___", state 347, "cache_dirty_urcu_active_readers = 0"
 346         line 417, "pan.___", state 365, "cache_dirty_rcu_ptr = 0"
 347         line 421, "pan.___", state 379, "cache_dirty_rcu_data[i] = 0"
 348         line 250, "pan.___", state 405, "(1)"
 349         line 254, "pan.___", state 417, "(1)"
 350         line 258, "pan.___", state 425, "(1)"
 351         line 408, "pan.___", state 450, "cache_dirty_urcu_gp_ctr = 0"
 352         line 408, "pan.___", state 452, "(1)"
 353         line 408, "pan.___", state 453, "(cache_dirty_urcu_gp_ctr)"
 354         line 408, "pan.___", state 453, "else"
 355         line 408, "pan.___", state 456, "(1)"
 356         line 412, "pan.___", state 464, "cache_dirty_urcu_active_readers = 0"
 357         line 412, "pan.___", state 466, "(1)"
 358         line 412, "pan.___", state 467, "(cache_dirty_urcu_active_readers)"
 359         line 412, "pan.___", state 467, "else"
 360         line 412, "pan.___", state 470, "(1)"
 361         line 412, "pan.___", state 471, "(1)"
 362         line 412, "pan.___", state 471, "(1)"
 363         line 410, "pan.___", state 476, "((i<1))"
 364         line 410, "pan.___", state 476, "((i>=1))"
 365         line 417, "pan.___", state 482, "cache_dirty_rcu_ptr = 0"
 366         line 417, "pan.___", state 484, "(1)"
 367         line 417, "pan.___", state 485, "(cache_dirty_rcu_ptr)"
 368         line 417, "pan.___", state 485, "else"
 369         line 417, "pan.___", state 488, "(1)"
 370         line 417, "pan.___", state 489, "(1)"
 371         line 417, "pan.___", state 489, "(1)"
 372         line 421, "pan.___", state 496, "cache_dirty_rcu_data[i] = 0"
 373         line 421, "pan.___", state 498, "(1)"
 374         line 421, "pan.___", state 499, "(cache_dirty_rcu_data[i])"
 375         line 421, "pan.___", state 499, "else"
 376         line 421, "pan.___", state 502, "(1)"
 377         line 421, "pan.___", state 503, "(1)"
 378         line 421, "pan.___", state 503, "(1)"
 379         line 419, "pan.___", state 508, "((i<2))"
 380         line 419, "pan.___", state 508, "((i>=2))"
 381         line 246, "pan.___", state 514, "(1)"
 382         line 250, "pan.___", state 522, "(1)"
 383         line 250, "pan.___", state 523, "(!(cache_dirty_urcu_active_readers))"
 384         line 250, "pan.___", state 523, "else"
 385         line 248, "pan.___", state 528, "((i<1))"
 386         line 248, "pan.___", state 528, "((i>=1))"
 387         line 254, "pan.___", state 534, "(1)"
 388         line 254, "pan.___", state 535, "(!(cache_dirty_rcu_ptr))"
 389         line 254, "pan.___", state 535, "else"
 390         line 258, "pan.___", state 542, "(1)"
 391         line 258, "pan.___", state 543, "(!(cache_dirty_rcu_data[i]))"
 392         line 258, "pan.___", state 543, "else"
 393         line 263, "pan.___", state 552, "(!(cache_dirty_urcu_gp_ctr))"
 394         line 263, "pan.___", state 552, "else"
 395         line 428, "pan.___", state 554, "(1)"
 396         line 428, "pan.___", state 554, "(1)"
 397         line 412, "pan.___", state 574, "cache_dirty_urcu_active_readers = 0"
 398         line 417, "pan.___", state 592, "cache_dirty_rcu_ptr = 0"
 399         line 421, "pan.___", state 606, "cache_dirty_rcu_data[i] = 0"
 400         line 250, "pan.___", state 632, "(1)"
 401         line 254, "pan.___", state 644, "(1)"
 402         line 258, "pan.___", state 652, "(1)"
 403         line 412, "pan.___", state 685, "cache_dirty_urcu_active_readers = 0"
 404         line 417, "pan.___", state 703, "cache_dirty_rcu_ptr = 0"
 405         line 421, "pan.___", state 717, "cache_dirty_rcu_data[i] = 0"
 406         line 250, "pan.___", state 743, "(1)"
 407         line 254, "pan.___", state 755, "(1)"
 408         line 258, "pan.___", state 763, "(1)"
 409         line 412, "pan.___", state 798, "cache_dirty_urcu_active_readers = 0"
 410         line 417, "pan.___", state 816, "cache_dirty_rcu_ptr = 0"
 411         line 421, "pan.___", state 830, "cache_dirty_rcu_data[i] = 0"
 412         line 250, "pan.___", state 856, "(1)"
 413         line 254, "pan.___", state 868, "(1)"
 414         line 258, "pan.___", state 876, "(1)"
 415         line 412, "pan.___", state 914, "cache_dirty_urcu_active_readers = 0"
 416         line 417, "pan.___", state 932, "cache_dirty_rcu_ptr = 0"
 417         line 421, "pan.___", state 946, "cache_dirty_rcu_data[i] = 0"
 418         line 250, "pan.___", state 972, "(1)"
 419         line 254, "pan.___", state 984, "(1)"
 420         line 258, "pan.___", state 992, "(1)"
 421         line 269, "pan.___", state 1036, "cache_dirty_urcu_gp_ctr = 0"
 422         line 273, "pan.___", state 1045, "cache_dirty_urcu_active_readers = 0"
 423         line 277, "pan.___", state 1060, "(1)"
 424         line 281, "pan.___", state 1067, "cache_dirty_rcu_data[i] = 0"
 425         line 246, "pan.___", state 1083, "(1)"
 426         line 250, "pan.___", state 1091, "(1)"
 427         line 254, "pan.___", state 1103, "(1)"
 428         line 258, "pan.___", state 1111, "(1)"
 429         line 269, "pan.___", state 1142, "cache_dirty_urcu_gp_ctr = 0"
 430         line 273, "pan.___", state 1151, "cache_dirty_urcu_active_readers = 0"
 431         line 277, "pan.___", state 1164, "cache_dirty_rcu_ptr = 0"
 432         line 281, "pan.___", state 1173, "cache_dirty_rcu_data[i] = 0"
 433         line 246, "pan.___", state 1189, "(1)"
 434         line 250, "pan.___", state 1197, "(1)"
 435         line 254, "pan.___", state 1209, "(1)"
 436         line 258, "pan.___", state 1217, "(1)"
 437         line 273, "pan.___", state 1243, "cache_dirty_urcu_active_readers = 0"
 438         line 277, "pan.___", state 1256, "cache_dirty_rcu_ptr = 0"
 439         line 281, "pan.___", state 1265, "cache_dirty_rcu_data[i] = 0"
 440         line 246, "pan.___", state 1281, "(1)"
 441         line 250, "pan.___", state 1289, "(1)"
 442         line 254, "pan.___", state 1301, "(1)"
 443         line 258, "pan.___", state 1309, "(1)"
 444         line 269, "pan.___", state 1340, "cache_dirty_urcu_gp_ctr = 0"
 445         line 273, "pan.___", state 1349, "cache_dirty_urcu_active_readers = 0"
 446         line 277, "pan.___", state 1362, "cache_dirty_rcu_ptr = 0"
 447         line 281, "pan.___", state 1371, "cache_dirty_rcu_data[i] = 0"
 448         line 246, "pan.___", state 1387, "(1)"
 449         line 250, "pan.___", state 1395, "(1)"
 450         line 254, "pan.___", state 1407, "(1)"
 451         line 258, "pan.___", state 1415, "(1)"
 452         line 1305, "pan.___", state 1431, "-end-"
 453         (110 of 1431 states)
 454 unreached in proctype :init:
 455         (0 of 28 states)
 456 unreached in proctype :never:
 457         line 1370, "pan.___", state 11, "-end-"
 458         (1 of 11 states)
 459
 460 pan: elapsed time 106 seconds
 461 pan: rate 29466.638 states/second
 462 pan: avg transition delay 2.9729e-06 usec
 463 cp .input.spin urcu_progress_writer_error.spin.input
 464 cp .input.spin.trail urcu_progress_writer_error.spin.input.trail
 465 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-intel-ipi-compress'