search

microsoft / CCF

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

[DO_NOT_MERGE] Investigate rollback_safety scenario trace #6000

Closed heidihoward closed 3 months ago

heidihoward commented 4 months ago

Using the CI to test trace validation and spec.

This PR is not for merging, just for experimenting with

ccf-bot commented 4 months ago

tla-rollback@81745 aka 20240212.42 vs main ewma over 20 builds from 81376 to 81732

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 | pi_basic_mt_virtual_cft^ | ls_jwt_sgx_cft^ | ls_jwt_sgx_cft_mem | tpcc_virtual_cft^ | pi_ls_jwt_sgx_cft^ | pi_ls_jwt_sgx_cft_mem | ls_virtual_cft^ | ls_js_sgx_cft^ | ls_js_sgx_cft_mem | pi_ls_virtual_cft^ | pi_basic_virtual_cft^ | ls_full_js_sgx_cft^ | ls_full_js_sgx_cft_mem | pi_basic_js_virtual_cft^ | ls_jwt_virtual_cft^ | ls_js_jwt_sgx_cft^ | ls_js_jwt_sgx_cft_mem | pi_ls_jwt_virtual_cft^ | ls_js_virtual_cft^ | ls_full_js_virtual_cft^ | ls_js_jwt_virtual_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 | hist_sgx_cft^ | RB put (/s)^ | CHAMP put (/s)^ | RB get (/s)^ | CHAMP get (/s)^ | tlc_sim_traces | tlc_sim_levelmean | |-----------:|:---------------|-----------------------:|--------------------------:|------------------------:|----------------:|-------------------:|--------------:|-----------------:|-----------------:|--------------------:|--------------------:|-----------------------:|-----------------------:|--------------------------:|---------------------------:|------------------:|---------------------:|--------------------:|---------------------:|------------------------:|------------------:|-----------------:|--------------------:|---------------------:|------------------------:|----------------------:|-------------------------:|---------------------------:|----------------------:|---------------------:|------------------------:|-------------------------:|---------------------:|--------------------------:|-------------------------:|-----------------------------:|-------------------------:|---------------------------------:|-----------------------------:|--------------------------:|----------------------:|----------------:|---------------:|------------------:|---------------:|------------------:|-----------------:|--------------------:| | 81376 | 20240207.5 | 28211.8 | 2.30851e+07 | 0.791487 | 5680.25 | 8.59996e+07 | 14052.1 | 1.88908e+07 | 14207.2 | 1.05021e+07 | 15675.8 | 1.25993e+07 | 1421.9 | 1.05021e+07 | 85830.9 | 7251.18 | 1.67936e+07 | 17347.4 | 6975.1 | 6.30784e+06 | 52775.6 | 5811.57 | 1.67936e+07 | 55089.1 | 62099.1 | 5487.37 | 1.88908e+07 | 4612 | 17330.1 | 3993.07 | 1.67936e+07 | 22048.3 | 20947.4 | 17341 | 11623.1 | 6 | 58806 | 168 | 4.51944e+06 | 582 | 1.35909e+07 | 42785.6 | 835691 | 1.17803e+06 | 8.13728e+06 | 2.98808e+07 | 48517 | 364 | | 81388 | 20240207.10 | 28441.1 | 2.30851e+07 | 0.771777 | 5612.01 | 8.59996e+07 | 14032.1 | 1.88908e+07 | 14116.1 | 1.05021e+07 | 15510.3 | 1.25993e+07 | 1422.3 | 1.25993e+07 | 70198.7 | 7233.78 | 1.67936e+07 | 17381.6 | 6970.9 | 6.30784e+06 | 53076.5 | 5775.18 | 1.67936e+07 | 56751.8 | 63721 | 5492.31 | 1.88908e+07 | 4678 | 20791.8 | 4002.9 | 1.67936e+07 | 21540.1 | 20957.3 | 17644.2 | 11590.4 | 5 | 58806 | 169 | 4.51944e+06 | 595 | 1.35909e+07 | 41551.8 | 837741 | 1.17943e+06 | 8.15098e+06 | 2.99196e+07 | 45698 | 358 | | 81400 | 20240207.13 | 27822.7 | 2.51822e+07 | 0.812168 | 5585.19 | 8.59996e+07 | 14068.6 | 1.88908e+07 | 14189.4 | 1.05021e+07 | 15544.2 | 1.46964e+07 | 1424.2 | 1.25993e+07 | 97187.8 | 6831.28 | 1.67936e+07 | 17350 | 6999.8 | 6.30784e+06 | 53253.6 | 5761.96 | 1.67936e+07 | 40909.5 | 63247.9 | 5474.09 | 1.67936e+07 | 4631.4 | 20653.5 | 3975.61 | 1.67936e+07 | 21669.9 | 20829.5 | 17703.5 | 11779.8 | 5 | 58806 | 173 | 4.51944e+06 | 579 | 1.35909e+07 | 40590 | 837373 | 1.18078e+06 | 8.15335e+06 | 3.07355e+07 | 47186 | 365 | | 81420 | 20240207.21 | 28256.8 | 2.51822e+07 | 0.810953 | 5571.71 | 8.59996e+07 | 13922.8 | 1.88908e+07 | 14066.6 | 1.05021e+07 | 15416.2 | 1.25993e+07 | 1414.9 | 1.25993e+07 | 79777.7 | 6780.36 | 1.67936e+07 | 17348.7 | 6913 | 6.30784e+06 | 52915 | 5792.24 | 1.67936e+07 | 55585.5 | 61723.5 | 5470.7 | 1.67936e+07 | 4573.2 | 20916.3 | 3988.75 | 1.67936e+07 | 20913.5 | 17651.7 | 17537.1 | 11804.6 | 5 | 58806 | 170 | 4.51944e+06 | 570 | 1.35909e+07 | 44411.9 | 834582 | 1.17672e+06 | 8.16457e+06 | 3.22606e+07 | 50234 | 367 | | 81432 | 20240207.25 | 28119.6 | 2.30851e+07 | 0.817283 | 5604.06 | 8.59996e+07 | 14018.8 | 1.88908e+07 | 14116.5 | 1.05021e+07 | 15455.6 | 1.46964e+07 | 1423 | 1.25993e+07 | 86989.4 | 7225.51 | 1.67936e+07 | 17558.4 | 7033.4 | 6.30784e+06 | 52895.7 | 5788.32 | 1.67936e+07 | 57094.2 | 58429.2 | 5731.38 | 1.67936e+07 | 4650.2 | 20646.2 | 3986.82 | 1.67936e+07 | 21122.4 | 21111.7 | 17157.2 | 11781.4 | 5 | 58806 | 183 | 4.51944e+06 | 593 | 1.35909e+07 | 46349.7 | 831735 | 1.18525e+06 | 8.16988e+06 | 3.08675e+07 | 48635 | 350 | | 81443 | 20240207.28 | 28277.5 | 2.30851e+07 | 0.817474 | 5607.24 | 8.59996e+07 | 14120.8 | 1.88908e+07 | 14198 | 1.05021e+07 | 15725.1 | 1.25993e+07 | 1441.1 | 1.25993e+07 | 81171.2 | 7286.81 | 1.67936e+07 | 17368.1 | 7135.2 | 6.30784e+06 | 53022 | 5808.89 | 1.67936e+07 | 56457 | 61659.1 | 5488.21 | 1.67936e+07 | 4659 | 20769.5 | 4027.72 | 1.67936e+07 | 21685.9 | 20803.2 | 17144.8 | 11819.6 | 5 | 58806 | 179 | 4.51944e+06 | 594 | 1.35909e+07 | 45582.8 | 823538 | 1.18268e+06 | 8.15183e+06 | 3.07604e+07 | 48414 | 357 | | 81455 | 20240208.2 | 27620.3 | 2.51822e+07 | 0.797625 | 5626.27 | 8.59996e+07 | 13998.7 | 1.88908e+07 | 14136.4 | 1.05021e+07 | 15579.9 | 1.46964e+07 | 1424.9 | 1.25993e+07 | 91792.7 | 7240.3 | 1.67936e+07 | 17387.3 | 6933 | 6.30784e+06 | 53091 | 5813.42 | 1.67936e+07 | 56697.4 | 62610.8 | 5489.97 | 1.88908e+07 | 4662.4 | 20614.6 | 4004.5 | 1.67936e+07 | 21368.4 | 21110.6 | 17584.8 | 11896.8 | 5 | 58806 | 167 | 4.51944e+06 | 587 | 1.35909e+07 | 43546.4 | 829074 | 1.17826e+06 | 8.15069e+06 | 3.07984e+07 | 47195 | 355 | | 81514 | 20240209.2 | 27915.8 | 2.30851e+07 | 0.776241 | 5593.91 | 8.59996e+07 | 14026.5 | 1.88908e+07 | 14133.8 | 1.05021e+07 | 15540.4 | 1.46964e+07 | 1426.1 | 1.25993e+07 | 72910.1 | 7164.29 | 1.88908e+07 | 17718 | 6921.7 | 6.30784e+06 | 50341.4 | 5809.57 | 1.67936e+07 | 55334.2 | 60836.6 | 5717.61 | 1.67936e+07 | 4579.1 | 17438.6 | 3996.31 | 1.67936e+07 | 20394 | 17584.3 | 17663.8 | 11789 | 5 | 58806 | 167 | 4.51944e+06 | 593 | 1.35909e+07 | 44280.1 | 828205 | 1.18317e+06 | 8.16786e+06 | 3.05914e+07 | 48370 | 365 | | 81524 | 20240209.6 | 27841.5 | 2.30851e+07 | 0.785246 | 5588.44 | 8.59996e+07 | 14055.4 | 1.88908e+07 | 14143.5 | 1.05021e+07 | 15566 | 1.46964e+07 | 1434.6 | 1.25993e+07 | 82497.2 | 6840.11 | 1.67936e+07 | 17370 | 7000 | 6.30784e+06 | 52802.6 | 5763.14 | 1.67936e+07 | 56617.1 | 62607.7 | 5491.76 | 1.67936e+07 | 4674.2 | 20877 | 4001.25 | 1.67936e+07 | 21858.9 | 20885.8 | 17550.7 | 11763 | 5 | 58806 | 169 | 4.51944e+06 | 587 | 1.35909e+07 | 43473.1 | 794017 | 1.17937e+06 | 8.17278e+06 | 3.07521e+07 | 49224 | 358 | | 81561 | 20240209.23 | 27876.8 | 2.51822e+07 | 0.790662 | 5579.62 | 8.59996e+07 | 13967 | 1.88908e+07 | 14066.5 | 1.05021e+07 | 15414.3 | 1.46964e+07 | 1408.4 | 1.25993e+07 | 75631.5 | 6813.33 | 1.88908e+07 | 17279.6 | 7075.3 | 6.30784e+06 | 52987.3 | 5804.07 | 1.67936e+07 | 57504.3 | 64054.3 | 5486.4 | 1.67936e+07 | 4663.1 | 20647.3 | 3987.03 | 1.67936e+07 | 22271.2 | 21189.6 | 17251.3 | 11953.5 | 5 | 58806 | 162 | 4.51944e+06 | 586 | 1.35909e+07 | 41939 | 844858 | 1.18032e+06 | 8.1516e+06 | 3.07637e+07 | 49194 | 365 | | 81577 | 20240209.30 | 27926.6 | 2.51822e+07 | 0.792208 | 5517.59 | 8.59996e+07 | 13931.4 | 1.88908e+07 | 14068.5 | 1.05021e+07 | 15544 | 1.46964e+07 | 1431.8 | 1.25993e+07 | 91337.3 | 6812.35 | 1.67936e+07 | 17378.6 | 7075.4 | 6.30784e+06 | 52955.1 | 5798.39 | 1.67936e+07 | 56362.5 | 63073.6 | 5460.63 | 1.88908e+07 | 4636.2 | 20980.9 | 3989.7 | 1.67936e+07 | 21848.8 | 21120.8 | 17165 | 11887.6 | 5 | 58806 | 161 | 4.51944e+06 | 581 | 1.35909e+07 | 43377.2 | 835433 | 1.17712e+06 | 8.13777e+06 | 3.04187e+07 | 48345 | 370 | | 81588 | 20240209.34 | 27783.9 | 2.51822e+07 | 0.830906 | 5520.06 | 8.59996e+07 | 13869 | 1.88908e+07 | 13977.9 | 1.05021e+07 | 15372.5 | 1.25993e+07 | 1408.9 | 1.25993e+07 | 84671.7 | 6816.62 | 1.88908e+07 | 17245.8 | 6962.7 | 6.30784e+06 | 53028.8 | 5784.1 | 1.67936e+07 | 56264.2 | 62934.2 | 5484.41 | 1.67936e+07 | 4685.4 | 21123.2 | 3989.14 | 1.67936e+07 | 22161.2 | 21162.9 | 17088.9 | 11961.3 | 5 | 58806 | 165 | 4.51944e+06 | 588 | 1.35909e+07 | 45314.8 | 837366 | 1.18439e+06 | 8.14836e+06 | 3.16994e+07 | 48276 | 359 | | 81604 | 20240209.41 | 28074.3 | 2.51822e+07 | 0.79632 | 5551.8 | 8.59996e+07 | 13920.2 | 1.88908e+07 | 13961.2 | 1.05021e+07 | 15398.2 | 1.25993e+07 | 1421.3 | 1.25993e+07 | 88382.6 | 6838.29 | 1.88908e+07 | 17303.4 | 6911.4 | 6.30784e+06 | 52951.3 | 5794.24 | 1.67936e+07 | 55245.3 | 61054.2 | 5450.49 | 1.67936e+07 | 4642.2 | 20910.8 | 3997.32 | 1.67936e+07 | 21428 | 17599.7 | 17384.9 | 11838.7 | 5 | 58806 | 276 | 6.79836e+06 | 870 | 1.90055e+07 | 44378.6 | 826462 | 1.17607e+06 | 8.12853e+06 | 3.07222e+07 | 46394 | 360 | | 81610 | 20240209.43 | 28113.5 | 2.51822e+07 | 0.831113 | 5452.05 | 8.59996e+07 | 13971.3 | 1.88908e+07 | 14055.1 | 1.05021e+07 | 15316.7 | 1.46964e+07 | 1411.3 | 1.25993e+07 | 74800.8 | 6769.48 | 1.67936e+07 | 17312.9 | 6829.1 | 6.30784e+06 | 53334.8 | 5785.06 | 1.67936e+07 | 56377.1 | 63345.5 | 5431.98 | 1.67936e+07 | 4549.3 | 20875.3 | 3983.75 | 1.67936e+07 | 21727.8 | 20872.7 | 17287.8 | 11740.9 | 5 | 58806 | 272 | 6.79836e+06 | 894 | 1.90055e+07 | 41491.4 | 828263 | 1.1861e+06 | 8.14735e+06 | 3.07e+07 | 46780 | 365 | | 81624 | 20240212.1 | 28160.1 | 2.30851e+07 | 0.840579 | 5618.33 | 8.59996e+07 | 14131.6 | 1.88908e+07 | 14237.7 | 1.05021e+07 | 15703.9 | 1.46964e+07 | 1433.2 | 1.25993e+07 | 76732.9 | 6854.74 | 1.67936e+07 | 17250 | 6976.9 | 6.30784e+06 | 52989.9 | 5807.12 | 1.67936e+07 | 56371.4 | 63069.6 | 5733.35 | 1.88908e+07 | 4614.8 | 21193.5 | 4003.65 | 1.67936e+07 | 21333.3 | 20726.4 | 17516.9 | 11696.1 | 5 | 58806 | 278 | 6.79836e+06 | 900 | 1.90055e+07 | 47466.5 | 817866 | 1.18164e+06 | 8.13644e+06 | 3.12543e+07 | 46044 | 359 | | 81633 | 20240212.5 | 27902.2 | 2.51822e+07 | 0.858976 | 5644.36 | 8.59996e+07 | 14075.5 | 1.88908e+07 | 14236.7 | 1.05021e+07 | 15713.4 | 1.25993e+07 | 1437.2 | 1.25993e+07 | 94529.7 | 7254.33 | 1.67936e+07 | 17328.9 | 6987.9 | 6.30784e+06 | 52996.2 | 5760 | 1.67936e+07 | 56459.2 | 63330.5 | 5489.04 | 1.88908e+07 | 4619.8 | 20718.5 | 3987.18 | 1.67936e+07 | 21627.2 | 20938.2 | 17612.2 | 11855.3 | 6 | 58806 | 280 | 6.79836e+06 | 892 | 1.90055e+07 | 42607.2 | 829013 | 1.18545e+06 | 8.17033e+06 | 3.04839e+07 | 46925 | 365 | | 81655 | 20240212.13 | 27898.6 | 2.30851e+07 | 0.803768 | 5563.8 | 8.59996e+07 | 13990.4 | 1.88908e+07 | 14131.4 | 1.05021e+07 | 15607.9 | 1.25993e+07 | 1430.6 | 1.25993e+07 | 76460 | 6798.34 | 1.67936e+07 | 17316.4 | 7014.8 | 6.30784e+06 | 52962.6 | 5801.86 | 1.67936e+07 | 47729.3 | 62963 | 5707.17 | 1.67936e+07 | 4609.6 | 20826.8 | 3984.33 | 1.67936e+07 | 22215.8 | 20982.2 | 17201.3 | 11702 | 6 | 58806 | 282 | 6.79836e+06 | 857 | 1.90055e+07 | 45338.9 | 837177 | 1.18565e+06 | 8.12705e+06 | 3.05914e+07 | 45375 | 356 | | 81698 | 20240212.26 | 27512.9 | 2.51822e+07 | 0.801797 | 5544.31 | 8.59996e+07 | 13988.3 | 1.88908e+07 | 14007.3 | 1.05021e+07 | 15458.2 | 1.46964e+07 | 1419.4 | 1.25993e+07 | 81841.4 | 6793.95 | 1.67936e+07 | 17343.5 | 6814.1 | 6.30784e+06 | 53339.3 | 5799.08 | 1.67936e+07 | 56997.9 | 63496.3 | 5451.72 | 1.67936e+07 | 4628.1 | 20830.9 | 3966.96 | 1.67936e+07 | 22081.4 | 21241.5 | 17273.1 | 11733.4 | 6 | 58806 | 263 | 6.79836e+06 | 854 | 1.90055e+07 | 47856 | 838135 | 1.1831e+06 | 8.17395e+06 | 3.08327e+07 | 46408 | 359 | | 81713 | 20240212.29 | 28092.6 | 2.30851e+07 | 0.813847 | 5580.79 | 8.59996e+07 | 13971 | 1.88908e+07 | 14066.3 | 1.05021e+07 | 15530.5 | 1.46964e+07 | 1403.1 | 1.25993e+07 | 88445.5 | 6787.68 | 1.88908e+07 | 17102.9 | 6820.5 | 6.30784e+06 | 53091.7 | 5749.76 | 1.67936e+07 | 57051.2 | 60375.5 | 5445.28 | 1.67936e+07 | 4517.3 | 17241 | 3992.32 | 1.67936e+07 | 21863.2 | 17389.8 | 17423 | 11630.8 | 5 | 58806 | 274 | 6.79836e+06 | 876 | 1.90055e+07 | 38811.1 | 838511 | 1.18495e+06 | 8.13641e+06 | 3.08983e+07 | 48318 | 358 | | 81732 | 20240212.37 | 27888.8 | 2.51822e+07 | 0.845989 | 5518.64 | 8.59996e+07 | 13910.9 | 1.88908e+07 | 14011.2 | 1.05021e+07 | 15394.5 | 1.25993e+07 | 1415.1 | 1.25993e+07 | 70549.7 | 6801.08 | 1.88908e+07 | 17229.3 | 6957.2 | 6.30784e+06 | 53165.2 | 5787.7 | 1.67936e+07 | 57484.1 | 62768.9 | 5473.48 | 1.67936e+07 | 4595.7 | 20604.4 | 3997.15 | 1.67936e+07 | 22223.7 | 20891.8 | 17526.8 | 11852.5 | 5 | 58806 | 278 | 6.79836e+06 | 866 | 1.90055e+07 | 45010.5 | 838282 | 1.18275e+06 | 8.12582e+06 | 3.07715e+07 | 48346 | 365 | tla-rollback | 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 | tpcc_virtual_cft^ | pi_ls_sgx_cft^ | pi_ls_sgx_cft_mem | pi_basic_sgx_cft^ | pi_basic_sgx_cft_mem | ls_virtual_cft^ | pi_ls_virtual_cft^ | pi_basic_virtual_cft^ | pi_basic_js_virtual_cft^ | ls_jwt_virtual_cft^ | pi_basic_js_sgx_cft^ | pi_basic_js_sgx_cft_mem | pi_ls_jwt_virtual_cft^ | ls_jwt_sgx_cft^ | ls_jwt_sgx_cft_mem | ls_js_virtual_cft^ | pi_ls_jwt_sgx_cft^ | pi_ls_jwt_sgx_cft_mem | ls_full_js_virtual_cft^ | ls_js_jwt_virtual_cft^ | ls_js_sgx_cft^ | ls_js_sgx_cft_mem | 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)^ | 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 | tlc_sim_traces | tlc_sim_levelmean | |-----------:|:---------------|-----------------------:|--------------------------:|------------------------:|----------------:|-------------------:|---------------------------:|--------------:|-----------------:|--------------------:|-----------------:|--------------------:|--------------------:|-----------------------:|------------------:|---------------------:|------------------------:|---------------------------:|----------------------:|-----------------------:|--------------------------:|-------------------------:|------------------:|---------------------:|---------------------:|---------------------:|------------------------:|--------------------------:|-------------------------:|-----------------:|--------------------:|----------------------:|-------------------------:|---------------------:|------------------------:|----------------:|---------------:|------------------:|---------------:|------------------:|-----------------------------:|-------------------------:|---------------------------------:|-----------------------------:|--------------------------:|----------------------:|-----------------:|--------------------:| | 81520 | 20240209.4 | 28084.1 | 2.51822e+07 | 0.83655 | 5599.56 | 8.59996e+07 | 100326 | 14067.4 | 1.88908e+07 | 17453 | 14225.9 | 1.05021e+07 | 15581.3 | 1.46964e+07 | 53035.5 | 56409.5 | 63135.8 | 4688.1 | 20449.3 | 1433.5 | 1.25993e+07 | 19354 | 7263.29 | 1.67936e+07 | 17634.1 | 7153.9 | 6.30784e+06 | 17697.1 | 11752.2 | 5815.29 | 1.67936e+07 | 5725.79 | 1.88908e+07 | 3983.17 | 1.67936e+07 | 40469.5 | 835900 | 1.18193e+06 | 8.15076e+06 | 3.07577e+07 | 5 | 58806 | 168 | 4.51944e+06 | 585 | 1.35909e+07 | 38938 | 403 | | 81719 | 20240212.31 | 28080.2 | 2.51822e+07 | 0.800455 | 5579.41 | 8.59996e+07 | 97152.1 | 14013.4 | 1.88908e+07 | 17124 | 14158.6 | 1.05021e+07 | 15367.9 | 1.25993e+07 | 53372.4 | 57356.2 | 62783.5 | 4641.1 | 20914.6 | 1434.6 | 1.25993e+07 | 22042 | 6845.47 | 1.67936e+07 | 17469.4 | 6960.3 | 6.30784e+06 | 17715.7 | 11675.2 | 5797.51 | 1.67936e+07 | 5473.36 | 1.67936e+07 | 3985.05 | 1.67936e+07 | 43350.5 | 834721 | 1.1821e+06 | 8.147e+06 | 3.07942e+07 | 5 | 58806 | 263 | 6.79836e+06 | 887 | 1.90055e+07 | 38488 | 403 | | 81739 | 20240212.39 | 28047.5 | 2.51822e+07 | 0.799788 | 5615.67 | 8.59996e+07 | 74824.6 | 14088.2 | 1.88908e+07 | 17425.5 | 14159.5 | 1.05021e+07 | 15678.7 | 1.46964e+07 | 53079 | 57607 | 64894.8 | 4624.8 | 21007.8 | 1433.7 | 1.25993e+07 | 22109.2 | 6857.73 | 1.88908e+07 | 20978.6 | 6959.6 | 6.30784e+06 | 17445.5 | 11831 | 5762.66 | 1.67936e+07 | 5728.22 | 1.67936e+07 | 3967.79 | 1.67936e+07 | 47145.5 | 833887 | 1.18121e+06 | 8.15257e+06 | 3.14419e+07 | 5 | 58806 | 269 | 6.79836e+06 | 883 | 1.90055e+07 | 39305 | 403 | | 81743 | 20240212.41 | 27768.4 | 2.51822e+07 | 0.820329 | 5633.94 | 8.80968e+07 | 79106.1 | 14076.1 | 1.88908e+07 | 17384.9 | 14168.8 | 1.05021e+07 | 15728.5 | 1.25993e+07 | 53335.1 | 56451.6 | 61853.4 | 4592.6 | 20979.5 | 1436 | 1.25993e+07 | 21988.2 | 6842.66 | 1.88908e+07 | 20903.2 | 6922.4 | 6.30784e+06 | 17695.8 | 11816.7 | 5809.35 | 1.67936e+07 | 5469.49 | 1.67936e+07 | 3992.39 | 1.67936e+07 | 45552.1 | 835832 | 1.18308e+06 | 8.15631e+06 | 3.11905e+07 | 5 | 58806 | 274 | 6.79836e+06 | 882 | 1.90055e+07 | 40109 | 403 | | 81745 | 20240212.42 | 28092.5 | 2.30851e+07 | 0.814797 | 5555.16 | 8.59996e+07 | 71786 | 13872.2 | 1.88908e+07 | 17248.3 | 13988.1 | 1.05021e+07 | 15434.9 | 1.46964e+07 | 53144.9 | 57079.9 | 61748.4 | 4544.7 | 21025 | 1408.9 | 1.25993e+07 | 21437.6 | 6825.52 | 1.88908e+07 | 17426.6 | 6876.3 | 6.30784e+06 | 17330.5 | 11641.2 | 5752.28 | 1.67936e+07 | 5470.63 | 1.67936e+07 | 3970.23 | 1.67936e+07 | 44944.3 | 836702 | 1.17529e+06 | 8.15115e+06 | 3.07979e+07 | 5 | 58806 | 273 | 6.79836e+06 | 906 | 1.90055e+07 | 40126 | 403 |

images

lemmy commented 4 months ago

This change makes TLC still accept rollback_safety.ndjson while showing proper action names.

diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
index 89ff917e8..f6d7146f6 100644
--- a/tla/consensus/Traceccfraft.tla
+++ b/tla/consensus/Traceccfraft.tla
@@ -373,9 +373,11 @@ TraceNext ==
     \/ IsExecuteAppendEntries

     \/ IsRcvProposeVoteRequest
+    \/ /\ l = 191
+       /\ DropMessages \cdot IsRcvRequestVoteRequest

 DropAndNext ==
-    \/ IF ENABLED TraceNext THEN TraceNext ELSE DropMessages \cdot TraceNext
+    \/ TraceNext
     \/ IsDropPendingTo

 TraceSpec ==
lemmy commented 4 months ago

Hypothesis why TV doesn't fail: 1) Validation in Traceccfraft is generally too weak, i.e., we have to come up with more things to assert about the trace (see @heidihoward _fake.ndjson above) 2) The json trace/raft scenario ends prematurely for TV to catch failures (some log lines such as execute_append_entries_sync are noops in Traceccfraft). 3) QuorumLogInv is a conjunct of TraceMatchesConstraints, whereas it's commented in e.g. SIMccfraft.cfg. 4) Occurrence of \cdot in ccfraft, combined with the incomplete implementation in TLC, may cause problems. 4a) The debugger's unsatisfied-next breakpoint and https://github.com/tlaplus/tlaplus/commit/c2713def38aa1d3255a6c2fe2aa037253e00e361 could both be incompatible with \cdot, causing states with a roll-backed log not to be in the model.

lemmy commented 4 months ago

Emitting two more log lines by appending dispatch_one,2 to the scenario, and commenting/removing QuorumLogInv adds states to the model where node #2's log has been rolled back:

image

Questions: 1) What non-determinism in ccfraft allows node 2 not to roll back its log at l=214? => AppendEntriesAlreadyDone (@eddyashton: You mentioned a known discrepancy during today's standup?!) 2) What assertions should be added to Traceccfraft to exclude states with the unchanged log? => state.last_idx, i.e., the length of a node's log, is nowhere asserted.

lemmy commented 4 months ago

main with

Hypothesis why TV doesn't fail:

  1. Validation in Traceccfraft is generally too weak, i.e., we have to come up with more things to assert about the trace (see @heidihoward _fake.ndjson above)
  2. The json trace/raft scenario ends prematurely for TV to catch failures (some log lines such as execute_append_entries_sync are noops in Traceccfraft).
  3. QuorumLogInv is a conjunct of TraceMatchesConstraints, whereas it's commented in e.g. SIMccfraft.cfg.
  4. Occurrence of \cdot in ccfraft, combined with the incomplete implementation in TLC, may cause problems. 4a) The debugger's unsatisfied-next breakpoint and tlaplus/tlaplus@c2713de could both be incompatible with \cdot, causing states with a roll-backed log not to be in the model.
  1. turned out to be a red herring, and 2. and 3. are optional; 1. (https://github.com/microsoft/CCF/pull/6010) is what makes TV find the violation at state 212 (even in main). I suggest we continue strengthening TV by working on the various TODOs in Traceccfraft.tla.
lemmy commented 4 months ago
  1. turned out to be a red herring, and 2. and 3. are optional; 1. (Strengthen assertions in trace validation #6010) is what makes TV find the violation at state 212 (even in main). I suggest we continue strengthening TV by working on the various TODOs in Traceccfraft.tla.

I take that back for now.

diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
index 1b69b4cb7..d9bbfece9 100644
--- a/tla/consensus/Traceccfraft.tla
+++ b/tla/consensus/Traceccfraft.tla
@@ -219,7 +219,8 @@ IsRcvAppendEntriesRequest ==
     /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
     \* TODO /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
     /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state]
-    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
+    /\ \/ Len(log[logline.msg.state.node_id])  = logline.msg.state.last_idx
+       \/ Len(log'[logline.msg.state.node_id]) = TraceLog[l-1].msg.state.last_idx

 IsSendAppendEntriesResponse ==
     \* Skip saer because ccfraft!HandleAppendEntriesRequest atomcially handles the request and sends the response.
lemmy commented 3 months ago

Absorbed by https://github.com/microsoft/CCF/pull/6010 and https://github.com/microsoft/CCF/pull/6009.

lemmy commented 3 months ago

@heidihoward Any reason to keep the tla-rollback branch around?

heidihoward commented 3 months ago

Nope, fine to delete

achamayou commented 3 months ago

@lemmy so what was the root cause in the end?

lemmy commented 3 months ago

Not enough/too weak assertions.