+++ /dev/null
-make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
-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.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 1245)
-depth 23: Claim reached state 9 (line 1250)
-depth 51: Claim reached state 9 (line 1249)
-pan: acceptance cycle (at depth 573)
-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 88 byte, depth reached 3997, errors: 1
- 24768 states, stored (55970 visited)
- 10426084 states, matched
- 10482054 transitions (= visited+matched)
- 56520057 atomic steps
-hash conflicts: 68749 (resolved)
-
-Stats on memory usage (in Megabytes):
- 2.740 equivalent memory usage for states (stored*(State-vector + overhead))
- 2.770 actual memory usage for states (unsuccessful compression: 101.10%)
- state-vector as stored = 89 byte + 28 byte overhead
- 8.000 memory used for hash table (-w20)
- 457.764 memory used for DFS stack (-m10000000)
- 468.498 total actual memory usage
-
-unreached in proctype urcu_reader
- line 647, "pan.___", state 20, "(1)"
- line 250, "pan.___", state 32, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 258, "pan.___", state 54, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 262, "pan.___", state 63, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 227, "pan.___", state 79, "(1)"
- line 231, "pan.___", state 87, "(1)"
- line 235, "pan.___", state 99, "(1)"
- line 239, "pan.___", state 107, "(1)"
- line 387, "pan.___", state 133, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 165, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 179, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 198, "(1)"
- line 413, "pan.___", state 228, "(1)"
- line 417, "pan.___", state 241, "(1)"
- line 663, "pan.___", state 262, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
- line 387, "pan.___", state 269, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 301, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 315, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 334, "(1)"
- line 413, "pan.___", state 364, "(1)"
- line 417, "pan.___", state 377, "(1)"
- line 387, "pan.___", state 398, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 430, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 444, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 463, "(1)"
- line 413, "pan.___", state 493, "(1)"
- line 417, "pan.___", state 506, "(1)"
- line 387, "pan.___", state 529, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 387, "pan.___", state 531, "(1)"
- line 387, "pan.___", state 532, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
- line 387, "pan.___", state 532, "else"
- line 387, "pan.___", state 535, "(1)"
- line 391, "pan.___", state 543, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 391, "pan.___", state 545, "(1)"
- line 391, "pan.___", state 546, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
- line 391, "pan.___", state 546, "else"
- line 391, "pan.___", state 549, "(1)"
- line 391, "pan.___", state 550, "(1)"
- line 391, "pan.___", state 550, "(1)"
- line 389, "pan.___", state 555, "((i<1))"
- line 389, "pan.___", state 555, "((i>=1))"
- line 396, "pan.___", state 561, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 563, "(1)"
- line 396, "pan.___", state 564, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
- line 396, "pan.___", state 564, "else"
- line 396, "pan.___", state 567, "(1)"
- line 396, "pan.___", state 568, "(1)"
- line 396, "pan.___", state 568, "(1)"
- line 400, "pan.___", state 575, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 577, "(1)"
- line 400, "pan.___", state 578, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
- line 400, "pan.___", state 578, "else"
- line 400, "pan.___", state 581, "(1)"
- line 400, "pan.___", state 582, "(1)"
- line 400, "pan.___", state 582, "(1)"
- line 398, "pan.___", state 587, "((i<2))"
- line 398, "pan.___", state 587, "((i>=2))"
- line 404, "pan.___", state 594, "(1)"
- line 404, "pan.___", state 595, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 404, "pan.___", state 595, "else"
- line 404, "pan.___", state 598, "(1)"
- line 404, "pan.___", state 599, "(1)"
- line 404, "pan.___", state 599, "(1)"
- line 408, "pan.___", state 607, "(1)"
- line 408, "pan.___", state 608, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 408, "pan.___", state 608, "else"
- line 408, "pan.___", state 611, "(1)"
- line 408, "pan.___", state 612, "(1)"
- line 408, "pan.___", state 612, "(1)"
- line 406, "pan.___", state 617, "((i<1))"
- line 406, "pan.___", state 617, "((i>=1))"
- line 413, "pan.___", state 624, "(1)"
- line 413, "pan.___", state 625, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 413, "pan.___", state 625, "else"
- line 413, "pan.___", state 628, "(1)"
- line 413, "pan.___", state 629, "(1)"
- line 413, "pan.___", state 629, "(1)"
- line 417, "pan.___", state 637, "(1)"
- line 417, "pan.___", state 638, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 417, "pan.___", state 638, "else"
- line 417, "pan.___", state 641, "(1)"
- line 417, "pan.___", state 642, "(1)"
- line 417, "pan.___", state 642, "(1)"
- line 415, "pan.___", state 647, "((i<2))"
- line 415, "pan.___", state 647, "((i>=2))"
- line 422, "pan.___", state 651, "(1)"
- line 422, "pan.___", state 651, "(1)"
- line 663, "pan.___", state 654, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
- line 663, "pan.___", state 655, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
- line 663, "pan.___", state 656, "(1)"
- line 387, "pan.___", state 663, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 695, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 709, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 728, "(1)"
- line 413, "pan.___", state 758, "(1)"
- line 417, "pan.___", state 771, "(1)"
- line 387, "pan.___", state 799, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 387, "pan.___", state 801, "(1)"
- line 387, "pan.___", state 802, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
- line 387, "pan.___", state 802, "else"
- line 387, "pan.___", state 805, "(1)"
- line 391, "pan.___", state 813, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 391, "pan.___", state 815, "(1)"
- line 391, "pan.___", state 816, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
- line 391, "pan.___", state 816, "else"
- line 391, "pan.___", state 819, "(1)"
- line 391, "pan.___", state 820, "(1)"
- line 391, "pan.___", state 820, "(1)"
- line 389, "pan.___", state 825, "((i<1))"
- line 389, "pan.___", state 825, "((i>=1))"
- line 396, "pan.___", state 831, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 833, "(1)"
- line 396, "pan.___", state 834, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
- line 396, "pan.___", state 834, "else"
- line 396, "pan.___", state 837, "(1)"
- line 396, "pan.___", state 838, "(1)"
- line 396, "pan.___", state 838, "(1)"
- line 400, "pan.___", state 845, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 847, "(1)"
- line 400, "pan.___", state 848, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
- line 400, "pan.___", state 848, "else"
- line 400, "pan.___", state 851, "(1)"
- line 400, "pan.___", state 852, "(1)"
- line 400, "pan.___", state 852, "(1)"
- line 398, "pan.___", state 857, "((i<2))"
- line 398, "pan.___", state 857, "((i>=2))"
- line 404, "pan.___", state 864, "(1)"
- line 404, "pan.___", state 865, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 404, "pan.___", state 865, "else"
- line 404, "pan.___", state 868, "(1)"
- line 404, "pan.___", state 869, "(1)"
- line 404, "pan.___", state 869, "(1)"
- line 408, "pan.___", state 877, "(1)"
- line 408, "pan.___", state 878, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 408, "pan.___", state 878, "else"
- line 408, "pan.___", state 881, "(1)"
- line 408, "pan.___", state 882, "(1)"
- line 408, "pan.___", state 882, "(1)"
- line 406, "pan.___", state 887, "((i<1))"
- line 406, "pan.___", state 887, "((i>=1))"
- line 413, "pan.___", state 894, "(1)"
- line 413, "pan.___", state 895, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 413, "pan.___", state 895, "else"
- line 413, "pan.___", state 898, "(1)"
- line 413, "pan.___", state 899, "(1)"
- line 413, "pan.___", state 899, "(1)"
- line 417, "pan.___", state 907, "(1)"
- line 417, "pan.___", state 908, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 417, "pan.___", state 908, "else"
- line 417, "pan.___", state 911, "(1)"
- line 417, "pan.___", state 912, "(1)"
- line 417, "pan.___", state 912, "(1)"
- line 422, "pan.___", state 921, "(1)"
- line 422, "pan.___", state 921, "(1)"
- line 387, "pan.___", state 928, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 387, "pan.___", state 930, "(1)"
- line 387, "pan.___", state 931, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
- line 387, "pan.___", state 931, "else"
- line 387, "pan.___", state 934, "(1)"
- line 391, "pan.___", state 942, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 391, "pan.___", state 944, "(1)"
- line 391, "pan.___", state 945, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
- line 391, "pan.___", state 945, "else"
- line 391, "pan.___", state 948, "(1)"
- line 391, "pan.___", state 949, "(1)"
- line 391, "pan.___", state 949, "(1)"
- line 389, "pan.___", state 954, "((i<1))"
- line 389, "pan.___", state 954, "((i>=1))"
- line 396, "pan.___", state 960, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 962, "(1)"
- line 396, "pan.___", state 963, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
- line 396, "pan.___", state 963, "else"
- line 396, "pan.___", state 966, "(1)"
- line 396, "pan.___", state 967, "(1)"
- line 396, "pan.___", state 967, "(1)"
- line 400, "pan.___", state 974, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 976, "(1)"
- line 400, "pan.___", state 977, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
- line 400, "pan.___", state 977, "else"
- line 400, "pan.___", state 980, "(1)"
- line 400, "pan.___", state 981, "(1)"
- line 400, "pan.___", state 981, "(1)"
- line 398, "pan.___", state 986, "((i<2))"
- line 398, "pan.___", state 986, "((i>=2))"
- line 404, "pan.___", state 993, "(1)"
- line 404, "pan.___", state 994, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 404, "pan.___", state 994, "else"
- line 404, "pan.___", state 997, "(1)"
- line 404, "pan.___", state 998, "(1)"
- line 404, "pan.___", state 998, "(1)"
- line 408, "pan.___", state 1006, "(1)"
- line 408, "pan.___", state 1007, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 408, "pan.___", state 1007, "else"
- line 408, "pan.___", state 1010, "(1)"
- line 408, "pan.___", state 1011, "(1)"
- line 408, "pan.___", state 1011, "(1)"
- line 406, "pan.___", state 1016, "((i<1))"
- line 406, "pan.___", state 1016, "((i>=1))"
- line 413, "pan.___", state 1023, "(1)"
- line 413, "pan.___", state 1024, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 413, "pan.___", state 1024, "else"
- line 413, "pan.___", state 1027, "(1)"
- line 413, "pan.___", state 1028, "(1)"
- line 413, "pan.___", state 1028, "(1)"
- line 417, "pan.___", state 1036, "(1)"
- line 417, "pan.___", state 1037, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 417, "pan.___", state 1037, "else"
- line 417, "pan.___", state 1040, "(1)"
- line 417, "pan.___", state 1041, "(1)"
- line 417, "pan.___", state 1041, "(1)"
- line 415, "pan.___", state 1046, "((i<2))"
- line 415, "pan.___", state 1046, "((i>=2))"
- line 422, "pan.___", state 1050, "(1)"
- line 422, "pan.___", state 1050, "(1)"
- line 671, "pan.___", state 1054, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))"
- line 387, "pan.___", state 1059, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 1091, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 1105, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 1124, "(1)"
- line 413, "pan.___", state 1154, "(1)"
- line 417, "pan.___", state 1167, "(1)"
- line 387, "pan.___", state 1191, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 1223, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 1237, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 1256, "(1)"
- line 413, "pan.___", state 1286, "(1)"
- line 417, "pan.___", state 1299, "(1)"
- line 387, "pan.___", state 1324, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 1356, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 1370, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 1389, "(1)"
- line 413, "pan.___", state 1419, "(1)"
- line 417, "pan.___", state 1432, "(1)"
- line 387, "pan.___", state 1453, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 1485, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 1499, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 1518, "(1)"
- line 413, "pan.___", state 1548, "(1)"
- line 417, "pan.___", state 1561, "(1)"
- line 387, "pan.___", state 1587, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 1619, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 1633, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 1652, "(1)"
- line 413, "pan.___", state 1682, "(1)"
- line 417, "pan.___", state 1695, "(1)"
- line 387, "pan.___", state 1716, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 1748, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 1762, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 1781, "(1)"
- line 413, "pan.___", state 1811, "(1)"
- line 417, "pan.___", state 1824, "(1)"
- line 387, "pan.___", state 1848, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 1880, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 1894, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 1913, "(1)"
- line 413, "pan.___", state 1943, "(1)"
- line 417, "pan.___", state 1956, "(1)"
- line 710, "pan.___", state 1977, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))"
- line 387, "pan.___", state 1984, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 2016, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 2030, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 2049, "(1)"
- line 413, "pan.___", state 2079, "(1)"
- line 417, "pan.___", state 2092, "(1)"
- line 387, "pan.___", state 2113, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 2145, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 2159, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 2178, "(1)"
- line 413, "pan.___", state 2208, "(1)"
- line 417, "pan.___", state 2221, "(1)"
- line 387, "pan.___", state 2244, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 387, "pan.___", state 2246, "(1)"
- line 387, "pan.___", state 2247, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
- line 387, "pan.___", state 2247, "else"
- line 387, "pan.___", state 2250, "(1)"
- line 391, "pan.___", state 2258, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 391, "pan.___", state 2260, "(1)"
- line 391, "pan.___", state 2261, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
- line 391, "pan.___", state 2261, "else"
- line 391, "pan.___", state 2264, "(1)"
- line 391, "pan.___", state 2265, "(1)"
- line 391, "pan.___", state 2265, "(1)"
- line 389, "pan.___", state 2270, "((i<1))"
- line 389, "pan.___", state 2270, "((i>=1))"
- line 396, "pan.___", state 2276, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 2278, "(1)"
- line 396, "pan.___", state 2279, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
- line 396, "pan.___", state 2279, "else"
- line 396, "pan.___", state 2282, "(1)"
- line 396, "pan.___", state 2283, "(1)"
- line 396, "pan.___", state 2283, "(1)"
- line 400, "pan.___", state 2290, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 2292, "(1)"
- line 400, "pan.___", state 2293, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
- line 400, "pan.___", state 2293, "else"
- line 400, "pan.___", state 2296, "(1)"
- line 400, "pan.___", state 2297, "(1)"
- line 400, "pan.___", state 2297, "(1)"
- line 398, "pan.___", state 2302, "((i<2))"
- line 398, "pan.___", state 2302, "((i>=2))"
- line 404, "pan.___", state 2309, "(1)"
- line 404, "pan.___", state 2310, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 404, "pan.___", state 2310, "else"
- line 404, "pan.___", state 2313, "(1)"
- line 404, "pan.___", state 2314, "(1)"
- line 404, "pan.___", state 2314, "(1)"
- line 408, "pan.___", state 2322, "(1)"
- line 408, "pan.___", state 2323, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 408, "pan.___", state 2323, "else"
- line 408, "pan.___", state 2326, "(1)"
- line 408, "pan.___", state 2327, "(1)"
- line 408, "pan.___", state 2327, "(1)"
- line 406, "pan.___", state 2332, "((i<1))"
- line 406, "pan.___", state 2332, "((i>=1))"
- line 413, "pan.___", state 2339, "(1)"
- line 413, "pan.___", state 2340, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 413, "pan.___", state 2340, "else"
- line 413, "pan.___", state 2343, "(1)"
- line 413, "pan.___", state 2344, "(1)"
- line 413, "pan.___", state 2344, "(1)"
- line 417, "pan.___", state 2352, "(1)"
- line 417, "pan.___", state 2353, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 417, "pan.___", state 2353, "else"
- line 417, "pan.___", state 2356, "(1)"
- line 417, "pan.___", state 2357, "(1)"
- line 417, "pan.___", state 2357, "(1)"
- line 415, "pan.___", state 2362, "((i<2))"
- line 415, "pan.___", state 2362, "((i>=2))"
- line 422, "pan.___", state 2366, "(1)"
- line 422, "pan.___", state 2366, "(1)"
- line 710, "pan.___", state 2369, "cached_urcu_active_readers.val[_pid] = (tmp+1)"
- line 710, "pan.___", state 2370, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))"
- line 710, "pan.___", state 2371, "(1)"
- line 387, "pan.___", state 2378, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 2410, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 2424, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 2443, "(1)"
- line 413, "pan.___", state 2473, "(1)"
- line 417, "pan.___", state 2486, "(1)"
- line 387, "pan.___", state 2513, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 2545, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 2559, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 2578, "(1)"
- line 413, "pan.___", state 2608, "(1)"
- line 417, "pan.___", state 2621, "(1)"
- line 387, "pan.___", state 2642, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 2674, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 2688, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 2707, "(1)"
- line 413, "pan.___", state 2737, "(1)"
- line 417, "pan.___", state 2750, "(1)"
- line 227, "pan.___", state 2783, "(1)"
- line 235, "pan.___", state 2803, "(1)"
- line 239, "pan.___", state 2811, "(1)"
- line 227, "pan.___", state 2826, "(1)"
- line 235, "pan.___", state 2846, "(1)"
- line 239, "pan.___", state 2854, "(1)"
- line 870, "pan.___", state 2871, "-end-"
- (279 of 2871 states)
-unreached in proctype urcu_writer
- line 387, "pan.___", state 18, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 387, "pan.___", state 24, "(1)"
- line 391, "pan.___", state 32, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 391, "pan.___", state 38, "(1)"
- line 391, "pan.___", state 39, "(1)"
- line 391, "pan.___", state 39, "(1)"
- line 389, "pan.___", state 44, "((i<1))"
- line 389, "pan.___", state 44, "((i>=1))"
- line 396, "pan.___", state 50, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 56, "(1)"
- line 396, "pan.___", state 57, "(1)"
- line 396, "pan.___", state 57, "(1)"
- line 400, "pan.___", state 64, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 70, "(1)"
- line 400, "pan.___", state 71, "(1)"
- line 400, "pan.___", state 71, "(1)"
- line 398, "pan.___", state 76, "((i<2))"
- line 398, "pan.___", state 76, "((i>=2))"
- line 404, "pan.___", state 83, "(1)"
- line 404, "pan.___", state 84, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 404, "pan.___", state 84, "else"
- line 404, "pan.___", state 87, "(1)"
- line 404, "pan.___", state 88, "(1)"
- line 404, "pan.___", state 88, "(1)"
- line 408, "pan.___", state 96, "(1)"
- line 408, "pan.___", state 97, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 408, "pan.___", state 97, "else"
- line 408, "pan.___", state 100, "(1)"
- line 408, "pan.___", state 101, "(1)"
- line 408, "pan.___", state 101, "(1)"
- line 406, "pan.___", state 106, "((i<1))"
- line 406, "pan.___", state 106, "((i>=1))"
- line 413, "pan.___", state 113, "(1)"
- line 413, "pan.___", state 114, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 413, "pan.___", state 114, "else"
- line 413, "pan.___", state 117, "(1)"
- line 413, "pan.___", state 118, "(1)"
- line 413, "pan.___", state 118, "(1)"
- line 417, "pan.___", state 126, "(1)"
- line 417, "pan.___", state 127, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 417, "pan.___", state 127, "else"
- line 417, "pan.___", state 130, "(1)"
- line 417, "pan.___", state 131, "(1)"
- line 417, "pan.___", state 131, "(1)"
- line 415, "pan.___", state 136, "((i<2))"
- line 415, "pan.___", state 136, "((i>=2))"
- line 422, "pan.___", state 140, "(1)"
- line 422, "pan.___", state 140, "(1)"
- line 250, "pan.___", state 149, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 254, "pan.___", state 158, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 252, "pan.___", state 166, "((i<1))"
- line 252, "pan.___", state 166, "((i>=1))"
- line 258, "pan.___", state 171, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 993, "pan.___", state 199, "old_data = cached_rcu_ptr.val[_pid]"
- line 387, "pan.___", state 211, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 391, "pan.___", state 225, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 243, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 257, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 404, "pan.___", state 276, "(1)"
- line 408, "pan.___", state 289, "(1)"
- line 413, "pan.___", state 306, "(1)"
- line 417, "pan.___", state 319, "(1)"
- line 391, "pan.___", state 356, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 374, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 388, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 408, "pan.___", state 420, "(1)"
- line 413, "pan.___", state 437, "(1)"
- line 417, "pan.___", state 450, "(1)"
- line 391, "pan.___", state 494, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 512, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 526, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 408, "pan.___", state 558, "(1)"
- line 413, "pan.___", state 575, "(1)"
- line 417, "pan.___", state 588, "(1)"
- line 391, "pan.___", state 623, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 641, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 655, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 408, "pan.___", state 687, "(1)"
- line 413, "pan.___", state 704, "(1)"
- line 417, "pan.___", state 717, "(1)"
- line 391, "pan.___", state 754, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 396, "pan.___", state 772, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 400, "pan.___", state 786, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 408, "pan.___", state 818, "(1)"
- line 413, "pan.___", state 835, "(1)"
- line 417, "pan.___", state 848, "(1)"
- line 1113, "pan.___", state 872, "_proc_urcu_writer = (_proc_urcu_writer&~(((1<<12)|(1<<11))))"
- line 250, "pan.___", state 903, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 254, "pan.___", state 912, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 252, "pan.___", state 920, "((i<1))"
- line 252, "pan.___", state 920, "((i>=1))"
- line 258, "pan.___", state 927, "(1)"
- line 258, "pan.___", state 928, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
- line 258, "pan.___", state 928, "else"
- line 262, "pan.___", state 934, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 260, "pan.___", state 942, "((i<2))"
- line 260, "pan.___", state 942, "((i>=2))"
- line 227, "pan.___", state 950, "(1)"
- line 231, "pan.___", state 958, "(1)"
- line 231, "pan.___", state 959, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 231, "pan.___", state 959, "else"
- line 229, "pan.___", state 964, "((i<1))"
- line 229, "pan.___", state 964, "((i>=1))"
- line 235, "pan.___", state 970, "(1)"
- line 235, "pan.___", state 971, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 235, "pan.___", state 971, "else"
- line 239, "pan.___", state 978, "(1)"
- line 239, "pan.___", state 979, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 239, "pan.___", state 979, "else"
- line 244, "pan.___", state 988, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 244, "pan.___", state 988, "else"
- line 250, "pan.___", state 1009, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 254, "pan.___", state 1018, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 258, "pan.___", state 1031, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 262, "pan.___", state 1040, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 227, "pan.___", state 1056, "(1)"
- line 231, "pan.___", state 1064, "(1)"
- line 235, "pan.___", state 1076, "(1)"
- line 239, "pan.___", state 1084, "(1)"
- line 250, "pan.___", state 1101, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 254, "pan.___", state 1110, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 252, "pan.___", state 1118, "((i<1))"
- line 252, "pan.___", state 1118, "((i>=1))"
- line 258, "pan.___", state 1123, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 262, "pan.___", state 1132, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 260, "pan.___", state 1140, "((i<2))"
- line 260, "pan.___", state 1140, "((i>=2))"
- line 227, "pan.___", state 1148, "(1)"
- line 231, "pan.___", state 1156, "(1)"
- line 231, "pan.___", state 1157, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 231, "pan.___", state 1157, "else"
- line 229, "pan.___", state 1162, "((i<1))"
- line 229, "pan.___", state 1162, "((i>=1))"
- line 235, "pan.___", state 1168, "(1)"
- line 235, "pan.___", state 1169, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 235, "pan.___", state 1169, "else"
- line 239, "pan.___", state 1176, "(1)"
- line 239, "pan.___", state 1177, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 239, "pan.___", state 1177, "else"
- line 244, "pan.___", state 1186, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 244, "pan.___", state 1186, "else"
- line 1180, "pan.___", state 1189, "i = 0"
- line 1180, "pan.___", state 1191, "reader_barrier = 1"
- line 1180, "pan.___", state 1202, "((i<1))"
- line 1180, "pan.___", state 1202, "((i>=1))"
- line 250, "pan.___", state 1207, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 254, "pan.___", state 1216, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 252, "pan.___", state 1224, "((i<1))"
- line 252, "pan.___", state 1224, "((i>=1))"
- line 258, "pan.___", state 1229, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 262, "pan.___", state 1238, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 260, "pan.___", state 1246, "((i<2))"
- line 260, "pan.___", state 1246, "((i>=2))"
- line 227, "pan.___", state 1254, "(1)"
- line 231, "pan.___", state 1262, "(1)"
- line 231, "pan.___", state 1263, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 231, "pan.___", state 1263, "else"
- line 229, "pan.___", state 1268, "((i<1))"
- line 229, "pan.___", state 1268, "((i>=1))"
- line 235, "pan.___", state 1274, "(1)"
- line 235, "pan.___", state 1275, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 235, "pan.___", state 1275, "else"
- line 239, "pan.___", state 1282, "(1)"
- line 239, "pan.___", state 1283, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 239, "pan.___", state 1283, "else"
- line 244, "pan.___", state 1292, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 244, "pan.___", state 1292, "else"
- line 250, "pan.___", state 1299, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 250, "pan.___", state 1301, "(1)"
- line 254, "pan.___", state 1308, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 254, "pan.___", state 1310, "(1)"
- line 254, "pan.___", state 1311, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
- line 254, "pan.___", state 1311, "else"
- line 252, "pan.___", state 1316, "((i<1))"
- line 252, "pan.___", state 1316, "((i>=1))"
- line 258, "pan.___", state 1321, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 258, "pan.___", state 1323, "(1)"
- line 258, "pan.___", state 1324, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
- line 258, "pan.___", state 1324, "else"
- line 262, "pan.___", state 1330, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 262, "pan.___", state 1332, "(1)"
- line 262, "pan.___", state 1333, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
- line 262, "pan.___", state 1333, "else"
- line 260, "pan.___", state 1338, "((i<2))"
- line 260, "pan.___", state 1338, "((i>=2))"
- line 227, "pan.___", state 1346, "(1)"
- line 231, "pan.___", state 1354, "(1)"
- line 231, "pan.___", state 1355, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 231, "pan.___", state 1355, "else"
- line 229, "pan.___", state 1360, "((i<1))"
- line 229, "pan.___", state 1360, "((i>=1))"
- line 235, "pan.___", state 1366, "(1)"
- line 235, "pan.___", state 1367, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 235, "pan.___", state 1367, "else"
- line 239, "pan.___", state 1374, "(1)"
- line 239, "pan.___", state 1375, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 239, "pan.___", state 1375, "else"
- line 244, "pan.___", state 1384, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 244, "pan.___", state 1384, "else"
- line 1183, "pan.___", state 1387, "i = 0"
- line 1183, "pan.___", state 1389, "reader_barrier = 1"
- line 1183, "pan.___", state 1400, "((i<1))"
- line 1183, "pan.___", state 1400, "((i>=1))"
- line 250, "pan.___", state 1405, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 250, "pan.___", state 1407, "(1)"
- line 254, "pan.___", state 1414, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 254, "pan.___", state 1416, "(1)"
- line 254, "pan.___", state 1417, "((cache_dirty_urcu_active_readers.bitfield&(1<<_pid)))"
- line 254, "pan.___", state 1417, "else"
- line 252, "pan.___", state 1422, "((i<1))"
- line 252, "pan.___", state 1422, "((i>=1))"
- line 258, "pan.___", state 1427, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 258, "pan.___", state 1429, "(1)"
- line 258, "pan.___", state 1430, "((cache_dirty_rcu_ptr.bitfield&(1<<_pid)))"
- line 258, "pan.___", state 1430, "else"
- line 262, "pan.___", state 1436, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 262, "pan.___", state 1438, "(1)"
- line 262, "pan.___", state 1439, "((cache_dirty_rcu_data[i].bitfield&(1<<_pid)))"
- line 262, "pan.___", state 1439, "else"
- line 260, "pan.___", state 1444, "((i<2))"
- line 260, "pan.___", state 1444, "((i>=2))"
- line 227, "pan.___", state 1452, "(1)"
- line 231, "pan.___", state 1460, "(1)"
- line 231, "pan.___", state 1461, "(!((cache_dirty_urcu_active_readers.bitfield&(1<<_pid))))"
- line 231, "pan.___", state 1461, "else"
- line 229, "pan.___", state 1466, "((i<1))"
- line 229, "pan.___", state 1466, "((i>=1))"
- line 235, "pan.___", state 1472, "(1)"
- line 235, "pan.___", state 1473, "(!((cache_dirty_rcu_ptr.bitfield&(1<<_pid))))"
- line 235, "pan.___", state 1473, "else"
- line 239, "pan.___", state 1480, "(1)"
- line 239, "pan.___", state 1481, "(!((cache_dirty_rcu_data[i].bitfield&(1<<_pid))))"
- line 239, "pan.___", state 1481, "else"
- line 244, "pan.___", state 1490, "(!((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid))))"
- line 244, "pan.___", state 1490, "else"
- line 277, "pan.___", state 1492, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
- line 277, "pan.___", state 1492, "else"
- line 1183, "pan.___", state 1493, "((cache_dirty_urcu_gp_ctr.bitfield&(1<<_pid)))"
- line 1183, "pan.___", state 1493, "else"
- line 254, "pan.___", state 1506, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 258, "pan.___", state 1519, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 262, "pan.___", state 1528, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 227, "pan.___", state 1544, "(1)"
- line 231, "pan.___", state 1552, "(1)"
- line 235, "pan.___", state 1564, "(1)"
- line 239, "pan.___", state 1572, "(1)"
- line 250, "pan.___", state 1603, "cache_dirty_urcu_gp_ctr.bitfield = (cache_dirty_urcu_gp_ctr.bitfield&~((1<<_pid)))"
- line 254, "pan.___", state 1612, "cache_dirty_urcu_active_readers.bitfield = (cache_dirty_urcu_active_readers.bitfield&~((1<<_pid)))"
- line 258, "pan.___", state 1625, "cache_dirty_rcu_ptr.bitfield = (cache_dirty_rcu_ptr.bitfield&~((1<<_pid)))"
- line 262, "pan.___", state 1634, "cache_dirty_rcu_data[i].bitfield = (cache_dirty_rcu_data[i].bitfield&~((1<<_pid)))"
- line 227, "pan.___", state 1650, "(1)"
- line 231, "pan.___", state 1658, "(1)"
- line 235, "pan.___", state 1670, "(1)"
- line 239, "pan.___", state 1678, "(1)"
- line 1191, "pan.___", state 1694, "-end-"
- (192 of 1694 states)
-unreached in proctype :init:
- (0 of 78 states)
-unreached in proctype :never:
- line 1252, "pan.___", state 11, "-end-"
- (1 of 11 states)
-
-pan: elapsed time 13.7 seconds
-pan: rate 4094.3672 states/second
-pan: avg transition delay 1.3041e-06 usec
-cp .input.spin urcu_progress_writer.spin.input
-cp .input.spin.trail urcu_progress_writer.spin.input.trail
-make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow'
projects / urcu.git / blobdiff