formal-model/urcu-nosched-model/result-signal-over-writer/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 40 byte, depth reached 7872, errors: 0
  21     20128 states, stored
  22    191477 states, matched
  23    211605 transitions (= stored+matched)
  24    712166 atomic steps
  25 hash conflicts:       942 (resolved)
  26
  27 Stats on memory usage (in Megabytes):
  28     1.305       equivalent memory usage for states (stored*(State-vector + overhead))
  29     1.467       actual memory usage for states (unsuccessful compression: 112.36%)
  30                 state-vector as stored = 48 byte + 28 byte overhead
  31     8.000       memory used for hash table (-w20)
  32   457.764       memory used for DFS stack (-m10000000)
  33   467.229       total actual memory usage
  34
  35 unreached in proctype urcu_reader_sig
  36         line 401, ".input.spin", state 330, "(1)"
  37         line 612, ".input.spin", state 411, "-end-"
  38         (2 of 411 states)
  39 unreached in proctype urcu_writer
  40         line 397, ".input.spin", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  41         line 406, ".input.spin", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  42         line 407, ".input.spin", state 59, "(1)"
  43         line 416, ".input.spin", state 89, "(1)"
  44         line 397, ".input.spin", state 115, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  45         line 407, ".input.spin", state 160, "(1)"
  46         line 650, ".input.spin", state 213, "(1)"
  47         line 173, ".input.spin", state 222, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  48         line 177, ".input.spin", state 233, "(1)"
  49         line 158, ".input.spin", state 254, "(1)"
  50         line 162, ".input.spin", state 262, "(1)"
  51         line 166, ".input.spin", state 274, "(1)"
  52         line 173, ".input.spin", state 285, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
  53         line 177, ".input.spin", state 294, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
  54         line 181, ".input.spin", state 307, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
  55         line 158, ".input.spin", state 317, "(1)"
  56         line 162, ".input.spin", state 325, "(1)"
  57         line 166, ".input.spin", state 337, "(1)"
  58         line 173, ".input.spin", state 352, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  59         line 177, ".input.spin", state 361, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
  60         line 181, ".input.spin", state 374, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  61         line 158, ".input.spin", state 384, "(1)"
  62         line 162, ".input.spin", state 392, "(1)"
  63         line 166, ".input.spin", state 404, "(1)"
  64         line 397, ".input.spin", state 425, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  65         line 401, ".input.spin", state 441, "(1)"
  66         line 406, ".input.spin", state 457, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  67         line 407, ".input.spin", state 470, "(1)"
  68         line 416, ".input.spin", state 500, "(1)"
  69         line 397, ".input.spin", state 526, "(1)"
  70         line 401, ".input.spin", state 540, "(1)"
  71         line 406, ".input.spin", state 556, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  72         line 416, ".input.spin", state 599, "(1)"
  73         line 401, ".input.spin", state 640, "(1)"
  74         line 406, ".input.spin", state 656, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  75         line 416, ".input.spin", state 699, "(1)"
  76         line 173, ".input.spin", state 720, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
  77         line 173, ".input.spin", state 722, "(1)"
  78         line 177, ".input.spin", state 729, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
  79         line 177, ".input.spin", state 731, "(1)"
  80         line 177, ".input.spin", state 732, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
  81         line 177, ".input.spin", state 732, "else"
  82         line 175, ".input.spin", state 737, "((j<1))"
  83         line 175, ".input.spin", state 737, "((j>=1))"
  84         line 181, ".input.spin", state 742, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
  85         line 158, ".input.spin", state 752, "(1)"
  86         line 162, ".input.spin", state 760, "(1)"
  87         line 162, ".input.spin", state 761, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
  88         line 162, ".input.spin", state 761, "else"
  89         line 160, ".input.spin", state 766, "((j<1))"
  90         line 160, ".input.spin", state 766, "((j>=1))"
  91         line 166, ".input.spin", state 772, "(1)"
  92         line 166, ".input.spin", state 773, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
  93         line 166, ".input.spin", state 773, "else"
  94         line 168, ".input.spin", state 776, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
  95         line 168, ".input.spin", state 776, "else"
  96         line 173, ".input.spin", state 783, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
  97         line 173, ".input.spin", state 785, "(1)"
  98         line 177, ".input.spin", state 792, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
  99         line 177, ".input.spin", state 794, "(1)"
 100         line 177, ".input.spin", state 795, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
 101         line 177, ".input.spin", state 795, "else"
 102         line 175, ".input.spin", state 800, "((j<1))"
 103         line 175, ".input.spin", state 800, "((j>=1))"
 104         line 181, ".input.spin", state 805, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 105         line 158, ".input.spin", state 815, "(1)"
 106         line 162, ".input.spin", state 823, "(1)"
 107         line 162, ".input.spin", state 824, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
 108         line 162, ".input.spin", state 824, "else"
 109         line 160, ".input.spin", state 829, "((j<1))"
 110         line 160, ".input.spin", state 829, "((j>=1))"
 111         line 166, ".input.spin", state 835, "(1)"
 112         line 166, ".input.spin", state 836, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
 113         line 166, ".input.spin", state 836, "else"
 114         line 168, ".input.spin", state 839, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
 115         line 168, ".input.spin", state 839, "else"
 116         line 200, ".input.spin", state 841, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
 117         line 200, ".input.spin", state 841, "else"
 118         line 212, ".input.spin", state 845, "((i<1))"
 119         line 212, ".input.spin", state 845, "((i>=1))"
 120         line 173, ".input.spin", state 850, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 121         line 173, ".input.spin", state 852, "(1)"
 122         line 177, ".input.spin", state 859, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 123         line 177, ".input.spin", state 861, "(1)"
 124         line 177, ".input.spin", state 862, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 125         line 177, ".input.spin", state 862, "else"
 126         line 175, ".input.spin", state 867, "((j<1))"
 127         line 175, ".input.spin", state 867, "((j>=1))"
 128         line 181, ".input.spin", state 872, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 129         line 158, ".input.spin", state 882, "(1)"
 130         line 162, ".input.spin", state 890, "(1)"
 131         line 162, ".input.spin", state 891, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 132         line 162, ".input.spin", state 891, "else"
 133         line 160, ".input.spin", state 896, "((j<1))"
 134         line 160, ".input.spin", state 896, "((j>=1))"
 135         line 166, ".input.spin", state 902, "(1)"
 136         line 166, ".input.spin", state 903, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 137         line 166, ".input.spin", state 903, "else"
 138         line 168, ".input.spin", state 906, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 139         line 168, ".input.spin", state 906, "else"
 140         line 200, ".input.spin", state 908, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 141         line 200, ".input.spin", state 908, "else"
 142         line 219, ".input.spin", state 909, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 143         line 219, ".input.spin", state 909, "else"
 144         line 354, ".input.spin", state 915, "((sighand_exec==1))"
 145         line 354, ".input.spin", state 915, "else"
 146         line 360, ".input.spin", state 918, "sighand_exec = 1"
 147         line 397, ".input.spin", state 931, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 148         line 397, ".input.spin", state 933, "(1)"
 149         line 397, ".input.spin", state 934, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 150         line 397, ".input.spin", state 934, "else"
 151         line 397, ".input.spin", state 937, "(1)"
 152         line 401, ".input.spin", state 945, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 153         line 401, ".input.spin", state 947, "(1)"
 154         line 401, ".input.spin", state 948, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 155         line 401, ".input.spin", state 948, "else"
 156         line 401, ".input.spin", state 951, "(1)"
 157         line 401, ".input.spin", state 952, "(1)"
 158         line 401, ".input.spin", state 952, "(1)"
 159         line 399, ".input.spin", state 957, "((i<1))"
 160         line 399, ".input.spin", state 957, "((i>=1))"
 161         line 406, ".input.spin", state 963, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 162         line 407, ".input.spin", state 976, "(1)"
 163         line 407, ".input.spin", state 977, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 164         line 407, ".input.spin", state 977, "else"
 165         line 407, ".input.spin", state 980, "(1)"
 166         line 407, ".input.spin", state 981, "(1)"
 167         line 407, ".input.spin", state 981, "(1)"
 168         line 411, ".input.spin", state 989, "(1)"
 169         line 411, ".input.spin", state 990, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 170         line 411, ".input.spin", state 990, "else"
 171         line 411, ".input.spin", state 993, "(1)"
 172         line 411, ".input.spin", state 994, "(1)"
 173         line 411, ".input.spin", state 994, "(1)"
 174         line 409, ".input.spin", state 999, "((i<1))"
 175         line 409, ".input.spin", state 999, "((i>=1))"
 176         line 416, ".input.spin", state 1006, "(1)"
 177         line 416, ".input.spin", state 1007, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 178         line 416, ".input.spin", state 1007, "else"
 179         line 416, ".input.spin", state 1010, "(1)"
 180         line 416, ".input.spin", state 1011, "(1)"
 181         line 416, ".input.spin", state 1011, "(1)"
 182         line 418, ".input.spin", state 1014, "(1)"
 183         line 418, ".input.spin", state 1014, "(1)"
 184         line 360, ".input.spin", state 1023, "sighand_exec = 1"
 185         line 401, ".input.spin", state 1054, "(1)"
 186         line 406, ".input.spin", state 1070, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 187         line 416, ".input.spin", state 1113, "(1)"
 188         line 401, ".input.spin", state 1151, "(1)"
 189         line 406, ".input.spin", state 1167, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 190         line 416, ".input.spin", state 1210, "(1)"
 191         line 397, ".input.spin", state 1236, "(1)"
 192         line 401, ".input.spin", state 1250, "(1)"
 193         line 406, ".input.spin", state 1266, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 194         line 416, ".input.spin", state 1309, "(1)"
 195         line 401, ".input.spin", state 1350, "(1)"
 196         line 406, ".input.spin", state 1366, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 197         line 416, ".input.spin", state 1409, "(1)"
 198         line 173, ".input.spin", state 1430, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 199         line 173, ".input.spin", state 1432, "(1)"
 200         line 177, ".input.spin", state 1439, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 201         line 177, ".input.spin", state 1441, "(1)"
 202         line 177, ".input.spin", state 1442, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 203         line 177, ".input.spin", state 1442, "else"
 204         line 175, ".input.spin", state 1447, "((j<1))"
 205         line 175, ".input.spin", state 1447, "((j>=1))"
 206         line 181, ".input.spin", state 1452, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 207         line 158, ".input.spin", state 1462, "(1)"
 208         line 162, ".input.spin", state 1470, "(1)"
 209         line 162, ".input.spin", state 1471, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 210         line 162, ".input.spin", state 1471, "else"
 211         line 160, ".input.spin", state 1476, "((j<1))"
 212         line 160, ".input.spin", state 1476, "((j>=1))"
 213         line 166, ".input.spin", state 1482, "(1)"
 214         line 166, ".input.spin", state 1483, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 215         line 166, ".input.spin", state 1483, "else"
 216         line 168, ".input.spin", state 1486, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 217         line 168, ".input.spin", state 1486, "else"
 218         line 173, ".input.spin", state 1493, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 219         line 173, ".input.spin", state 1495, "(1)"
 220         line 177, ".input.spin", state 1502, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
 221         line 177, ".input.spin", state 1504, "(1)"
 222         line 177, ".input.spin", state 1505, "((cache_dirty_urcu_active_readers.bitfield&(1<<i)))"
 223         line 177, ".input.spin", state 1505, "else"
 224         line 175, ".input.spin", state 1510, "((j<1))"
 225         line 175, ".input.spin", state 1510, "((j>=1))"
 226         line 181, ".input.spin", state 1515, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 227         line 158, ".input.spin", state 1525, "(1)"
 228         line 162, ".input.spin", state 1533, "(1)"
 229         line 162, ".input.spin", state 1534, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
 230         line 162, ".input.spin", state 1534, "else"
 231         line 160, ".input.spin", state 1539, "((j<1))"
 232         line 160, ".input.spin", state 1539, "((j>=1))"
 233         line 166, ".input.spin", state 1545, "(1)"
 234         line 166, ".input.spin", state 1546, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
 235         line 166, ".input.spin", state 1546, "else"
 236         line 168, ".input.spin", state 1549, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
 237         line 168, ".input.spin", state 1549, "else"
 238         line 200, ".input.spin", state 1551, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<i)))"
 239         line 200, ".input.spin", state 1551, "else"
 240         line 212, ".input.spin", state 1555, "((i<1))"
 241         line 212, ".input.spin", state 1555, "((i>=1))"
 242         line 173, ".input.spin", state 1560, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 243         line 173, ".input.spin", state 1562, "(1)"
 244         line 177, ".input.spin", state 1569, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 245         line 177, ".input.spin", state 1571, "(1)"
 246         line 177, ".input.spin", state 1572, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 247         line 177, ".input.spin", state 1572, "else"
 248         line 175, ".input.spin", state 1577, "((j<1))"
 249         line 175, ".input.spin", state 1577, "((j>=1))"
 250         line 181, ".input.spin", state 1582, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 251         line 158, ".input.spin", state 1592, "(1)"
 252         line 162, ".input.spin", state 1600, "(1)"
 253         line 162, ".input.spin", state 1601, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 254         line 162, ".input.spin", state 1601, "else"
 255         line 160, ".input.spin", state 1606, "((j<1))"
 256         line 160, ".input.spin", state 1606, "((j>=1))"
 257         line 166, ".input.spin", state 1612, "(1)"
 258         line 166, ".input.spin", state 1613, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 259         line 166, ".input.spin", state 1613, "else"
 260         line 168, ".input.spin", state 1616, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 261         line 168, ".input.spin", state 1616, "else"
 262         line 200, ".input.spin", state 1618, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 263         line 200, ".input.spin", state 1618, "else"
 264         line 219, ".input.spin", state 1619, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 265         line 219, ".input.spin", state 1619, "else"
 266         line 354, ".input.spin", state 1625, "((sighand_exec==1))"
 267         line 354, ".input.spin", state 1625, "else"
 268         line 360, ".input.spin", state 1628, "sighand_exec = 1"
 269         line 397, ".input.spin", state 1641, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 270         line 397, ".input.spin", state 1643, "(1)"
 271         line 397, ".input.spin", state 1644, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<0)))"
 272         line 397, ".input.spin", state 1644, "else"
 273         line 397, ".input.spin", state 1647, "(1)"
 274         line 401, ".input.spin", state 1655, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 275         line 401, ".input.spin", state 1657, "(1)"
 276         line 401, ".input.spin", state 1658, "((cache_dirty_urcu_active_readers.bitfield&(1<<0)))"
 277         line 401, ".input.spin", state 1658, "else"
 278         line 401, ".input.spin", state 1661, "(1)"
 279         line 401, ".input.spin", state 1662, "(1)"
 280         line 401, ".input.spin", state 1662, "(1)"
 281         line 399, ".input.spin", state 1667, "((i<1))"
 282         line 399, ".input.spin", state 1667, "((i>=1))"
 283         line 406, ".input.spin", state 1673, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 284         line 407, ".input.spin", state 1686, "(1)"
 285         line 407, ".input.spin", state 1687, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<0))))"
 286         line 407, ".input.spin", state 1687, "else"
 287         line 407, ".input.spin", state 1690, "(1)"
 288         line 407, ".input.spin", state 1691, "(1)"
 289         line 407, ".input.spin", state 1691, "(1)"
 290         line 411, ".input.spin", state 1699, "(1)"
 291         line 411, ".input.spin", state 1700, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<0))))"
 292         line 411, ".input.spin", state 1700, "else"
 293         line 411, ".input.spin", state 1703, "(1)"
 294         line 411, ".input.spin", state 1704, "(1)"
 295         line 411, ".input.spin", state 1704, "(1)"
 296         line 409, ".input.spin", state 1709, "((i<1))"
 297         line 409, ".input.spin", state 1709, "((i>=1))"
 298         line 416, ".input.spin", state 1716, "(1)"
 299         line 416, ".input.spin", state 1717, "(!((cache_dirty_generation_ptr.bitfield&(1<<0))))"
 300         line 416, ".input.spin", state 1717, "else"
 301         line 416, ".input.spin", state 1720, "(1)"
 302         line 416, ".input.spin", state 1721, "(1)"
 303         line 416, ".input.spin", state 1721, "(1)"
 304         line 418, ".input.spin", state 1724, "(1)"
 305         line 418, ".input.spin", state 1724, "(1)"
 306         line 360, ".input.spin", state 1733, "sighand_exec = 1"
 307         line 177, ".input.spin", state 1758, "(1)"
 308         line 181, ".input.spin", state 1769, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 309         line 158, ".input.spin", state 1779, "(1)"
 310         line 162, ".input.spin", state 1787, "(1)"
 311         line 166, ".input.spin", state 1799, "(1)"
 312         line 173, ".input.spin", state 1810, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
 313         line 177, ".input.spin", state 1819, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
 314         line 181, ".input.spin", state 1832, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
 315         line 158, ".input.spin", state 1842, "(1)"
 316         line 162, ".input.spin", state 1850, "(1)"
 317         line 166, ".input.spin", state 1862, "(1)"
 318         line 173, ".input.spin", state 1877, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<0)))"
 319         line 177, ".input.spin", state 1886, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<0)))"
 320         line 181, ".input.spin", state 1899, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<0)))"
 321         line 158, ".input.spin", state 1909, "(1)"
 322         line 162, ".input.spin", state 1917, "(1)"
 323         line 166, ".input.spin", state 1929, "(1)"
 324         line 700, ".input.spin", state 1968, "-end-"
 325         (215 of 1968 states)
 326 unreached in proctype :init:
 327         (0 of 46 states)
 328
 329 pan: elapsed time 0.12 seconds
 330 pan: rate 167733.33 states/second
 331 pan: avg transition delay 5.6709e-07 usec
 332 cp .input.spin asserts.spin.input
 333 cp .input.spin.trail asserts.spin.input.trail
 334 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'