Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Swapping nextIndex for sentIndex #5897

Merged
merged 9 commits into from
Jan 9, 2024
Merged

Swapping nextIndex for sentIndex #5897

merged 9 commits into from
Jan 9, 2024

Conversation

heidihoward
Copy link
Member

@heidihoward heidihoward commented Jan 8, 2024 •
edited
Loading

Currently, raft.h uses sent_index to track the last index sent to a follower (ish) but the TLA+ specification uses nextIndex to track the next index to send to each follower (sent_index +1). As a result, the trace checker needs to increment sent_index before comparison to nextIndex.

This PR updates the TLA+ specification to swap nextIndex from sentIndex, renaming the variable and decreasing its value by one.

Previously mentioned here: #5895 (comment)

@heidihoward heidihoward added the tla TLA+ specifications label Jan 8, 2024
@lemmy
Copy link
Contributor

lemmy commented Jan 8, 2024

@heidihoward As an FYI: nextIndex and sent_idx gave me a hard time when aligning the spec and impl, which is why I would recommend to backport this change to before we changed the bootstrapping logic. The coverage of the current trace validation is rather low.

@ghost
Copy link

ghost commented Jan 8, 2024 •
edited by ghost
Loading

tla-off-by-one@80062 aka 20240109.19 vs main ewma over 20 builds from 79809 to 80055

Click to see table

main

build_id build_number Commit latency factor pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem 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 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 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 tpcc_virtual_cft^ ls_full_js_sgx_cft^ ls_full_js_sgx_cft_mem ls_virtual_cft^ pi_ls_virtual_cft^ ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem 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^ hist_sgx_cft^ ls_js_jwt_virtual_cft^ RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^ tlc_sim_traces tlc_sim_levelmean pi_basic_mt_virtual_cft^
79809 20240102.3 0.818907 27998 2.51822e+07 5582.58 8.59996e+07 14069 1.88908e+07 14207.7 1.05021e+07 15632.9 1.46964e+07 1438 1.25993e+07 7254.86 1.67936e+07 6979.5 6.30784e+06 5809.21 1.67936e+07 6 86496 427 1.2541e+07 241 6.31473e+06 17426.2 5725.47 1.88908e+07 52688.3 56487.3 4000.63 1.67936e+07 62076.8 4588.5 20938.1 21383.1 17806.2 17373.5 39813.8 11613.7 838128 1.18558e+06 8.15241e+06 3.07577e+07 2304 403 89517.2
79821 20240102.7 0.812237 28223.4 2.30851e+07 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 7246.07 1.67936e+07 6934.2 6.30784e+06 5809.09 1.67936e+07 7 86496 446 1.2541e+07 237 6.31473e+06 17312.2 5478.56 1.67936e+07 53352.6 57235.7 4007.06 1.67936e+07 62129.2 4590.4 21078.7 22285.6 20842.2 17429 40366 11612.2 832255 1.17903e+06 8.15355e+06 3.03592e+07 2331 403 100850
79832 20240102.10 0.780568 27705.2 2.51822e+07 5592.62 8.59996e+07 14075.6 1.88908e+07 14247 1.05021e+07 15580.2 1.46964e+07 1429.8 1.25993e+07 6842.56 1.67936e+07 7079.5 6.30784e+06 5781.21 1.67936e+07 6 86496 424 1.2541e+07 245 6.31473e+06 17247.1 5767.74 1.67936e+07 52935.7 56910 3982.1 1.67936e+07 62683.8 4647.1 20739.3 20193.9 20729.9 17575.8 42743.5 11690.8 823735 1.18304e+06 8.15511e+06 3.0778e+07 2301 403 90345.4
79836 20240103.1 0.8277 28173 2.51822e+07 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 7262.76 1.67936e+07 6980.2 6.30784e+06 5814.99 1.67936e+07 6 86496 417 1.2541e+07 238 6.31473e+06 17163.7 5465.89 1.88908e+07 52985.4 57238.7 3973.9 1.67936e+07 62511.8 4622.6 20776.5 21693.9 20385 17974.8 43365.4 11889.2 827987 1.18005e+06 8.16857e+06 3.13533e+07 2109 403 68113.2
79850 20240104.1 0.774183 28107.5 2.51822e+07 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 7263.29 1.67936e+07 7142 6.30784e+06 5808.21 1.67936e+07 6 86496 447 1.2541e+07 239 6.31473e+06 17222.5 5739.03 1.88908e+07 53076.9 56886.7 4019.28 1.67936e+07 62583 4618.3 20820.4 21956.8 17246.1 17545.1 45361.8 11727 833007 1.17531e+06 8.1401e+06 3.07056e+07 2277 403 88847.3
79858 20240104.5 0.762951 28151.4 2.30851e+07 5612.73 8.59996e+07 14105.1 1.88908e+07 14237.6 1.05021e+07 15657.2 1.46964e+07 1437 1.05021e+07 7259.07 1.88908e+07 6983.6 6.30784e+06 5791.47 1.67936e+07 6 86496 420 1.2541e+07 238 6.31473e+06 17237.2 5734.66 1.67936e+07 53156.1 56700.3 4001.19 1.67936e+07 62251.6 4624.7 20802.9 22305.5 17912 17600.9 46312.7 12005.6 832473 1.18246e+06 8.14589e+06 3.0464e+07 2357 403 72092.6
79876 20240104.10 0.770841 27983.2 2.51822e+07 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 7241.98 1.67936e+07 6915.4 6.30784e+06 5771.22 1.67936e+07 6 86496 429 1.2541e+07 234 6.31473e+06 17196.9 5737.28 1.67936e+07 53164.5 56410.8 3985.63 1.67936e+07 62397 4645.9 20949.8 22178.9 17324.7 17551.5 40222.9 11659.7 829045 1.18083e+06 8.15014e+06 3.10298e+07 2315 403 82253.2
79893 20240105.3 0.770387 28242.6 2.30851e+07 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 7241.21 1.67936e+07 7028.1 6.30784e+06 5776.46 1.67936e+07 6 86496 438 1.2541e+07 234 6.31473e+06 17195.7 5739.53 1.67936e+07 53109.3 56423.9 4001.54 1.67936e+07 61913.6 4637.7 21053.6 21897.2 17479.2 17489.6 41192.1 11786.3 834184 1.18333e+06 8.13454e+06 3.07928e+07 2312 403 79459.2
79901 20240105.6 0.804442 28134.7 2.51822e+07 5625.32 8.59996e+07 14099 1.88908e+07 14266.8 1.05021e+07 15657.8 1.46964e+07 1428.6 1.25993e+07 6896.08 1.67936e+07 7033.2 6.30784e+06 5807.41 1.67936e+07 6 86496 445 1.2541e+07 240 6.31473e+06 17253.5 5744.67 1.88908e+07 52754.9 54886.9 4003.65 1.67936e+07 61431.1 4615.1 20971.5 21889.5 17410.2 17219.9 42166 11532.7 837682 1.17356e+06 8.14881e+06 3.18111e+07 2258 403 96416.1
79920 20240105.14 0.804667 28090.3 2.51822e+07 5642.82 8.59996e+07 14097.8 1.88908e+07 14249.7 1.05021e+07 15643 1.46964e+07 1426.1 1.25993e+07 6883.92 1.88908e+07 6976.3 6.30784e+06 5819.57 1.67936e+07 6 86496 434 1.2541e+07 235 6.31473e+06 17195.4 5767.4 1.67936e+07 53484.4 56927.5 3983.21 1.67936e+07 63034.1 4635.9 20600.9 21708 20208.9 17600.9 42864.9 11868.5 816929 1.18007e+06 8.14615e+06 3.06564e+07 2325 403 72389.5
79931 20240105.18 0.830304 28155.9 2.51822e+07 5572.38 8.59996e+07 14067.9 1.67936e+07 14143.9 1.05021e+07 15609.5 1.25993e+07 1433 1.25993e+07 6844.24 1.67936e+07 6937.8 6.30784e+06 5775.62 1.67936e+07 6 86496 436 1.2541e+07 236 6.31473e+06 17203.8 5454.13 1.67936e+07 53081 57491.7 3990.64 1.67936e+07 63657.6 4644.3 20979.1 21753.3 20837.9 17426.7 41115.6 11781.2 835630 1.17185e+06 8.15319e+06 3.14385e+07 2224 403 78451.8
79937 20240105.20 0.788583 28053.5 2.51822e+07 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 7233.07 1.67936e+07 6844.1 6.30784e+06 5802.33 1.67936e+07 6 77678 366 1.14441e+07 223 5.86578e+06 17208.8 5491.67 1.67936e+07 56022.5 56925.6 3998.46 1.67936e+07 63903.6 4666.7 20742.8 21552.2 20961.9 17614 47083.7 11908.4 832419 1.18053e+06 8.15387e+06 3.21896e+07 2256 403 85420.8
79954 20240108.2 0.811783 28237 2.30851e+07 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 7263.29 1.67936e+07 7083.5 6.30784e+06 5819.68 1.67936e+07 6 77678 393 1.14441e+07 225 5.86578e+06 17316.8 5772.06 1.67936e+07 53076.6 55248.3 4006.27 1.67936e+07 60320.6 4528.2 20993.9 21334.7 17858.4 17621.1 41219.2 11538.3 823934 1.18456e+06 8.13305e+06 3.08225e+07 2191 403 99047.8
79961 20240108.5 0.812651 27925.4 2.51822e+07 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 7265.93 1.67936e+07 6978.2 6.30784e+06 5819.84 1.67936e+07 5 77678 377 1.14441e+07 219 5.86578e+06 17247.2 5491.66 1.88908e+07 53409.5 56958 3978.52 1.67936e+07 63490.4 4632.7 20797.7 22702.5 20869.2 17815.9 43913.1 11888.8 834677 1.17721e+06 8.13573e+06 3.1303e+07 2280 403 85416
79989 20240108.17 0.812918 28271 2.51822e+07 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 7249.22 1.67936e+07 6933.6 6.30784e+06 5811.81 1.67936e+07 6 77678 392 1.14441e+07 220 5.87421e+06 17262.7 5488.58 1.67936e+07 52887.3 55918.4 3984.32 1.67936e+07 62745.3 4610.5 20923.3 22286.1 20921.3 17621.5 45321.3 11740.7 831008 1.18097e+06 8.15374e+06 3.08415e+07 2380 403 78403.9
80001 20240108.22 0.786976 28214.4 2.30851e+07 5635.92 8.59996e+07 14107 1.67936e+07 14229 1.05021e+07 15650.3 1.25993e+07 1429.2 1.05021e+07 7261.71 1.67936e+07 7084.9 6.30784e+06 5822.41 1.67936e+07 6 77678 147 3.90715e+06 144 3.83177e+06 17220.1 5738.66 1.67936e+07 52740.1 56590.9 3986.1 1.67936e+07 62501.5 4637.4 20710.5 21594.5 20773 17397.2 45877 11679.9 835642 1.18258e+06 8.17072e+06 3.06881e+07 2749 403 82485.2
80019 20240109.2 0.779573 27799.4 2.51822e+07 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 6843.67 1.67936e+07 6964.2 6.30784e+06 5808.73 1.67936e+07 5 77678 150 3.90715e+06 149 3.83177e+06 17676.2 5734.06 1.67936e+07 53244.4 56053.5 4019.09 1.67936e+07 61572.3 4586.7 20734.2 22425.5 17371.7 17383.5 40846.9 11766.6 840733 1.17962e+06 8.12931e+06 3.06812e+07 2587 403 92062.2
80028 20240109.6 0.773671 28077.7 2.51822e+07 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 6914.02 1.88908e+07 7048.5 6.30784e+06 5802.22 1.67936e+07 5 77678 150 3.90715e+06 146 3.83177e+06 17211.9 5766.41 1.67936e+07 53026.8 58109.1 3999.26 1.67936e+07 61402.2 4691.4 20760.8 22245 20537.9 17634 43293 11758.4 830215 1.18604e+06 8.15176e+06 3.07125e+07 2686 403 80572.2
80038 20240109.10 0.804995 27757.8 2.30851e+07 5590.07 8.59996e+07 14106.5 1.88908e+07 14170.6 1.05021e+07 15627.6 1.25993e+07 1424.9 1.25993e+07 6806.45 1.67936e+07 7055.6 6.30784e+06 5772.08 1.67936e+07 6 77678 148 3.90715e+06 149 3.83177e+06 17787.8 5731.73 1.67936e+07 52786.7 56588 3997.66 1.67936e+07 62017.1 4618.3 21127.5 22348.4 20872.7 17348.9 46610.2 11716.9 793924 1.17586e+06 8.15647e+06 3.07947e+07 2762 403 82244.9
80055 20240109.17 0.801944 28125.3 2.51822e+07 5553.42 8.59996e+07 14011.9 1.88908e+07 14117.8 1.05021e+07 15653.4 1.25993e+07 1440.5 1.25993e+07 6840.17 1.88908e+07 6906.2 6.30784e+06 5773.25 1.67936e+07 6 77678 150 3.90715e+06 150 3.83177e+06 17168 5487.83 1.88908e+07 53353.8 56983.3 3992.89 1.67936e+07 62914.7 4671.7 20784.1 21676.9 20551.7 17667.4 45493 11750.6 839102 1.17961e+06 8.13667e+06 3.07457e+07 2683 403 83110

tla-off-by-one

build_id build_number 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 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 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 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^ pi_basic_mt_virtual_cft^ ls_js_virtual_cft^ ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^ tlc_sim_traces tlc_sim_levelmean
80006 20240108.23 0 180 2 31736 2 17134 27832.8 2.51822e+07 0.788753 5642.01 8.59996e+07 14069.4 1.88908e+07 14201.4 1.05021e+07 15677.8 1.25993e+07 1428.9 1.25993e+07 7265.93 1.88908e+07 6994.8 6.30784e+06 5802.21 1.67936e+07 5489.83 1.67936e+07 3998.35 1.67936e+07 45425.2 833873 1.18353e+06 8.1552e+06 3.2004e+07 17177.8 53204.3 57192.5 62317.8 4626.3 20942.5 22236.1 81683.1 17241.1 17547.2 11802.5 6017 403
80046 20240109.12 6 77678 148 3.90715e+06 141 3.83177e+06 27747.4 2.51822e+07 0.817308 5637.6 8.59996e+07 14053.4 1.67936e+07 14170 1.05021e+07 15675.8 1.46964e+07 1425.2 1.05021e+07 7229.84 1.67936e+07 6978.6 6.30784e+06 5778.17 1.67936e+07 5730.95 1.67936e+07 3972.15 1.67936e+07 44658.8 837220 1.17993e+06 8.14829e+06 3.15796e+07 17320.5 53176.7 56890.6 62924.7 4663.2 21022.9 20297.6 75569.1 20914.3 17551.2 11716 2742 403
80060 20240109.18 6 77678 147 3.90715e+06 147 3.83177e+06 28070.3 2.51822e+07 0.806032 5521.39 8.59996e+07 14087.2 1.67936e+07 14190.4 1.05021e+07 15662.9 1.25993e+07 1430.6 1.25993e+07 7237.81 1.67936e+07 7101.6 6.30784e+06 5771.8 1.67936e+07 5482.51 1.88908e+07 3983.83 1.67936e+07 41980.4 831685 1.17606e+06 8.03333e+06 3.06238e+07 17134.7 52979.2 48043.4 61938.9 4664.6 20481.7 19888.2 83853.4 17339.6 17661.3 11709.4 2782 403
80062 20240109.19 6 77678 150 3.90715e+06 145 3.83177e+06 27814.7 2.30851e+07 0.78781 5580.73 8.59996e+07 14006.9 1.88908e+07 14096.5 1.05021e+07 15483.2 1.25993e+07 1424.4 1.25993e+07 6834.7 1.88908e+07 7040.7 6.30784e+06 5758.34 1.67936e+07 5474.98 1.67936e+07 3977.13 1.67936e+07 43789.5 833235 1.18134e+06 8.15507e+06 3.08513e+07 17276.8 52720.3 57056.8 62724.8 4677 20830 22305 79131.3 20939.3 17368.4 11855 2694 403

images

@heidihoward
Copy link
Member Author

CI metrics are looking suspicious. I expect we are not reaching the expected state of states, but I'll take a look tomorrow

I would be great to add reachability to the test suite (like we have for the consistency specs) https://github.com/microsoft/CCF/blob/main/tla/consistency/MCMultiNodeCommitReachability.cfg

@heidihoward heidihoward marked this pull request as ready for review January 9, 2024 11:52
@heidihoward heidihoward requested a review from a team January 9, 2024 11:52
@heidihoward heidihoward changed the title [WIP] Swapping nextIndex for sentIndex Swapping nextIndex for sentIndex Jan 9, 2024
@heidihoward heidihoward merged commit 2c60b90 into main Jan 9, 2024
26 checks passed
@heidihoward heidihoward deleted the tla-off-by-one branch January 9, 2024 13:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@achamayou achamayou achamayou approved these changes

Assignees
No one assigned
Labels
tla TLA+ specifications
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@heidihoward @lemmy @achamayou