formal-model/urcu/result-signal-over-writer/urcu_free_no_rmb.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 touch .input.define
   4 cat .input.define >> pan.ltl
   5 cat DEFINES >> pan.ltl
   6 spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl
   7 cp urcu_free_no_rmb.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 -o pan pan.c
  15 ./pan -a -v -c1 -X -m10000000 -w20
  16 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
  17 (never claims generated from LTL formulae are stutter-invariant)
  18 depth 0: Claim reached state 5 (line 742)
  19
  20 (Spin Version 5.1.7 -- 23 December 2008)
  21         + Partial Order Reduction
  22
  23 Full statespace search for:
  24         never claim             +
  25         assertion violations    + (if within scope of claim)
  26         acceptance   cycles     + (fairness disabled)
  27         invalid end states      - (disabled by never claim)
  28
  29 State-vector 56 byte, depth reached 10519, errors: 0
  30     20146 states, stored
  31    191615 states, matched
  32    211761 transitions (= stored+matched)
  33    711676 atomic steps
  34 hash conflicts:      1222 (resolved)
  35
  36 Stats on memory usage (in Megabytes):
  37     1.614       equivalent memory usage for states (stored*(State-vector + overhead))
  38     1.509       actual memory usage for states (compression: 93.51%)
  39                 state-vector as stored = 51 byte + 28 byte overhead
  40     8.000       memory used for hash table (-w20)
  41   457.764       memory used for DFS stack (-m10000000)
  42   467.229       total actual memory usage
  43
  44 unreached in proctype urcu_reader_sig
  45         line 402, "pan.___", state 330, "(1)"
  46         line 613, "pan.___", state 411, "-end-"
  47         (2 of 411 states)
  48 unreached in proctype urcu_writer
  49         line 398, "pan.___", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  50         line 407, "pan.___", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  51         line 408, "pan.___", state 59, "(1)"
  52         line 417, "pan.___", state 89, "(1)"
  53         line 398, "pan.___", state 115, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  54         line 408, "pan.___", state 160, "(1)"
  55         line 651, "pan.___", state 213, "(1)"
  56         line 174, "pan.___", state 222, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  57         line 178, "pan.___", state 233, "(1)"
  58         line 174, "pan.___", state 257, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
  59         line 178, "pan.___", state 266, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
  60         line 182, "pan.___", state 279, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
  61         line 174, "pan.___", state 296, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  62         line 178, "pan.___", state 305, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
  63         line 182, "pan.___", state 318, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  64         line 398, "pan.___", state 341, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  65         line 402, "pan.___", state 357, "(1)"
  66         line 407, "pan.___", state 373, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  67         line 408, "pan.___", state 386, "(1)"
  68         line 417, "pan.___", state 416, "(1)"
  69         line 398, "pan.___", state 442, "(1)"
  70         line 402, "pan.___", state 456, "(1)"
  71         line 407, "pan.___", state 472, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  72         line 417, "pan.___", state 515, "(1)"
  73         line 402, "pan.___", state 556, "(1)"
  74         line 407, "pan.___", state 572, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  75         line 417, "pan.___", state 615, "(1)"
  76         line 174, "pan.___", state 636, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  77         line 174, "pan.___", state 638, "(1)"
  78         line 178, "pan.___", state 645, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
  79         line 178, "pan.___", state 647, "(1)"
  80         line 178, "pan.___", state 648, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
  81         line 178, "pan.___", state 648, "else"
  82         line 176, "pan.___", state 653, "((j<1))"
  83         line 176, "pan.___", state 653, "((j>=1))"
  84         line 182, "pan.___", state 658, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  85         line 182, "pan.___", state 660, "(1)"
  86         line 182, "pan.___", state 661, "((cache_dirty_generation_ptr.bitfield&(1<<0)))"
  87         line 182, "pan.___", state 661, "else"
  88         line 174, "pan.___", state 671, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
  89         line 174, "pan.___", state 673, "(1)"
  90         line 178, "pan.___", state 680, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
  91         line 178, "pan.___", state 682, "(1)"
  92         line 178, "pan.___", state 683, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
  93         line 178, "pan.___", state 683, "else"
  94         line 176, "pan.___", state 688, "((j<1))"
  95         line 176, "pan.___", state 688, "((j>=1))"
  96         line 182, "pan.___", state 693, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
  97         line 182, "pan.___", state 695, "(1)"
  98         line 182, "pan.___", state 696, "((cache_dirty_generation_ptr.bitfield&(1<<i)))"
  99         line 182, "pan.___", state 696, "else"
 100         line 192, "pan.___", state 701, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
 101         line 192, "pan.___", state 701, "else"
 102         line 213, "pan.___", state 705, "((i<1))"
 103         line 213, "pan.___", state 705, "((i>=1))"
 104         line 174, "pan.___", state 710, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 105         line 174, "pan.___", state 712, "(1)"
 106         line 178, "pan.___", state 719, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 107         line 178, "pan.___", state 721, "(1)"
 108         line 178, "pan.___", state 722, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 109         line 178, "pan.___", state 722, "else"
 110         line 176, "pan.___", state 727, "((j<1))"
 111         line 176, "pan.___", state 727, "((j>=1))"
 112         line 182, "pan.___", state 732, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 113         line 182, "pan.___", state 734, "(1)"
 114         line 182, "pan.___", state 735, "((cache_dirty_generation_ptr.bitfield&(1<<0)))"
 115         line 182, "pan.___", state 735, "else"
 116         line 192, "pan.___", state 740, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 117         line 192, "pan.___", state 740, "else"
 118         line 220, "pan.___", state 741, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 119         line 220, "pan.___", state 741, "else"
 120         line 355, "pan.___", state 747, "((sighand_exec==1))"
 121         line 355, "pan.___", state 747, "else"
 122         line 361, "pan.___", state 750, "sighand_exec = 1"
 123         line 398, "pan.___", state 763, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 124         line 398, "pan.___", state 765, "(1)"
 125         line 398, "pan.___", state 766, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 126         line 398, "pan.___", state 766, "else"
 127         line 398, "pan.___", state 769, "(1)"
 128         line 402, "pan.___", state 777, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 129         line 402, "pan.___", state 779, "(1)"
 130         line 402, "pan.___", state 780, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 131         line 402, "pan.___", state 780, "else"
 132         line 402, "pan.___", state 783, "(1)"
 133         line 402, "pan.___", state 784, "(1)"
 134         line 402, "pan.___", state 784, "(1)"
 135         line 400, "pan.___", state 789, "((i<1))"
 136         line 400, "pan.___", state 789, "((i>=1))"
 137         line 407, "pan.___", state 795, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 138         line 408, "pan.___", state 808, "(1)"
 139         line 408, "pan.___", state 809, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 140         line 408, "pan.___", state 809, "else"
 141         line 408, "pan.___", state 812, "(1)"
 142         line 408, "pan.___", state 813, "(1)"
 143         line 408, "pan.___", state 813, "(1)"
 144         line 412, "pan.___", state 821, "(1)"
 145         line 412, "pan.___", state 822, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 146         line 412, "pan.___", state 822, "else"
 147         line 412, "pan.___", state 825, "(1)"
 148         line 412, "pan.___", state 826, "(1)"
 149         line 412, "pan.___", state 826, "(1)"
 150         line 410, "pan.___", state 831, "((i<1))"
 151         line 410, "pan.___", state 831, "((i>=1))"
 152         line 417, "pan.___", state 838, "(1)"
 153         line 417, "pan.___", state 839, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 154         line 417, "pan.___", state 839, "else"
 155         line 417, "pan.___", state 842, "(1)"
 156         line 417, "pan.___", state 843, "(1)"
 157         line 417, "pan.___", state 843, "(1)"
 158         line 419, "pan.___", state 846, "(1)"
 159         line 419, "pan.___", state 846, "(1)"
 160         line 361, "pan.___", state 855, "sighand_exec = 1"
 161         line 402, "pan.___", state 886, "(1)"
 162         line 407, "pan.___", state 902, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 163         line 417, "pan.___", state 945, "(1)"
 164         line 402, "pan.___", state 983, "(1)"
 165         line 407, "pan.___", state 999, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 166         line 417, "pan.___", state 1042, "(1)"
 167         line 398, "pan.___", state 1068, "(1)"
 168         line 402, "pan.___", state 1082, "(1)"
 169         line 407, "pan.___", state 1098, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 170         line 417, "pan.___", state 1141, "(1)"
 171         line 402, "pan.___", state 1182, "(1)"
 172         line 407, "pan.___", state 1198, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 173         line 417, "pan.___", state 1241, "(1)"
 174         line 174, "pan.___", state 1262, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 175         line 174, "pan.___", state 1264, "(1)"
 176         line 178, "pan.___", state 1271, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 177         line 178, "pan.___", state 1273, "(1)"
 178         line 178, "pan.___", state 1274, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 179         line 178, "pan.___", state 1274, "else"
 180         line 176, "pan.___", state 1279, "((j<1))"
 181         line 176, "pan.___", state 1279, "((j>=1))"
 182         line 182, "pan.___", state 1284, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 183         line 182, "pan.___", state 1286, "(1)"
 184         line 182, "pan.___", state 1287, "((cache_dirty_generation_ptr.bitfield&(1<<0)))"
 185         line 182, "pan.___", state 1287, "else"
 186         line 174, "pan.___", state 1297, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 187         line 174, "pan.___", state 1299, "(1)"
 188         line 178, "pan.___", state 1306, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
 189         line 178, "pan.___", state 1308, "(1)"
 190         line 178, "pan.___", state 1309, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
 191         line 178, "pan.___", state 1309, "else"
 192         line 176, "pan.___", state 1314, "((j<1))"
 193         line 176, "pan.___", state 1314, "((j>=1))"
 194         line 182, "pan.___", state 1319, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 195         line 182, "pan.___", state 1321, "(1)"
 196         line 182, "pan.___", state 1322, "((cache_dirty_generation_ptr.bitfield&(1<<i)))"
 197         line 182, "pan.___", state 1322, "else"
 198         line 192, "pan.___", state 1327, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
 199         line 192, "pan.___", state 1327, "else"
 200         line 213, "pan.___", state 1331, "((i<1))"
 201         line 213, "pan.___", state 1331, "((i>=1))"
 202         line 174, "pan.___", state 1336, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 203         line 174, "pan.___", state 1338, "(1)"
 204         line 178, "pan.___", state 1345, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 205         line 178, "pan.___", state 1347, "(1)"
 206         line 178, "pan.___", state 1348, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 207         line 178, "pan.___", state 1348, "else"
 208         line 176, "pan.___", state 1353, "((j<1))"
 209         line 176, "pan.___", state 1353, "((j>=1))"
 210         line 182, "pan.___", state 1358, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 211         line 182, "pan.___", state 1360, "(1)"
 212         line 182, "pan.___", state 1361, "((cache_dirty_generation_ptr.bitfield&(1<<0)))"
 213         line 182, "pan.___", state 1361, "else"
 214         line 192, "pan.___", state 1366, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 215         line 192, "pan.___", state 1366, "else"
 216         line 220, "pan.___", state 1367, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 217         line 220, "pan.___", state 1367, "else"
 218         line 355, "pan.___", state 1373, "((sighand_exec==1))"
 219         line 355, "pan.___", state 1373, "else"
 220         line 361, "pan.___", state 1376, "sighand_exec = 1"
 221         line 398, "pan.___", state 1389, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 222         line 398, "pan.___", state 1391, "(1)"
 223         line 398, "pan.___", state 1392, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 224         line 398, "pan.___", state 1392, "else"
 225         line 398, "pan.___", state 1395, "(1)"
 226         line 402, "pan.___", state 1403, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 227         line 402, "pan.___", state 1405, "(1)"
 228         line 402, "pan.___", state 1406, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 229         line 402, "pan.___", state 1406, "else"
 230         line 402, "pan.___", state 1409, "(1)"
 231         line 402, "pan.___", state 1410, "(1)"
 232         line 402, "pan.___", state 1410, "(1)"
 233         line 400, "pan.___", state 1415, "((i<1))"
 234         line 400, "pan.___", state 1415, "((i>=1))"
 235         line 407, "pan.___", state 1421, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 236         line 408, "pan.___", state 1434, "(1)"
 237         line 408, "pan.___", state 1435, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 238         line 408, "pan.___", state 1435, "else"
 239         line 408, "pan.___", state 1438, "(1)"
 240         line 408, "pan.___", state 1439, "(1)"
 241         line 408, "pan.___", state 1439, "(1)"
 242         line 412, "pan.___", state 1447, "(1)"
 243         line 412, "pan.___", state 1448, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 244         line 412, "pan.___", state 1448, "else"
 245         line 412, "pan.___", state 1451, "(1)"
 246         line 412, "pan.___", state 1452, "(1)"
 247         line 412, "pan.___", state 1452, "(1)"
 248         line 410, "pan.___", state 1457, "((i<1))"
 249         line 410, "pan.___", state 1457, "((i>=1))"
 250         line 417, "pan.___", state 1464, "(1)"
 251         line 417, "pan.___", state 1465, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 252         line 417, "pan.___", state 1465, "else"
 253         line 417, "pan.___", state 1468, "(1)"
 254         line 417, "pan.___", state 1469, "(1)"
 255         line 417, "pan.___", state 1469, "(1)"
 256         line 419, "pan.___", state 1472, "(1)"
 257         line 419, "pan.___", state 1472, "(1)"
 258         line 361, "pan.___", state 1481, "sighand_exec = 1"
 259         line 178, "pan.___", state 1506, "(1)"
 260         line 182, "pan.___", state 1517, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 261         line 174, "pan.___", state 1530, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 262         line 178, "pan.___", state 1539, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
 263         line 182, "pan.___", state 1552, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 264         line 174, "pan.___", state 1569, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 265         line 178, "pan.___", state 1578, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 266         line 182, "pan.___", state 1591, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 267         line 701, "pan.___", state 1632, "-end-"
 268         (167 of 1632 states)
 269 unreached in proctype :init:
 270         (0 of 46 states)
 271 unreached in proctype :never:
 272         line 747, "pan.___", state 8, "-end-"
 273         (1 of 8 states)
 274
 275 pan: elapsed time 0.15 seconds
 276 pan: rate 134306.67 states/second
 277 pan: avg transition delay 7.0835e-07 usec
 278 cp .input.spin urcu_free_no_rmb.spin.input
 279 cp .input.spin.trail urcu_free_no_rmb.spin.input.trail
 280 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'