make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-alpha-ipi' rm -f pan* trail.out .input.spin* *.spin.trail .input.define cat DEFINES > .input.spin cat urcu.spin >> .input.spin rm -f .input.spin.trail spin -a -X .input.spin Exit-Status 0 gcc -O2 -w -DHASH64 -DCOLLAPSE -DSAFETY -o pan pan.c ./pan -v -c1 -X -m10000000 -w20 Depth= 6176 States= 1e+06 Transitions= 1.77e+08 Memory= 497.600 t= 218 R= 5e+03 Depth= 7720 States= 2e+06 Transitions= 3.71e+08 Memory= 528.654 t= 474 R= 4e+03 Depth= 7720 States= 3e+06 Transitions= 5.8e+08 Memory= 561.955 t= 768 R= 4e+03 pan: resizing hashtable to -w22.. done Depth= 7720 States= 4e+06 Transitions= 7.6e+08 Memory= 627.549 t= 999 R= 4e+03 Depth= 7720 States= 5e+06 Transitions= 9.44e+08 Memory= 662.217 t= 1.24e+03 R= 4e+03 Depth= 7720 States= 6e+06 Transitions= 1.35e+09 Memory= 699.619 t= 1.79e+03 R= 3e+03 Depth= 7720 States= 7e+06 Transitions= 1.79e+09 Memory= 735.361 t= 2.39e+03 R= 3e+03 Depth= 7720 States= 8e+06 Transitions= 2.11e+09 Memory= 773.545 t= 2.83e+03 R= 3e+03 Depth= 7720 States= 9e+06 Transitions= 2.49e+09 Memory= 811.143 t= 3.37e+03 R= 3e+03 pan: resizing hashtable to -w24.. done Depth= 7720 States= 1e+07 Transitions= 2.83e+09 Memory= 973.518 t= 3.8e+03 R= 3e+03 Depth= 7720 States= 1.1e+07 Transitions= 3.2e+09 Memory= 1011.506 t= 4.27e+03 R= 3e+03 Depth= 7720 States= 1.2e+07 Transitions= 3.59e+09 Memory= 1049.885 t= 4.78e+03 R= 3e+03 Depth= 7720 States= 1.3e+07 Transitions= 3.81e+09 Memory= 1087.678 t= 5.06e+03 R= 3e+03 Depth= 7720 States= 1.4e+07 Transitions= 4.12e+09 Memory= 1122.834 t= 5.46e+03 R= 3e+03 Depth= 7720 States= 1.5e+07 Transitions= 4.35e+09 Memory= 1159.358 t= 5.75e+03 R= 3e+03 Depth= 7720 States= 1.6e+07 Transitions= 4.88e+09 Memory= 1195.783 t= 6.46e+03 R= 2e+03 Depth= 7720 States= 1.7e+07 Transitions= 5.67e+09 Memory= 1231.721 t= 7.51e+03 R= 2e+03 Depth= 7720 States= 1.8e+07 Transitions= 6.31e+09 Memory= 1268.537 t= 8.37e+03 R= 2e+03 Depth= 7720 States= 1.9e+07 Transitions= 6.77e+09 Memory= 1306.526 t= 8.98e+03 R= 2e+03 Depth= 7720 States= 2e+07 Transitions= 7.09e+09 Memory= 1345.393 t= 9.41e+03 R= 2e+03 Depth= 7720 States= 2.1e+07 Transitions= 7.48e+09 Memory= 1383.576 t= 9.93e+03 R= 2e+03 Depth= 7720 States= 2.2e+07 Transitions= 7.94e+09 Memory= 1421.955 t= 1.06e+04 R= 2e+03 Depth= 7720 States= 2.3e+07 Transitions= 8.37e+09 Memory= 1459.846 t= 1.11e+04 R= 2e+03 Depth= 7720 States= 2.4e+07 Transitions= 8.77e+09 Memory= 1497.346 t= 1.17e+04 R= 2e+03 Depth= 7720 States= 2.5e+07 Transitions= 9.22e+09 Memory= 1535.529 t= 1.23e+04 R= 2e+03 Depth= 7720 States= 2.6e+07 Transitions= 9.48e+09 Memory= 1574.006 t= 1.26e+04 R= 2e+03 Depth= 7720 States= 2.7e+07 Transitions= 9.85e+09 Memory= 1612.385 t= 1.31e+04 R= 2e+03 Depth= 7720 States= 2.8e+07 Transitions= 1.02e+10 Memory= 1650.666 t= 1.37e+04 R= 2e+03 Depth= 7940 States= 2.9e+07 Transitions= 1.06e+10 Memory= 1688.752 t= 1.41e+04 R= 2e+03 Depth= 7998 States= 3e+07 Transitions= 1.09e+10 Memory= 1726.936 t= 1.46e+04 R= 2e+03 Depth= 7998 States= 3.1e+07 Transitions= 1.13e+10 Memory= 1765.315 t= 1.51e+04 R= 2e+03 Depth= 7998 States= 3.2e+07 Transitions= 1.16e+10 Memory= 1803.498 t= 1.55e+04 R= 2e+03 Depth= 7998 States= 3.3e+07 Transitions= 1.19e+10 Memory= 1841.682 t= 1.6e+04 R= 2e+03 Depth= 7998 States= 3.4e+07 Transitions= 1.23e+10 Memory= 1879.963 t= 1.65e+04 R= 2e+03 pan: resizing hashtable to -w26.. done Depth= 7998 States= 3.5e+07 Transitions= 1.26e+10 Memory= 2414.131 t= 1.69e+04 R= 2e+03 Depth= 7998 States= 3.6e+07 Transitions= 1.29e+10 Memory= 2452.315 t= 1.73e+04 R= 2e+03 Depth= 7998 States= 3.7e+07 Transitions= 1.32e+10 Memory= 2490.498 t= 1.77e+04 R= 2e+03 Depth= 7998 States= 3.8e+07 Transitions= 1.35e+10 Memory= 2528.584 t= 1.82e+04 R= 2e+03 Depth= 7998 States= 3.9e+07 Transitions= 1.39e+10 Memory= 2566.768 t= 1.86e+04 R= 2e+03 Depth= 7998 States= 4e+07 Transitions= 1.41e+10 Memory= 2604.951 t= 1.89e+04 R= 2e+03 Depth= 7998 States= 4.1e+07 Transitions= 1.44e+10 Memory= 2643.135 t= 1.93e+04 R= 2e+03 Depth= 7998 States= 4.2e+07 Transitions= 1.48e+10 Memory= 2682.002 t= 1.98e+04 R= 2e+03 Depth= 7998 States= 4.3e+07 Transitions= 1.51e+10 Memory= 2720.283 t= 2.03e+04 R= 2e+03 Depth= 7998 States= 4.4e+07 Transitions= 1.56e+10 Memory= 2759.053 t= 2.09e+04 R= 2e+03 Depth= 7998 States= 4.5e+07 Transitions= 1.59e+10 Memory= 2797.432 t= 2.13e+04 R= 2e+03 Depth= 7998 States= 4.6e+07 Transitions= 1.64e+10 Memory= 2836.201 t= 2.19e+04 R= 2e+03 Depth= 7998 States= 4.7e+07 Transitions= 1.68e+10 Memory= 2875.068 t= 2.24e+04 R= 2e+03 Depth= 7998 States= 4.8e+07 Transitions= 1.72e+10 Memory= 2913.643 t= 2.29e+04 R= 2e+03 Depth= 7998 States= 4.9e+07 Transitions= 1.76e+10 Memory= 2952.412 t= 2.34e+04 R= 2e+03 Depth= 7998 States= 5e+07 Transitions= 1.78e+10 Memory= 2989.619 t= 2.38e+04 R= 2e+03 Depth= 7998 States= 5.1e+07 Transitions= 1.81e+10 Memory= 3027.901 t= 2.42e+04 R= 2e+03 Depth= 7998 States= 5.2e+07 Transitions= 1.84e+10 Memory= 3066.279 t= 2.46e+04 R= 2e+03 Depth= 7998 States= 5.3e+07 Transitions= 1.87e+10 Memory= 3104.463 t= 2.49e+04 R= 2e+03 Depth= 7998 States= 5.4e+07 Transitions= 1.93e+10 Memory= 3142.842 t= 2.57e+04 R= 2e+03 Depth= 7998 States= 5.5e+07 Transitions= 2.01e+10 Memory= 3181.026 t= 2.68e+04 R= 2e+03 Depth= 7998 States= 5.6e+07 Transitions= 2.07e+10 Memory= 3219.990 t= 2.76e+04 R= 2e+03 Depth= 7998 States= 5.7e+07 Transitions= 2.11e+10 Memory= 3258.467 t= 2.82e+04 R= 2e+03 Depth= 7998 States= 5.8e+07 Transitions= 2.15e+10 Memory= 3297.236 t= 2.87e+04 R= 2e+03 Depth= 7998 States= 5.9e+07 Transitions= 2.18e+10 Memory= 3334.151 t= 2.91e+04 R= 2e+03 Depth= 7998 States= 6e+07 Transitions= 2.22e+10 Memory= 3372.432 t= 2.97e+04 R= 2e+03 Depth= 7998 States= 6.1e+07 Transitions= 2.27e+10 Memory= 3410.713 t= 3.03e+04 R= 2e+03 Depth= 7998 States= 6.2e+07 Transitions= 2.32e+10 Memory= 3448.701 t= 3.09e+04 R= 2e+03 Depth= 7998 States= 6.3e+07 Transitions= 2.35e+10 Memory= 3485.615 t= 3.15e+04 R= 2e+03 Depth= 7998 States= 6.4e+07 Transitions= 2.38e+10 Memory= 3523.604 t= 3.19e+04 R= 2e+03 Depth= 7998 States= 6.5e+07 Transitions= 2.42e+10 Memory= 3561.690 t= 3.23e+04 R= 2e+03 Depth= 7998 States= 6.6e+07 Transitions= 2.46e+10 Memory= 3598.799 t= 3.28e+04 R= 2e+03 Depth= 7998 States= 6.7e+07 Transitions= 2.49e+10 Memory= 3635.225 t= 3.33e+04 R= 2e+03 Depth= 7998 States= 6.8e+07 Transitions= 2.53e+10 Memory= 3672.139 t= 3.38e+04 R= 2e+03 Depth= 7998 States= 6.9e+07 Transitions= 2.56e+10 Memory= 3706.807 t= 3.42e+04 R= 2e+03 Depth= 7998 States= 7e+07 Transitions= 2.59e+10 Memory= 3743.916 t= 3.47e+04 R= 2e+03 Depth= 7998 States= 7.1e+07 Transitions= 2.62e+10 Memory= 3781.026 t= 3.51e+04 R= 2e+03 Depth= 7998 States= 7.2e+07 Transitions= 2.66e+10 Memory= 3818.721 t= 3.56e+04 R= 2e+03 Depth= 7998 States= 7.3e+07 Transitions= 2.68e+10 Memory= 3855.244 t= 3.59e+04 R= 2e+03 Depth= 7998 States= 7.4e+07 Transitions= 2.72e+10 Memory= 3892.647 t= 3.64e+04 R= 2e+03 Depth= 7998 States= 7.5e+07 Transitions= 2.76e+10 Memory= 3930.049 t= 3.69e+04 R= 2e+03 Depth= 7998 States= 7.6e+07 Transitions= 2.78e+10 Memory= 3966.963 t= 3.72e+04 R= 2e+03 Depth= 7998 States= 7.7e+07 Transitions= 2.81e+10 Memory= 4003.975 t= 3.77e+04 R= 2e+03 Depth= 7998 States= 7.8e+07 Transitions= 2.84e+10 Memory= 4041.084 t= 3.8e+04 R= 2e+03 Depth= 7998 States= 7.9e+07 Transitions= 2.87e+10 Memory= 4078.584 t= 3.84e+04 R= 2e+03 Depth= 7998 States= 8e+07 Transitions= 2.91e+10 Memory= 4114.815 t= 3.9e+04 R= 2e+03 Depth= 7998 States= 8.1e+07 Transitions= 2.95e+10 Memory= 4151.240 t= 3.95e+04 R= 2e+03 Depth= 7998 States= 8.2e+07 Transitions= 2.99e+10 Memory= 4189.131 t= 4e+04 R= 2e+03 Depth= 7998 States= 8.3e+07 Transitions= 3.03e+10 Memory= 4226.533 t= 4.06e+04 R= 2e+03 Depth= 7998 States= 8.4e+07 Transitions= 3.07e+10 Memory= 4264.912 t= 4.11e+04 R= 2e+03 Depth= 7998 States= 8.5e+07 Transitions= 3.11e+10 Memory= 4302.998 t= 4.16e+04 R= 2e+03 Depth= 7998 States= 8.6e+07 Transitions= 3.15e+10 Memory= 4340.693 t= 4.21e+04 R= 2e+03 Depth= 7998 States= 8.7e+07 Transitions= 3.19e+10 Memory= 4378.877 t= 4.27e+04 R= 2e+03 Depth= 7998 States= 8.8e+07 Transitions= 3.23e+10 Memory= 4417.061 t= 4.32e+04 R= 2e+03 (Spin Version 5.1.7 -- 23 December 2008) + Partial Order Reduction + Compression Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 72 byte, depth reached 7998, errors: 0 88716525 states, stored 3.2432758e+10 states, matched 3.2521475e+10 transitions (= stored+matched) 1.8325967e+11 atomic steps hash conflicts: 1.7127982e+10 (resolved) Stats on memory usage (in Megabytes): 8460.667 equivalent memory usage for states (stored*(State-vector + overhead)) 3474.757 actual memory usage for states (compression: 41.07%) state-vector as stored = 13 byte + 28 byte overhead 512.000 memory used for hash table (-w26) 457.764 memory used for DFS stack (-m10000000) 4444.111 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 606546 5194 3779 2 ] unreached in proctype urcu_reader line 267, ".input.spin", state 57, "cache_dirty_urcu_gp_ctr = 0" line 275, ".input.spin", state 79, "cache_dirty_rcu_ptr = 0" line 279, ".input.spin", state 88, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 104, "(1)" line 248, ".input.spin", state 112, "(1)" line 252, ".input.spin", state 124, "(1)" line 256, ".input.spin", state 132, "(1)" line 406, ".input.spin", state 158, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 190, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 204, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 223, "(1)" line 433, ".input.spin", state 253, "(1)" line 437, ".input.spin", state 266, "(1)" line 686, ".input.spin", state 287, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<1))" line 406, ".input.spin", state 294, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 326, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 340, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 359, "(1)" line 433, ".input.spin", state 389, "(1)" line 437, ".input.spin", state 402, "(1)" line 406, ".input.spin", state 423, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 455, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 469, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 488, "(1)" line 433, ".input.spin", state 518, "(1)" line 437, ".input.spin", state 531, "(1)" line 406, ".input.spin", state 554, "cache_dirty_urcu_gp_ctr = 0" line 406, ".input.spin", state 556, "(1)" line 406, ".input.spin", state 557, "(cache_dirty_urcu_gp_ctr)" line 406, ".input.spin", state 557, "else" line 406, ".input.spin", state 560, "(1)" line 410, ".input.spin", state 568, "cache_dirty_urcu_active_readers = 0" line 410, ".input.spin", state 570, "(1)" line 410, ".input.spin", state 571, "(cache_dirty_urcu_active_readers)" line 410, ".input.spin", state 571, "else" line 410, ".input.spin", state 574, "(1)" line 410, ".input.spin", state 575, "(1)" line 410, ".input.spin", state 575, "(1)" line 408, ".input.spin", state 580, "((i<1))" line 408, ".input.spin", state 580, "((i>=1))" line 415, ".input.spin", state 586, "cache_dirty_rcu_ptr = 0" line 415, ".input.spin", state 588, "(1)" line 415, ".input.spin", state 589, "(cache_dirty_rcu_ptr)" line 415, ".input.spin", state 589, "else" line 415, ".input.spin", state 592, "(1)" line 415, ".input.spin", state 593, "(1)" line 415, ".input.spin", state 593, "(1)" line 419, ".input.spin", state 600, "cache_dirty_rcu_data[i] = 0" line 419, ".input.spin", state 602, "(1)" line 419, ".input.spin", state 603, "(cache_dirty_rcu_data[i])" line 419, ".input.spin", state 603, "else" line 419, ".input.spin", state 606, "(1)" line 419, ".input.spin", state 607, "(1)" line 419, ".input.spin", state 607, "(1)" line 417, ".input.spin", state 612, "((i<2))" line 417, ".input.spin", state 612, "((i>=2))" line 424, ".input.spin", state 619, "(1)" line 424, ".input.spin", state 620, "(!(cache_dirty_urcu_gp_ctr))" line 424, ".input.spin", state 620, "else" line 424, ".input.spin", state 623, "(1)" line 424, ".input.spin", state 624, "(1)" line 424, ".input.spin", state 624, "(1)" line 428, ".input.spin", state 632, "(1)" line 428, ".input.spin", state 633, "(!(cache_dirty_urcu_active_readers))" line 428, ".input.spin", state 633, "else" line 428, ".input.spin", state 636, "(1)" line 428, ".input.spin", state 637, "(1)" line 428, ".input.spin", state 637, "(1)" line 426, ".input.spin", state 642, "((i<1))" line 426, ".input.spin", state 642, "((i>=1))" line 433, ".input.spin", state 649, "(1)" line 433, ".input.spin", state 650, "(!(cache_dirty_rcu_ptr))" line 433, ".input.spin", state 650, "else" line 433, ".input.spin", state 653, "(1)" line 433, ".input.spin", state 654, "(1)" line 433, ".input.spin", state 654, "(1)" line 437, ".input.spin", state 662, "(1)" line 437, ".input.spin", state 663, "(!(cache_dirty_rcu_data[i]))" line 437, ".input.spin", state 663, "else" line 437, ".input.spin", state 666, "(1)" line 437, ".input.spin", state 667, "(1)" line 437, ".input.spin", state 667, "(1)" line 435, ".input.spin", state 672, "((i<2))" line 435, ".input.spin", state 672, "((i>=2))" line 445, ".input.spin", state 676, "(1)" line 445, ".input.spin", state 676, "(1)" line 686, ".input.spin", state 679, "cached_urcu_active_readers = (tmp+1)" line 686, ".input.spin", state 680, "_proc_urcu_reader = (_proc_urcu_reader|(1<<5))" line 686, ".input.spin", state 681, "(1)" line 406, ".input.spin", state 688, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 720, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 734, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 753, "(1)" line 433, ".input.spin", state 783, "(1)" line 437, ".input.spin", state 796, "(1)" line 406, ".input.spin", state 824, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 856, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 870, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 889, "(1)" line 433, ".input.spin", state 919, "(1)" line 437, ".input.spin", state 932, "(1)" line 406, ".input.spin", state 953, "cache_dirty_urcu_gp_ctr = 0" line 406, ".input.spin", state 955, "(1)" line 406, ".input.spin", state 956, "(cache_dirty_urcu_gp_ctr)" line 406, ".input.spin", state 956, "else" line 406, ".input.spin", state 959, "(1)" line 410, ".input.spin", state 967, "cache_dirty_urcu_active_readers = 0" line 410, ".input.spin", state 969, "(1)" line 410, ".input.spin", state 970, "(cache_dirty_urcu_active_readers)" line 410, ".input.spin", state 970, "else" line 410, ".input.spin", state 973, "(1)" line 410, ".input.spin", state 974, "(1)" line 410, ".input.spin", state 974, "(1)" line 408, ".input.spin", state 979, "((i<1))" line 408, ".input.spin", state 979, "((i>=1))" line 415, ".input.spin", state 985, "cache_dirty_rcu_ptr = 0" line 415, ".input.spin", state 987, "(1)" line 415, ".input.spin", state 988, "(cache_dirty_rcu_ptr)" line 415, ".input.spin", state 988, "else" line 415, ".input.spin", state 991, "(1)" line 415, ".input.spin", state 992, "(1)" line 415, ".input.spin", state 992, "(1)" line 419, ".input.spin", state 999, "cache_dirty_rcu_data[i] = 0" line 419, ".input.spin", state 1001, "(1)" line 419, ".input.spin", state 1002, "(cache_dirty_rcu_data[i])" line 419, ".input.spin", state 1002, "else" line 419, ".input.spin", state 1005, "(1)" line 419, ".input.spin", state 1006, "(1)" line 419, ".input.spin", state 1006, "(1)" line 417, ".input.spin", state 1011, "((i<2))" line 417, ".input.spin", state 1011, "((i>=2))" line 424, ".input.spin", state 1018, "(1)" line 424, ".input.spin", state 1019, "(!(cache_dirty_urcu_gp_ctr))" line 424, ".input.spin", state 1019, "else" line 424, ".input.spin", state 1022, "(1)" line 424, ".input.spin", state 1023, "(1)" line 424, ".input.spin", state 1023, "(1)" line 428, ".input.spin", state 1031, "(1)" line 428, ".input.spin", state 1032, "(!(cache_dirty_urcu_active_readers))" line 428, ".input.spin", state 1032, "else" line 428, ".input.spin", state 1035, "(1)" line 428, ".input.spin", state 1036, "(1)" line 428, ".input.spin", state 1036, "(1)" line 426, ".input.spin", state 1041, "((i<1))" line 426, ".input.spin", state 1041, "((i>=1))" line 433, ".input.spin", state 1048, "(1)" line 433, ".input.spin", state 1049, "(!(cache_dirty_rcu_ptr))" line 433, ".input.spin", state 1049, "else" line 433, ".input.spin", state 1052, "(1)" line 433, ".input.spin", state 1053, "(1)" line 433, ".input.spin", state 1053, "(1)" line 437, ".input.spin", state 1061, "(1)" line 437, ".input.spin", state 1062, "(!(cache_dirty_rcu_data[i]))" line 437, ".input.spin", state 1062, "else" line 437, ".input.spin", state 1065, "(1)" line 437, ".input.spin", state 1066, "(1)" line 437, ".input.spin", state 1066, "(1)" line 435, ".input.spin", state 1071, "((i<2))" line 435, ".input.spin", state 1071, "((i>=2))" line 445, ".input.spin", state 1075, "(1)" line 445, ".input.spin", state 1075, "(1)" line 694, ".input.spin", state 1079, "_proc_urcu_reader = (_proc_urcu_reader|(1<<11))" line 406, ".input.spin", state 1084, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 1116, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 1130, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 1149, "(1)" line 433, ".input.spin", state 1179, "(1)" line 437, ".input.spin", state 1192, "(1)" line 406, ".input.spin", state 1216, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 1248, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 1262, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 1281, "(1)" line 433, ".input.spin", state 1311, "(1)" line 437, ".input.spin", state 1324, "(1)" line 406, ".input.spin", state 1349, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 1381, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 1395, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 1414, "(1)" line 433, ".input.spin", state 1444, "(1)" line 437, ".input.spin", state 1457, "(1)" line 406, ".input.spin", state 1478, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 1510, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 1524, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 1543, "(1)" line 433, ".input.spin", state 1573, "(1)" line 437, ".input.spin", state 1586, "(1)" line 406, ".input.spin", state 1612, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 1644, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 1658, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 1677, "(1)" line 433, ".input.spin", state 1707, "(1)" line 437, ".input.spin", state 1720, "(1)" line 406, ".input.spin", state 1741, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 1773, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 1787, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 1806, "(1)" line 433, ".input.spin", state 1836, "(1)" line 437, ".input.spin", state 1849, "(1)" line 406, ".input.spin", state 1873, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 1905, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 1919, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 1938, "(1)" line 433, ".input.spin", state 1968, "(1)" line 437, ".input.spin", state 1981, "(1)" line 733, ".input.spin", state 2002, "_proc_urcu_reader = (_proc_urcu_reader|((1<<2)<<19))" line 406, ".input.spin", state 2009, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 2041, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 2055, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 2074, "(1)" line 433, ".input.spin", state 2104, "(1)" line 437, ".input.spin", state 2117, "(1)" line 406, ".input.spin", state 2138, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 2170, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 2184, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 2203, "(1)" line 433, ".input.spin", state 2233, "(1)" line 437, ".input.spin", state 2246, "(1)" line 406, ".input.spin", state 2269, "cache_dirty_urcu_gp_ctr = 0" line 406, ".input.spin", state 2271, "(1)" line 406, ".input.spin", state 2272, "(cache_dirty_urcu_gp_ctr)" line 406, ".input.spin", state 2272, "else" line 406, ".input.spin", state 2275, "(1)" line 410, ".input.spin", state 2283, "cache_dirty_urcu_active_readers = 0" line 410, ".input.spin", state 2285, "(1)" line 410, ".input.spin", state 2286, "(cache_dirty_urcu_active_readers)" line 410, ".input.spin", state 2286, "else" line 410, ".input.spin", state 2289, "(1)" line 410, ".input.spin", state 2290, "(1)" line 410, ".input.spin", state 2290, "(1)" line 408, ".input.spin", state 2295, "((i<1))" line 408, ".input.spin", state 2295, "((i>=1))" line 415, ".input.spin", state 2301, "cache_dirty_rcu_ptr = 0" line 415, ".input.spin", state 2303, "(1)" line 415, ".input.spin", state 2304, "(cache_dirty_rcu_ptr)" line 415, ".input.spin", state 2304, "else" line 415, ".input.spin", state 2307, "(1)" line 415, ".input.spin", state 2308, "(1)" line 415, ".input.spin", state 2308, "(1)" line 419, ".input.spin", state 2315, "cache_dirty_rcu_data[i] = 0" line 419, ".input.spin", state 2317, "(1)" line 419, ".input.spin", state 2318, "(cache_dirty_rcu_data[i])" line 419, ".input.spin", state 2318, "else" line 419, ".input.spin", state 2321, "(1)" line 419, ".input.spin", state 2322, "(1)" line 419, ".input.spin", state 2322, "(1)" line 417, ".input.spin", state 2327, "((i<2))" line 417, ".input.spin", state 2327, "((i>=2))" line 424, ".input.spin", state 2334, "(1)" line 424, ".input.spin", state 2335, "(!(cache_dirty_urcu_gp_ctr))" line 424, ".input.spin", state 2335, "else" line 424, ".input.spin", state 2338, "(1)" line 424, ".input.spin", state 2339, "(1)" line 424, ".input.spin", state 2339, "(1)" line 428, ".input.spin", state 2347, "(1)" line 428, ".input.spin", state 2348, "(!(cache_dirty_urcu_active_readers))" line 428, ".input.spin", state 2348, "else" line 428, ".input.spin", state 2351, "(1)" line 428, ".input.spin", state 2352, "(1)" line 428, ".input.spin", state 2352, "(1)" line 426, ".input.spin", state 2357, "((i<1))" line 426, ".input.spin", state 2357, "((i>=1))" line 433, ".input.spin", state 2364, "(1)" line 433, ".input.spin", state 2365, "(!(cache_dirty_rcu_ptr))" line 433, ".input.spin", state 2365, "else" line 433, ".input.spin", state 2368, "(1)" line 433, ".input.spin", state 2369, "(1)" line 433, ".input.spin", state 2369, "(1)" line 437, ".input.spin", state 2377, "(1)" line 437, ".input.spin", state 2378, "(!(cache_dirty_rcu_data[i]))" line 437, ".input.spin", state 2378, "else" line 437, ".input.spin", state 2381, "(1)" line 437, ".input.spin", state 2382, "(1)" line 437, ".input.spin", state 2382, "(1)" line 435, ".input.spin", state 2387, "((i<2))" line 435, ".input.spin", state 2387, "((i>=2))" line 445, ".input.spin", state 2391, "(1)" line 445, ".input.spin", state 2391, "(1)" line 733, ".input.spin", state 2394, "cached_urcu_active_readers = (tmp+1)" line 733, ".input.spin", state 2395, "_proc_urcu_reader = (_proc_urcu_reader|(1<<23))" line 733, ".input.spin", state 2396, "(1)" line 406, ".input.spin", state 2403, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 2435, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 2449, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 2468, "(1)" line 433, ".input.spin", state 2498, "(1)" line 437, ".input.spin", state 2511, "(1)" line 406, ".input.spin", state 2538, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 2570, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 2584, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 2603, "(1)" line 433, ".input.spin", state 2633, "(1)" line 437, ".input.spin", state 2646, "(1)" line 406, ".input.spin", state 2667, "cache_dirty_urcu_gp_ctr = 0" line 415, ".input.spin", state 2699, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 2713, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 2732, "(1)" line 433, ".input.spin", state 2762, "(1)" line 437, ".input.spin", state 2775, "(1)" line 244, ".input.spin", state 2808, "(1)" line 252, ".input.spin", state 2828, "(1)" line 256, ".input.spin", state 2836, "(1)" line 244, ".input.spin", state 2851, "(1)" line 252, ".input.spin", state 2871, "(1)" line 256, ".input.spin", state 2879, "(1)" line 928, ".input.spin", state 2896, "-end-" (245 of 2896 states) unreached in proctype urcu_writer line 406, ".input.spin", state 45, "cache_dirty_urcu_gp_ctr = 0" line 410, ".input.spin", state 59, "cache_dirty_urcu_active_readers = 0" line 415, ".input.spin", state 77, "cache_dirty_rcu_ptr = 0" line 424, ".input.spin", state 110, "(1)" line 428, ".input.spin", state 123, "(1)" line 433, ".input.spin", state 140, "(1)" line 267, ".input.spin", state 176, "cache_dirty_urcu_gp_ctr = 0" line 271, ".input.spin", state 185, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 198, "cache_dirty_rcu_ptr = 0" line 406, ".input.spin", state 238, "cache_dirty_urcu_gp_ctr = 0" line 410, ".input.spin", state 252, "cache_dirty_urcu_active_readers = 0" line 415, ".input.spin", state 270, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 284, "cache_dirty_rcu_data[i] = 0" line 424, ".input.spin", state 303, "(1)" line 428, ".input.spin", state 316, "(1)" line 433, ".input.spin", state 333, "(1)" line 437, ".input.spin", state 346, "(1)" line 410, ".input.spin", state 383, "cache_dirty_urcu_active_readers = 0" line 415, ".input.spin", state 401, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 415, "cache_dirty_rcu_data[i] = 0" line 428, ".input.spin", state 447, "(1)" line 433, ".input.spin", state 464, "(1)" line 437, ".input.spin", state 477, "(1)" line 410, ".input.spin", state 522, "cache_dirty_urcu_active_readers = 0" line 415, ".input.spin", state 540, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 554, "cache_dirty_rcu_data[i] = 0" line 428, ".input.spin", state 586, "(1)" line 433, ".input.spin", state 603, "(1)" line 437, ".input.spin", state 616, "(1)" line 410, ".input.spin", state 651, "cache_dirty_urcu_active_readers = 0" line 415, ".input.spin", state 669, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 683, "cache_dirty_rcu_data[i] = 0" line 428, ".input.spin", state 715, "(1)" line 433, ".input.spin", state 732, "(1)" line 437, ".input.spin", state 745, "(1)" line 410, ".input.spin", state 782, "cache_dirty_urcu_active_readers = 0" line 415, ".input.spin", state 800, "cache_dirty_rcu_ptr = 0" line 419, ".input.spin", state 814, "cache_dirty_rcu_data[i] = 0" line 428, ".input.spin", state 846, "(1)" line 433, ".input.spin", state 863, "(1)" line 437, ".input.spin", state 876, "(1)" line 267, ".input.spin", state 931, "cache_dirty_urcu_gp_ctr = 0" line 271, ".input.spin", state 940, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 955, "(1)" line 279, ".input.spin", state 962, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 978, "(1)" line 248, ".input.spin", state 986, "(1)" line 252, ".input.spin", state 998, "(1)" line 256, ".input.spin", state 1006, "(1)" line 267, ".input.spin", state 1037, "cache_dirty_urcu_gp_ctr = 0" line 271, ".input.spin", state 1046, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 1059, "cache_dirty_rcu_ptr = 0" line 279, ".input.spin", state 1068, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 1084, "(1)" line 248, ".input.spin", state 1092, "(1)" line 252, ".input.spin", state 1104, "(1)" line 256, ".input.spin", state 1112, "(1)" line 271, ".input.spin", state 1138, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 1151, "cache_dirty_rcu_ptr = 0" line 279, ".input.spin", state 1160, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 1176, "(1)" line 248, ".input.spin", state 1184, "(1)" line 252, ".input.spin", state 1196, "(1)" line 256, ".input.spin", state 1204, "(1)" line 267, ".input.spin", state 1235, "cache_dirty_urcu_gp_ctr = 0" line 271, ".input.spin", state 1244, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 1257, "cache_dirty_rcu_ptr = 0" line 279, ".input.spin", state 1266, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 1282, "(1)" line 248, ".input.spin", state 1290, "(1)" line 252, ".input.spin", state 1302, "(1)" line 256, ".input.spin", state 1310, "(1)" line 271, ".input.spin", state 1336, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 1349, "cache_dirty_rcu_ptr = 0" line 279, ".input.spin", state 1358, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 1374, "(1)" line 248, ".input.spin", state 1382, "(1)" line 252, ".input.spin", state 1394, "(1)" line 256, ".input.spin", state 1402, "(1)" line 267, ".input.spin", state 1433, "cache_dirty_urcu_gp_ctr = 0" line 271, ".input.spin", state 1442, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 1455, "cache_dirty_rcu_ptr = 0" line 279, ".input.spin", state 1464, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 1480, "(1)" line 248, ".input.spin", state 1488, "(1)" line 252, ".input.spin", state 1500, "(1)" line 256, ".input.spin", state 1508, "(1)" line 271, ".input.spin", state 1534, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 1547, "cache_dirty_rcu_ptr = 0" line 279, ".input.spin", state 1556, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 1572, "(1)" line 248, ".input.spin", state 1580, "(1)" line 252, ".input.spin", state 1592, "(1)" line 256, ".input.spin", state 1600, "(1)" line 267, ".input.spin", state 1631, "cache_dirty_urcu_gp_ctr = 0" line 271, ".input.spin", state 1640, "cache_dirty_urcu_active_readers = 0" line 275, ".input.spin", state 1653, "cache_dirty_rcu_ptr = 0" line 279, ".input.spin", state 1662, "cache_dirty_rcu_data[i] = 0" line 244, ".input.spin", state 1678, "(1)" line 248, ".input.spin", state 1686, "(1)" line 252, ".input.spin", state 1698, "(1)" line 256, ".input.spin", state 1706, "(1)" line 1303, ".input.spin", state 1722, "-end-" (103 of 1722 states) unreached in proctype :init: (0 of 28 states) pan: elapsed time 4.35e+04 seconds pan: rate 2039.1355 states/second pan: avg transition delay 1.3378e-06 usec cp .input.spin asserts.spin.input cp .input.spin.trail asserts.spin.input.trail make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-alpha-ipi'