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.

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

matchIndex lower bound for nextIndex #5630

Merged
merged 1 commit into from
Sep 8, 2023
Merged

matchIndex lower bound for nextIndex #5630

merged 1 commit into from
Sep 8, 2023

Conversation

lemmy
Copy link
Contributor

@lemmy lemmy commented Sep 6, 2023

@lemmy lemmy added consensus tla TLA+ specifications labels Sep 6, 2023
@lemmy
Copy link
Contributor Author

lemmy commented Sep 6, 2023

node->second.sent_idx = std::max(this_match, node->second.match_idx + 1);

As expected, build/raft_tests has four failures and the four raft_scenarios 4582.2, election_while_reconfiguration, fancy_election.1, and suffix_collision.2 core-dumps with +1.

@ghost
Copy link

ghost commented Sep 6, 2023

mku-pr5341impl@75575 aka 20230907.21 vs main ewma over 20 builds from 75234 to 75570

Click to see table

main

build_id build_number Commit latency factor ls_sgx_cft^ ls_sgx_cft_mem ls_virtual_cft^ pi_ls_sgx_cft^ pi_ls_sgx_cft_mem pi_ls_virtual_cft^ pi_basic_virtual_cft^ pi_basic_sgx_cft^ pi_basic_sgx_cft_mem pi_basic_js_virtual_cft^ ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_js_virtual_cft^ pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem ls_full_js_virtual_cft^ ls_jwt_sgx_cft^ ls_jwt_sgx_cft_mem pi_ls_jwt_sgx_cft^ pi_ls_jwt_sgx_cft_mem 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)^ pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem pi_basic_mt_virtual_cft^
75234 20230901.26 0.799024 16412 1.88908e+07 45763 16520.2 1.05021e+07 48415.1 52445.3 18034.1 1.46964e+07 4461.9 17320.3 19267.1 17307.8 1640.1 1.25993e+07 16727 8046.24 1.88908e+07 7975.8 6.30784e+06 9900.84 6617.55 1.67936e+07 6583.32 1.67936e+07 4562.49 1.88908e+07 47832.7 814140 1.17862e+06 8.11427e+06 3.09824e+07 31298.5 2.51822e+07 81323.7
75255 20230904.2 0.800459 16585.1 1.88908e+07 45618.4 16649.8 1.05021e+07 47656 52809.9 18179.8 1.46964e+07 4482.3 17231.3 19040.4 15210.2 1659.1 1.25993e+07 16875 8133.32 1.88908e+07 8318.8 6.30784e+06 9795.68 7070.58 1.67936e+07 6589.49 1.67936e+07 4555.83 1.88908e+07 50413 834549 1.18199e+06 8.15296e+06 3.13879e+07 31877.2 2.51822e+07 70284.9
75265 20230904.6 0.797237 16561.7 1.88908e+07 45627.4 16683.7 1.05021e+07 48343.5 52792.7 18219.1 1.46964e+07 4465.8 17315 19935.4 17552.3 1658 1.25993e+07 15100.5 8180.61 1.88908e+07 8300.5 6.30784e+06 9851.17 7057.78 1.67936e+07 6644.72 1.67936e+07 4583.56 1.88908e+07 45461.7 831805 1.17771e+06 8.15034e+06 3.12653e+07 31457.4 2.51822e+07 63213.7
75271 20230904.8 0.807553 16703.8 1.88908e+07 45699.4 16797.4 1.05021e+07 48066.8 54336.2 18353.3 1.46964e+07 4468.2 17313.8 19411.1 16926.8 1655.8 1.25993e+07 14815 8200.03 1.88908e+07 8097.4 6.30784e+06 9820.68 7074.81 1.67936e+07 6593.84 1.67936e+07 4556.21 1.88908e+07 45397.8 839817 1.18163e+06 8.15446e+06 3.10369e+07 32193.1 2.51822e+07 78961.1
75282 20230904.12 0.796235 16694.9 1.88908e+07 45690.9 16916.6 1.05021e+07 49077.3 54125.9 18325.5 1.46964e+07 4479.4 17623.4 16298.1 17113.3 1648.6 1.25993e+07 14553.5 8156.02 1.88908e+07 7968.6 6.30784e+06 9824.1 7040.55 1.67936e+07 6637.16 1.67936e+07 4557.13 1.88908e+07 48180.1 834932 1.18089e+06 8.15433e+06 3.07392e+07 31979.1 2.51822e+07 79345.1
75288 20230904.14 0.801078 16679.2 1.88908e+07 45797.3 16871.4 1.05021e+07 47838.9 53668.7 18477.5 1.46964e+07 4491.1 17414.1 19684.7 17347 1656.9 1.25993e+07 14843.7 8152.93 1.88908e+07 8019.1 6.30784e+06 9878.27 7036.64 1.67936e+07 6584.04 1.67936e+07 4551.27 1.88908e+07 44845.8 830898 1.18237e+06 8.1505e+06 3.0772e+07 32335.9 2.51822e+07 80429.9
75300 20230905.1 0.770774 16645.6 1.88908e+07 45506.3 16823.7 1.05021e+07 48842.4 53087.4 18313.7 1.46964e+07 4485.3 17474.3 19306.5 17442.8 1652.3 1.25993e+07 15046.5 8180.27 1.88908e+07 8177 6.30784e+06 9898.89 7051.17 1.67936e+07 6596.68 1.67936e+07 4571.26 1.88908e+07 50271.9 821926 1.1746e+06 8.1143e+06 3.17018e+07 32207.2 2.51822e+07 79372.1
75314 20230905.8 0.820898 16738.7 1.88908e+07 45656.7 16868.1 1.05021e+07 48164.7 53451 18392.4 1.46964e+07 4387.1 17378.6 19385.9 17350.5 1648.2 1.25993e+07 14763.3 8201.26 1.88908e+07 8305.8 6.30784e+06 10113.2 7067.89 1.67936e+07 6593.78 1.67936e+07 4587.48 1.88908e+07 45347.1 830368 1.17868e+06 8.15579e+06 3.08615e+07 32224.6 2.51822e+07 71193
75332 20230905.15 0.795074 16686.1 1.88908e+07 45805 16806.5 1.05021e+07 48010.4 53472.6 18374.4 1.46964e+07 4468.6 17303.8 19203.1 17495.4 1663.1 1.25993e+07 14979.2 8145.3 1.88908e+07 8056.1 6.30784e+06 9760 7062.03 1.67936e+07 6644.82 1.67936e+07 4549.04 1.88908e+07 47860 830160 1.17693e+06 8.15631e+06 3.07813e+07 32237.6 2.51822e+07 73261.1
75348 20230905.21 0.818926 16897 1.88908e+07 45750.9 16860.5 1.05021e+07 48204.9 52524 18475.4 1.46964e+07 4466 17413.2 19456.4 17519 1657.2 1.25993e+07 15001.3 8211.83 1.88908e+07 8045.4 6.30784e+06 10200.3 7058.49 1.67936e+07 6594.25 1.67936e+07 4559.4 1.88908e+07 43975.4 820294 1.17696e+06 8.17128e+06 3.07581e+07 31697 2.51822e+07 69941.9
75360 20230905.26 0.800555 16639.2 1.88908e+07 45554.4 16865.9 1.05021e+07 42866.8 51334.5 18094.7 1.46964e+07 4480 17462.1 19193.1 16930.1 1629.4 1.25993e+07 15179.2 8097.92 1.88908e+07 8244.9 6.30784e+06 9898.05 6577.72 1.67936e+07 6573.38 1.67936e+07 4545.58 1.67936e+07 47617.4 834158 1.17952e+06 8.1542e+06 3.0816e+07 32429.6 2.51822e+07 75493.7
75413 20230905.41 0.822033 16619.4 1.88908e+07 42002.8 16634.2 1.05021e+07 47678.8 53684.4 18150.8 1.46964e+07 4426.7 17180.1 19169.9 17447.2 1640.4 1.25993e+07 14839.1 8128.27 1.88908e+07 7918 6.30784e+06 10272.6 6668.1 1.67936e+07 6561.8 1.67936e+07 4544.2 1.67936e+07 46378.9 831657 1.18593e+06 8.15381e+06 3.25544e+07 32149.1 2.51822e+07 84700.2
75427 20230905.45 0.79923 16851.9 1.88908e+07 43818.6 16843.5 1.05021e+07 47219.3 54172.4 18380.2 1.46964e+07 4474.6 17207 20035.7 17125.1 1660.9 1.25993e+07 16863.6 8204.56 1.88908e+07 8033.3 6.30784e+06 9757.72 7055.71 1.67936e+07 6604.32 1.67936e+07 4591.15 1.88908e+07 49899.7 831718 1.18507e+06 8.16148e+06 3.07891e+07 32303 2.51822e+07 72646.1
75432 20230906.1 0.792911 16953.5 1.88908e+07 44002.6 16886.8 1.05021e+07 47749.6 54054.4 18426.2 1.46964e+07 4440.1 17184.3 19123.7 17476.7 1656.7 1.25993e+07 14970.7 8197.08 1.88908e+07 8067.4 6.30784e+06 10416.6 7062.48 1.67936e+07 6650.18 1.67936e+07 4558.5 1.88908e+07 47511.8 836786 1.17882e+06 8.13596e+06 3.09679e+07 32134 2.72794e+07 72254
75453 20230906.8 0.786039 16911.9 1.88908e+07 45758.2 16854.2 1.05021e+07 48251.8 54707.9 18339 1.46964e+07 4474.7 17380.4 18840.6 17589.3 1666.3 1.25993e+07 14994.8 8195.46 1.88908e+07 8236.7 6.30784e+06 9887.4 7050.11 1.67936e+07 6651.5 1.67936e+07 4550.56 1.88908e+07 47836.8 831787 1.17789e+06 8.12511e+06 3.08063e+07 31842.2 2.51822e+07 62844.4
75489 20230906.23 0.800124 16654.9 1.88908e+07 43804.6 16776.6 1.05021e+07 47435.6 54050.3 18256.7 1.25993e+07 4459.5 17073.3 18929 17464.5 1636.7 1.25993e+07 14865.8 8153.42 1.88908e+07 8125.5 6.30784e+06 10073.8 6677.29 1.67936e+07 6628.14 1.67936e+07 4550.28 1.88908e+07 49990.9 835269 1.17747e+06 8.13363e+06 3.07143e+07 31743.9 2.51822e+07 82560
75522 20230907.3 0.772057 16673.7 1.88908e+07 45714.3 16929.9 1.05021e+07 48111.2 54314.5 18283.4 1.46964e+07 4463.3 17295.6 19589.4 17065.4 1656.8 1.25993e+07 14677.8 8168.97 1.88908e+07 8023.9 6.30784e+06 10062.2 7052.03 1.67936e+07 6594.49 1.67936e+07 4565.33 1.88908e+07 49662.8 828056 1.18636e+06 8.1552e+06 3.07808e+07 32075.6 2.51822e+07 66260.1
75527 20230907.5 0.781303 16807.7 1.88908e+07 43523 16890.6 1.05021e+07 47340.4 53737.5 18259.9 1.46964e+07 4404.9 17097.4 19462.4 17630.6 1648.4 1.25993e+07 15065 8151.7 1.88908e+07 7992.3 6.30784e+06 10283.8 7014.17 1.67936e+07 6599.19 1.67936e+07 4558.03 1.88908e+07 42500.3 823830 1.18114e+06 8.1554e+06 3.07249e+07 32308 2.51822e+07 86171.1
75554 20230907.14 0.784733 16776.5 1.88908e+07 45865.6 16911.3 1.05021e+07 47959.1 54950.9 18490.9 1.46964e+07 4492.7 17191.6 19221.2 17286.2 1659.7 1.25993e+07 16906.8 8214.84 1.88908e+07 8100.2 6.30784e+06 9966.44 7060.74 1.67936e+07 6600.24 1.67936e+07 4579.56 1.88908e+07 47720.1 832953 1.17863e+06 8.1447e+06 3.05827e+07 32296.2 2.51822e+07 89286.5
75570 20230907.20 0.799646 16832.6 1.88908e+07 45705.3 17001.3 1.05021e+07 48300.1 55108.2 18451.6 1.46964e+07 4494.8 17134.4 19570.6 17098.8 1661.9 1.25993e+07 16872.1 8246.8 1.88908e+07 8192.6 6.30784e+06 9890.69 7051.77 1.67936e+07 6608.3 1.67936e+07 4556.94 1.88908e+07 46267.7 831516 1.18245e+06 8.13564e+06 3.11644e+07 32177.9 2.51822e+07 62416.2

mku-pr5341impl

build_id build_number Commit latency factor 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_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ 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 pi_basic_js_virtual_cft^ pi_ls_jwt_sgx_cft^ pi_ls_jwt_sgx_cft_mem ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_js_sgx_cft^ ls_js_sgx_cft_mem ls_js_virtual_cft^ ls_full_js_virtual_cft^ ls_full_js_sgx_cft^ ls_full_js_sgx_cft_mem ls_js_jwt_virtual_cft^ 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)^
75512 20230906.30 0.76505 16562.3 1.88908e+07 16793 1.05021e+07 18126.9 1.46964e+07 32434.9 2.51822e+07 43550.9 47547.7 53832.8 1630.9 1.25993e+07 81031.5 8168.32 1.88908e+07 4434.5 8029.9 6.30784e+06 17008.1 19075.6 6661.84 1.67936e+07 17268 15090.2 6624.43 1.67936e+07 9996.6 4540.36 1.67936e+07 43872.9 836168 1.17847e+06 8.15624e+06 3.076e+07
75569 20230907.19 0.806743 16743.8 1.88908e+07 16929.4 1.05021e+07 18426.3 1.46964e+07 32257.2 2.51822e+07 45513 48328.8 54323.2 1656 1.25993e+07 76369.3 8189.3 1.88908e+07 4466.7 8271.6 6.30784e+06 17321.1 19262.3 7052.15 1.67936e+07 17576.6 14865.5 6645.08 1.67936e+07 9889.6 4561.37 1.88908e+07 47193.3 832235 1.17292e+06 8.13512e+06 3.14622e+07
75575 20230907.21 0.817632 16954.1 1.88908e+07 16921.4 1.05021e+07 18526.6 1.46964e+07 32351.6 2.51822e+07 43726.4 47520.6 53784.1 1658.9 1.25993e+07 71527.6 8205.39 1.88908e+07 4470.1 8254 6.30784e+06 17119.5 19767.9 7123.09 1.67936e+07 17574.9 14823.8 6602.13 1.67936e+07 10069.1 4554.46 1.88908e+07 44888 831823 1.18253e+06 8.15277e+06 3.23815e+07

images

@lemmy
Copy link
Contributor Author

lemmy commented Sep 6, 2023

node->second.sent_idx = std::max(this_match, node->second.match_idx);

This fails thesuffix_collision.2 raft scenario.


The test failure appears to be a liveness issue s.t. n[0] fails to repair its log (added custom logging to raft.h and several periodic_all,100 dispatch_all at the end of suffix_collision.2):

{"h_ts":"728","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 4, r.last_log_idx 8"}
{"h_ts":"777","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 4, matchIndex 0, sent_idx 12, r.term 1, r.last_log_idx 8"}
{"h_ts":"780","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 4, r.term 4, r.last_log_idx 8"}
{"h_ts":"783","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 8, r.term 4, r.last_log_idx 8"}
{"h_ts":"834","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 4, matchIndex 0, sent_idx 12, r.term 1, r.last_log_idx 8"}
{"h_ts":"837","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 4, r.term 4, r.last_log_idx 8"}
{"h_ts":"840","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 8, r.term 4, r.last_log_idx 8"}
{"h_ts":"891","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 4, matchIndex 0, sent_idx 12, r.term 1, r.last_log_idx 8"}
{"h_ts":"894","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 4, r.term 4, r.last_log_idx 8"}
{"h_ts":"897","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 8, r.term 4, r.last_log_idx 8"}
{"h_ts":"1011","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 5, r.last_log_idx 8"}
{"h_ts":"1121","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 6, r.last_log_idx 8"}
{"h_ts":"1231","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 7, r.last_log_idx 8"}
{"h_ts":"1341","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 8, r.last_log_idx 8"}
{"h_ts":"1451","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 9, r.last_log_idx 8"}
{"h_ts":"1561","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 10, r.last_log_idx 8"}
{"h_ts":"1671","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 11, r.last_log_idx 8"}
{"h_ts":"1781","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 12, r.last_log_idx 8"}
{"h_ts":"1891","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 13, r.last_log_idx 8"}
{"h_ts":"2001","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 14, r.last_log_idx 8"}
{"h_ts":"2111","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 15, r.last_log_idx 8"}
{"h_ts":"2221","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 16, r.last_log_idx 8"}
{"h_ts":"2331","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 17, r.last_log_idx 8"}
{"h_ts":"2441","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 18, r.last_log_idx 8"}
{"h_ts":"2551","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 19, r.last_log_idx 8"}
{"h_ts":"2661","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 20, r.last_log_idx 8"}
{"h_ts":"2771","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[2] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 21, r.last_log_idx 8"}
{"h_ts":"2881","thread_id":"100","level":"debug","tag":"raft","file":"../src/consensus/aft/raft.h","number":"1446","msg":"n[1] | Leader | Active | Recv append entries response from n[0] with possible match 8, matchIndex 0, sent_idx 12, r.term 22, r.last_log_idx 8"}

Hypothesis: The NACK should include the prevLogIndex from the AE request instead of n[0]'s highest possible match.

@eddyashton
Copy link
Member

suffix_collision.2 is failing because we process multiple NACKs in a row, and discard a helpful/correct sent_idx with a still-too-late estimate from the later NACK.

(slightly modified logging)

# [1] sends [0] 2 append entries
2023-09-07T09:28:49.027466Z        100 [debug][raft] ./src/consensus/aft/raft.h:907 | n[1] | Leader | Active | Send append entries from n[1] to n[0]: (2.8, 3.10] (12)
2023-09-07T09:28:49.027472Z        100 [debug][raft] ./src/consensus/aft/raft.h:907 | n[1] | Leader | Active | Send append entries from n[1] to n[0]: (3.10, 4.12] (12)

# [0] says "What is this 2.8? I can't append to that. I have a thing called 1.8"
2023-09-07T09:28:49.027517Z        100 [debug][raft] ./src/consensus/aft/raft.h:959 | n[0] | Follower | Active | Received append entries: 2.8 to 3.10 (from n[1] in term 4)
2023-09-07T09:28:49.027520Z        100 [debug][raft] /src/consensus/aft/raft.h:1005 | n[0] | Follower | Active | Previous term for 8 should be 1
2023-09-07T09:28:49.027524Z        100 [debug][raft] /src/consensus/aft/raft.h:1028 | n[0] | Follower | Active | Recv append entries to n[0] from n[1] but our log at 8 has the wrong previous term (ours: 1, theirs: 2)
2023-09-07T09:28:49.027529Z        100 [debug][raft] /src/consensus/aft/raft.h:1321 | n[0] | Follower | Active | Send append entries response from n[0] to n[1] for entry 1.8: 1

# [0] says "What is this 3.10? I can't append to that. I have a thing called 2.8"
2023-09-07T09:28:49.027537Z        100 [debug][raft] ./src/consensus/aft/raft.h:959 | n[0] | Follower | Active | Received append entries: 3.10 to 4.12 (from n[1] in term 4)
2023-09-07T09:28:49.027542Z        100 [debug][raft] /src/consensus/aft/raft.h:1005 | n[0] | Follower | Active | Previous term for 10 should be 0
2023-09-07T09:28:49.027548Z        100 [debug][raft] /src/consensus/aft/raft.h:1016 | n[0] | Follower | Active | Recv append entries to n[0] from n[1] but our log does not yet contain index 10
2023-09-07T09:28:49.027554Z        100 [debug][raft] /src/consensus/aft/raft.h:1321 | n[0] | Follower | Active | Send append entries response from n[0] to n[1] for entry 4.8: 1

# [1] reads the first NACK, and (correctly) works out that maybe they have 1.4 in common, and should send from there
2023-09-07T09:28:49.027602Z        100 [debug][raft] /src/consensus/aft/raft.h:1436 | n[1] | Leader | Active | Recv append entries response to n[1] from n[0]: failed
2023-09-07T09:28:49.027607Z        100 [debug][raft] /src/consensus/aft/raft.h:1445 | n[1] | Leader | Active | Processing NACK, with this_match=4 and match_idx=0, I've updated sent_idx to 4

# [2] reads the second NACK, and overwrites 1.4 with the (plausible but less precise) 2.8
2023-09-07T09:28:49.027614Z        100 [debug][raft] /src/consensus/aft/raft.h:1436 | n[1] | Leader | Active | Recv append entries response to n[1] from n[0]: failed
2023-09-07T09:28:49.027619Z        100 [debug][raft] /src/consensus/aft/raft.h:1445 | n[1] | Leader | Active | Processing NACK, with this_match=8 and match_idx=0, I've updated sent_idx to 8

# Repeat ad infinitum
2023-09-07T09:28:49.027672Z        100 [debug][raft] ./src/consensus/aft/raft.h:907 | n[1] | Leader | Active | Send append entries from n[1] to n[0]: (2.8, 3.10] (12)
2023-09-07T09:28:49.027678Z        100 [debug][raft] ./src/consensus/aft/raft.h:907 | n[1] | Leader | Active | Send append entries from n[1] to n[0]: (3.10, 4.12] (12)

Since we send optimistically-late AEs, we may receive later-than-precise NACKs, and shouldn't advance sent_idx for those.

@eddyashton
Copy link
Member

eddyashton commented Sep 7, 2023

There are many Safe assignments we can make to next_idx, and we're trying to find one of those which is also best for Liveness.

As a thought experiment, consider a primary trying to catch up a follower within the same term, where each AE contains only a single entry.

P:  1  2  3  4  5
B:  1

# Possible messages
AE(2)  AE(3)  AE(4)  AE(5)

# If B receives any-but-the-first, it emits a corresponding NACK, so other possible messages are
ACK(2) NACK(3)  NACK(4)  NACK(5)

# Since P has a match_index of 1, and could receive any of these NACKs, it is _Safe_ to assign sent_idx to any of these
# (ie - there is a valid path that led here, so maybe we can hallucinate our way there from anywhere)
# So we could assign any of these
sent_idx=2 sent_idx=3  sent_idx=4  sent_idx=5

# I see the min(sent_idx) behaviour as a Liveness choice amongst those.
# We'd prefer to keep the lower value, since that tends-towards a smaller set of messages (assuming non-infinite duplication)

# The observation that match_index is a lower-bound is true
# It gets us out of another liveness hole if we have infinite message duplication
# Imagine P processes ACK(2), and then ACK(3), and then ACK(4)
P: 1  2  3  4  5
B: 1  2  3

P.sent_idx[B] = 4

# (I think you can get here _once_ with just delayed/out-of-order delivery, but to return here _permanently_ I think
# you need infinite message duplication? A very weak claim)

# However, NACK(3) is still a potential message from earlier!
# If it arrives now, and is processed by P (under the existing code), then we unnecessarily (Safely, but unLively) decrement sent_idx!
# Using match_idx as a lower-bound avoids decrementing it too-far.
# But to handle out-of-order NACKs, we should then use the previous sent_idx as an upper-bound.

We are able to test some liveness scenarios with the scenario driver, but we don't simulate message duplication or re-ordering there. So I don't think we can create a test that proves the benefit of this new lower-bound, but believe it is worth adding.

@eddyashton
Copy link
Member

eddyashton commented Sep 7, 2023

This change uses both bounds, and passes the tests I've tried:

node->second.sent_idx = std::max(
          std::min(this_match, node->second.sent_idx), node->second.match_idx);

I also understand some of the confusion around the +1:
I'm sure we don't want it. We're storing sent_idx, where the Raft paper and spec talks about nextIndex. These obviously differ by +1 ("what is the last thing I think I sent you" is exactly 1 less than "what is the next thing I should send you"), and we find next_index when constructing AEs:

  send_append_entries(it.first, it.second.sent_idx + 1);

Our spec also uses nextIndex.

So sentIndex, if we represented that in the spec

  • could be 0 (when we've not sent them anything yet), and
  • could equal matchIndex (in lots of stable states it does - you're up-to-date and match at the last thing I sent you).

That differs from nextIndex, which

  • must be positive (earliest thing I can send you is entry 1, 0 doesn't exist), and
  • is strictly greater than matchIndex (I'll never resend you something I know you know).

Gluing that all together, I think that the spec change to match my proposed implementation assignment above, would be:

nextIndex' = [nextIndex EXCEPT ![i][j] = max(min(tm, nextIndex[i][j]), matchIndex[i][j]) + 1 ]

@achamayou
Copy link
Member

We are able to test some liveness scenarios with the scenario driver, but we don't simulate message duplication or re-ordering there. So I don't think we can create a test that proves the benefit of this new lower-bound, but believe it is worth adding.

shuffle_one and shuffle_all do some re-ordering, but to trigger this particular case, you're right that we would need further extensions.

The slightly improved nextIndex calculation does seem worth adding, I agree.

@lemmy lemmy force-pushed the mku-pr5341impl branch 3 times, most recently from 725f932 to 64fb336 Compare September 7, 2023 18:37
@lemmy lemmy marked this pull request as ready for review September 8, 2023 00:56
@lemmy lemmy requested a review from a team September 8, 2023 00:56
@achamayou achamayou merged commit 98206da into main Sep 8, 2023
24 checks passed
@achamayou achamayou deleted the mku-pr5341impl branch September 8, 2023 06:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
consensus tla TLA+ specifications
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants