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