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

matchIndex lower bound for nextIndex #5614

Merged
merged 4 commits into from
Sep 6, 2023
Merged

matchIndex lower bound for nextIndex #5614

merged 4 commits into from
Sep 6, 2023

Conversation

lemmy
Copy link
Contributor

@lemmy lemmy commented Sep 5, 2023

@lemmy lemmy added the tla TLA+ specifications label Sep 5, 2023
@lemmy lemmy requested a review from a team September 5, 2023 04:35
@ghost
Copy link

ghost commented Sep 5, 2023 •
edited by ghost
Loading

mku-pr5341@75418 aka 20230905.42 vs main ewma over 20 builds from 75075 to 75413

Click to see table

main

build_id build_number pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem 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_js_sgx_cft^ pi_basic_js_sgx_cft_mem pi_basic_mt_virtual_cft^ 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_virtual_cft^ 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_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_js_virtual_cft^ ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^ hist_sgx_cft^ RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^
75075 20230830.2 31443.3 2.51822e+07 0.83702 16563.8 1.88908e+07 16654.7 1.05021e+07 18189.3 1.46964e+07 1657.2 1.25993e+07 86648.2 8167.29 1.88908e+07 8230.5 6.30784e+06 7047.25 1.67936e+07 43456.6 46733.1 52213.1 6593.9 1.67936e+07 4398.3 4554.07 1.88908e+07 17014 19070.9 17062.6 16817.8 9974.4 45484.8 826908 1.18068e+06 8.15254e+06 3.11507e+07
75118 20230830.13 31938.4 2.51822e+07 0.795668 16491 1.88908e+07 16680 1.05021e+07 18051 1.46964e+07 1663.1 1.25993e+07 72874.4 8112.14 1.88908e+07 7954.1 6.30784e+06 7033.9 1.67936e+07 45593.2 48059.4 52813.5 6580.25 1.67936e+07 4457.8 4552.79 1.88908e+07 17349.4 20106.6 17373.9 14942.4 9804.35 47358.5 832726 1.18129e+06 8.14764e+06 3.08745e+07
75138 20230831.1 31562.4 2.51822e+07 0.773449 16645.3 1.88908e+07 16771.3 1.05021e+07 18311.5 1.46964e+07 1663 1.25993e+07 79560.7 8210.87 1.88908e+07 8101.1 6.30784e+06 7084.23 1.67936e+07 43630.2 47411.3 52119.9 6583.37 1.67936e+07 4397.6 4562.01 1.88908e+07 17082.2 19267.5 17317.9 14683.8 10262.5 44903.6 830487 1.17891e+06 8.16955e+06 3.07873e+07
75147 20230831.5 31681.2 2.51822e+07 0.8359 16620.2 1.88908e+07 16630.1 1.05021e+07 18144.9 1.46964e+07 1666.7 1.25993e+07 81401.7 8196.8 1.88908e+07 8057.8 6.30784e+06 7048.63 1.67936e+07 45573.1 48177.4 52131.9 6608.94 1.67936e+07 4405.6 4562.55 1.88908e+07 17303.2 19827.5 17369.8 14758.6 9891.05 41701.5 830948 1.18148e+06 8.15446e+06 3.0816e+07
75161 20230831.13 31568.6 2.51822e+07 0.81577 16612.1 1.88908e+07 16689.8 1.05021e+07 18176.9 1.46964e+07 1662.5 1.25993e+07 76022.4 8177.4 1.88908e+07 8247.9 6.30784e+06 7057.42 1.67936e+07 45571.9 47766.7 53718.3 6656.13 1.67936e+07 4503 4592.61 1.88908e+07 17400.8 19874 17702.4 14986 9882.54 45490.8 835212 1.18234e+06 8.14249e+06 3.10944e+07
75179 20230901.1 31914.7 2.51822e+07 0.797232 16579.7 1.88908e+07 16750.6 1.05021e+07 18260.6 1.46964e+07 1651.5 1.25993e+07 71122.1 8210.63 1.88908e+07 8323.5 6.30784e+06 7118.74 1.67936e+07 45657.3 47855.8 53488.1 6616.41 1.67936e+07 4495.8 4612.34 1.88908e+07 17477.4 19934.6 17505.9 16835.2 9785.78 41584.1 825699 1.17706e+06 8.1735e+06 3.05134e+07
75187 20230901.5 31852.3 2.51822e+07 0.766884 16587 1.88908e+07 16666.6 1.05021e+07 18204.9 1.46964e+07 1664.1 1.25993e+07 76743.7 8202.09 1.88908e+07 8078 6.30784e+06 6682.26 1.67936e+07 45662.6 48325.3 53440.6 6598.69 1.67936e+07 4512.9 4583.19 1.88908e+07 17221 19316.2 17486.5 14957.1 9967.15 45560.3 827788 1.17683e+06 8.15403e+06 3.07134e+07
75221 20230901.20 32113.1 2.51822e+07 0.806705 16540.9 1.88908e+07 16657.1 1.05021e+07 18199.7 1.25993e+07 1658.8 1.25993e+07 67827.1 8186.95 1.88908e+07 8391.7 6.30784e+06 7065.59 1.67936e+07 45841.2 46657 51767.4 6636.06 1.67936e+07 4441.4 4580.72 1.88908e+07 17067.9 19837.3 17273 14959.9 9904.99 45518.4 836676 1.1816e+06 8.10531e+06 3.06734e+07
75234 20230901.26 31298.5 2.51822e+07 0.799024 16412 1.88908e+07 16520.2 1.05021e+07 18034.1 1.46964e+07 1640.1 1.25993e+07 81323.7 8046.24 1.88908e+07 7975.8 6.30784e+06 6617.55 1.67936e+07 45763 48415.1 52445.3 6583.32 1.67936e+07 4461.9 4562.49 1.88908e+07 17320.3 19267.1 17307.8 16727 9900.84 47832.7 814140 1.17862e+06 8.11427e+06 3.09824e+07
75255 20230904.2 31877.2 2.51822e+07 0.800459 16585.1 1.88908e+07 16649.8 1.05021e+07 18179.8 1.46964e+07 1659.1 1.25993e+07 70284.9 8133.32 1.88908e+07 8318.8 6.30784e+06 7070.58 1.67936e+07 45618.4 47656 52809.9 6589.49 1.67936e+07 4482.3 4555.83 1.88908e+07 17231.3 19040.4 15210.2 16875 9795.68 50413 834549 1.18199e+06 8.15296e+06 3.13879e+07
75265 20230904.6 31457.4 2.51822e+07 0.797237 16561.7 1.88908e+07 16683.7 1.05021e+07 18219.1 1.46964e+07 1658 1.25993e+07 63213.7 8180.61 1.88908e+07 8300.5 6.30784e+06 7057.78 1.67936e+07 45627.4 48343.5 52792.7 6644.72 1.67936e+07 4465.8 4583.56 1.88908e+07 17315 19935.4 17552.3 15100.5 9851.17 45461.7 831805 1.17771e+06 8.15034e+06 3.12653e+07
75271 20230904.8 32193.1 2.51822e+07 0.807553 16703.8 1.88908e+07 16797.4 1.05021e+07 18353.3 1.46964e+07 1655.8 1.25993e+07 78961.1 8200.03 1.88908e+07 8097.4 6.30784e+06 7074.81 1.67936e+07 45699.4 48066.8 54336.2 6593.84 1.67936e+07 4468.2 4556.21 1.88908e+07 17313.8 19411.1 16926.8 14815 9820.68 45397.8 839817 1.18163e+06 8.15446e+06 3.10369e+07
75282 20230904.12 31979.1 2.51822e+07 0.796235 16694.9 1.88908e+07 16916.6 1.05021e+07 18325.5 1.46964e+07 1648.6 1.25993e+07 79345.1 8156.02 1.88908e+07 7968.6 6.30784e+06 7040.55 1.67936e+07 45690.9 49077.3 54125.9 6637.16 1.67936e+07 4479.4 4557.13 1.88908e+07 17623.4 16298.1 17113.3 14553.5 9824.1 48180.1 834932 1.18089e+06 8.15433e+06 3.07392e+07
75288 20230904.14 32335.9 2.51822e+07 0.801078 16679.2 1.88908e+07 16871.4 1.05021e+07 18477.5 1.46964e+07 1656.9 1.25993e+07 80429.9 8152.93 1.88908e+07 8019.1 6.30784e+06 7036.64 1.67936e+07 45797.3 47838.9 53668.7 6584.04 1.67936e+07 4491.1 4551.27 1.88908e+07 17414.1 19684.7 17347 14843.7 9878.27 44845.8 830898 1.18237e+06 8.1505e+06 3.0772e+07
75300 20230905.1 32207.2 2.51822e+07 0.770774 16645.6 1.88908e+07 16823.7 1.05021e+07 18313.7 1.46964e+07 1652.3 1.25993e+07 79372.1 8180.27 1.88908e+07 8177 6.30784e+06 7051.17 1.67936e+07 45506.3 48842.4 53087.4 6596.68 1.67936e+07 4485.3 4571.26 1.88908e+07 17474.3 19306.5 17442.8 15046.5 9898.89 50271.9 821926 1.1746e+06 8.1143e+06 3.17018e+07
75314 20230905.8 32224.6 2.51822e+07 0.820898 16738.7 1.88908e+07 16868.1 1.05021e+07 18392.4 1.46964e+07 1648.2 1.25993e+07 71193 8201.26 1.88908e+07 8305.8 6.30784e+06 7067.89 1.67936e+07 45656.7 48164.7 53451 6593.78 1.67936e+07 4387.1 4587.48 1.88908e+07 17378.6 19385.9 17350.5 14763.3 10113.2 45347.1 830368 1.17868e+06 8.15579e+06 3.08615e+07
75332 20230905.15 32237.6 2.51822e+07 0.795074 16686.1 1.88908e+07 16806.5 1.05021e+07 18374.4 1.46964e+07 1663.1 1.25993e+07 73261.1 8145.3 1.88908e+07 8056.1 6.30784e+06 7062.03 1.67936e+07 45805 48010.4 53472.6 6644.82 1.67936e+07 4468.6 4549.04 1.88908e+07 17303.8 19203.1 17495.4 14979.2 9760 47860 830160 1.17693e+06 8.15631e+06 3.07813e+07
75348 20230905.21 31697 2.51822e+07 0.818926 16897 1.88908e+07 16860.5 1.05021e+07 18475.4 1.46964e+07 1657.2 1.25993e+07 69941.9 8211.83 1.88908e+07 8045.4 6.30784e+06 7058.49 1.67936e+07 45750.9 48204.9 52524 6594.25 1.67936e+07 4466 4559.4 1.88908e+07 17413.2 19456.4 17519 15001.3 10200.3 43975.4 820294 1.17696e+06 8.17128e+06 3.07581e+07
75360 20230905.26 32429.6 2.51822e+07 0.800555 16639.2 1.88908e+07 16865.9 1.05021e+07 18094.7 1.46964e+07 1629.4 1.25993e+07 75493.7 8097.92 1.88908e+07 8244.9 6.30784e+06 6577.72 1.67936e+07 45554.4 42866.8 51334.5 6573.38 1.67936e+07 4480 4545.58 1.67936e+07 17462.1 19193.1 16930.1 15179.2 9898.05 47617.4 834158 1.17952e+06 8.1542e+06 3.0816e+07
75413 20230905.41 32149.1 2.51822e+07 0.822033 16619.4 1.88908e+07 16634.2 1.05021e+07 18150.8 1.46964e+07 1640.4 1.25993e+07 84700.2 8128.27 1.88908e+07 7918 6.30784e+06 6668.1 1.67936e+07 42002.8 47678.8 53684.4 6561.8 1.67936e+07 4426.7 4544.2 1.67936e+07 17180.1 19169.9 17447.2 14839.1 10272.6 46378.9 831657 1.18593e+06 8.15381e+06 3.25544e+07

mku-pr5341

build_id build_number pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem pi_basic_mt_virtual_cft^ Commit latency factor ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ pi_basic_js_virtual_cft^ ls_sgx_cft^ ls_sgx_cft_mem pi_ls_sgx_cft^ pi_ls_sgx_cft_mem ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ pi_basic_sgx_cft^ pi_basic_sgx_cft_mem ls_js_virtual_cft^ ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^ 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 hist_sgx_cft^ ls_full_js_sgx_cft^ ls_full_js_sgx_cft_mem ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^
75309 20230905.5 32015.1 2.51822e+07 74033.9 0.774266 45733.7 48755.3 53225.7 4500.4 16820.1 1.88908e+07 16811.4 1.05021e+07 17308.9 20107 18355.1 1.46964e+07 17085.6 15359.1 9866.83 1652.7 1.25993e+07 8143.01 1.88908e+07 8251.6 6.30784e+06 7050.1 1.67936e+07 46529.9 6638.35 1.67936e+07 4553.45 1.88908e+07 840293 1.17861e+06 8.15222e+06 3.08341e+07
75396 20230905.36 32002 2.51822e+07 62428.6 0.80431 46050.6 48841.2 53432.2 4464 16703.9 1.88908e+07 16687.7 1.05021e+07 17427.3 19690.5 18197.6 1.46964e+07 16996.9 14964.8 9869.05 1635 1.25993e+07 8126.74 1.88908e+07 7972.1 6.30784e+06 6619.62 1.67936e+07 46302.9 6634.75 1.67936e+07 4560.15 1.88908e+07 835079 1.17402e+06 8.15485e+06 3.18834e+07
75418 20230905.42 31896.6 2.51822e+07 73632.9 0.804662 45990.7 47779.5 54696.2 4494.2 16915.4 1.88908e+07 16869.2 1.05021e+07 17185.9 19810.6 18383.3 1.25993e+07 17105.6 14819.9 9796.48 1649.7 1.25993e+07 8196.6 1.88908e+07 8302.2 6.30784e+06 7044.31 1.67936e+07 46002.3 6594 1.67936e+07 4559.26 1.88908e+07 828097 1.17462e+06 8.13467e+06 3.07392e+07

images

heidihoward
heidihoward reviewed Sep 5, 2023
View reviewed changes
tla/ccfraft.tla
@@ -950,8 +952,7 @@ HandleAppendEntriesResponse(i, j, m) ==
/\ nextIndex' = [nextIndex EXCEPT ![i][j] = max(@, m.lastLogIndex + 1)]
\/ /\ \lnot m.success \* not successful
/\ LET tm == FindHighestPossibleMatch(log[i], m.lastLogIndex, m.term)
IN nextIndex' = [nextIndex EXCEPT ![i][j] =
(IF matchIndex[i][j] = 0 THEN tm ELSE min(tm, matchIndex[i][j])) + 1 ]
IN nextIndex' = [nextIndex EXCEPT ![i][j] = max(tm, matchIndex[i][j]) + 1 ]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Using the matchIndex as a lower bound for the nextIndex makes sense to me. Does this match the implementation?

Copy link
Contributor Author

@lemmy lemmy Sep 5, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No:

CCF/src/consensus/aft/raft.h

Lines 1437 to 1440 in 2fbf878

const auto this_match =
find_highest_possible_match({r.term, r.last_log_idx});
node->second.sent_idx = std::min(this_match, node->second.sent_idx);
return;

which is Fix A described in #5341 (comment):

  /\ LET tm == FindHighestPossibleMatch(log[i], m.lastLogIndex, m.term)
             IN nextIndex' = [nextIndex EXCEPT ![i][j] = min(@, tm) ]

@lemmy lemmy enabled auto-merge (rebase) September 6, 2023 16:52
@lemmy lemmy disabled auto-merge September 6, 2023 16:52
@lemmy lemmy enabled auto-merge (squash) September 6, 2023 16:53
@lemmy lemmy disabled auto-merge September 6, 2023 17:15
@lemmy lemmy merged commit 4a7c951 into main Sep 6, 2023
19 of 21 checks passed
@lemmy lemmy deleted the mku-pr5341 branch September 6, 2023 17:28
@lemmy
Copy link
Contributor Author

lemmy commented Sep 6, 2023

Merged because the build failures were unrelated.

@lemmy lemmy mentioned this pull request Sep 6, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@heidihoward heidihoward heidihoward 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.
2 participants
@lemmy @heidihoward