search

microsoft / CCF

Confidential Consortium Framework
https://microsoft.github.io/CCF/
Apache License 2.0
764 stars 205 forks source link

Generate scenario from trace #5875

Closed achamayou closed 4 months ago

achamayou commented 5 months ago

Very basic script, using functionality introduced by https://github.com/tlaplus/tlaplus/issues/853, try and translate a trace to a raft scenario, for the purpose of executing counter-examples on the implementation.

Example run, using the following spec break:

LogMatchingInv ==
    \A i, j \in Servers : i /= j => Len(log[i]) < 10
./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json

$ python3 trace2scen.py MCccfraftWithReconfig.json > scen
start_node,n1
emit_signature,2
# MCClientRequest MCccfraft:65
replicate,2,42
assert_is_primary,n1
# MCSignCommittableMessages MCccfraft:73
emit_signature,2
assert_is_primary,n1
# ChangeConfiguration ccfraft:660
replicate_new_configuration,2,n1,n2
assert_is_primary,n1
# MCSignCommittableMessages MCccfraft:73
emit_signature,2
assert_is_primary,n1
# MCClientRequest MCccfraft:65
replicate,2,42
assert_is_primary,n1
# MCSignCommittableMessages MCccfraft:73
emit_signature,2
assert_is_primary,n1
# ChangeConfiguration ccfraft:660
replicate_new_configuration,2,n2
assert_is_primary,n1
# MCSignCommittableMessages MCccfraft:73
emit_signature,2
assert_is_primary,n1
assert_commit_idx,n1,2
assert_commit_idx,n2,0

It's not straightforward to do this correctly, because the spec is set up differently from the driver: individual message delivery and consumption is contained in steps, whereas the driver has a separate dispatch action. This difference in granularity means that we probably can't reproduce every scenario precisely, but we can get quite close most of the time still.

ccf-bot commented 5 months ago

generate_scenario_from_trace@80033 aka 20240109.7 vs main ewma over 20 builds from 79781 to 80028

Click to see table main | build_id | build_number | pi_basic_mt_sgx_cft^ | pi_basic_mt_sgx_cft_mem | Commit latency factor | tpcc_sgx_cft^ | tpcc_sgx_cft_mem | ls_sgx_cft^ | ls_sgx_cft_mem | pi_ls_sgx_cft^ | pi_ls_sgx_cft_mem | pi_basic_sgx_cft^ | pi_basic_sgx_cft_mem | pi_basic_js_sgx_cft^ | pi_basic_js_sgx_cft_mem | tlc_3node_fixed_duration_s | tlc_3node_fixed_states | tlc_atomic_reconfig_duration_s | tlc_atomic_reconfig_states | tlc_reconfig_duration_s | tlc_reconfig_states | ls_jwt_sgx_cft^ | ls_jwt_sgx_cft_mem | pi_ls_jwt_sgx_cft^ | pi_ls_jwt_sgx_cft_mem | ls_js_sgx_cft^ | ls_js_sgx_cft_mem | pi_basic_mt_virtual_cft^ | ls_full_js_sgx_cft^ | ls_full_js_sgx_cft_mem | ls_js_jwt_sgx_cft^ | ls_js_jwt_sgx_cft_mem | hist_sgx_cft^ | RB put (/s)^ | CHAMP put (/s)^ | RB get (/s)^ | CHAMP get (/s)^ | tpcc_virtual_cft^ | ls_virtual_cft^ | pi_ls_virtual_cft^ | pi_basic_virtual_cft^ | pi_basic_js_virtual_cft^ | ls_jwt_virtual_cft^ | pi_ls_jwt_virtual_cft^ | ls_js_virtual_cft^ | ls_full_js_virtual_cft^ | ls_js_jwt_virtual_cft^ | tlc_sim_traces | tlc_sim_levelmean | |-----------:|:---------------|-----------------------:|--------------------------:|------------------------:|----------------:|-------------------:|--------------:|-----------------:|-----------------:|--------------------:|--------------------:|-----------------------:|-----------------------:|--------------------------:|-----------------------------:|-------------------------:|---------------------------------:|-----------------------------:|--------------------------:|----------------------:|------------------:|---------------------:|---------------------:|------------------------:|-----------------:|--------------------:|---------------------------:|----------------------:|-------------------------:|---------------------:|------------------------:|----------------:|---------------:|------------------:|---------------:|------------------:|--------------------:|------------------:|---------------------:|------------------------:|---------------------------:|----------------------:|-------------------------:|---------------------:|--------------------------:|-------------------------:|-----------------:|--------------------:| | 79781 | 20231229.2 | 27896.7 | 2.51822e+07 | 0.801636 | 5589.66 | 8.59996e+07 | 14027.6 | 1.88908e+07 | 14166.7 | 1.05021e+07 | 15567.2 | 1.46964e+07 | 1425.2 | 1.25993e+07 | 6 | 86496 | 436 | 1.2541e+07 | 240 | 6.31473e+06 | 6793.52 | 1.67936e+07 | 7078.9 | 6.30784e+06 | 5797.56 | 1.67936e+07 | 70323.6 | 5483.48 | 1.67936e+07 | 3993.74 | 1.67936e+07 | 40847.4 | 834593 | 1.18035e+06 | 8.15979e+06 | 3.07217e+07 | 17379.6 | 53058 | 56634.4 | 62290.7 | 4544.7 | 21324.7 | 22159.2 | 17388.8 | 17492.5 | 11838.8 | 2181 | 403 | | 79795 | 20240101.3 | 28203.3 | 2.51822e+07 | 0.78501 | 5573.08 | 8.59996e+07 | 14058.6 | 1.88908e+07 | 14075.3 | 1.05021e+07 | 15400.4 | 1.25993e+07 | 1433.5 | 1.25993e+07 | 7 | 86496 | 437 | 1.2541e+07 | 244 | 6.31473e+06 | 6907.22 | 1.88908e+07 | 6981.9 | 6.30784e+06 | 5797.99 | 1.67936e+07 | 88523 | 5721.54 | 1.67936e+07 | 3992.77 | 1.67936e+07 | 45491.3 | 828138 | 1.18098e+06 | 8.16847e+06 | 3.08021e+07 | 17464.7 | 53125.1 | 57116.7 | 61313 | 4568.7 | 20746.1 | 22281.6 | 17744.9 | 17841.4 | 11654.5 | 2254 | 403 | | 79809 | 20240102.3 | 27998 | 2.51822e+07 | 0.818907 | 5582.58 | 8.59996e+07 | 14069 | 1.88908e+07 | 14207.7 | 1.05021e+07 | 15632.9 | 1.46964e+07 | 1438 | 1.25993e+07 | 6 | 86496 | 427 | 1.2541e+07 | 241 | 6.31473e+06 | 7254.86 | 1.67936e+07 | 6979.5 | 6.30784e+06 | 5809.21 | 1.67936e+07 | 89517.2 | 5725.47 | 1.88908e+07 | 4000.63 | 1.67936e+07 | 39813.8 | 838128 | 1.18558e+06 | 8.15241e+06 | 3.07577e+07 | 17426.2 | 52688.3 | 56487.3 | 62076.8 | 4588.5 | 20938.1 | 21383.1 | 17806.2 | 17373.5 | 11613.7 | 2304 | 403 | | 79821 | 20240102.7 | 28223.4 | 2.30851e+07 | 0.812237 | 5591.2 | 8.59996e+07 | 14003.1 | 1.88908e+07 | 14188.3 | 1.05021e+07 | 15498.1 | 1.46964e+07 | 1429.2 | 1.25993e+07 | 7 | 86496 | 446 | 1.2541e+07 | 237 | 6.31473e+06 | 7246.07 | 1.67936e+07 | 6934.2 | 6.30784e+06 | 5809.09 | 1.67936e+07 | 100850 | 5478.56 | 1.67936e+07 | 4007.06 | 1.67936e+07 | 40366 | 832255 | 1.17903e+06 | 8.15355e+06 | 3.03592e+07 | 17312.2 | 53352.6 | 57235.7 | 62129.2 | 4590.4 | 21078.7 | 22285.6 | 20842.2 | 17429 | 11612.2 | 2331 | 403 | | 79832 | 20240102.10 | 27705.2 | 2.51822e+07 | 0.780568 | 5592.62 | 8.59996e+07 | 14075.6 | 1.88908e+07 | 14247 | 1.05021e+07 | 15580.2 | 1.46964e+07 | 1429.8 | 1.25993e+07 | 6 | 86496 | 424 | 1.2541e+07 | 245 | 6.31473e+06 | 6842.56 | 1.67936e+07 | 7079.5 | 6.30784e+06 | 5781.21 | 1.67936e+07 | 90345.4 | 5767.74 | 1.67936e+07 | 3982.1 | 1.67936e+07 | 42743.5 | 823735 | 1.18304e+06 | 8.15511e+06 | 3.0778e+07 | 17247.1 | 52935.7 | 56910 | 62683.8 | 4647.1 | 20739.3 | 20193.9 | 20729.9 | 17575.8 | 11690.8 | 2301 | 403 | | 79836 | 20240103.1 | 28173 | 2.51822e+07 | 0.8277 | 5617.23 | 8.59996e+07 | 14088.9 | 1.88908e+07 | 14246.2 | 1.05021e+07 | 15684.4 | 1.46964e+07 | 1430.6 | 1.25993e+07 | 6 | 86496 | 417 | 1.2541e+07 | 238 | 6.31473e+06 | 7262.76 | 1.67936e+07 | 6980.2 | 6.30784e+06 | 5814.99 | 1.67936e+07 | 68113.2 | 5465.89 | 1.88908e+07 | 3973.9 | 1.67936e+07 | 43365.4 | 827987 | 1.18005e+06 | 8.16857e+06 | 3.13533e+07 | 17163.7 | 52985.4 | 57238.7 | 62511.8 | 4622.6 | 20776.5 | 21693.9 | 20385 | 17974.8 | 11889.2 | 2109 | 403 | | 79850 | 20240104.1 | 28107.5 | 2.51822e+07 | 0.774183 | 5647.78 | 8.59996e+07 | 14069.1 | 1.88908e+07 | 14203.3 | 1.05021e+07 | 15616.9 | 1.25993e+07 | 1430.7 | 1.25993e+07 | 6 | 86496 | 447 | 1.2541e+07 | 239 | 6.31473e+06 | 7263.29 | 1.67936e+07 | 7142 | 6.30784e+06 | 5808.21 | 1.67936e+07 | 88847.3 | 5739.03 | 1.88908e+07 | 4019.28 | 1.67936e+07 | 45361.8 | 833007 | 1.17531e+06 | 8.1401e+06 | 3.07056e+07 | 17222.5 | 53076.9 | 56886.7 | 62583 | 4618.3 | 20820.4 | 21956.8 | 17246.1 | 17545.1 | 11727 | 2277 | 403 | | 79858 | 20240104.5 | 28151.4 | 2.30851e+07 | 0.762951 | 5612.73 | 8.59996e+07 | 14105.1 | 1.88908e+07 | 14237.6 | 1.05021e+07 | 15657.2 | 1.46964e+07 | 1437 | 1.05021e+07 | 6 | 86496 | 420 | 1.2541e+07 | 238 | 6.31473e+06 | 7259.07 | 1.88908e+07 | 6983.6 | 6.30784e+06 | 5791.47 | 1.67936e+07 | 72092.6 | 5734.66 | 1.67936e+07 | 4001.19 | 1.67936e+07 | 46312.7 | 832473 | 1.18246e+06 | 8.14589e+06 | 3.0464e+07 | 17237.2 | 53156.1 | 56700.3 | 62251.6 | 4624.7 | 20802.9 | 22305.5 | 17912 | 17600.9 | 12005.6 | 2357 | 403 | | 79876 | 20240104.10 | 27983.2 | 2.51822e+07 | 0.770841 | 5617.52 | 8.59996e+07 | 14034.5 | 1.67936e+07 | 14165.8 | 1.05021e+07 | 15592.9 | 1.25993e+07 | 1427.3 | 1.25993e+07 | 6 | 86496 | 429 | 1.2541e+07 | 234 | 6.31473e+06 | 7241.98 | 1.67936e+07 | 6915.4 | 6.30784e+06 | 5771.22 | 1.67936e+07 | 82253.2 | 5737.28 | 1.67936e+07 | 3985.63 | 1.67936e+07 | 40222.9 | 829045 | 1.18083e+06 | 8.15014e+06 | 3.10298e+07 | 17196.9 | 53164.5 | 56410.8 | 62397 | 4645.9 | 20949.8 | 22178.9 | 17324.7 | 17551.5 | 11659.7 | 2315 | 403 | | 79893 | 20240105.3 | 28242.6 | 2.30851e+07 | 0.770387 | 5619.63 | 8.59996e+07 | 14091.5 | 1.88908e+07 | 14247.6 | 1.05021e+07 | 15674.3 | 1.25993e+07 | 1436.8 | 1.25993e+07 | 6 | 86496 | 438 | 1.2541e+07 | 234 | 6.31473e+06 | 7241.21 | 1.67936e+07 | 7028.1 | 6.30784e+06 | 5776.46 | 1.67936e+07 | 79459.2 | 5739.53 | 1.67936e+07 | 4001.54 | 1.67936e+07 | 41192.1 | 834184 | 1.18333e+06 | 8.13454e+06 | 3.07928e+07 | 17195.7 | 53109.3 | 56423.9 | 61913.6 | 4637.7 | 21053.6 | 21897.2 | 17479.2 | 17489.6 | 11786.3 | 2312 | 403 | | 79901 | 20240105.6 | 28134.7 | 2.51822e+07 | 0.804442 | 5625.32 | 8.59996e+07 | 14099 | 1.88908e+07 | 14266.8 | 1.05021e+07 | 15657.8 | 1.46964e+07 | 1428.6 | 1.25993e+07 | 6 | 86496 | 445 | 1.2541e+07 | 240 | 6.31473e+06 | 6896.08 | 1.67936e+07 | 7033.2 | 6.30784e+06 | 5807.41 | 1.67936e+07 | 96416.1 | 5744.67 | 1.88908e+07 | 4003.65 | 1.67936e+07 | 42166 | 837682 | 1.17356e+06 | 8.14881e+06 | 3.18111e+07 | 17253.5 | 52754.9 | 54886.9 | 61431.1 | 4615.1 | 20971.5 | 21889.5 | 17410.2 | 17219.9 | 11532.7 | 2258 | 403 | | 79920 | 20240105.14 | 28090.3 | 2.51822e+07 | 0.804667 | 5642.82 | 8.59996e+07 | 14097.8 | 1.88908e+07 | 14249.7 | 1.05021e+07 | 15643 | 1.46964e+07 | 1426.1 | 1.25993e+07 | 6 | 86496 | 434 | 1.2541e+07 | 235 | 6.31473e+06 | 6883.92 | 1.88908e+07 | 6976.3 | 6.30784e+06 | 5819.57 | 1.67936e+07 | 72389.5 | 5767.4 | 1.67936e+07 | 3983.21 | 1.67936e+07 | 42864.9 | 816929 | 1.18007e+06 | 8.14615e+06 | 3.06564e+07 | 17195.4 | 53484.4 | 56927.5 | 63034.1 | 4635.9 | 20600.9 | 21708 | 20208.9 | 17600.9 | 11868.5 | 2325 | 403 | | 79931 | 20240105.18 | 28155.9 | 2.51822e+07 | 0.830304 | 5572.38 | 8.59996e+07 | 14067.9 | 1.67936e+07 | 14143.9 | 1.05021e+07 | 15609.5 | 1.25993e+07 | 1433 | 1.25993e+07 | 6 | 86496 | 436 | 1.2541e+07 | 236 | 6.31473e+06 | 6844.24 | 1.67936e+07 | 6937.8 | 6.30784e+06 | 5775.62 | 1.67936e+07 | 78451.8 | 5454.13 | 1.67936e+07 | 3990.64 | 1.67936e+07 | 41115.6 | 835630 | 1.17185e+06 | 8.15319e+06 | 3.14385e+07 | 17203.8 | 53081 | 57491.7 | 63657.6 | 4644.3 | 20979.1 | 21753.3 | 20837.9 | 17426.7 | 11781.2 | 2224 | 403 | | 79937 | 20240105.20 | 28053.5 | 2.51822e+07 | 0.788583 | 5577.35 | 8.59996e+07 | 14052.4 | 1.88908e+07 | 14109.9 | 1.05021e+07 | 15547.2 | 1.46964e+07 | 1435.2 | 1.25993e+07 | 6 | 77678 | 366 | 1.14441e+07 | 223 | 5.86578e+06 | 7233.07 | 1.67936e+07 | 6844.1 | 6.30784e+06 | 5802.33 | 1.67936e+07 | 85420.8 | 5491.67 | 1.67936e+07 | 3998.46 | 1.67936e+07 | 47083.7 | 832419 | 1.18053e+06 | 8.15387e+06 | 3.21896e+07 | 17208.8 | 56022.5 | 56925.6 | 63903.6 | 4666.7 | 20742.8 | 21552.2 | 20961.9 | 17614 | 11908.4 | 2256 | 403 | | 79954 | 20240108.2 | 28237 | 2.30851e+07 | 0.811783 | 5591.06 | 8.59996e+07 | 14064.6 | 1.88908e+07 | 14197.4 | 1.05021e+07 | 15540.4 | 1.46964e+07 | 1431.6 | 1.25993e+07 | 6 | 77678 | 393 | 1.14441e+07 | 225 | 5.86578e+06 | 7263.29 | 1.67936e+07 | 7083.5 | 6.30784e+06 | 5819.68 | 1.67936e+07 | 99047.8 | 5772.06 | 1.67936e+07 | 4006.27 | 1.67936e+07 | 41219.2 | 823934 | 1.18456e+06 | 8.13305e+06 | 3.08225e+07 | 17316.8 | 53076.6 | 55248.3 | 60320.6 | 4528.2 | 20993.9 | 21334.7 | 17858.4 | 17621.1 | 11538.3 | 2191 | 403 | | 79961 | 20240108.5 | 27925.4 | 2.51822e+07 | 0.812651 | 5643.13 | 8.59996e+07 | 14080.8 | 1.67936e+07 | 14230.5 | 1.05021e+07 | 15627.5 | 1.25993e+07 | 1428.6 | 1.25993e+07 | 5 | 77678 | 377 | 1.14441e+07 | 219 | 5.86578e+06 | 7265.93 | 1.67936e+07 | 6978.2 | 6.30784e+06 | 5819.84 | 1.67936e+07 | 85416 | 5491.66 | 1.88908e+07 | 3978.52 | 1.67936e+07 | 43913.1 | 834677 | 1.17721e+06 | 8.13573e+06 | 3.1303e+07 | 17247.2 | 53409.5 | 56958 | 63490.4 | 4632.7 | 20797.7 | 22702.5 | 20869.2 | 17815.9 | 11888.8 | 2280 | 403 | | 79989 | 20240108.17 | 28271 | 2.51822e+07 | 0.812918 | 5581.25 | 8.59996e+07 | 14031.6 | 1.67936e+07 | 14136.4 | 1.05021e+07 | 15523.6 | 1.46964e+07 | 1415.9 | 1.25993e+07 | 6 | 77678 | 392 | 1.14441e+07 | 220 | 5.87421e+06 | 7249.22 | 1.67936e+07 | 6933.6 | 6.30784e+06 | 5811.81 | 1.67936e+07 | 78403.9 | 5488.58 | 1.67936e+07 | 3984.32 | 1.67936e+07 | 45321.3 | 831008 | 1.18097e+06 | 8.15374e+06 | 3.08415e+07 | 17262.7 | 52887.3 | 55918.4 | 62745.3 | 4610.5 | 20923.3 | 22286.1 | 20921.3 | 17621.5 | 11740.7 | 2380 | 403 | | 80001 | 20240108.22 | 28214.4 | 2.30851e+07 | 0.786976 | 5635.92 | 8.59996e+07 | 14107 | 1.67936e+07 | 14229 | 1.05021e+07 | 15650.3 | 1.25993e+07 | 1429.2 | 1.05021e+07 | 6 | 77678 | 147 | 3.90715e+06 | 144 | 3.83177e+06 | 7261.71 | 1.67936e+07 | 7084.9 | 6.30784e+06 | 5822.41 | 1.67936e+07 | 82485.2 | 5738.66 | 1.67936e+07 | 3986.1 | 1.67936e+07 | 45877 | 835642 | 1.18258e+06 | 8.17072e+06 | 3.06881e+07 | 17220.1 | 52740.1 | 56590.9 | 62501.5 | 4637.4 | 20710.5 | 21594.5 | 20773 | 17397.2 | 11679.9 | 2749 | 403 | | 80019 | 20240109.2 | 27799.4 | 2.51822e+07 | 0.779573 | 5541.95 | 8.59996e+07 | 13996.1 | 1.88908e+07 | 14114.4 | 1.05021e+07 | 15421.9 | 1.25993e+07 | 1423.3 | 1.25993e+07 | 5 | 77678 | 150 | 3.90715e+06 | 149 | 3.83177e+06 | 6843.67 | 1.67936e+07 | 6964.2 | 6.30784e+06 | 5808.73 | 1.67936e+07 | 92062.2 | 5734.06 | 1.67936e+07 | 4019.09 | 1.67936e+07 | 40846.9 | 840733 | 1.17962e+06 | 8.12931e+06 | 3.06812e+07 | 17676.2 | 53244.4 | 56053.5 | 61572.3 | 4586.7 | 20734.2 | 22425.5 | 17371.7 | 17383.5 | 11766.6 | 2587 | 403 | | 80028 | 20240109.6 | 28077.7 | 2.51822e+07 | 0.773671 | 5668.81 | 8.59996e+07 | 14080.8 | 1.88908e+07 | 14176.2 | 1.05021e+07 | 15684.6 | 1.46964e+07 | 1435.3 | 1.25993e+07 | 5 | 77678 | 150 | 3.90715e+06 | 146 | 3.83177e+06 | 6914.02 | 1.88908e+07 | 7048.5 | 6.30784e+06 | 5802.22 | 1.67936e+07 | 80572.2 | 5766.41 | 1.67936e+07 | 3999.26 | 1.67936e+07 | 43293 | 830215 | 1.18604e+06 | 8.15176e+06 | 3.07125e+07 | 17211.9 | 53026.8 | 58109.1 | 61402.2 | 4691.4 | 20760.8 | 22245 | 20537.9 | 17634 | 11758.4 | 2686 | 403 | generate_scenario_from_trace | build_id | build_number | pi_basic_mt_sgx_cft^ | pi_basic_mt_sgx_cft_mem | Commit latency factor | tpcc_sgx_cft^ | tpcc_sgx_cft_mem | pi_basic_mt_virtual_cft^ | ls_sgx_cft^ | ls_sgx_cft_mem | pi_ls_sgx_cft^ | pi_ls_sgx_cft_mem | pi_basic_sgx_cft^ | pi_basic_sgx_cft_mem | tpcc_virtual_cft^ | ls_virtual_cft^ | pi_ls_virtual_cft^ | pi_basic_virtual_cft^ | pi_basic_js_sgx_cft^ | pi_basic_js_sgx_cft_mem | pi_basic_js_virtual_cft^ | ls_jwt_sgx_cft^ | ls_jwt_sgx_cft_mem | ls_jwt_virtual_cft^ | pi_ls_jwt_sgx_cft^ | pi_ls_jwt_sgx_cft_mem | pi_ls_jwt_virtual_cft^ | ls_js_virtual_cft^ | ls_js_sgx_cft^ | ls_js_sgx_cft_mem | ls_full_js_virtual_cft^ | ls_js_jwt_virtual_cft^ | ls_full_js_sgx_cft^ | ls_full_js_sgx_cft_mem | ls_js_jwt_sgx_cft^ | ls_js_jwt_sgx_cft_mem | hist_sgx_cft^ | tlc_3node_fixed_duration_s | tlc_3node_fixed_states | tlc_atomic_reconfig_duration_s | tlc_atomic_reconfig_states | tlc_reconfig_duration_s | tlc_reconfig_states | RB put (/s)^ | CHAMP put (/s)^ | RB get (/s)^ | CHAMP get (/s)^ | tlc_sim_traces | tlc_sim_levelmean | |-----------:|:---------------|-----------------------:|--------------------------:|------------------------:|----------------:|-------------------:|---------------------------:|--------------:|-----------------:|-----------------:|--------------------:|--------------------:|-----------------------:|--------------------:|------------------:|---------------------:|------------------------:|-----------------------:|--------------------------:|---------------------------:|------------------:|---------------------:|----------------------:|---------------------:|------------------------:|-------------------------:|---------------------:|-----------------:|--------------------:|--------------------------:|-------------------------:|----------------------:|-------------------------:|---------------------:|------------------------:|----------------:|-----------------------------:|-------------------------:|---------------------------------:|-----------------------------:|--------------------------:|----------------------:|---------------:|------------------:|---------------:|------------------:|-----------------:|--------------------:| | 79919 | 20240105.13 | 28238.9 | 2.30851e+07 | 0.798124 | 5634.54 | 8.59996e+07 | 80114.8 | 14074.4 | 1.88908e+07 | 14202.2 | 1.05021e+07 | 15647.1 | 1.46964e+07 | 17313 | 53151.7 | 56966.7 | 62131.2 | 1427.5 | 1.25993e+07 | 4581.5 | 6904.57 | 1.67936e+07 | 21070.3 | 6987.3 | 6.30784e+06 | 21694.3 | 17713.1 | 5772.35 | 1.67936e+07 | 17513.4 | 11580.8 | 5506.77 | 1.88908e+07 | 3977.24 | 1.67936e+07 | 45694.6 | 6 | 86496 | 417 | 1.2541e+07 | 233 | 6.31473e+06 | 839386 | 1.18497e+06 | 8.09825e+06 | 3.06376e+07 | 2410 | 403 | | 79929 | 20240105.17 | 28105.3 | 2.51822e+07 | 0.766809 | 5545.36 | 8.59996e+07 | 70487.8 | 14018.3 | 1.88908e+07 | 14081.6 | 1.05021e+07 | 15383.5 | 1.25993e+07 | 17272.9 | 53390.8 | 56918.1 | 63246.5 | 1407.9 | 1.25993e+07 | 4653.4 | 6817.13 | 1.88908e+07 | 20761.2 | 6939.4 | 6.30784e+06 | 22249.9 | 17534.6 | 5804 | 1.67936e+07 | 17594.4 | 11811.4 | 5450.77 | 1.67936e+07 | 3992.16 | 1.67936e+07 | 43268.3 | 6 | 86496 | 425 | 1.2541e+07 | 242 | 6.31473e+06 | 828911 | 1.17857e+06 | 8.15462e+06 | 3.08411e+07 | 2252 | 403 | | 79946 | 20240105.23 | 28022.7 | 2.51822e+07 | 0.825867 | 5621.3 | 8.59996e+07 | 73753.8 | 14046.5 | 1.88908e+07 | 14150.3 | 1.05021e+07 | 15619.7 | 1.25993e+07 | 17254.9 | 53370.7 | 57023.6 | 63387.7 | 1422.3 | 1.25993e+07 | 4555.2 | 6845.02 | 1.88908e+07 | 20629.5 | 6969.7 | 6.30784e+06 | 22253.9 | 20899.5 | 5814.19 | 1.67936e+07 | 17557 | 11864.7 | 5749.76 | 1.88908e+07 | 3971.43 | 1.67936e+07 | 45159.3 | 6 | 77678 | 388 | 1.14441e+07 | 221 | 5.86578e+06 | 826262 | 1.17621e+06 | 8.13955e+06 | 3.06931e+07 | 2238 | 403 | | 80033 | 20240109.7 | 27995.2 | 2.30851e+07 | 0.769708 | 5538.05 | 8.59996e+07 | 72286 | 14038 | 1.88908e+07 | 14217.6 | 1.05021e+07 | 15581.7 | 1.46964e+07 | 17249.2 | 53175.5 | 56923.3 | 62806.2 | 1433.5 | 1.25993e+07 | 4634.1 | 7245.92 | 1.67936e+07 | 20684.6 | 6984.1 | 6.30784e+06 | 22287.1 | 17434.1 | 5802.15 | 1.67936e+07 | 17557.5 | 11741.9 | 5692.2 | 1.67936e+07 | 3985.28 | 1.67936e+07 | 45856 | 6 | 77678 | 149 | 3.90715e+06 | 146 | 3.83177e+06 | 827060 | 1.17824e+06 | 8.15764e+06 | 3.06147e+07 | 2685 | 403 |

images

lemmy commented 5 months ago

Some discoveries:

Node with TLA+ state "None" never created in scenario causing core dump when, e.g., asserting its state

Driver log ```shell root@codespaces-a47fa6:/workspaces/CCF/tests/raft_scenarios# ../../build/raft_driver MCccfraftAtomicReconfig 2023-12-19T21:59:35.734666Z 100 [info ][raft] ./src/consensus/aft/raft.h:491 | n[n1] | None | Active | Election timer has become active 2023-12-19T21:59:35.734735Z 100 [debug][raft] /src/consensus/aft/raft.h:1820 | n[n1] | None | Active | Election index is 0 in term 2 n[n1]->>n[n1]: [KV] initialising in term 2 2023-12-19T21:59:35.734754Z 100 [info ][raft] /src/consensus/aft/raft.h:1844 | n[n1] | Leader | Active | Becoming leader n[n1]: 2 2023-12-19T21:59:35.734761Z 100 [debug][raft] /src/consensus/aft/raft.h:2185 | n[n1] | Leader | Active | Starting commit n[n1]->>n[n1]: replicate 2.1 = [0 bytes] [reconfiguration] 2023-12-19T21:59:35.735182Z 100 [debug][raft] ./src/consensus/aft/raft.h:567 | n[n1] | Leader | Active | Replicating 1 entries 2023-12-19T21:59:35.735193Z 100 [debug][raft] ./src/consensus/aft/raft.h:591 | n[n1] | Leader | Active | Replicated on leader n[n1]: 1 (1 hooks) 2023-12-19T21:59:35.735199Z 100 [debug][raft] ./src/consensus/aft/raft.h:451 | n[n1] | Leader | Active | Configurations: add new configuration at 1: {{n[n1]}} n[n1]->>n[n1]: [ledger] appending: 2.1=[68 bytes] {"data":"eyJuMS 2023-12-19T21:59:35.735209Z 100 [debug] ../src/consensus/aft/impl/state.h:39 | Updating view to: 2 at version: 1 2023-12-19T21:59:35.735214Z 100 [debug] ../src/consensus/aft/impl/state.h:56 | Resulting views: 1, 1 Note over n1: Node n1 created n[n1]->>n[n1]: replicate 2.2 = [9 bytes] signature [raw] 2023-12-19T21:59:35.735237Z 100 [debug][raft] ./src/consensus/aft/raft.h:567 | n[n1] | Leader | Active | Replicating 1 entries 2023-12-19T21:59:35.735244Z 100 [debug][raft] ./src/consensus/aft/raft.h:591 | n[n1] | Leader | Active | Replicated on leader n[n1]: 2 committable (0 hooks) 2023-12-19T21:59:35.735249Z 100 [debug][raft] ./src/consensus/aft/raft.h:613 | n[n1] | Leader | Active | membership: Active leadership: Leader n[n1]->>n[n1]: [ledger] appending: 2.2=[36 bytes] {"data":"c2lnbm 2023-12-19T21:59:35.735260Z 100 [debug] ../src/consensus/aft/impl/state.h:39 | Updating view to: 2 at version: 2 2023-12-19T21:59:35.735264Z 100 [debug] ../src/consensus/aft/impl/state.h:56 | Resulting views: 1, 1 2023-12-19T21:59:35.735269Z 100 [debug][raft] /src/consensus/aft/raft.h:2128 | n[n1] | Leader | Active | In update_commit, new_commit_idx: 2, last_idx: 2 2023-12-19T21:59:35.735274Z 100 [debug][raft] /src/consensus/aft/raft.h:2185 | n[n1] | Leader | Active | Starting commit 2023-12-19T21:59:35.735279Z 100 [debug][raft] /src/consensus/aft/raft.h:2203 | n[n1] | Leader | Active | Compacting... n[n1]->>n[n1]: [KV] compacting to 2 2023-12-19T21:59:35.735288Z 100 [debug][raft] /src/consensus/aft/raft.h:2207 | n[n1] | Leader | Active | Commit on n[n1]: 2 n[n1]->>n[n1]: replicate 2.3 = [2 bytes] 42 [raw] 2023-12-19T21:59:35.735303Z 100 [debug][raft] ./src/consensus/aft/raft.h:567 | n[n1] | Leader | Active | Replicating 1 entries 2023-12-19T21:59:35.735308Z 100 [debug][raft] ./src/consensus/aft/raft.h:591 | n[n1] | Leader | Active | Replicated on leader n[n1]: 3 (0 hooks) n[n1]->>n[n1]: [ledger] appending: 2.3=[28 bytes] {"data":"NDI=", 2023-12-19T21:59:35.735318Z 100 [debug] ../src/consensus/aft/impl/state.h:39 | Updating view to: 2 at version: 3 2023-12-19T21:59:35.735322Z 100 [debug] ../src/consensus/aft/impl/state.h:56 | Resulting views: 1, 1 libc++abi: terminating due to uncaught exception of type std::out_of_range: map::at: key not found Aborted (core dumped) ```
TLA Trace ```tla Error: Invariant LogMatchingInv is violated. Error: The behavior up to this point is: State 1: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 0) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>> @@ n2 :> <<>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<>>) State 2: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 0) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<>>) State 3: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 2, dest |-> n2, source |-> n1, term |-> 2, type |-> AppendEntriesRequest, prevLogIndex |-> 0, prevLogTerm |-> 2, entries |-> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}]>>]>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 0) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<>>) State 4: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 2, dest |-> n2, source |-> n1, term |-> 2, type |-> AppendEntriesRequest, prevLogIndex |-> 0, prevLogTerm |-> 2, entries |-> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}]>>]>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> << >>) State 5: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<[dest |-> n1, source |-> n2, term |-> 2, type |-> AppendEntriesResponse, success |-> TRUE, lastLogIndex |-> 1]>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}]>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 6: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 2) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}]>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 7: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 2, dest |-> n2, source |-> n1, term |-> 2, type |-> AppendEntriesRequest, prevLogIndex |-> 1, prevLogTerm |-> 2, entries |-> <<[contentType |-> Signature, term |-> 2]>>]>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}]>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 8: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 2) /\ messages = (n1 :> <<[dest |-> n1, source |-> n2, term |-> 2, type |-> AppendEntriesResponse, success |-> TRUE, lastLogIndex |-> 2]>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 9: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 2) /\ messages = (n1 :> <<>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 10: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 4) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 2) /\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 2, dest |-> n2, source |-> n1, term |-> 2, type |-> AppendEntriesRequest, prevLogIndex |-> 2, prevLogTerm |-> 2, entries |-> <<[contentType |-> Entry, term |-> 2, request |-> 42]>>]>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 11: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Follower @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 4) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 2) /\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 2, dest |-> n2, source |-> n1, term |-> 2, type |-> AppendEntriesRequest, prevLogIndex |-> 2, prevLogTerm |-> 2, entries |-> <<[contentType |-> Entry, term |-> 2, request |-> 42]>>]>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>>) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 12: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Candidate @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> n1 @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 4) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 2) /\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 2, dest |-> n2, source |-> n1, term |-> 2, type |-> AppendEntriesRequest, prevLogIndex |-> 2, prevLogTerm |-> 2, entries |-> <<[contentType |-> Entry, term |-> 2, request |-> 42]>>]>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>>) /\ votesGranted = (n1 :> {n1} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 13: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> n1 @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 3 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 2) /\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 2, dest |-> n2, source |-> n1, term |-> 2, type |-> AppendEntriesRequest, prevLogIndex |-> 2, prevLogTerm |-> 2, entries |-> <<[contentType |-> Entry, term |-> 2, request |-> 42]>>]>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>>) /\ votesGranted = (n1 :> {n1} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<{n1}>>) State 14: /\ reconfigurationCount = 1 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {n1} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> n1 @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 3 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 2) /\ messages = (n1 :> <<>> @@ n2 :> <<[commitIndex |-> 2, dest |-> n2, source |-> n1, term |-> 2, type |-> AppendEntriesRequest, prevLogIndex |-> 2, prevLogTerm |-> 2, entries |-> <<[contentType |-> Entry, term |-> 2, request |-> 42]>>]>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Reconfiguration, term |-> 2, configuration |-> {n2}]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2]>>) /\ votesGranted = (n1 :> {n1} @@ n2 :> {}) /\ configurations = (n1 :> (1 :> {n1} @@ 3 :> {n2}) @@ n2 :> <<{n1}>>) State 15: /\ reconfigurationCount = 1 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {n1} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> n1 @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 3 @@ n2 :> 3) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 2) /\ messages = (n1 :> <<[dest |-> n1, source |-> n2, term |-> 2, type |-> AppendEntriesResponse, success |-> TRUE, lastLogIndex |-> 3]>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 2) /\ log = (n1 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Reconfiguration, term |-> 2, configuration |-> {n2}]>> @@ n2 :> <<[contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42]>>) /\ votesGranted = (n1 :> {n1} @@ n2 :> {}) /\ configurations = (n1 :> (1 :> {n1} @@ 3 :> {n2}) @@ n2 :> <<{n1}>>) ```
Driver scenario ``` start_node,n1 emit_signature,2 # MCClientRequest MCccfraft:65 replicate,2,42 assert_commit_idx,n1,2 # AppendEntries ccfraft:551 dispatch_all assert_commit_idx,n1,2 # RcvUpdateTerm ccfraft:997 # Noop assert_commit_idx,n1,2 # RcvAppendEntriesRequest ccfraft:1016 # Noop assert_commit_idx,n1,2 # RcvDropIgnoredMessage ccfraft:990 # Noop assert_commit_idx,n1,2 # AppendEntries ccfraft:551 dispatch_all assert_commit_idx,n1,2 # RcvAppendEntriesRequest ccfraft:1016 # Noop assert_commit_idx,n1,2 ### assert below causes code dump because n2 doesn't exist. assert_commit_idx,n2,2 # RcvDropIgnoredMessage ccfraft:990 # Noop assert_commit_idx,n1,2 assert_commit_idx,n2,2 # AppendEntries ccfraft:551 dispatch_all assert_commit_idx,n1,2 assert_commit_idx,n2,2 # CheckQuorum ccfraft:723 periodic_one,n1,110 assert_commit_idx,n1,2 assert_commit_idx,n2,2 # MCTimeout MCccfraft:49 periodic_one,n1,110 assert_commit_idx,n1,2 assert_commit_idx,n2,2 # BecomeLeader ccfraft:585 # Noop assert_commit_idx,n1,2 assert_commit_idx,n2,2 # ChangeConfiguration ccfraft:660 # Noop assert_commit_idx,n1,2 assert_commit_idx,n2,2 # RcvAppendEntriesRequest ccfraft:1016 # Noop assert_commit_idx,n1,2 assert_commit_idx,n2,2 ```
achamayou commented 5 months ago

@lemmy apologies for editing the comment, but adding the collapsible blocks makes the PR much more readable.

The first issue is that the mapping ignores ChangeConfiguration, because the (unreasonably optimistic) expectation was that it would translate ChangeConfigurationInt instead, given that:

    \E newConfiguration \in SUBSET(Servers \ removedFromConfiguration) :
        ChangeConfigurationInt(i, newConfiguration)

But ChangeConfigurationInt doesn't seem to make it to the trace, I guess because it's a function called by the action and not the action itself. That's annoying, because logging ChangeConfiguration alone and its parameter i is obviously insufficient. I guess we need to diff the pre and post states to find the new configuration in this case.

The second issue is that we should use trust_node, rather than replicate_new_configuration, since that does the creation and trusting, that's my mistake.

The third issue is that this performing complete replacement, not just a node addition, and that we don't have good way to do that in the driver now.

achamayou commented 5 months ago

Found another mismatch, before even getting to the reconfig:

TLA Trace ``` Finished computing initial states: 1 distinct state generated at 2023-12-20 11:36:46. Error: Invariant LogMatchingInv is violated. Error: The behavior up to this point is: State 1: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 0) /\ log = ( n1 :> << [contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2] >> @@ n2 :> <<>> ) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<>>) State 2: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 0) /\ log = ( n1 :> << [contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42] >> @@ n2 :> <<>> ) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<>>) State 3: /\ reconfigurationCount = 0 /\ committableIndices = (n1 :> {4} @@ n2 :> {}) /\ removedFromConfiguration = {} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) /\ messages = (n1 :> <<>> @@ n2 :> <<>>) /\ currentTerm = (n1 :> 2 @@ n2 :> 0) /\ log = ( n1 :> << [contentType |-> Reconfiguration, term |-> 2, configuration |-> {n1}], [contentType |-> Signature, term |-> 2], [contentType |-> Entry, term |-> 2, request |-> 42], [contentType |-> Signature, term |-> 2] >> @@ n2 :> <<>> ) /\ votesGranted = (n1 :> {} @@ n2 :> {}) /\ configurations = (n1 :> <<{n1}>> @@ n2 :> <<>>) State 4: /\ reconfigurationCount = 1 /\ committableIndices = (n1 :> {4} @@ n2 :> {}) /\ removedFromConfiguration = {n1} /\ state = (n1 :> Leader @@ n2 :> None) /\ matchIndex = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0)) /\ votedFor = (n1 :> Nil @@ n2 :> Nil) /\ nextIndex = (n1 :> (n1 :> 1 @@ n2 :> 1) @@ n2 :> (n1 :> 1 @@ n2 :> 1)) /\ commitIndex = (n1 :> 2 @@ n2 :> 0) ```

The generated assert for the end of state 4 is for commit index 2 on n1:

start_node,n1
emit_signature,2
# MCClientRequest MCccfraft:65
replicate,2,42
assert_commit_idx,n1,2
# MCSignCommittableMessages MCccfraft:73
emit_signature,2
assert_commit_idx,n1,2

But it is 4 in the implementation, since 4 is committable and the whole config ({n1}) is aware. Which now that I think about is exactly what #5798 uncovered.

achamayou commented 5 months ago

@lemmy I've fixed reconfiguration by tweaking replicate_new_configuration to create nodes when they are missing rather than throw, and added logic that fetches the last config for the node from the post state. That seems work ok on a scenario similar to the one you pasted, but the issue with commit asserts remains, since the spec just behaves differently.

lemmy commented 5 months ago

Trace > execution > trace - spec to code and back :-)

1) Simulate SIMccfraft 2) Convert with trace2scen.py 3) Feed into ~raft_driver~ raft_scenarios_runner.py (former no longer produces ndjsons that can be fed into Traceccfraft, compare https://github.com/microsoft/CCF/commit/a6384ef20f7ff46aa96254c9d208d00ceb830f12#r135809467 and https://github.com/microsoft/CCF/commit/7230570efe3986ce4d93e945b062d1459aa47a37#r135808748) 4) Dump raft_trace to ndjson 5) Feed into Traceccfraft

root@codespaces-a47fa6:/workspaces/CCF/tla/consensus# TS=$(date +%s) && \
../tlc.sh -note SIMccfraft.tla -simulate num=1 -dumptrace json SIMccfraft-$TS.json > SIMccfraft-$TS.out ; \
python3 ../trace2scen.py SIMccfraft-$TS.json > SIMccfraft-$TS.rt ; \ 
python3 ../raft_scenarios_runner.py ../../build/raft_driver SIMccfraft-$TS.rt | tee >(grep '"tag":"raft_trace"' > SIMccraft-$TS.ndjson) && \
JSON=SIMccraft-$TS.ndjson ../tlc.sh -note Traceccfraft.tla
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index b920aaba8..e4375a917 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -90,3 +90,4 @@ INVARIANTS
     \* DebugInvSuccessfulCommitAfterReconfig
     \* DebugInvAllMessagesProcessable
     \* DebugInvRetirementReachable
+    DebugUpToDepth
diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
index bfacc4e7f..e14af7924 100644
--- a/tla/consensus/SIMccfraft.tla
+++ b/tla/consensus/SIMccfraft.tla
@@ -39,7 +39,7 @@ SIMNext ==
           [] OTHER -> IF ENABLED Forward THEN Forward ELSE Next

 SIMSpec ==
-    Init /\ [][SIMNext]_vars
+    Init /\ [][Next]_vars \* Next and not SIMNext to get proper action names & params.

 \* The state constraint  StopAfter  stops TLC after the alloted
 \* time budget is up, unless TLC encounteres an error first.
@@ -48,6 +48,8 @@ StopAfter ==
     (* The smoke test has a time budget of 20 minutes. *)
     IN TLCSet("exit", TLCGet("duration") > timeout)

+DebugUpToDepth ==
+    TLCGet("level") < TLCGet("config").depth
 =============================================================================
 ------------------------------- MODULE SIMPostCondition -------------------------------
diff --git a/tla/trace2scen.py b/tla/trace2scen.py
index d4e9ddb66..2811a5c09 100644
--- a/tla/trace2scen.py
+++ b/tla/trace2scen.py
@@ -32,6 +32,12 @@ MAP = {
     "RejectAppendEntriesRequest": lambda _, __, ___: ["# Noop"],
     "ReturnToFollowerState": lambda _, __, ___: ["# Noop"],
     "AppendEntriesAlreadyDone": lambda _, __, ___: ["# Noop"],
+    "RcvUpdateTerm": lambda _, __, ___: ["# Noop"],
+    "RcvAppendEntriesRequest": lambda _, __, ___: ["# Noop"],
+    "RcvAppendEntriesResponse": lambda _, __, ___: ["# Noop"],
+    "RcvDropIgnoredMessage": lambda _, __, ___: ["# Noop"],
+    "RcvRequestVoteRequest": lambda _, __, ___: ["# Noop"],
+    "RcvRequestVoteResponse": lambda _, __, ___: ["# Noop"],
 }

 def post_commit(post):
lemmy commented 5 months ago

The first issue is that the mapping ignores ChangeConfiguration, because the (unreasonably optimistic) expectation was that it would translate ChangeConfigurationInt instead, given that:

    \E newConfiguration \in SUBSET(Servers \ removedFromConfiguration) :
        ChangeConfigurationInt(i, newConfiguration)

But ChangeConfigurationInt doesn't seem to make it to the trace, I guess because it's a function called by the action and not the action itself. That's annoying, because logging ChangeConfiguration alone and its parameter i is obviously insufficient. I guess we need to diff the pre and post states to find the new configuration in this case.

This (syntactic) change (now part of https://github.com/microsoft/CCF/pull/5880) causes ChangeConfigurationInt with parameters i and newConfiguration to be included in the trace.

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index 7d5fae84c..af1eefd69 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -635,6 +635,8 @@ SignCommittableMessages(i) ==
 ChangeConfigurationInt(i, newConfiguration) ==
     \* Only leader can propose changes
     /\ state[i] = Leader
+    \* Configuration is not a previously removed configuration.
+    /\ newConfiguration \notin removedFromConfiguration
     \* Configuration is non empty
     /\ newConfiguration /= {}
     \* Configuration is a proper subset of the Servers
@@ -657,7 +659,7 @@ ChangeConfigurationInt(i, newConfiguration) ==
                     leaderVars, commitIndex, committableIndices>>

 ChangeConfiguration(i) ==
-    \E newConfiguration \in SUBSET(Servers \ removedFromConfiguration) :
+    \E newConfiguration \in SUBSET(Servers) :
         ChangeConfigurationInt(i, newConfiguration)

 \* Leader i advances its commitIndex to the next possible Index.
lemmy commented 5 months ago

What are the use cases for lockstep debugging (ccfraft.tla > raft.h > Traececcfraft.tla) of the spec and the impl (via raft_driver)?

It appears as if a main benefit of co-debugging/lockstep debugging is locked away by the fact that the driver cannot reverse the impl. Otherwise, one could interactively explore the state space at every state of a behavior.

Technical considerations

1) Emit the next raft scenario command a) When generating a complete scenario from a TLA+ trace b) One by one when creating a TLA+ trace with e.g. the TLA+ debugger 2) Validate the resulting json output a) With Traceccfraft.tla after the json log has been serialized b) Interactively, when moving to the next state with e.g. the TLA+ debugger

"Batch" is trivial: Write trace and print raft scenario command with an Alias or a (Python) script. Verify the json output with existing Traceccfraft.tla. Interactive is more challenging: Emit 1b) with TLCDefer as part of the next-state relation, and verify 2b in an action-constraint.

TLA+/TLC infra
achamayou commented 4 months ago

@lemmy thank you for making the change in #5880, I've update the conversion, and also added the missing actions you spotted when running the sim. It's a little annoying that the default SIM traces don't work, and that changing the Next is necessary, but the improved coverage is desirable.

(Question: How do we debug multiple nodes with raft_driver?)

raft_driver is single threaded, nodes are separate objects but all execution is serialised.

It appears as if a main benefit of co-debugging/lockstep debugging is locked away by the fact that the driver cannot reverse the impl.

Agreed, though as discussed before the new year, making the driver able to reverse the state of each node is probably achievable: nearly all of it already supports trivial json ser/deser. We would also need to put the messages back on the queues, and restore time elapsed. I don't know that we want to go much further before we complete #5822 at least.

For now, the intermediate result this gives us is: "A validation trace can (mostly) be fed back to the driver for investigation".

eddyashton commented 4 months ago

Can we get traces from the existing (matching) scenarios, and see what scenarios this generates from them?

lemmy commented 4 months ago

Can we get traces from the existing (matching) scenarios, and see what scenarios this generates from them?

We have only two scenarios compatible with the new bootstrapping logic. @achamayou does it make sense to port all deprecated scenarios?

achamayou commented 4 months ago

Can we get traces from the existing (matching) scenarios, and see what scenarios this generates from them?

We have only two scenarios compatible with the new bootstrapping logic. @achamayou does it make sense to port all deprecated scenarios?

I've been trying to do that (#5839), but have not found enough time so far.

The traces won't match, because all information related to message dispatch and periodic/time elapsed is lost right now. I don't think we can get them to match without substantially reworking either the spec or the driver, as discussed.