+++ /dev/null
-make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-min-progress'
-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_free.ltl | grep -v ^//`)" >> pan.ltl
-cp urcu_free_no_mb.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 -DCOLLAPSE -o pan pan.c
-./pan -a -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 1179)
-pan: claim violated! (at depth 1246)
-pan: wrote .input.spin.trail
-
-(Spin Version 5.1.7 -- 23 December 2008)
-Warning: Search not completed
- + Partial Order Reduction
- + Compression
-
-Full statespace search for:
- never claim +
- assertion violations + (if within scope of claim)
- acceptance cycles + (fairness disabled)
- invalid end states - (disabled by never claim)
-
-State-vector 80 byte, depth reached 3190, errors: 1
- 124498 states, stored
- 15198533 states, matched
- 15323031 transitions (= stored+matched)
- 86866126 atomic steps
-hash conflicts: 473423 (resolved)
-
-Stats on memory usage (in Megabytes):
- 13.773 equivalent memory usage for states (stored*(State-vector + overhead))
- 6.400 actual memory usage for states (compression: 46.47%)
- state-vector as stored = 18 byte + 36 byte overhead
- 8.000 memory used for hash table (-w20)
- 457.764 memory used for DFS stack (-m10000000)
- 472.111 total actual memory usage
-
-nr of templates: [ globals chans procs ]
-collapse counts: [ 2572 1245 179 2 2 ]
-unreached in proctype urcu_reader
- line 713, "pan.___", state 12, "((i<1))"
- line 713, "pan.___", state 12, "((i>=1))"
- line 268, "pan.___", state 57, "cache_dirty_urcu_gp_ctr = 0"
- line 276, "pan.___", state 79, "cache_dirty_rcu_ptr = 0"
- line 280, "pan.___", state 88, "cache_dirty_rcu_data[i] = 0"
- line 245, "pan.___", state 104, "(1)"
- line 249, "pan.___", state 112, "(1)"
- line 253, "pan.___", state 124, "(1)"
- line 257, "pan.___", state 132, "(1)"
- line 404, "pan.___", state 158, "cache_dirty_urcu_gp_ctr = 0"
- line 413, "pan.___", state 190, "cache_dirty_rcu_ptr = 0"
- line 417, "pan.___", state 204, "cache_dirty_rcu_data[i] = 0"
- line 422, "pan.___", state 223, "(1)"
- line 431, "pan.___", state 253, "(1)"
- line 435, "pan.___", state 266, "(1)"
- line 614, "pan.___", state 287, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))"
- line 404, "pan.___", state 294, "cache_dirty_urcu_gp_ctr = 0"
- line 413, "pan.___", state 326, "cache_dirty_rcu_ptr = 0"
- line 417, "pan.___", state 340, "cache_dirty_rcu_data[i] = 0"
- line 422, "pan.___", state 359, "(1)"
- line 431, "pan.___", state 389, "(1)"
- line 435, "pan.___", state 402, "(1)"
- line 404, "pan.___", state 423, "cache_dirty_urcu_gp_ctr = 0"
- line 413, "pan.___", state 455, "cache_dirty_rcu_ptr = 0"
- line 417, "pan.___", state 469, "cache_dirty_rcu_data[i] = 0"
- line 422, "pan.___", state 488, "(1)"
- line 431, "pan.___", state 518, "(1)"
- line 435, "pan.___", state 531, "(1)"
- line 404, "pan.___", state 554, "cache_dirty_urcu_gp_ctr = 0"
- line 404, "pan.___", state 556, "(1)"
- line 404, "pan.___", state 557, "(cache_dirty_urcu_gp_ctr)"
- line 404, "pan.___", state 557, "else"
- line 404, "pan.___", state 560, "(1)"
- line 408, "pan.___", state 568, "cache_dirty_urcu_active_readers = 0"
- line 408, "pan.___", state 570, "(1)"
- line 408, "pan.___", state 571, "(cache_dirty_urcu_active_readers)"
- line 408, "pan.___", state 571, "else"
- line 408, "pan.___", state 574, "(1)"
- line 408, "pan.___", state 575, "(1)"
- line 408, "pan.___", state 575, "(1)"
- line 406, "pan.___", state 580, "((i<1))"
- line 406, "pan.___", state 580, "((i>=1))"
- line 413, "pan.___", state 586, "cache_dirty_rcu_ptr = 0"
- line 413, "pan.___", state 588, "(1)"
- line 413, "pan.___", state 589, "(cache_dirty_rcu_ptr)"
- line 413, "pan.___", state 589, "else"
- line 413, "pan.___", state 592, "(1)"
- line 413, "pan.___", state 593, "(1)"
- line 413, "pan.___", state 593, "(1)"
- line 417, "pan.___", state 600, "cache_dirty_rcu_data[i] = 0"
- line 417, "pan.___", state 602, "(1)"
- line 417, "pan.___", state 603, "(cache_dirty_rcu_data[i])"
- line 417, "pan.___", state 603, "else"
- line 417, "pan.___", state 606, "(1)"
- line 417, "pan.___", state 607, "(1)"
- line 417, "pan.___", state 607, "(1)"
- line 415, "pan.___", state 612, "((i<2))"
- line 415, "pan.___", state 612, "((i>=2))"
- line 422, "pan.___", state 619, "(1)"
- line 422, "pan.___", state 620, "(!(cache_dirty_urcu_gp_ctr))"
- line 422, "pan.___", state 620, "else"
- line 422, "pan.___", state 623, "(1)"
- line 422, "pan.___", state 624, "(1)"
- line 422, "pan.___", state 624, "(1)"
- line 426, "pan.___", state 632, "(1)"
- line 426, "pan.___", state 633, "(!(cache_dirty_urcu_active_readers))"
- line 426, "pan.___", state 633, "else"
- line 426, "pan.___", state 636, "(1)"
- line 426, "pan.___", state 637, "(1)"
- line 426, "pan.___", state 637, "(1)"
- line 424, "pan.___", state 642, "((i<1))"
- line 424, "pan.___", state 642, "((i>=1))"
- line 431, "pan.___", state 649, "(1)"
- line 431, "pan.___", state 650, "(!(cache_dirty_rcu_ptr))"
- line 431, "pan.___", state 650, "else"
- line 431, "pan.___", state 653, "(1)"
- line 431, "pan.___", state 654, "(1)"
- line 431, "pan.___", state 654, "(1)"
- line 435, "pan.___", state 662, "(1)"
- line 435, "pan.___", state 663, "(!(cache_dirty_rcu_data[i]))"
- line 435, "pan.___", state 663, "else"
- line 435, "pan.___", state 666, "(1)"
- line 435, "pan.___", state 667, "(1)"
- line 435, "pan.___", state 667, "(1)"
- line 433, "pan.___", state 672, "((i<2))"
- line 433, "pan.___", state 672, "((i>=2))"
- line 443, "pan.___", state 676, "(1)"
- line 443, "pan.___", state 676, "(1)"
- line 614, "pan.___", state 679, "cached_urcu_active_readers = (tmp+1)"
- line 614, "pan.___", state 680, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))"
- line 614, "pan.___", state 681, "(1)"
- line 404, "pan.___", state 688, "cache_dirty_urcu_gp_ctr = 0"
- line 413, "pan.___", state 720, "cache_dirty_rcu_ptr = 0"
- line 417, "pan.___", state 734, "cache_dirty_rcu_data[i] = 0"
- line 422, "pan.___", state 753, "(1)"
- line 431, "pan.___", state 783, "(1)"
- line 435, "pan.___", state 796, "(1)"
- line 404, "pan.___", state 823, "cache_dirty_urcu_gp_ctr = 0"
- line 413, "pan.___", state 855, "cache_dirty_rcu_ptr = 0"
- line 417, "pan.___", state 869, "cache_dirty_rcu_data[i] = 0"
- line 422, "pan.___", state 888, "(1)"
- line 431, "pan.___", state 918, "(1)"
- line 435, "pan.___", state 931, "(1)"
- line 404, "pan.___", state 952, "cache_dirty_urcu_gp_ctr = 0"
- line 413, "pan.___", state 984, "cache_dirty_rcu_ptr = 0"
- line 417, "pan.___", state 998, "cache_dirty_rcu_data[i] = 0"
- line 422, "pan.___", state 1017, "(1)"
- line 431, "pan.___", state 1047, "(1)"
- line 435, "pan.___", state 1060, "(1)"
- line 245, "pan.___", state 1093, "(1)"
- line 253, "pan.___", state 1113, "(1)"
- line 257, "pan.___", state 1121, "(1)"
- line 748, "pan.___", state 1138, "-end-"
- (92 of 1138 states)
-unreached in proctype urcu_writer
- line 837, "pan.___", state 12, "((i<1))"
- line 837, "pan.___", state 12, "((i>=1))"
- line 404, "pan.___", state 47, "cache_dirty_urcu_gp_ctr = 0"
- line 404, "pan.___", state 53, "(1)"
- line 408, "pan.___", state 61, "cache_dirty_urcu_active_readers = 0"
- line 408, "pan.___", state 67, "(1)"
- line 408, "pan.___", state 68, "(1)"
- line 408, "pan.___", state 68, "(1)"
- line 406, "pan.___", state 73, "((i<1))"
- line 406, "pan.___", state 73, "((i>=1))"
- line 413, "pan.___", state 79, "cache_dirty_rcu_ptr = 0"
- line 413, "pan.___", state 85, "(1)"
- line 413, "pan.___", state 86, "(1)"
- line 413, "pan.___", state 86, "(1)"
- line 417, "pan.___", state 99, "(1)"
- line 417, "pan.___", state 100, "(1)"
- line 417, "pan.___", state 100, "(1)"
- line 415, "pan.___", state 105, "((i<2))"
- line 415, "pan.___", state 105, "((i>=2))"
- line 422, "pan.___", state 112, "(1)"
- line 422, "pan.___", state 113, "(!(cache_dirty_urcu_gp_ctr))"
- line 422, "pan.___", state 113, "else"
- line 422, "pan.___", state 116, "(1)"
- line 422, "pan.___", state 117, "(1)"
- line 422, "pan.___", state 117, "(1)"
- line 426, "pan.___", state 125, "(1)"
- line 426, "pan.___", state 126, "(!(cache_dirty_urcu_active_readers))"
- line 426, "pan.___", state 126, "else"
- line 426, "pan.___", state 129, "(1)"
- line 426, "pan.___", state 130, "(1)"
- line 426, "pan.___", state 130, "(1)"
- line 424, "pan.___", state 135, "((i<1))"
- line 424, "pan.___", state 135, "((i>=1))"
- line 431, "pan.___", state 142, "(1)"
- line 431, "pan.___", state 143, "(!(cache_dirty_rcu_ptr))"
- line 431, "pan.___", state 143, "else"
- line 431, "pan.___", state 146, "(1)"
- line 431, "pan.___", state 147, "(1)"
- line 431, "pan.___", state 147, "(1)"
- line 435, "pan.___", state 155, "(1)"
- line 435, "pan.___", state 156, "(!(cache_dirty_rcu_data[i]))"
- line 435, "pan.___", state 156, "else"
- line 435, "pan.___", state 159, "(1)"
- line 435, "pan.___", state 160, "(1)"
- line 435, "pan.___", state 160, "(1)"
- line 433, "pan.___", state 165, "((i<2))"
- line 433, "pan.___", state 165, "((i>=2))"
- line 443, "pan.___", state 169, "(1)"
- line 443, "pan.___", state 169, "(1)"
- line 268, "pan.___", state 178, "cache_dirty_urcu_gp_ctr = 0"
- line 272, "pan.___", state 187, "cache_dirty_urcu_active_readers = 0"
- line 270, "pan.___", state 195, "((i<1))"
- line 270, "pan.___", state 195, "((i>=1))"
- line 276, "pan.___", state 200, "cache_dirty_rcu_ptr = 0"
- line 907, "pan.___", state 228, "old_data = cached_rcu_ptr"
- line 918, "pan.___", state 232, "_proc_urcu_writer = (_proc_urcu_writer|(1<<4))"
- line 404, "pan.___", state 240, "cache_dirty_urcu_gp_ctr = 0"
- line 404, "pan.___", state 246, "(1)"
- line 408, "pan.___", state 254, "cache_dirty_urcu_active_readers = 0"
- line 408, "pan.___", state 260, "(1)"
- line 408, "pan.___", state 261, "(1)"
- line 408, "pan.___", state 261, "(1)"
- line 406, "pan.___", state 266, "((i<1))"
- line 406, "pan.___", state 266, "((i>=1))"
- line 413, "pan.___", state 274, "(1)"
- line 413, "pan.___", state 275, "(cache_dirty_rcu_ptr)"
- line 413, "pan.___", state 275, "else"
- line 413, "pan.___", state 278, "(1)"
- line 413, "pan.___", state 279, "(1)"
- line 413, "pan.___", state 279, "(1)"
- line 417, "pan.___", state 286, "cache_dirty_rcu_data[i] = 0"
- line 417, "pan.___", state 292, "(1)"
- line 417, "pan.___", state 293, "(1)"
- line 417, "pan.___", state 293, "(1)"
- line 415, "pan.___", state 298, "((i<2))"
- line 415, "pan.___", state 298, "((i>=2))"
- line 422, "pan.___", state 305, "(1)"
- line 422, "pan.___", state 306, "(!(cache_dirty_urcu_gp_ctr))"
- line 422, "pan.___", state 306, "else"
- line 422, "pan.___", state 309, "(1)"
- line 422, "pan.___", state 310, "(1)"
- line 422, "pan.___", state 310, "(1)"
- line 426, "pan.___", state 318, "(1)"
- line 426, "pan.___", state 319, "(!(cache_dirty_urcu_active_readers))"
- line 426, "pan.___", state 319, "else"
- line 426, "pan.___", state 322, "(1)"
- line 426, "pan.___", state 323, "(1)"
- line 426, "pan.___", state 323, "(1)"
- line 424, "pan.___", state 328, "((i<1))"
- line 424, "pan.___", state 328, "((i>=1))"
- line 431, "pan.___", state 335, "(1)"
- line 431, "pan.___", state 336, "(!(cache_dirty_rcu_ptr))"
- line 431, "pan.___", state 336, "else"
- line 431, "pan.___", state 339, "(1)"
- line 431, "pan.___", state 340, "(1)"
- line 431, "pan.___", state 340, "(1)"
- line 435, "pan.___", state 348, "(1)"
- line 435, "pan.___", state 349, "(!(cache_dirty_rcu_data[i]))"
- line 435, "pan.___", state 349, "else"
- line 435, "pan.___", state 352, "(1)"
- line 435, "pan.___", state 353, "(1)"
- line 435, "pan.___", state 353, "(1)"
- line 433, "pan.___", state 358, "((i<2))"
- line 433, "pan.___", state 358, "((i>=2))"
- line 443, "pan.___", state 362, "(1)"
- line 443, "pan.___", state 362, "(1)"
- line 404, "pan.___", state 373, "(1)"
- line 404, "pan.___", state 374, "(cache_dirty_urcu_gp_ctr)"
- line 404, "pan.___", state 374, "else"
- line 404, "pan.___", state 377, "(1)"
- line 408, "pan.___", state 385, "cache_dirty_urcu_active_readers = 0"
- line 408, "pan.___", state 391, "(1)"
- line 408, "pan.___", state 392, "(1)"
- line 408, "pan.___", state 392, "(1)"
- line 406, "pan.___", state 397, "((i<1))"
- line 406, "pan.___", state 397, "((i>=1))"
- line 413, "pan.___", state 403, "cache_dirty_rcu_ptr = 0"
- line 413, "pan.___", state 409, "(1)"
- line 413, "pan.___", state 410, "(1)"
- line 413, "pan.___", state 410, "(1)"
- line 417, "pan.___", state 417, "cache_dirty_rcu_data[i] = 0"
- line 417, "pan.___", state 423, "(1)"
- line 417, "pan.___", state 424, "(1)"
- line 417, "pan.___", state 424, "(1)"
- line 415, "pan.___", state 429, "((i<2))"
- line 415, "pan.___", state 429, "((i>=2))"
- line 422, "pan.___", state 436, "(1)"
- line 422, "pan.___", state 437, "(!(cache_dirty_urcu_gp_ctr))"
- line 422, "pan.___", state 437, "else"
- line 422, "pan.___", state 440, "(1)"
- line 422, "pan.___", state 441, "(1)"
- line 422, "pan.___", state 441, "(1)"
- line 426, "pan.___", state 449, "(1)"
- line 426, "pan.___", state 450, "(!(cache_dirty_urcu_active_readers))"
- line 426, "pan.___", state 450, "else"
- line 426, "pan.___", state 453, "(1)"
- line 426, "pan.___", state 454, "(1)"
- line 426, "pan.___", state 454, "(1)"
- line 424, "pan.___", state 459, "((i<1))"
- line 424, "pan.___", state 459, "((i>=1))"
- line 431, "pan.___", state 466, "(1)"
- line 431, "pan.___", state 467, "(!(cache_dirty_rcu_ptr))"
- line 431, "pan.___", state 467, "else"
- line 431, "pan.___", state 470, "(1)"
- line 431, "pan.___", state 471, "(1)"
- line 431, "pan.___", state 471, "(1)"
- line 435, "pan.___", state 479, "(1)"
- line 435, "pan.___", state 480, "(!(cache_dirty_rcu_data[i]))"
- line 435, "pan.___", state 480, "else"
- line 435, "pan.___", state 483, "(1)"
- line 435, "pan.___", state 484, "(1)"
- line 435, "pan.___", state 484, "(1)"
- line 433, "pan.___", state 489, "((i<2))"
- line 433, "pan.___", state 489, "((i>=2))"
- line 443, "pan.___", state 493, "(1)"
- line 443, "pan.___", state 493, "(1)"
- line 972, "pan.___", state 504, "_proc_urcu_writer = (_proc_urcu_writer&~((1<<9)))"
- line 977, "pan.___", state 505, "_proc_urcu_writer = (_proc_urcu_writer&~(((1<<8)|(1<<7))))"
- line 404, "pan.___", state 510, "cache_dirty_urcu_gp_ctr = 0"
- line 404, "pan.___", state 516, "(1)"
- line 408, "pan.___", state 524, "cache_dirty_urcu_active_readers = 0"
- line 408, "pan.___", state 530, "(1)"
- line 408, "pan.___", state 531, "(1)"
- line 408, "pan.___", state 531, "(1)"
- line 406, "pan.___", state 536, "((i<1))"
- line 406, "pan.___", state 536, "((i>=1))"
- line 413, "pan.___", state 542, "cache_dirty_rcu_ptr = 0"
- line 413, "pan.___", state 548, "(1)"
- line 413, "pan.___", state 549, "(1)"
- line 413, "pan.___", state 549, "(1)"
- line 417, "pan.___", state 556, "cache_dirty_rcu_data[i] = 0"
- line 417, "pan.___", state 562, "(1)"
- line 417, "pan.___", state 563, "(1)"
- line 417, "pan.___", state 563, "(1)"
- line 415, "pan.___", state 568, "((i<2))"
- line 415, "pan.___", state 568, "((i>=2))"
- line 422, "pan.___", state 575, "(1)"
- line 422, "pan.___", state 576, "(!(cache_dirty_urcu_gp_ctr))"
- line 422, "pan.___", state 576, "else"
- line 422, "pan.___", state 579, "(1)"
- line 422, "pan.___", state 580, "(1)"
- line 422, "pan.___", state 580, "(1)"
- line 426, "pan.___", state 588, "(1)"
- line 426, "pan.___", state 589, "(!(cache_dirty_urcu_active_readers))"
- line 426, "pan.___", state 589, "else"
- line 426, "pan.___", state 592, "(1)"
- line 426, "pan.___", state 593, "(1)"
- line 426, "pan.___", state 593, "(1)"
- line 424, "pan.___", state 598, "((i<1))"
- line 424, "pan.___", state 598, "((i>=1))"
- line 431, "pan.___", state 605, "(1)"
- line 431, "pan.___", state 606, "(!(cache_dirty_rcu_ptr))"
- line 431, "pan.___", state 606, "else"
- line 431, "pan.___", state 609, "(1)"
- line 431, "pan.___", state 610, "(1)"
- line 431, "pan.___", state 610, "(1)"
- line 435, "pan.___", state 618, "(1)"
- line 435, "pan.___", state 619, "(!(cache_dirty_rcu_data[i]))"
- line 435, "pan.___", state 619, "else"
- line 435, "pan.___", state 622, "(1)"
- line 435, "pan.___", state 623, "(1)"
- line 435, "pan.___", state 623, "(1)"
- line 443, "pan.___", state 632, "(1)"
- line 443, "pan.___", state 632, "(1)"
- line 404, "pan.___", state 639, "cache_dirty_urcu_gp_ctr = 0"
- line 408, "pan.___", state 653, "cache_dirty_urcu_active_readers = 0"
- line 413, "pan.___", state 671, "cache_dirty_rcu_ptr = 0"
- line 422, "pan.___", state 704, "(1)"
- line 426, "pan.___", state 717, "(1)"
- line 431, "pan.___", state 734, "(1)"
- line 435, "pan.___", state 747, "(1)"
- line 408, "pan.___", state 784, "cache_dirty_urcu_active_readers = 0"
- line 413, "pan.___", state 802, "cache_dirty_rcu_ptr = 0"
- line 417, "pan.___", state 816, "cache_dirty_rcu_data[i] = 0"
- line 426, "pan.___", state 848, "(1)"
- line 431, "pan.___", state 865, "(1)"
- line 435, "pan.___", state 878, "(1)"
- line 1054, "pan.___", state 905, "_proc_urcu_writer = (_proc_urcu_writer|(1<<13))"
- line 268, "pan.___", state 933, "cache_dirty_urcu_gp_ctr = 0"
- line 268, "pan.___", state 935, "(1)"
- line 272, "pan.___", state 942, "cache_dirty_urcu_active_readers = 0"
- line 272, "pan.___", state 944, "(1)"
- line 272, "pan.___", state 945, "(cache_dirty_urcu_active_readers)"
- line 272, "pan.___", state 945, "else"
- line 270, "pan.___", state 950, "((i<1))"
- line 270, "pan.___", state 950, "((i>=1))"
- line 276, "pan.___", state 955, "cache_dirty_rcu_ptr = 0"
- line 276, "pan.___", state 957, "(1)"
- line 276, "pan.___", state 958, "(cache_dirty_rcu_ptr)"
- line 276, "pan.___", state 958, "else"
- line 280, "pan.___", state 964, "cache_dirty_rcu_data[i] = 0"
- line 280, "pan.___", state 966, "(1)"
- line 280, "pan.___", state 967, "(cache_dirty_rcu_data[i])"
- line 280, "pan.___", state 967, "else"
- line 278, "pan.___", state 972, "((i<2))"
- line 278, "pan.___", state 972, "((i>=2))"
- line 245, "pan.___", state 980, "(1)"
- line 249, "pan.___", state 988, "(1)"
- line 249, "pan.___", state 989, "(!(cache_dirty_urcu_active_readers))"
- line 249, "pan.___", state 989, "else"
- line 247, "pan.___", state 994, "((i<1))"
- line 247, "pan.___", state 994, "((i>=1))"
- line 253, "pan.___", state 1000, "(1)"
- line 253, "pan.___", state 1001, "(!(cache_dirty_rcu_ptr))"
- line 253, "pan.___", state 1001, "else"
- line 257, "pan.___", state 1008, "(1)"
- line 257, "pan.___", state 1009, "(!(cache_dirty_rcu_data[i]))"
- line 257, "pan.___", state 1009, "else"
- line 262, "pan.___", state 1018, "(!(cache_dirty_urcu_gp_ctr))"
- line 262, "pan.___", state 1018, "else"
- line 1108, "pan.___", state 1034, "((i<1))"
- line 1108, "pan.___", state 1034, "((i>=1))"
- line 268, "pan.___", state 1039, "cache_dirty_urcu_gp_ctr = 0"
- line 268, "pan.___", state 1041, "(1)"
- line 272, "pan.___", state 1048, "cache_dirty_urcu_active_readers = 0"
- line 272, "pan.___", state 1050, "(1)"
- line 272, "pan.___", state 1051, "(cache_dirty_urcu_active_readers)"
- line 272, "pan.___", state 1051, "else"
- line 270, "pan.___", state 1056, "((i<1))"
- line 270, "pan.___", state 1056, "((i>=1))"
- line 276, "pan.___", state 1061, "cache_dirty_rcu_ptr = 0"
- line 276, "pan.___", state 1063, "(1)"
- line 276, "pan.___", state 1064, "(cache_dirty_rcu_ptr)"
- line 276, "pan.___", state 1064, "else"
- line 280, "pan.___", state 1070, "cache_dirty_rcu_data[i] = 0"
- line 280, "pan.___", state 1072, "(1)"
- line 280, "pan.___", state 1073, "(cache_dirty_rcu_data[i])"
- line 280, "pan.___", state 1073, "else"
- line 278, "pan.___", state 1078, "((i<2))"
- line 278, "pan.___", state 1078, "((i>=2))"
- line 245, "pan.___", state 1086, "(1)"
- line 249, "pan.___", state 1094, "(1)"
- line 249, "pan.___", state 1095, "(!(cache_dirty_urcu_active_readers))"
- line 249, "pan.___", state 1095, "else"
- line 247, "pan.___", state 1100, "((i<1))"
- line 247, "pan.___", state 1100, "((i>=1))"
- line 253, "pan.___", state 1106, "(1)"
- line 253, "pan.___", state 1107, "(!(cache_dirty_rcu_ptr))"
- line 253, "pan.___", state 1107, "else"
- line 257, "pan.___", state 1114, "(1)"
- line 257, "pan.___", state 1115, "(!(cache_dirty_rcu_data[i]))"
- line 257, "pan.___", state 1115, "else"
- line 262, "pan.___", state 1124, "(!(cache_dirty_urcu_gp_ctr))"
- line 262, "pan.___", state 1124, "else"
- line 295, "pan.___", state 1126, "(cache_dirty_urcu_gp_ctr)"
- line 295, "pan.___", state 1126, "else"
- line 1108, "pan.___", state 1127, "(cache_dirty_urcu_gp_ctr)"
- line 1108, "pan.___", state 1127, "else"
- line 268, "pan.___", state 1131, "cache_dirty_urcu_gp_ctr = 0"
- line 268, "pan.___", state 1133, "(1)"
- line 272, "pan.___", state 1140, "cache_dirty_urcu_active_readers = 0"
- line 272, "pan.___", state 1142, "(1)"
- line 272, "pan.___", state 1143, "(cache_dirty_urcu_active_readers)"
- line 272, "pan.___", state 1143, "else"
- line 270, "pan.___", state 1148, "((i<1))"
- line 270, "pan.___", state 1148, "((i>=1))"
- line 276, "pan.___", state 1153, "cache_dirty_rcu_ptr = 0"
- line 276, "pan.___", state 1155, "(1)"
- line 276, "pan.___", state 1156, "(cache_dirty_rcu_ptr)"
- line 276, "pan.___", state 1156, "else"
- line 280, "pan.___", state 1162, "cache_dirty_rcu_data[i] = 0"
- line 280, "pan.___", state 1164, "(1)"
- line 280, "pan.___", state 1165, "(cache_dirty_rcu_data[i])"
- line 280, "pan.___", state 1165, "else"
- line 278, "pan.___", state 1170, "((i<2))"
- line 278, "pan.___", state 1170, "((i>=2))"
- line 245, "pan.___", state 1178, "(1)"
- line 249, "pan.___", state 1186, "(1)"
- line 249, "pan.___", state 1187, "(!(cache_dirty_urcu_active_readers))"
- line 249, "pan.___", state 1187, "else"
- line 247, "pan.___", state 1192, "((i<1))"
- line 247, "pan.___", state 1192, "((i>=1))"
- line 253, "pan.___", state 1198, "(1)"
- line 253, "pan.___", state 1199, "(!(cache_dirty_rcu_ptr))"
- line 253, "pan.___", state 1199, "else"
- line 257, "pan.___", state 1206, "(1)"
- line 257, "pan.___", state 1207, "(!(cache_dirty_rcu_data[i]))"
- line 257, "pan.___", state 1207, "else"
- line 262, "pan.___", state 1216, "(!(cache_dirty_urcu_gp_ctr))"
- line 262, "pan.___", state 1216, "else"
- line 1112, "pan.___", state 1219, "i = 0"
- line 1112, "pan.___", state 1221, "reader_barrier = 1"
- line 1112, "pan.___", state 1232, "((i<1))"
- line 1112, "pan.___", state 1232, "((i>=1))"
- line 268, "pan.___", state 1237, "cache_dirty_urcu_gp_ctr = 0"
- line 268, "pan.___", state 1239, "(1)"
- line 272, "pan.___", state 1246, "cache_dirty_urcu_active_readers = 0"
- line 272, "pan.___", state 1248, "(1)"
- line 272, "pan.___", state 1249, "(cache_dirty_urcu_active_readers)"
- line 272, "pan.___", state 1249, "else"
- line 270, "pan.___", state 1254, "((i<1))"
- line 270, "pan.___", state 1254, "((i>=1))"
- line 276, "pan.___", state 1259, "cache_dirty_rcu_ptr = 0"
- line 276, "pan.___", state 1261, "(1)"
- line 276, "pan.___", state 1262, "(cache_dirty_rcu_ptr)"
- line 276, "pan.___", state 1262, "else"
- line 280, "pan.___", state 1268, "cache_dirty_rcu_data[i] = 0"
- line 280, "pan.___", state 1270, "(1)"
- line 280, "pan.___", state 1271, "(cache_dirty_rcu_data[i])"
- line 280, "pan.___", state 1271, "else"
- line 278, "pan.___", state 1276, "((i<2))"
- line 278, "pan.___", state 1276, "((i>=2))"
- line 245, "pan.___", state 1284, "(1)"
- line 249, "pan.___", state 1292, "(1)"
- line 249, "pan.___", state 1293, "(!(cache_dirty_urcu_active_readers))"
- line 249, "pan.___", state 1293, "else"
- line 247, "pan.___", state 1298, "((i<1))"
- line 247, "pan.___", state 1298, "((i>=1))"
- line 253, "pan.___", state 1304, "(1)"
- line 253, "pan.___", state 1305, "(!(cache_dirty_rcu_ptr))"
- line 253, "pan.___", state 1305, "else"
- line 257, "pan.___", state 1312, "(1)"
- line 257, "pan.___", state 1313, "(!(cache_dirty_rcu_data[i]))"
- line 257, "pan.___", state 1313, "else"
- line 262, "pan.___", state 1322, "(!(cache_dirty_urcu_gp_ctr))"
- line 262, "pan.___", state 1322, "else"
- line 295, "pan.___", state 1324, "(cache_dirty_urcu_gp_ctr)"
- line 295, "pan.___", state 1324, "else"
- line 1112, "pan.___", state 1325, "(cache_dirty_urcu_gp_ctr)"
- line 1112, "pan.___", state 1325, "else"
- line 272, "pan.___", state 1338, "cache_dirty_urcu_active_readers = 0"
- line 276, "pan.___", state 1351, "cache_dirty_rcu_ptr = 0"
- line 280, "pan.___", state 1360, "cache_dirty_rcu_data[i] = 0"
- line 245, "pan.___", state 1376, "(1)"
- line 249, "pan.___", state 1384, "(1)"
- line 253, "pan.___", state 1396, "(1)"
- line 257, "pan.___", state 1404, "(1)"
- line 268, "pan.___", state 1435, "cache_dirty_urcu_gp_ctr = 0"
- line 272, "pan.___", state 1444, "cache_dirty_urcu_active_readers = 0"
- line 276, "pan.___", state 1457, "cache_dirty_rcu_ptr = 0"
- line 280, "pan.___", state 1466, "cache_dirty_rcu_data[i] = 0"
- line 245, "pan.___", state 1482, "(1)"
- line 249, "pan.___", state 1490, "(1)"
- line 253, "pan.___", state 1502, "(1)"
- line 257, "pan.___", state 1510, "(1)"
- line 268, "pan.___", state 1527, "cache_dirty_urcu_gp_ctr = 0"
- line 268, "pan.___", state 1529, "(1)"
- line 272, "pan.___", state 1536, "cache_dirty_urcu_active_readers = 0"
- line 272, "pan.___", state 1538, "(1)"
- line 272, "pan.___", state 1539, "(cache_dirty_urcu_active_readers)"
- line 272, "pan.___", state 1539, "else"
- line 270, "pan.___", state 1544, "((i<1))"
- line 270, "pan.___", state 1544, "((i>=1))"
- line 276, "pan.___", state 1549, "cache_dirty_rcu_ptr = 0"
- line 276, "pan.___", state 1551, "(1)"
- line 276, "pan.___", state 1552, "(cache_dirty_rcu_ptr)"
- line 276, "pan.___", state 1552, "else"
- line 280, "pan.___", state 1558, "cache_dirty_rcu_data[i] = 0"
- line 280, "pan.___", state 1560, "(1)"
- line 280, "pan.___", state 1561, "(cache_dirty_rcu_data[i])"
- line 280, "pan.___", state 1561, "else"
- line 278, "pan.___", state 1566, "((i<2))"
- line 278, "pan.___", state 1566, "((i>=2))"
- line 245, "pan.___", state 1574, "(1)"
- line 249, "pan.___", state 1582, "(1)"
- line 249, "pan.___", state 1583, "(!(cache_dirty_urcu_active_readers))"
- line 249, "pan.___", state 1583, "else"
- line 247, "pan.___", state 1588, "((i<1))"
- line 247, "pan.___", state 1588, "((i>=1))"
- line 253, "pan.___", state 1594, "(1)"
- line 253, "pan.___", state 1595, "(!(cache_dirty_rcu_ptr))"
- line 253, "pan.___", state 1595, "else"
- line 257, "pan.___", state 1602, "(1)"
- line 257, "pan.___", state 1603, "(!(cache_dirty_rcu_data[i]))"
- line 257, "pan.___", state 1603, "else"
- line 262, "pan.___", state 1612, "(!(cache_dirty_urcu_gp_ctr))"
- line 262, "pan.___", state 1612, "else"
- line 1119, "pan.___", state 1615, "i = 0"
- line 1119, "pan.___", state 1617, "reader_barrier = 1"
- line 1119, "pan.___", state 1628, "((i<1))"
- line 1119, "pan.___", state 1628, "((i>=1))"
- line 268, "pan.___", state 1633, "cache_dirty_urcu_gp_ctr = 0"
- line 268, "pan.___", state 1635, "(1)"
- line 272, "pan.___", state 1642, "cache_dirty_urcu_active_readers = 0"
- line 272, "pan.___", state 1644, "(1)"
- line 272, "pan.___", state 1645, "(cache_dirty_urcu_active_readers)"
- line 272, "pan.___", state 1645, "else"
- line 270, "pan.___", state 1650, "((i<1))"
- line 270, "pan.___", state 1650, "((i>=1))"
- line 276, "pan.___", state 1655, "cache_dirty_rcu_ptr = 0"
- line 276, "pan.___", state 1657, "(1)"
- line 276, "pan.___", state 1658, "(cache_dirty_rcu_ptr)"
- line 276, "pan.___", state 1658, "else"
- line 280, "pan.___", state 1664, "cache_dirty_rcu_data[i] = 0"
- line 280, "pan.___", state 1666, "(1)"
- line 280, "pan.___", state 1667, "(cache_dirty_rcu_data[i])"
- line 280, "pan.___", state 1667, "else"
- line 278, "pan.___", state 1672, "((i<2))"
- line 278, "pan.___", state 1672, "((i>=2))"
- line 245, "pan.___", state 1680, "(1)"
- line 249, "pan.___", state 1688, "(1)"
- line 249, "pan.___", state 1689, "(!(cache_dirty_urcu_active_readers))"
- line 249, "pan.___", state 1689, "else"
- line 247, "pan.___", state 1694, "((i<1))"
- line 247, "pan.___", state 1694, "((i>=1))"
- line 253, "pan.___", state 1700, "(1)"
- line 253, "pan.___", state 1701, "(!(cache_dirty_rcu_ptr))"
- line 253, "pan.___", state 1701, "else"
- line 257, "pan.___", state 1708, "(1)"
- line 257, "pan.___", state 1709, "(!(cache_dirty_rcu_data[i]))"
- line 257, "pan.___", state 1709, "else"
- line 262, "pan.___", state 1718, "(!(cache_dirty_urcu_gp_ctr))"
- line 262, "pan.___", state 1718, "else"
- line 295, "pan.___", state 1720, "(cache_dirty_urcu_gp_ctr)"
- line 295, "pan.___", state 1720, "else"
- line 1119, "pan.___", state 1721, "(cache_dirty_urcu_gp_ctr)"
- line 1119, "pan.___", state 1721, "else"
- line 1123, "pan.___", state 1724, "-end-"
- (312 of 1724 states)
-unreached in proctype :init:
- line 1138, "pan.___", state 11, "((i<1))"
- line 1138, "pan.___", state 11, "((i>=1))"
- (1 of 26 states)
-unreached in proctype :never:
- line 1184, "pan.___", state 8, "-end-"
- (1 of 8 states)
-
-pan: elapsed time 23.7 seconds
-pan: rate 5259.7381 states/second
-pan: avg transition delay 1.5447e-06 usec
-cp .input.spin urcu_free_no_mb.spin.input
-cp .input.spin.trail urcu_free_no_mb.spin.input.trail
-make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-min-progress'
projects / urcu.git / blobdiff