formal-model/urcu/result-standard-execution-nonest/asserts.log

   1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
   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
  11 (Spin Version 5.1.7 -- 23 December 2008)
  12         + Partial Order Reduction
  13
  14 Full statespace search for:
  15         never claim             - (none specified)
  16         assertion violations    +
  17         cycle checks            - (disabled by -DSAFETY)
  18         invalid end states      +
  19
  20 State-vector 48 byte, depth reached 2084, errors: 0
  21    847558 states, stored
  22   9221089 states, matched
  23  10068647 transitions (= stored+matched)
  24  36786866 atomic steps
  25 hash conflicts:   2126850 (resolved)
  26
  27 Stats on memory usage (in Megabytes):
  28    61.430       equivalent memory usage for states (stored*(State-vector + overhead))
  29    45.632       actual memory usage for states (compression: 74.28%)
  30                 state-vector as stored = 28 byte + 28 byte overhead
  31     8.000       memory used for hash table (-w20)
  32   457.764       memory used for DFS stack (-m10000000)
  33   511.369       total actual memory usage
  34
  35 unreached in proctype urcu_reader
  36         line 398, ".input.spin", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  37         line 407, ".input.spin", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  38         line 408, ".input.spin", state 61, "(1)"
  39         line 417, ".input.spin", state 91, "(1)"
  40         line 398, ".input.spin", state 106, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  41         line 407, ".input.spin", state 138, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  42         line 408, ".input.spin", state 151, "(1)"
  43         line 417, ".input.spin", state 181, "(1)"
  44         line 398, ".input.spin", state 197, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  45         line 407, ".input.spin", state 229, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  46         line 408, ".input.spin", state 242, "(1)"
  47         line 417, ".input.spin", state 272, "(1)"
  48         line 398, ".input.spin", state 315, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  49         line 407, ".input.spin", state 347, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  50         line 408, ".input.spin", state 360, "(1)"
  51         line 417, ".input.spin", state 390, "(1)"
  52         line 539, ".input.spin", state 414, "-end-"
  53         (17 of 414 states)
  54 unreached in proctype urcu_writer
  55         line 398, ".input.spin", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  56         line 402, ".input.spin", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  57         line 407, ".input.spin", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  58         line 408, ".input.spin", state 59, "(1)"
  59         line 412, ".input.spin", state 72, "(1)"
  60         line 417, ".input.spin", state 89, "(1)"
  61         line 398, ".input.spin", state 108, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  62         line 402, ".input.spin", state 122, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  63         line 408, ".input.spin", state 153, "(1)"
  64         line 412, ".input.spin", state 166, "(1)"
  65         line 651, ".input.spin", state 199, "(1)"
  66         line 174, ".input.spin", state 208, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  67         line 178, ".input.spin", state 217, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  68         line 159, ".input.spin", state 240, "(1)"
  69         line 163, ".input.spin", state 248, "(1)"
  70         line 167, ".input.spin", state 260, "(1)"
  71         line 174, ".input.spin", state 271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
  72         line 182, ".input.spin", state 293, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
  73         line 159, ".input.spin", state 303, "(1)"
  74         line 163, ".input.spin", state 311, "(1)"
  75         line 167, ".input.spin", state 323, "(1)"
  76         line 174, ".input.spin", state 338, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  77         line 178, ".input.spin", state 347, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  78         line 182, ".input.spin", state 360, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  79         line 159, ".input.spin", state 370, "(1)"
  80         line 163, ".input.spin", state 378, "(1)"
  81         line 167, ".input.spin", state 390, "(1)"
  82         line 398, ".input.spin", state 404, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
  83         line 402, ".input.spin", state 418, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  84         line 407, ".input.spin", state 436, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  85         line 408, ".input.spin", state 449, "(1)"
  86         line 412, ".input.spin", state 462, "(1)"
  87         line 417, ".input.spin", state 479, "(1)"
  88         line 398, ".input.spin", state 498, "(1)"
  89         line 402, ".input.spin", state 510, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  90         line 407, ".input.spin", state 528, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  91         line 412, ".input.spin", state 554, "(1)"
  92         line 417, ".input.spin", state 571, "(1)"
  93         line 402, ".input.spin", state 603, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  94         line 407, ".input.spin", state 621, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  95         line 412, ".input.spin", state 647, "(1)"
  96         line 417, ".input.spin", state 664, "(1)"
  97         line 178, ".input.spin", state 687, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
  98         line 182, ".input.spin", state 700, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
  99         line 159, ".input.spin", state 710, "(1)"
 100         line 163, ".input.spin", state 718, "(1)"
 101         line 167, ".input.spin", state 730, "(1)"
 102         line 174, ".input.spin", state 741, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 103         line 182, ".input.spin", state 763, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 104         line 159, ".input.spin", state 773, "(1)"
 105         line 163, ".input.spin", state 781, "(1)"
 106         line 167, ".input.spin", state 793, "(1)"
 107         line 174, ".input.spin", state 808, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 108         line 178, ".input.spin", state 817, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 109         line 182, ".input.spin", state 830, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 110         line 159, ".input.spin", state 840, "(1)"
 111         line 163, ".input.spin", state 848, "(1)"
 112         line 167, ".input.spin", state 860, "(1)"
 113         line 398, ".input.spin", state 882, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 114         line 398, ".input.spin", state 884, "(1)"
 115         line 398, ".input.spin", state 885, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 116         line 398, ".input.spin", state 885, "else"
 117         line 398, ".input.spin", state 888, "(1)"
 118         line 402, ".input.spin", state 896, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 119         line 402, ".input.spin", state 898, "(1)"
 120         line 402, ".input.spin", state 899, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 121         line 402, ".input.spin", state 899, "else"
 122         line 402, ".input.spin", state 902, "(1)"
 123         line 402, ".input.spin", state 903, "(1)"
 124         line 402, ".input.spin", state 903, "(1)"
 125         line 400, ".input.spin", state 908, "((i<1))"
 126         line 400, ".input.spin", state 908, "((i>=1))"
 127         line 407, ".input.spin", state 914, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 128         line 408, ".input.spin", state 927, "(1)"
 129         line 408, ".input.spin", state 928, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 130         line 408, ".input.spin", state 928, "else"
 131         line 408, ".input.spin", state 931, "(1)"
 132         line 408, ".input.spin", state 932, "(1)"
 133         line 408, ".input.spin", state 932, "(1)"
 134         line 412, ".input.spin", state 940, "(1)"
 135         line 412, ".input.spin", state 941, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 136         line 412, ".input.spin", state 941, "else"
 137         line 412, ".input.spin", state 944, "(1)"
 138         line 412, ".input.spin", state 945, "(1)"
 139         line 412, ".input.spin", state 945, "(1)"
 140         line 410, ".input.spin", state 950, "((i<1))"
 141         line 410, ".input.spin", state 950, "((i>=1))"
 142         line 417, ".input.spin", state 957, "(1)"
 143         line 417, ".input.spin", state 958, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
 144         line 417, ".input.spin", state 958, "else"
 145         line 417, ".input.spin", state 961, "(1)"
 146         line 417, ".input.spin", state 962, "(1)"
 147         line 417, ".input.spin", state 962, "(1)"
 148         line 419, ".input.spin", state 965, "(1)"
 149         line 419, ".input.spin", state 965, "(1)"
 150         line 402, ".input.spin", state 996, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 151         line 407, ".input.spin", state 1014, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 152         line 412, ".input.spin", state 1040, "(1)"
 153         line 417, ".input.spin", state 1057, "(1)"
 154         line 402, ".input.spin", state 1086, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 155         line 407, ".input.spin", state 1104, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 156         line 412, ".input.spin", state 1130, "(1)"
 157         line 417, ".input.spin", state 1147, "(1)"
 158         line 398, ".input.spin", state 1166, "(1)"
 159         line 402, ".input.spin", state 1178, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 160         line 407, ".input.spin", state 1196, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 161         line 412, ".input.spin", state 1222, "(1)"
 162         line 417, ".input.spin", state 1239, "(1)"
 163         line 402, ".input.spin", state 1271, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 164         line 407, ".input.spin", state 1289, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 165         line 412, ".input.spin", state 1315, "(1)"
 166         line 417, ".input.spin", state 1332, "(1)"
 167         line 178, ".input.spin", state 1355, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 168         line 182, ".input.spin", state 1368, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 169         line 159, ".input.spin", state 1378, "(1)"
 170         line 163, ".input.spin", state 1386, "(1)"
 171         line 167, ".input.spin", state 1398, "(1)"
 172         line 174, ".input.spin", state 1409, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 173         line 182, ".input.spin", state 1431, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 174         line 159, ".input.spin", state 1441, "(1)"
 175         line 163, ".input.spin", state 1449, "(1)"
 176         line 167, ".input.spin", state 1461, "(1)"
 177         line 174, ".input.spin", state 1476, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 178         line 178, ".input.spin", state 1485, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 179         line 182, ".input.spin", state 1498, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 180         line 159, ".input.spin", state 1508, "(1)"
 181         line 163, ".input.spin", state 1516, "(1)"
 182         line 167, ".input.spin", state 1528, "(1)"
 183         line 398, ".input.spin", state 1550, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 184         line 398, ".input.spin", state 1552, "(1)"
 185         line 398, ".input.spin", state 1553, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
 186         line 398, ".input.spin", state 1553, "else"
 187         line 398, ".input.spin", state 1556, "(1)"
 188         line 402, ".input.spin", state 1564, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 189         line 402, ".input.spin", state 1566, "(1)"
 190         line 402, ".input.spin", state 1567, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
 191         line 402, ".input.spin", state 1567, "else"
 192         line 402, ".input.spin", state 1570, "(1)"
 193         line 402, ".input.spin", state 1571, "(1)"
 194         line 402, ".input.spin", state 1571, "(1)"
 195         line 400, ".input.spin", state 1576, "((i<1))"
 196         line 400, ".input.spin", state 1576, "((i>=1))"
 197         line 407, ".input.spin", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 198         line 408, ".input.spin", state 1595, "(1)"
 199         line 408, ".input.spin", state 1596, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
 200         line 408, ".input.spin", state 1596, "else"
 201         line 408, ".input.spin", state 1599, "(1)"
 202         line 408, ".input.spin", state 1600, "(1)"
 203         line 408, ".input.spin", state 1600, "(1)"
 204         line 412, ".input.spin", state 1608, "(1)"
 205         line 412, ".input.spin", state 1609, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
 206         line 412, ".input.spin", state 1609, "else"
 207         line 412, ".input.spin", state 1612, "(1)"
 208         line 412, ".input.spin", state 1613, "(1)"
 209         line 412, ".input.spin", state 1613, "(1)"
 210         line 410, ".input.spin", state 1618, "((i<1))"
 211         line 410, ".input.spin", state 1618, "((i>=1))"
 212         line 417, ".input.spin", state 1625, "(1)"
 213         line 417, ".input.spin", state 1626, "(!((cache_dirty_generation_ptr.bitfield&(1<<_pid))))"
 214         line 417, ".input.spin", state 1626, "else"
 215         line 417, ".input.spin", state 1629, "(1)"
 216         line 417, ".input.spin", state 1630, "(1)"
 217         line 417, ".input.spin", state 1630, "(1)"
 218         line 419, ".input.spin", state 1633, "(1)"
 219         line 419, ".input.spin", state 1633, "(1)"
 220         line 178, ".input.spin", state 1658, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 221         line 182, ".input.spin", state 1671, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 222         line 159, ".input.spin", state 1681, "(1)"
 223         line 163, ".input.spin", state 1689, "(1)"
 224         line 167, ".input.spin", state 1701, "(1)"
 225         line 174, ".input.spin", state 1712, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 226         line 182, ".input.spin", state 1734, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 227         line 159, ".input.spin", state 1744, "(1)"
 228         line 163, ".input.spin", state 1752, "(1)"
 229         line 167, ".input.spin", state 1764, "(1)"
 230         line 174, ".input.spin", state 1779, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
 231         line 178, ".input.spin", state 1788, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
 232         line 182, ".input.spin", state 1801, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<_pid)))"
 233         line 159, ".input.spin", state 1811, "(1)"
 234         line 163, ".input.spin", state 1819, "(1)"
 235         line 167, ".input.spin", state 1831, "(1)"
 236         line 701, ".input.spin", state 1856, "-end-"
 237         (158 of 1856 states)
 238 unreached in proctype :init:
 239         (0 of 46 states)
 240
 241 pan: elapsed time 6.68 seconds
 242 pan: rate 126879.94 states/second
 243 pan: avg transition delay 6.6345e-07 usec
 244 cp .input.spin asserts.spin.input
 245 cp .input.spin.trail asserts.spin.input.trail
 246 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'