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