--- /dev/null
+make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
+rm -f pan* trail.out .input.spin* *.spin.trail .input.define
+touch .input.define
+cat .input.define > pan.ltl
+cat DEFINES >> pan.ltl
+spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl
+cp urcu_progress_writer_error.define .input.define
+cat .input.define > .input.spin
+cat DEFINES >> .input.spin
+cat urcu.spin >> .input.spin
+rm -f .input.spin.trail
+spin -a -X -N pan.ltl .input.spin
+Exit-Status 0
+gcc -O2 -w -DHASH64 -o pan pan.c
+./pan -a -f -v -c1 -X -m10000000 -w20
+warning: for p.o. reduction to be valid the never claim must be stutter-invariant
+(never claims generated from LTL formulae are stutter-invariant)
+depth 0: Claim reached state 5 (line 745)
+depth 15: Claim reached state 9 (line 750)
+depth 1194: Claim reached state 9 (line 749)
+Depth= 3253 States= 1e+06 Transitions= 1.06e+07 Memory= 484.416 t= 9.57 R= 1e+05
+Depth= 3253 States= 2e+06 Transitions= 2.04e+07 Memory= 501.311 t= 18.5 R= 1e+05
+pan: acceptance cycle (at depth 1938)
+pan: wrote .input.spin.trail
+
+(Spin Version 5.1.7 -- 23 December 2008)
+Warning: Search not completed
+ + Partial Order Reduction
+
+Full statespace search for:
+ never claim +
+ assertion violations + (if within scope of claim)
+ acceptance cycles + (fairness enabled)
+ invalid end states - (disabled by never claim)
+
+State-vector 64 byte, depth reached 23684, errors: 1
+ 682672 states, stored (2.81536e+06 visited)
+ 30226122 states, matched
+ 33041487 transitions (= visited+matched)
+1.1631626e+08 atomic steps
+hash conflicts: 6056013 (resolved)
+
+Stats on memory usage (in Megabytes):
+ 59.896 equivalent memory usage for states (stored*(State-vector + overhead))
+ 47.456 actual memory usage for states (compression: 79.23%)
+ state-vector as stored = 45 byte + 28 byte overhead
+ 8.000 memory used for hash table (-w20)
+ 457.764 memory used for DFS stack (-m10000000)
+ 513.127 total actual memory usage
+
+unreached in proctype urcu_reader
+ line 400, "pan.___", state 16, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 48, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 61, "(1)"
+ line 419, "pan.___", state 91, "(1)"
+ line 400, "pan.___", state 113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 145, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 158, "(1)"
+ line 419, "pan.___", state 188, "(1)"
+ line 400, "pan.___", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 243, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 256, "(1)"
+ line 419, "pan.___", state 286, "(1)"
+ line 400, "pan.___", state 350, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 382, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 395, "(1)"
+ line 419, "pan.___", state 425, "(1)"
+ line 541, "pan.___", state 456, "-end-"
+ (17 of 456 states)
+unreached in proctype urcu_reader_sig
+ line 400, "pan.___", state 25, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 57, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 70, "(1)"
+ line 419, "pan.___", state 100, "(1)"
+ line 400, "pan.___", state 113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 145, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 158, "(1)"
+ line 419, "pan.___", state 188, "(1)"
+ line 400, "pan.___", state 202, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 234, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 247, "(1)"
+ line 419, "pan.___", state 277, "(1)"
+ line 400, "pan.___", state 314, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 346, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 359, "(1)"
+ line 419, "pan.___", state 389, "(1)"
+ line 615, "pan.___", state 411, "-end-"
+ (17 of 411 states)
+unreached in proctype urcu_writer
+ line 400, "pan.___", state 14, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 20, "(1)"
+ line 404, "pan.___", state 28, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 34, "(1)"
+ line 404, "pan.___", state 35, "(1)"
+ line 404, "pan.___", state 35, "(1)"
+ line 402, "pan.___", state 40, "((i<1))"
+ line 402, "pan.___", state 40, "((i>=1))"
+ line 409, "pan.___", state 46, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 59, "(1)"
+ line 410, "pan.___", state 60, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 60, "else"
+ line 410, "pan.___", state 63, "(1)"
+ line 410, "pan.___", state 64, "(1)"
+ line 410, "pan.___", state 64, "(1)"
+ line 414, "pan.___", state 72, "(1)"
+ line 414, "pan.___", state 73, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 73, "else"
+ line 414, "pan.___", state 76, "(1)"
+ line 414, "pan.___", state 77, "(1)"
+ line 414, "pan.___", state 77, "(1)"
+ line 412, "pan.___", state 82, "((i<1))"
+ line 412, "pan.___", state 82, "((i>=1))"
+ line 419, "pan.___", state 89, "(1)"
+ line 419, "pan.___", state 90, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 90, "else"
+ line 419, "pan.___", state 93, "(1)"
+ line 419, "pan.___", state 94, "(1)"
+ line 419, "pan.___", state 94, "(1)"
+ line 370, "pan.___", state 99, "(1)"
+ line 640, "pan.___", state 103, "cached_generation_ptr.val[( ((_pid<2)) ? (0) : (1) )] = (old_gen+1)"
+ line 638, "pan.___", state 104, "old_gen = cached_generation_ptr.val[( ((_pid<2)) ? (0) : (1) )]"
+ line 400, "pan.___", state 108, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 114, "(1)"
+ line 404, "pan.___", state 122, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 128, "(1)"
+ line 404, "pan.___", state 129, "(1)"
+ line 404, "pan.___", state 129, "(1)"
+ line 402, "pan.___", state 134, "((i<1))"
+ line 402, "pan.___", state 134, "((i>=1))"
+ line 410, "pan.___", state 153, "(1)"
+ line 410, "pan.___", state 154, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 154, "else"
+ line 410, "pan.___", state 157, "(1)"
+ line 410, "pan.___", state 158, "(1)"
+ line 410, "pan.___", state 158, "(1)"
+ line 414, "pan.___", state 166, "(1)"
+ line 414, "pan.___", state 167, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 167, "else"
+ line 414, "pan.___", state 170, "(1)"
+ line 414, "pan.___", state 171, "(1)"
+ line 414, "pan.___", state 171, "(1)"
+ line 412, "pan.___", state 176, "((i<1))"
+ line 412, "pan.___", state 176, "((i>=1))"
+ line 419, "pan.___", state 183, "(1)"
+ line 419, "pan.___", state 184, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 184, "else"
+ line 419, "pan.___", state 187, "(1)"
+ line 419, "pan.___", state 188, "(1)"
+ line 419, "pan.___", state 188, "(1)"
+ line 421, "pan.___", state 191, "(1)"
+ line 421, "pan.___", state 191, "(1)"
+ line 370, "pan.___", state 193, "(1)"
+ line 653, "pan.___", state 199, "(1)"
+ line 647, "pan.___", state 202, "((write_lock==0))"
+ line 647, "pan.___", state 202, "else"
+ line 645, "pan.___", state 203, "(1)"
+ line 176, "pan.___", state 208, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 180, "pan.___", state 217, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 178, "pan.___", state 225, "((j<1))"
+ line 178, "pan.___", state 225, "((j>=1))"
+ line 184, "pan.___", state 230, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 161, "pan.___", state 240, "(1)"
+ line 165, "pan.___", state 248, "(1)"
+ line 165, "pan.___", state 249, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 165, "pan.___", state 249, "else"
+ line 163, "pan.___", state 254, "((j<1))"
+ line 163, "pan.___", state 254, "((j>=1))"
+ line 169, "pan.___", state 260, "(1)"
+ line 169, "pan.___", state 261, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 169, "pan.___", state 261, "else"
+ line 171, "pan.___", state 264, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 171, "pan.___", state 264, "else"
+ line 176, "pan.___", state 271, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
+ line 180, "pan.___", state 280, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<i)))"
+ line 178, "pan.___", state 288, "((j<1))"
+ line 178, "pan.___", state 288, "((j>=1))"
+ line 184, "pan.___", state 293, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
+ line 161, "pan.___", state 303, "(1)"
+ line 165, "pan.___", state 311, "(1)"
+ line 165, "pan.___", state 312, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<i))))"
+ line 165, "pan.___", state 312, "else"
+ line 163, "pan.___", state 317, "((j<1))"
+ line 163, "pan.___", state 317, "((j>=1))"
+ line 169, "pan.___", state 323, "(1)"
+ line 169, "pan.___", state 324, "(!((cache_dirty_generation_ptr.bitfield&(1<<i))))"
+ line 169, "pan.___", state 324, "else"
+ line 171, "pan.___", state 327, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<i))))"
+ line 171, "pan.___", state 327, "else"
+ line 215, "pan.___", state 333, "((i<1))"
+ line 215, "pan.___", state 333, "((i>=1))"
+ line 176, "pan.___", state 338, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 180, "pan.___", state 347, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 178, "pan.___", state 355, "((j<1))"
+ line 178, "pan.___", state 355, "((j>=1))"
+ line 184, "pan.___", state 360, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 161, "pan.___", state 370, "(1)"
+ line 165, "pan.___", state 378, "(1)"
+ line 165, "pan.___", state 379, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 165, "pan.___", state 379, "else"
+ line 163, "pan.___", state 384, "((j<1))"
+ line 163, "pan.___", state 384, "((j>=1))"
+ line 169, "pan.___", state 390, "(1)"
+ line 169, "pan.___", state 391, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 169, "pan.___", state 391, "else"
+ line 171, "pan.___", state 394, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 171, "pan.___", state 394, "else"
+ line 400, "pan.___", state 404, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 410, "(1)"
+ line 404, "pan.___", state 418, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 424, "(1)"
+ line 404, "pan.___", state 425, "(1)"
+ line 404, "pan.___", state 425, "(1)"
+ line 402, "pan.___", state 430, "((i<1))"
+ line 402, "pan.___", state 430, "((i>=1))"
+ line 409, "pan.___", state 436, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 449, "(1)"
+ line 410, "pan.___", state 450, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 450, "else"
+ line 410, "pan.___", state 453, "(1)"
+ line 410, "pan.___", state 454, "(1)"
+ line 410, "pan.___", state 454, "(1)"
+ line 414, "pan.___", state 462, "(1)"
+ line 414, "pan.___", state 463, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 463, "else"
+ line 414, "pan.___", state 466, "(1)"
+ line 414, "pan.___", state 467, "(1)"
+ line 414, "pan.___", state 467, "(1)"
+ line 412, "pan.___", state 472, "((i<1))"
+ line 412, "pan.___", state 472, "((i>=1))"
+ line 419, "pan.___", state 479, "(1)"
+ line 419, "pan.___", state 480, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 480, "else"
+ line 419, "pan.___", state 483, "(1)"
+ line 419, "pan.___", state 484, "(1)"
+ line 419, "pan.___", state 484, "(1)"
+ line 421, "pan.___", state 487, "(1)"
+ line 421, "pan.___", state 487, "(1)"
+ line 370, "pan.___", state 489, "(1)"
+ line 662, "pan.___", state 492, "cached_urcu_gp_ctr.val[( ((_pid<2)) ? (0) : (1) )] = (tmp^(1<<7))"
+ line 400, "pan.___", state 498, "(1)"
+ line 400, "pan.___", state 499, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 499, "else"
+ line 400, "pan.___", state 502, "(1)"
+ line 404, "pan.___", state 510, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 516, "(1)"
+ line 404, "pan.___", state 517, "(1)"
+ line 404, "pan.___", state 517, "(1)"
+ line 402, "pan.___", state 522, "((i<1))"
+ line 402, "pan.___", state 522, "((i>=1))"
+ line 409, "pan.___", state 528, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 541, "(1)"
+ line 410, "pan.___", state 542, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 542, "else"
+ line 410, "pan.___", state 545, "(1)"
+ line 410, "pan.___", state 546, "(1)"
+ line 410, "pan.___", state 546, "(1)"
+ line 414, "pan.___", state 554, "(1)"
+ line 414, "pan.___", state 555, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 555, "else"
+ line 414, "pan.___", state 558, "(1)"
+ line 414, "pan.___", state 559, "(1)"
+ line 414, "pan.___", state 559, "(1)"
+ line 412, "pan.___", state 564, "((i<1))"
+ line 412, "pan.___", state 564, "((i>=1))"
+ line 419, "pan.___", state 571, "(1)"
+ line 419, "pan.___", state 572, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 572, "else"
+ line 419, "pan.___", state 575, "(1)"
+ line 419, "pan.___", state 576, "(1)"
+ line 419, "pan.___", state 576, "(1)"
+ line 421, "pan.___", state 579, "(1)"
+ line 421, "pan.___", state 579, "(1)"
+ line 370, "pan.___", state 581, "(1)"
+ line 400, "pan.___", state 589, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 595, "(1)"
+ line 404, "pan.___", state 603, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 609, "(1)"
+ line 404, "pan.___", state 610, "(1)"
+ line 404, "pan.___", state 610, "(1)"
+ line 402, "pan.___", state 615, "((i<1))"
+ line 402, "pan.___", state 615, "((i>=1))"
+ line 409, "pan.___", state 621, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 634, "(1)"
+ line 410, "pan.___", state 635, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 635, "else"
+ line 410, "pan.___", state 638, "(1)"
+ line 410, "pan.___", state 639, "(1)"
+ line 410, "pan.___", state 639, "(1)"
+ line 414, "pan.___", state 647, "(1)"
+ line 414, "pan.___", state 648, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 648, "else"
+ line 414, "pan.___", state 651, "(1)"
+ line 414, "pan.___", state 652, "(1)"
+ line 414, "pan.___", state 652, "(1)"
+ line 412, "pan.___", state 657, "((i<1))"
+ line 412, "pan.___", state 657, "((i>=1))"
+ line 419, "pan.___", state 664, "(1)"
+ line 419, "pan.___", state 665, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 665, "else"
+ line 419, "pan.___", state 668, "(1)"
+ line 419, "pan.___", state 669, "(1)"
+ line 419, "pan.___", state 669, "(1)"
+ line 421, "pan.___", state 672, "(1)"
+ line 421, "pan.___", state 672, "(1)"
+ line 370, "pan.___", state 674, "(1)"
+ line 400, "pan.___", state 679, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 681, "(1)"
+ line 400, "pan.___", state 682, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 682, "else"
+ line 400, "pan.___", state 685, "(1)"
+ line 404, "pan.___", state 693, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 695, "(1)"
+ line 404, "pan.___", state 696, "((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 696, "else"
+ line 404, "pan.___", state 699, "(1)"
+ line 404, "pan.___", state 700, "(1)"
+ line 404, "pan.___", state 700, "(1)"
+ line 402, "pan.___", state 705, "((i<1))"
+ line 402, "pan.___", state 705, "((i>=1))"
+ line 409, "pan.___", state 711, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 724, "(1)"
+ line 410, "pan.___", state 725, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 725, "else"
+ line 410, "pan.___", state 728, "(1)"
+ line 410, "pan.___", state 729, "(1)"
+ line 410, "pan.___", state 729, "(1)"
+ line 414, "pan.___", state 737, "(1)"
+ line 414, "pan.___", state 738, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 738, "else"
+ line 414, "pan.___", state 741, "(1)"
+ line 414, "pan.___", state 742, "(1)"
+ line 414, "pan.___", state 742, "(1)"
+ line 412, "pan.___", state 747, "((i<1))"
+ line 412, "pan.___", state 747, "((i>=1))"
+ line 419, "pan.___", state 754, "(1)"
+ line 419, "pan.___", state 755, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 755, "else"
+ line 419, "pan.___", state 758, "(1)"
+ line 419, "pan.___", state 759, "(1)"
+ line 419, "pan.___", state 759, "(1)"
+ line 421, "pan.___", state 762, "(1)"
+ line 421, "pan.___", state 762, "(1)"
+ line 370, "pan.___", state 764, "(1)"
+ line 430, "pan.___", state 767, "(((tmp2&((1<<7)-1))&&((tmp2^cached_urcu_gp_ctr.val[( ((_pid<2)) ? (0) : (1) )])&(1<<7))))"
+ line 430, "pan.___", state 767, "else"
+ line 400, "pan.___", state 777, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 779, "(1)"
+ line 400, "pan.___", state 780, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 780, "else"
+ line 400, "pan.___", state 783, "(1)"
+ line 404, "pan.___", state 791, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 793, "(1)"
+ line 404, "pan.___", state 794, "((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 794, "else"
+ line 404, "pan.___", state 797, "(1)"
+ line 404, "pan.___", state 798, "(1)"
+ line 404, "pan.___", state 798, "(1)"
+ line 402, "pan.___", state 803, "((i<1))"
+ line 402, "pan.___", state 803, "((i>=1))"
+ line 409, "pan.___", state 809, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 822, "(1)"
+ line 410, "pan.___", state 823, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 823, "else"
+ line 410, "pan.___", state 826, "(1)"
+ line 410, "pan.___", state 827, "(1)"
+ line 410, "pan.___", state 827, "(1)"
+ line 414, "pan.___", state 835, "(1)"
+ line 414, "pan.___", state 836, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 836, "else"
+ line 414, "pan.___", state 839, "(1)"
+ line 414, "pan.___", state 840, "(1)"
+ line 414, "pan.___", state 840, "(1)"
+ line 412, "pan.___", state 845, "((i<1))"
+ line 412, "pan.___", state 845, "((i>=1))"
+ line 419, "pan.___", state 852, "(1)"
+ line 419, "pan.___", state 853, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 853, "else"
+ line 419, "pan.___", state 856, "(1)"
+ line 419, "pan.___", state 857, "(1)"
+ line 419, "pan.___", state 857, "(1)"
+ line 421, "pan.___", state 860, "(1)"
+ line 421, "pan.___", state 860, "(1)"
+ line 370, "pan.___", state 862, "(1)"
+ line 449, "pan.___", state 870, "((tmp<1))"
+ line 449, "pan.___", state 870, "((tmp>=1))"
+ line 462, "pan.___", state 873, "tmp = 0"
+ line 400, "pan.___", state 877, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 883, "(1)"
+ line 404, "pan.___", state 891, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 897, "(1)"
+ line 404, "pan.___", state 898, "(1)"
+ line 404, "pan.___", state 898, "(1)"
+ line 402, "pan.___", state 903, "((i<1))"
+ line 402, "pan.___", state 903, "((i>=1))"
+ line 409, "pan.___", state 909, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 922, "(1)"
+ line 410, "pan.___", state 923, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 923, "else"
+ line 410, "pan.___", state 926, "(1)"
+ line 410, "pan.___", state 927, "(1)"
+ line 410, "pan.___", state 927, "(1)"
+ line 414, "pan.___", state 935, "(1)"
+ line 414, "pan.___", state 936, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 936, "else"
+ line 414, "pan.___", state 939, "(1)"
+ line 414, "pan.___", state 940, "(1)"
+ line 414, "pan.___", state 940, "(1)"
+ line 412, "pan.___", state 945, "((i<1))"
+ line 412, "pan.___", state 945, "((i>=1))"
+ line 419, "pan.___", state 952, "(1)"
+ line 419, "pan.___", state 953, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 953, "else"
+ line 419, "pan.___", state 956, "(1)"
+ line 419, "pan.___", state 957, "(1)"
+ line 419, "pan.___", state 957, "(1)"
+ line 421, "pan.___", state 960, "(1)"
+ line 421, "pan.___", state 960, "(1)"
+ line 370, "pan.___", state 962, "(1)"
+ line 671, "pan.___", state 963, "tmp = cached_urcu_gp_ctr.val[( ((_pid<2)) ? (0) : (1) )]"
+ line 400, "pan.___", state 967, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 973, "(1)"
+ line 404, "pan.___", state 981, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 987, "(1)"
+ line 404, "pan.___", state 988, "(1)"
+ line 404, "pan.___", state 988, "(1)"
+ line 402, "pan.___", state 993, "((i<1))"
+ line 402, "pan.___", state 993, "((i>=1))"
+ line 409, "pan.___", state 999, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 1012, "(1)"
+ line 410, "pan.___", state 1013, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 1013, "else"
+ line 410, "pan.___", state 1016, "(1)"
+ line 410, "pan.___", state 1017, "(1)"
+ line 410, "pan.___", state 1017, "(1)"
+ line 414, "pan.___", state 1025, "(1)"
+ line 414, "pan.___", state 1026, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 1026, "else"
+ line 414, "pan.___", state 1029, "(1)"
+ line 414, "pan.___", state 1030, "(1)"
+ line 414, "pan.___", state 1030, "(1)"
+ line 412, "pan.___", state 1035, "((i<1))"
+ line 412, "pan.___", state 1035, "((i>=1))"
+ line 419, "pan.___", state 1042, "(1)"
+ line 419, "pan.___", state 1043, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 1043, "else"
+ line 419, "pan.___", state 1046, "(1)"
+ line 419, "pan.___", state 1047, "(1)"
+ line 419, "pan.___", state 1047, "(1)"
+ line 421, "pan.___", state 1050, "(1)"
+ line 421, "pan.___", state 1050, "(1)"
+ line 370, "pan.___", state 1052, "(1)"
+ line 400, "pan.___", state 1061, "(1)"
+ line 404, "pan.___", state 1073, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 1091, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 414, "pan.___", state 1117, "(1)"
+ line 419, "pan.___", state 1134, "(1)"
+ line 404, "pan.___", state 1166, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 1184, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 414, "pan.___", state 1210, "(1)"
+ line 419, "pan.___", state 1227, "(1)"
+ line 400, "pan.___", state 1242, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 1256, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 409, "pan.___", state 1274, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 1287, "(1)"
+ line 414, "pan.___", state 1300, "(1)"
+ line 419, "pan.___", state 1317, "(1)"
+ line 400, "pan.___", state 1340, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 1342, "(1)"
+ line 400, "pan.___", state 1343, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 400, "pan.___", state 1343, "else"
+ line 400, "pan.___", state 1346, "(1)"
+ line 404, "pan.___", state 1354, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 1356, "(1)"
+ line 404, "pan.___", state 1357, "((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 404, "pan.___", state 1357, "else"
+ line 404, "pan.___", state 1360, "(1)"
+ line 404, "pan.___", state 1361, "(1)"
+ line 404, "pan.___", state 1361, "(1)"
+ line 402, "pan.___", state 1366, "((i<1))"
+ line 402, "pan.___", state 1366, "((i>=1))"
+ line 409, "pan.___", state 1372, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 410, "pan.___", state 1385, "(1)"
+ line 410, "pan.___", state 1386, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 410, "pan.___", state 1386, "else"
+ line 410, "pan.___", state 1389, "(1)"
+ line 410, "pan.___", state 1390, "(1)"
+ line 410, "pan.___", state 1390, "(1)"
+ line 414, "pan.___", state 1398, "(1)"
+ line 414, "pan.___", state 1399, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 414, "pan.___", state 1399, "else"
+ line 414, "pan.___", state 1402, "(1)"
+ line 414, "pan.___", state 1403, "(1)"
+ line 414, "pan.___", state 1403, "(1)"
+ line 412, "pan.___", state 1408, "((i<1))"
+ line 412, "pan.___", state 1408, "((i>=1))"
+ line 419, "pan.___", state 1415, "(1)"
+ line 419, "pan.___", state 1416, "(!((cache_dirty_generation_ptr.bitfield&(1<<( ((_pid<2)) -> (0) : (1) )))))"
+ line 419, "pan.___", state 1416, "else"
+ line 419, "pan.___", state 1419, "(1)"
+ line 419, "pan.___", state 1420, "(1)"
+ line 419, "pan.___", state 1420, "(1)"
+ line 421, "pan.___", state 1423, "(1)"
+ line 421, "pan.___", state 1423, "(1)"
+ line 180, "pan.___", state 1448, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 184, "pan.___", state 1461, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 161, "pan.___", state 1471, "(1)"
+ line 165, "pan.___", state 1479, "(1)"
+ line 169, "pan.___", state 1491, "(1)"
+ line 176, "pan.___", state 1502, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<i)))"
+ line 184, "pan.___", state 1524, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<i)))"
+ line 161, "pan.___", state 1534, "(1)"
+ line 165, "pan.___", state 1542, "(1)"
+ line 169, "pan.___", state 1554, "(1)"
+ line 176, "pan.___", state 1569, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 180, "pan.___", state 1578, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 184, "pan.___", state 1591, "cache_dirty_generation_ptr.bitfield = (cache_dirty_generation_ptr.bitfield&~((1<<( ((_pid<2)) -> (0) : (1) ))))"
+ line 161, "pan.___", state 1601, "(1)"
+ line 165, "pan.___", state 1609, "(1)"
+ line 169, "pan.___", state 1621, "(1)"
+ line 370, "pan.___", state 1642, "(1)"
+ line 696, "pan.___", state 1643, "(1)"
+ line 703, "pan.___", state 1646, "-end-"
+ (308 of 1646 states)
+unreached in proctype :init:
+ (0 of 46 states)
+unreached in proctype :never:
+ line 752, "pan.___", state 11, "-end-"
+ (1 of 11 states)
+
+pan: elapsed time 30.2 seconds
+pan: rate 93347.646 states/second
+pan: avg transition delay 9.1279e-07 usec
+cp .input.spin urcu_progress_writer_error.spin.input
+cp .input.spin.trail urcu_progress_writer_error.spin.input.trail
+make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu'
projects / urcu.git / blobdiff