formal-model/urcu-controldataflow-alpha-no-ipi/asserts.log

   1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-alpha-no-ipi'
   2 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
   3 cat DEFINES > .input.spin
   4 cat urcu.spin >> .input.spin
   5 rm -f .input.spin.trail
   6 spin -a -X .input.spin
   7 Exit-Status 0
   8 gcc -O2 -w -DHASH64 -DSAFETY -o pan pan.c
   9 ./pan -v -c1 -X -m10000000 -w20
  10 Depth=    4773 States=    1e+06 Transitions= 6.22e+08 Memory=   542.717 t=    624 R=   2e+03
  11 Depth=    5040 States=    2e+06 Transitions=  1.3e+09 Memory=   618.986 t= 1.33e+03 R=   1e+03
  12 Depth=    5040 States=    3e+06 Transitions= 1.95e+09 Memory=   695.256 t= 2.03e+03 R=   1e+03
  13 pan: resizing hashtable to -w22..  done
  14 Depth=    5040 States=    4e+06 Transitions= 2.64e+09 Memory=   802.647 t= 2.73e+03 R=   1e+03
  15 Depth=    5040 States=    5e+06 Transitions=  3.3e+09 Memory=   878.916 t= 3.41e+03 R=   1e+03
  16 Depth=    5141 States=    6e+06 Transitions= 3.99e+09 Memory=   955.186 t= 4.12e+03 R=   1e+03
  17
  18 (Spin Version 5.1.7 -- 23 December 2008)
  19         + Partial Order Reduction
  20
  21 Full statespace search for:
  22         never claim             - (none specified)
  23         assertion violations    +
  24         cycle checks            - (disabled by -DSAFETY)
  25         invalid end states      +
  26
  27 State-vector 72 byte, depth reached 5141, errors: 0
  28   6711104 states, stored
  29 4.4393201e+09 states, matched
  30 4.4460312e+09 transitions (= stored+matched)
  31 2.5322962e+10 atomic steps
  32 hash conflicts: 3.3332015e+09 (resolved)
  33
  34 Stats on memory usage (in Megabytes):
  35   640.021       equivalent memory usage for states (stored*(State-vector + overhead))
  36   519.783       actual memory usage for states (compression: 81.21%)
  37                 state-vector as stored = 53 byte + 28 byte overhead
  38    32.000       memory used for hash table (-w22)
  39   457.764       memory used for DFS stack (-m10000000)
  40  1009.483       total actual memory usage
  41
  42 unreached in proctype urcu_reader
  43         line 410, ".input.spin", state 17, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  44         line 419, ".input.spin", state 49, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  45         line 423, ".input.spin", state 63, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  46         line 428, ".input.spin", state 82, "(1)"
  47         line 437, ".input.spin", state 112, "(1)"
  48         line 441, ".input.spin", state 125, "(1)"
  49         line 596, ".input.spin", state 146, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
  50         line 410, ".input.spin", state 153, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  51         line 419, ".input.spin", state 185, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  52         line 423, ".input.spin", state 199, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  53         line 428, ".input.spin", state 218, "(1)"
  54         line 437, ".input.spin", state 248, "(1)"
  55         line 441, ".input.spin", state 261, "(1)"
  56         line 410, ".input.spin", state 282, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  57         line 419, ".input.spin", state 314, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  58         line 423, ".input.spin", state 328, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  59         line 428, ".input.spin", state 347, "(1)"
  60         line 437, ".input.spin", state 377, "(1)"
  61         line 441, ".input.spin", state 390, "(1)"
  62         line 410, ".input.spin", state 413, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  63         line 410, ".input.spin", state 415, "(1)"
  64         line 410, ".input.spin", state 416, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
  65         line 410, ".input.spin", state 416, "else"
  66         line 410, ".input.spin", state 419, "(1)"
  67         line 414, ".input.spin", state 427, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  68         line 414, ".input.spin", state 429, "(1)"
  69         line 414, ".input.spin", state 430, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
  70         line 414, ".input.spin", state 430, "else"
  71         line 414, ".input.spin", state 433, "(1)"
  72         line 414, ".input.spin", state 434, "(1)"
  73         line 414, ".input.spin", state 434, "(1)"
  74         line 412, ".input.spin", state 439, "((i<1))"
  75         line 412, ".input.spin", state 439, "((i>=1))"
  76         line 419, ".input.spin", state 445, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
  77         line 419, ".input.spin", state 447, "(1)"
  78         line 419, ".input.spin", state 448, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
  79         line 419, ".input.spin", state 448, "else"
  80         line 419, ".input.spin", state 451, "(1)"
  81         line 419, ".input.spin", state 452, "(1)"
  82         line 419, ".input.spin", state 452, "(1)"
  83         line 423, ".input.spin", state 459, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
  84         line 423, ".input.spin", state 461, "(1)"
  85         line 423, ".input.spin", state 462, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
  86         line 423, ".input.spin", state 462, "else"
  87         line 423, ".input.spin", state 465, "(1)"
  88         line 423, ".input.spin", state 466, "(1)"
  89         line 423, ".input.spin", state 466, "(1)"
  90         line 421, ".input.spin", state 471, "((i<2))"
  91         line 421, ".input.spin", state 471, "((i>=2))"
  92         line 428, ".input.spin", state 478, "(1)"
  93         line 428, ".input.spin", state 479, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
  94         line 428, ".input.spin", state 479, "else"
  95         line 428, ".input.spin", state 482, "(1)"
  96         line 428, ".input.spin", state 483, "(1)"
  97         line 428, ".input.spin", state 483, "(1)"
  98         line 432, ".input.spin", state 491, "(1)"
  99         line 432, ".input.spin", state 492, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 100         line 432, ".input.spin", state 492, "else"
 101         line 432, ".input.spin", state 495, "(1)"
 102         line 432, ".input.spin", state 496, "(1)"
 103         line 432, ".input.spin", state 496, "(1)"
 104         line 430, ".input.spin", state 501, "((i<1))"
 105         line 430, ".input.spin", state 501, "((i>=1))"
 106         line 437, ".input.spin", state 508, "(1)"
 107         line 437, ".input.spin", state 509, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 108         line 437, ".input.spin", state 509, "else"
 109         line 437, ".input.spin", state 512, "(1)"
 110         line 437, ".input.spin", state 513, "(1)"
 111         line 437, ".input.spin", state 513, "(1)"
 112         line 441, ".input.spin", state 521, "(1)"
 113         line 441, ".input.spin", state 522, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 114         line 441, ".input.spin", state 522, "else"
 115         line 441, ".input.spin", state 525, "(1)"
 116         line 441, ".input.spin", state 526, "(1)"
 117         line 441, ".input.spin", state 526, "(1)"
 118         line 439, ".input.spin", state 531, "((i<2))"
 119         line 439, ".input.spin", state 531, "((i>=2))"
 120         line 449, ".input.spin", state 535, "(1)"
 121         line 449, ".input.spin", state 535, "(1)"
 122         line 596, ".input.spin", state 538, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 123         line 596, ".input.spin", state 539, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
 124         line 596, ".input.spin", state 540, "(1)"
 125         line 271, ".input.spin", state 544, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 126         line 275, ".input.spin", state 555, "(1)"
 127         line 279, ".input.spin", state 566, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 128         line 283, ".input.spin", state 575, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 129         line 248, ".input.spin", state 591, "(1)"
 130         line 252, ".input.spin", state 599, "(1)"
 131         line 256, ".input.spin", state 611, "(1)"
 132         line 260, ".input.spin", state 619, "(1)"
 133         line 410, ".input.spin", state 637, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 134         line 414, ".input.spin", state 651, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 135         line 419, ".input.spin", state 669, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 136         line 423, ".input.spin", state 683, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 137         line 428, ".input.spin", state 702, "(1)"
 138         line 432, ".input.spin", state 715, "(1)"
 139         line 437, ".input.spin", state 732, "(1)"
 140         line 441, ".input.spin", state 745, "(1)"
 141         line 410, ".input.spin", state 773, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 142         line 419, ".input.spin", state 805, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 143         line 423, ".input.spin", state 819, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 144         line 428, ".input.spin", state 838, "(1)"
 145         line 437, ".input.spin", state 868, "(1)"
 146         line 441, ".input.spin", state 881, "(1)"
 147         line 410, ".input.spin", state 902, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 148         line 410, ".input.spin", state 904, "(1)"
 149         line 410, ".input.spin", state 905, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 150         line 410, ".input.spin", state 905, "else"
 151         line 410, ".input.spin", state 908, "(1)"
 152         line 414, ".input.spin", state 916, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 153         line 414, ".input.spin", state 918, "(1)"
 154         line 414, ".input.spin", state 919, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 155         line 414, ".input.spin", state 919, "else"
 156         line 414, ".input.spin", state 922, "(1)"
 157         line 414, ".input.spin", state 923, "(1)"
 158         line 414, ".input.spin", state 923, "(1)"
 159         line 412, ".input.spin", state 928, "((i<1))"
 160         line 412, ".input.spin", state 928, "((i>=1))"
 161         line 419, ".input.spin", state 934, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 162         line 419, ".input.spin", state 936, "(1)"
 163         line 419, ".input.spin", state 937, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 164         line 419, ".input.spin", state 937, "else"
 165         line 419, ".input.spin", state 940, "(1)"
 166         line 419, ".input.spin", state 941, "(1)"
 167         line 419, ".input.spin", state 941, "(1)"
 168         line 423, ".input.spin", state 948, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 169         line 423, ".input.spin", state 950, "(1)"
 170         line 423, ".input.spin", state 951, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 171         line 423, ".input.spin", state 951, "else"
 172         line 423, ".input.spin", state 954, "(1)"
 173         line 423, ".input.spin", state 955, "(1)"
 174         line 423, ".input.spin", state 955, "(1)"
 175         line 421, ".input.spin", state 960, "((i<2))"
 176         line 421, ".input.spin", state 960, "((i>=2))"
 177         line 428, ".input.spin", state 967, "(1)"
 178         line 428, ".input.spin", state 968, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 179         line 428, ".input.spin", state 968, "else"
 180         line 428, ".input.spin", state 971, "(1)"
 181         line 428, ".input.spin", state 972, "(1)"
 182         line 428, ".input.spin", state 972, "(1)"
 183         line 432, ".input.spin", state 980, "(1)"
 184         line 432, ".input.spin", state 981, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 185         line 432, ".input.spin", state 981, "else"
 186         line 432, ".input.spin", state 984, "(1)"
 187         line 432, ".input.spin", state 985, "(1)"
 188         line 432, ".input.spin", state 985, "(1)"
 189         line 430, ".input.spin", state 990, "((i<1))"
 190         line 430, ".input.spin", state 990, "((i>=1))"
 191         line 437, ".input.spin", state 997, "(1)"
 192         line 437, ".input.spin", state 998, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 193         line 437, ".input.spin", state 998, "else"
 194         line 437, ".input.spin", state 1001, "(1)"
 195         line 437, ".input.spin", state 1002, "(1)"
 196         line 437, ".input.spin", state 1002, "(1)"
 197         line 441, ".input.spin", state 1010, "(1)"
 198         line 441, ".input.spin", state 1011, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 199         line 441, ".input.spin", state 1011, "else"
 200         line 441, ".input.spin", state 1014, "(1)"
 201         line 441, ".input.spin", state 1015, "(1)"
 202         line 441, ".input.spin", state 1015, "(1)"
 203         line 439, ".input.spin", state 1020, "((i<2))"
 204         line 439, ".input.spin", state 1020, "((i>=2))"
 205         line 449, ".input.spin", state 1024, "(1)"
 206         line 449, ".input.spin", state 1024, "(1)"
 207         line 604, ".input.spin", state 1028, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
 208         line 410, ".input.spin", state 1033, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 209         line 414, ".input.spin", state 1047, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 210         line 419, ".input.spin", state 1065, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 211         line 423, ".input.spin", state 1079, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 212         line 428, ".input.spin", state 1098, "(1)"
 213         line 432, ".input.spin", state 1111, "(1)"
 214         line 437, ".input.spin", state 1128, "(1)"
 215         line 441, ".input.spin", state 1141, "(1)"
 216         line 410, ".input.spin", state 1165, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 217         line 419, ".input.spin", state 1197, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 218         line 423, ".input.spin", state 1211, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 219         line 428, ".input.spin", state 1230, "(1)"
 220         line 437, ".input.spin", state 1260, "(1)"
 221         line 441, ".input.spin", state 1273, "(1)"
 222         line 410, ".input.spin", state 1298, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 223         line 419, ".input.spin", state 1330, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 224         line 423, ".input.spin", state 1344, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 225         line 428, ".input.spin", state 1363, "(1)"
 226         line 437, ".input.spin", state 1393, "(1)"
 227         line 441, ".input.spin", state 1406, "(1)"
 228         line 410, ".input.spin", state 1427, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 229         line 419, ".input.spin", state 1459, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 230         line 423, ".input.spin", state 1473, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 231         line 428, ".input.spin", state 1492, "(1)"
 232         line 437, ".input.spin", state 1522, "(1)"
 233         line 441, ".input.spin", state 1535, "(1)"
 234         line 271, ".input.spin", state 1558, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 235         line 279, ".input.spin", state 1580, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 236         line 283, ".input.spin", state 1589, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 237         line 248, ".input.spin", state 1605, "(1)"
 238         line 252, ".input.spin", state 1613, "(1)"
 239         line 256, ".input.spin", state 1625, "(1)"
 240         line 260, ".input.spin", state 1633, "(1)"
 241         line 410, ".input.spin", state 1651, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 242         line 414, ".input.spin", state 1665, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 243         line 419, ".input.spin", state 1683, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 244         line 423, ".input.spin", state 1697, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 245         line 428, ".input.spin", state 1716, "(1)"
 246         line 432, ".input.spin", state 1729, "(1)"
 247         line 437, ".input.spin", state 1746, "(1)"
 248         line 441, ".input.spin", state 1759, "(1)"
 249         line 410, ".input.spin", state 1780, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 250         line 414, ".input.spin", state 1794, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 251         line 419, ".input.spin", state 1812, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 252         line 423, ".input.spin", state 1826, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 253         line 428, ".input.spin", state 1845, "(1)"
 254         line 432, ".input.spin", state 1858, "(1)"
 255         line 437, ".input.spin", state 1875, "(1)"
 256         line 441, ".input.spin", state 1888, "(1)"
 257         line 410, ".input.spin", state 1912, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 258         line 419, ".input.spin", state 1944, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 259         line 423, ".input.spin", state 1958, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 260         line 428, ".input.spin", state 1977, "(1)"
 261         line 437, ".input.spin", state 2007, "(1)"
 262         line 441, ".input.spin", state 2020, "(1)"
 263         line 643, ".input.spin", state 2041, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
 264         line 410, ".input.spin", state 2048, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 265         line 419, ".input.spin", state 2080, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 266         line 423, ".input.spin", state 2094, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 267         line 428, ".input.spin", state 2113, "(1)"
 268         line 437, ".input.spin", state 2143, "(1)"
 269         line 441, ".input.spin", state 2156, "(1)"
 270         line 410, ".input.spin", state 2177, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 271         line 419, ".input.spin", state 2209, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 272         line 423, ".input.spin", state 2223, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 273         line 428, ".input.spin", state 2242, "(1)"
 274         line 437, ".input.spin", state 2272, "(1)"
 275         line 441, ".input.spin", state 2285, "(1)"
 276         line 410, ".input.spin", state 2308, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 277         line 410, ".input.spin", state 2310, "(1)"
 278         line 410, ".input.spin", state 2311, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 279         line 410, ".input.spin", state 2311, "else"
 280         line 410, ".input.spin", state 2314, "(1)"
 281         line 414, ".input.spin", state 2322, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 282         line 414, ".input.spin", state 2324, "(1)"
 283         line 414, ".input.spin", state 2325, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 284         line 414, ".input.spin", state 2325, "else"
 285         line 414, ".input.spin", state 2328, "(1)"
 286         line 414, ".input.spin", state 2329, "(1)"
 287         line 414, ".input.spin", state 2329, "(1)"
 288         line 412, ".input.spin", state 2334, "((i<1))"
 289         line 412, ".input.spin", state 2334, "((i>=1))"
 290         line 419, ".input.spin", state 2340, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 291         line 419, ".input.spin", state 2342, "(1)"
 292         line 419, ".input.spin", state 2343, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
 293         line 419, ".input.spin", state 2343, "else"
 294         line 419, ".input.spin", state 2346, "(1)"
 295         line 419, ".input.spin", state 2347, "(1)"
 296         line 419, ".input.spin", state 2347, "(1)"
 297         line 423, ".input.spin", state 2354, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 298         line 423, ".input.spin", state 2356, "(1)"
 299         line 423, ".input.spin", state 2357, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
 300         line 423, ".input.spin", state 2357, "else"
 301         line 423, ".input.spin", state 2360, "(1)"
 302         line 423, ".input.spin", state 2361, "(1)"
 303         line 423, ".input.spin", state 2361, "(1)"
 304         line 421, ".input.spin", state 2366, "((i<2))"
 305         line 421, ".input.spin", state 2366, "((i>=2))"
 306         line 428, ".input.spin", state 2373, "(1)"
 307         line 428, ".input.spin", state 2374, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 308         line 428, ".input.spin", state 2374, "else"
 309         line 428, ".input.spin", state 2377, "(1)"
 310         line 428, ".input.spin", state 2378, "(1)"
 311         line 428, ".input.spin", state 2378, "(1)"
 312         line 432, ".input.spin", state 2386, "(1)"
 313         line 432, ".input.spin", state 2387, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 314         line 432, ".input.spin", state 2387, "else"
 315         line 432, ".input.spin", state 2390, "(1)"
 316         line 432, ".input.spin", state 2391, "(1)"
 317         line 432, ".input.spin", state 2391, "(1)"
 318         line 430, ".input.spin", state 2396, "((i<1))"
 319         line 430, ".input.spin", state 2396, "((i>=1))"
 320         line 437, ".input.spin", state 2403, "(1)"
 321         line 437, ".input.spin", state 2404, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
 322         line 437, ".input.spin", state 2404, "else"
 323         line 437, ".input.spin", state 2407, "(1)"
 324         line 437, ".input.spin", state 2408, "(1)"
 325         line 437, ".input.spin", state 2408, "(1)"
 326         line 441, ".input.spin", state 2416, "(1)"
 327         line 441, ".input.spin", state 2417, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
 328         line 441, ".input.spin", state 2417, "else"
 329         line 441, ".input.spin", state 2420, "(1)"
 330         line 441, ".input.spin", state 2421, "(1)"
 331         line 441, ".input.spin", state 2421, "(1)"
 332         line 439, ".input.spin", state 2426, "((i<2))"
 333         line 439, ".input.spin", state 2426, "((i>=2))"
 334         line 449, ".input.spin", state 2430, "(1)"
 335         line 449, ".input.spin", state 2430, "(1)"
 336         line 643, ".input.spin", state 2433, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
 337         line 643, ".input.spin", state 2434, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
 338         line 643, ".input.spin", state 2435, "(1)"
 339         line 271, ".input.spin", state 2439, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 340         line 279, ".input.spin", state 2461, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 341         line 283, ".input.spin", state 2470, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 342         line 248, ".input.spin", state 2486, "(1)"
 343         line 252, ".input.spin", state 2494, "(1)"
 344         line 256, ".input.spin", state 2506, "(1)"
 345         line 260, ".input.spin", state 2514, "(1)"
 346         line 410, ".input.spin", state 2532, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 347         line 414, ".input.spin", state 2546, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 348         line 419, ".input.spin", state 2564, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 349         line 423, ".input.spin", state 2578, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 350         line 428, ".input.spin", state 2597, "(1)"
 351         line 432, ".input.spin", state 2610, "(1)"
 352         line 437, ".input.spin", state 2627, "(1)"
 353         line 441, ".input.spin", state 2640, "(1)"
 354         line 271, ".input.spin", state 2664, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 355         line 275, ".input.spin", state 2673, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 356         line 279, ".input.spin", state 2686, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 357         line 283, ".input.spin", state 2695, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 358         line 248, ".input.spin", state 2711, "(1)"
 359         line 252, ".input.spin", state 2719, "(1)"
 360         line 256, ".input.spin", state 2731, "(1)"
 361         line 260, ".input.spin", state 2739, "(1)"
 362         line 410, ".input.spin", state 2757, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 363         line 414, ".input.spin", state 2771, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 364         line 419, ".input.spin", state 2789, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 365         line 423, ".input.spin", state 2803, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 366         line 428, ".input.spin", state 2822, "(1)"
 367         line 432, ".input.spin", state 2835, "(1)"
 368         line 437, ".input.spin", state 2852, "(1)"
 369         line 441, ".input.spin", state 2865, "(1)"
 370         line 410, ".input.spin", state 2886, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 371         line 414, ".input.spin", state 2900, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 372         line 419, ".input.spin", state 2918, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 373         line 423, ".input.spin", state 2932, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 374         line 428, ".input.spin", state 2951, "(1)"
 375         line 432, ".input.spin", state 2964, "(1)"
 376         line 437, ".input.spin", state 2981, "(1)"
 377         line 441, ".input.spin", state 2994, "(1)"
 378         line 248, ".input.spin", state 3027, "(1)"
 379         line 256, ".input.spin", state 3047, "(1)"
 380         line 260, ".input.spin", state 3055, "(1)"
 381         line 248, ".input.spin", state 3070, "(1)"
 382         line 252, ".input.spin", state 3078, "(1)"
 383         line 256, ".input.spin", state 3090, "(1)"
 384         line 260, ".input.spin", state 3098, "(1)"
 385         line 897, ".input.spin", state 3115, "-end-"
 386         (283 of 3115 states)
 387 unreached in proctype urcu_writer
 388         line 410, ".input.spin", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 389         line 414, ".input.spin", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 390         line 419, ".input.spin", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 391         line 428, ".input.spin", state 83, "(1)"
 392         line 432, ".input.spin", state 96, "(1)"
 393         line 437, ".input.spin", state 113, "(1)"
 394         line 271, ".input.spin", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 395         line 275, ".input.spin", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 396         line 279, ".input.spin", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 397         line 410, ".input.spin", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 398         line 414, ".input.spin", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 399         line 419, ".input.spin", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 400         line 423, ".input.spin", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 401         line 428, ".input.spin", state 276, "(1)"
 402         line 432, ".input.spin", state 289, "(1)"
 403         line 437, ".input.spin", state 306, "(1)"
 404         line 441, ".input.spin", state 319, "(1)"
 405         line 414, ".input.spin", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 406         line 419, ".input.spin", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 407         line 423, ".input.spin", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 408         line 432, ".input.spin", state 420, "(1)"
 409         line 437, ".input.spin", state 437, "(1)"
 410         line 441, ".input.spin", state 450, "(1)"
 411         line 414, ".input.spin", state 495, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 412         line 419, ".input.spin", state 513, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 413         line 423, ".input.spin", state 527, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 414         line 432, ".input.spin", state 559, "(1)"
 415         line 437, ".input.spin", state 576, "(1)"
 416         line 441, ".input.spin", state 589, "(1)"
 417         line 414, ".input.spin", state 624, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 418         line 419, ".input.spin", state 642, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 419         line 423, ".input.spin", state 656, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 420         line 432, ".input.spin", state 688, "(1)"
 421         line 437, ".input.spin", state 705, "(1)"
 422         line 441, ".input.spin", state 718, "(1)"
 423         line 414, ".input.spin", state 755, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 424         line 419, ".input.spin", state 773, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 425         line 423, ".input.spin", state 787, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 426         line 432, ".input.spin", state 819, "(1)"
 427         line 437, ".input.spin", state 836, "(1)"
 428         line 441, ".input.spin", state 849, "(1)"
 429         line 271, ".input.spin", state 904, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 430         line 275, ".input.spin", state 913, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 431         line 279, ".input.spin", state 928, "(1)"
 432         line 283, ".input.spin", state 935, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 433         line 248, ".input.spin", state 951, "(1)"
 434         line 252, ".input.spin", state 959, "(1)"
 435         line 256, ".input.spin", state 971, "(1)"
 436         line 260, ".input.spin", state 979, "(1)"
 437         line 275, ".input.spin", state 1004, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 438         line 279, ".input.spin", state 1017, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 439         line 283, ".input.spin", state 1026, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 440         line 248, ".input.spin", state 1042, "(1)"
 441         line 252, ".input.spin", state 1050, "(1)"
 442         line 256, ".input.spin", state 1062, "(1)"
 443         line 260, ".input.spin", state 1070, "(1)"
 444         line 275, ".input.spin", state 1095, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 445         line 279, ".input.spin", state 1108, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 446         line 283, ".input.spin", state 1117, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 447         line 248, ".input.spin", state 1133, "(1)"
 448         line 252, ".input.spin", state 1141, "(1)"
 449         line 256, ".input.spin", state 1153, "(1)"
 450         line 260, ".input.spin", state 1161, "(1)"
 451         line 275, ".input.spin", state 1186, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 452         line 279, ".input.spin", state 1199, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
 453         line 283, ".input.spin", state 1208, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
 454         line 248, ".input.spin", state 1224, "(1)"
 455         line 252, ".input.spin", state 1232, "(1)"
 456         line 256, ".input.spin", state 1244, "(1)"
 457         line 260, ".input.spin", state 1252, "(1)"
 458         line 1236, ".input.spin", state 1267, "-end-"
 459         (71 of 1267 states)
 460 unreached in proctype :init:
 461         (0 of 78 states)
 462
 463 pan: elapsed time 4.59e+03 seconds
 464 pan: rate 1460.6376 states/second
 465 pan: avg transition delay 1.0334e-06 usec
 466 cp .input.spin asserts.spin.input
 467 cp .input.spin.trail asserts.spin.input.trail
 468 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-alpha-no-ipi'