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

Validate the successor state *after* defining it #5797

Merged
merged 5 commits into from
Oct 31, 2023
Merged

Validate the successor state *after* defining it #5797

merged 5 commits into from
Oct 31, 2023

Conversation

lemmy
Copy link
Contributor

@lemmy lemmy commented Oct 30, 2023 •
edited
Loading

@lemmy lemmy requested a review from a team October 30, 2023 15:44
@lemmy lemmy added the tla TLA+ specifications label Oct 30, 2023
@lemmy lemmy added this to the TLA+ Trace Validation milestone Oct 30, 2023
@lemmy lemmy enabled auto-merge (squash) October 30, 2023 15:45
@lemmy lemmy disabled auto-merge October 30, 2023 15:56
@lemmy lemmy enabled auto-merge (rebase) October 30, 2023 15:56
@lemmy lemmy force-pushed the mku-defineThenMatch branch from 83ce880 to 36f3890 Compare October 30, 2023 16:02
@ghost
Copy link

ghost commented Oct 30, 2023 •
edited by ghost
Loading

mku-defineThenMatch@78141 aka 20231031.14 vs main ewma over 20 builds from 77532 to 78128

Click to see table

main

build_id build_number pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem Commit latency factor pi_basic_mt_virtual_cft^ tpcc_sgx_cft^ tpcc_sgx_cft_mem tpcc_virtual_cft^ ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ ls_sgx_cft^ ls_sgx_cft_mem pi_ls_sgx_cft^ pi_ls_sgx_cft_mem pi_basic_js_virtual_cft^ pi_basic_sgx_cft^ pi_basic_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^ 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)^
77532 20231020.31 27967.5 2.51822e+07 0.835073 60943.5 5614.22 8.59996e+07 17092.6 43713.6 47796.6 52609.1 14001.1 1.88908e+07 14174.9 1.05021e+07 4332.3 15520.9 1.46964e+07 17195.4 19336.7 17022.6 14750.8 10188.5 1429.6 1.25993e+07 7252.76 1.67936e+07 7086.5 6.30784e+06 5806.4 1.67936e+07 40351.5 5491.29 1.67936e+07 4001.82 1.67936e+07 833120 1.18235e+06 8.17343e+06 3.12829e+07
77555 20231023.5 28238.2 2.51822e+07 0.816011 74767.3 5639.66 8.59996e+07 17264.2 45924.9 47674 53843.3 14029.3 1.88908e+07 14118.1 1.05021e+07 4365.2 15640.2 1.46964e+07 17152.3 19152.3 17286.3 14910.6 10169.6 1432.7 1.25993e+07 7273.33 1.67936e+07 6953.5 6.30784e+06 5781.01 1.67936e+07 43068.6 5742.5 1.67936e+07 3995.51 1.67936e+07 829052 1.18151e+06 8.148e+06 3.09408e+07
77584 20231023.15 27775.2 2.51822e+07 0.839543 63643 5525.06 8.59996e+07 17237.3 43785.4 47940.2 54114.3 13936 1.88908e+07 13990.4 1.05021e+07 4430 15424.6 1.46964e+07 17010.7 19396.4 17307.2 14810.6 9823.55 1427 1.25993e+07 6853.5 1.88908e+07 6881.2 6.30784e+06 5758.93 1.67936e+07 42679.4 5762.09 1.67936e+07 3983.52 1.67936e+07 825381 1.18095e+06 8.16893e+06 3.13159e+07
77665 20231024.10 28077.5 2.30851e+07 0.782853 71956.1 5565 8.59996e+07 17332.4 43627.5 47460.4 55764.1 13918.6 1.88908e+07 14015.8 1.05021e+07 4480.7 15439.4 1.46964e+07 16984.5 19600.5 17210.4 15032.4 9934.79 1417.5 1.25993e+07 6827.52 1.88908e+07 6933.8 6.30784e+06 5759.87 1.67936e+07 42277.7 5778.73 1.67936e+07 3994.77 1.67936e+07 837727 1.17659e+06 8.1335e+06 3.08424e+07
77722 20231024.29 28002.9 2.51822e+07 0.808583 68825.6 5477.83 8.59996e+07 17482.9 43910 47389.3 55105.8 13980.7 1.88908e+07 14011.7 1.05021e+07 4422.3 15103.3 1.46964e+07 16897.2 19100.4 17082.1 15051.5 9901.25 1409.7 1.25993e+07 6842.46 1.88908e+07 6811.8 6.30784e+06 5772.89 1.67936e+07 43837.6 5489.45 1.67936e+07 4013.18 1.67936e+07 824014 1.17985e+06 8.16421e+06 3.03628e+07
77856 20231025.44 27880.1 2.30851e+07 0.830072 84849.8 5666.89 8.59996e+07 17303.7 45783 47925.3 54083.6 14118.2 1.88908e+07 14176.7 1.05021e+07 4428.6 15508.7 1.46964e+07 17130.6 18998.8 17531.7 14906.9 9965.7 1425.1 1.25993e+07 7259.6 1.67936e+07 6931.4 6.30784e+06 5816.26 1.67936e+07 44821 5714.88 1.67936e+07 3996.87 1.67936e+07 832615 1.17692e+06 8.17447e+06 3.1229e+07
77900 20231025.59 27968.9 2.30851e+07 0.816541 81852.5 5546.67 8.59996e+07 17281.4 45862.6 47692.2 54378.7 13948.6 1.88908e+07 14105.4 1.05021e+07 4430.3 15469.3 1.46964e+07 17128.6 18994.4 17211.3 14724.7 9880.77 1430.1 1.25993e+07 6806.65 1.88908e+07 6880.7 6.30784e+06 5770.88 1.67936e+07 42489.7 5488.27 1.88908e+07 3990.38 1.67936e+07 839143 1.18218e+06 8.15475e+06 3.09642e+07
77909 20231025.62 27790.9 2.30851e+07 0.79592 82618.8 5576.25 8.59996e+07 17614.6 45746.3 48128.1 53844.8 13953.5 1.88908e+07 13887.2 1.05021e+07 4388 15385.2 1.25993e+07 17161.3 19081.4 17522.5 14627.1 10342.4 1410.9 1.25993e+07 6741.99 1.88908e+07 6827.9 6.30784e+06 5792.34 1.67936e+07 43740.4 5446.53 1.67936e+07 3975.81 1.67936e+07 830943 1.17967e+06 8.14732e+06 3.07715e+07
77921 20231026.3 27942.2 2.30851e+07 0.791384 72066.7 5619.54 8.80968e+07 17373 45699.4 48314.8 54188.2 14116.6 1.88908e+07 14237.9 1.05021e+07 4351.5 15679.6 1.25993e+07 17286.9 19246.7 17012.1 14641.1 10204.5 1439.5 1.25993e+07 6842.16 1.67936e+07 7086.5 6.30784e+06 5774.21 1.67936e+07 44491.1 5775.45 1.67936e+07 3999.2 1.67936e+07 835419 1.1779e+06 8.15017e+06 3.23452e+07
77958 20231026.14 27891.3 2.30851e+07 0.772274 68096.1 5566.37 8.59996e+07 17260.9 45673.6 48273.7 54086 14074.9 1.88908e+07 14198.3 1.05021e+07 4383.2 15598.1 1.46964e+07 17108.5 19101.5 17286.3 14984.8 10377.2 1432.2 1.25993e+07 6840.93 1.67936e+07 6965.9 6.30784e+06 5777.94 1.67936e+07 43732 5783.74 1.67936e+07 3984.61 1.67936e+07 834153 1.18014e+06 8.15037e+06 3.08165e+07
77980 20231026.23 27919.7 2.30851e+07 0.799401 84229.4 5544.83 8.59996e+07 17301.4 45630 47959.1 54124.7 13945.1 1.88908e+07 14005.8 1.05021e+07 4420.8 15441 1.25993e+07 17150.6 19602.5 17059.4 14690.5 9850.2 1419.8 1.25993e+07 7232.3 1.67936e+07 6917.8 6.30784e+06 5811.09 1.67936e+07 42472.7 5487 1.67936e+07 4003.14 1.67936e+07 827669 1.18001e+06 8.13674e+06 3.08104e+07
77994 20231026.29 27941.4 2.51822e+07 0.80113 82095.1 5582.56 8.59996e+07 17290 43873.2 47649.7 54065 14017.2 1.88908e+07 14167 1.05021e+07 4441.8 15610.3 1.25993e+07 17136.7 19419.7 17733.8 16838 9840.75 1446 1.25993e+07 6841.03 1.88908e+07 6962.5 6.30784e+06 5764.66 1.67936e+07 44959.6 5729.26 1.67936e+07 4003.36 1.67936e+07 840437 1.18274e+06 8.15494e+06 3.07517e+07
78007 20231026.34 27449.9 2.51822e+07 0.765143 81427 5628.96 8.59996e+07 17307 45407.5 47735 54044.5 14025.1 1.88908e+07 14089.7 1.05021e+07 4441.4 15601.5 1.46964e+07 17288.5 18904.7 17015.3 16872.1 9816.73 1432.4 1.25993e+07 6850.52 1.88908e+07 7096.8 6.30784e+06 5773.88 1.67936e+07 43179.9 5486.07 1.67936e+07 3985.52 1.67936e+07 826445 1.17834e+06 8.14738e+06 3.19605e+07
78033 20231027.4 28127.4 2.51822e+07 0.798824 65638.2 5577.93 8.59996e+07 17273 45862.4 48024.5 53817.4 13972.7 1.88908e+07 14096.8 1.05021e+07 4439.6 15447.2 1.25993e+07 17160.1 19602.8 17044.2 16883.5 9854.32 1432.2 1.25993e+07 7250.65 1.67936e+07 6938.4 6.30784e+06 5786.4 1.67936e+07 42046.2 5743.72 1.67936e+07 4002.74 1.67936e+07 829984 1.18448e+06 8.13813e+06 3.06775e+07
78035 20231027.5 27938.3 2.51822e+07 0.785967 83501.4 5573.65 8.59996e+07 17213.8 45970.2 48037.9 54501.8 14007.5 1.88908e+07 14114.5 1.05021e+07 4447.9 15503.3 1.46964e+07 17062.2 19333.8 16911.6 17015.7 9990.67 1434.7 1.25993e+07 6832.63 1.67936e+07 6983.9 6.30784e+06 5786.59 1.67936e+07 47144 5775.4 1.67936e+07 3982.36 1.67936e+07 831267 1.18066e+06 8.09742e+06 3.06715e+07
78049 20231027.10 28049.5 2.51822e+07 0.781085 85552.5 5504.64 8.59996e+07 17300.2 43575 46933.4 55026 14023.9 1.88908e+07 14102.3 1.05021e+07 4431 15421.6 1.46964e+07 17056.6 19111.7 17359 14869.3 9805.16 1424.4 1.25993e+07 6846.42 1.67936e+07 6826.6 6.30784e+06 5791.73 1.67936e+07 41017.4 5707.49 1.67936e+07 3980.86 1.67936e+07 840517 1.18098e+06 8.16672e+06 3.06803e+07
78065 20231030.3 27850.6 2.30851e+07 0.803529 80986.2 5645.18 8.59996e+07 17287.6 43811.1 46782.1 54407.3 14038.5 1.88908e+07 14125 1.05021e+07 4392.3 15560.2 1.46964e+07 17198.2 19724.6 17634.6 14791.7 10345.8 1434 1.25993e+07 7241.2 1.67936e+07 7023.9 6.30784e+06 5804.59 1.67936e+07 38753.2 5779.74 1.67936e+07 3998.35 1.67936e+07 831589 1.1757e+06 8.07743e+06 3.07175e+07
78110 20231031.2 28002.1 2.30851e+07 0.801968 90290.4 5577.82 8.59996e+07 17706.2 43757.1 47025.6 54021.7 14078.8 1.88908e+07 14211.9 1.05021e+07 4412.2 15500.2 1.46964e+07 17043.4 19501.2 17190 14923.3 10161.5 1434.1 1.25993e+07 7246.56 1.67936e+07 7122.3 6.30784e+06 5824.15 1.67936e+07 44321.1 5724.41 1.67936e+07 3999.43 1.67936e+07 833541 1.17964e+06 8.15397e+06 3.09702e+07
78115 20231031.5 28096.6 2.51822e+07 0.788781 90398.6 5597.14 8.59996e+07 17153.5 45717.6 47743.9 55284.5 14046.4 1.88908e+07 14149.3 1.05021e+07 4374.5 15573.1 1.46964e+07 17204.3 19257.8 17318.7 14893.2 9790.65 1438.8 1.25993e+07 6857.73 1.67936e+07 6984.1 6.30784e+06 5786.81 1.67936e+07 44365.6 5770.07 1.67936e+07 3994.27 1.67936e+07 818357 1.17717e+06 8.15176e+06 3.07813e+07
78128 20231031.10 27738.1 2.51822e+07 0.75716 71982.3 5630.66 8.59996e+07 17076.3 43862 47267.7 55100.9 14058.5 1.88908e+07 14160.9 1.05021e+07 4371.6 15631.8 1.46964e+07 17200.1 19235.2 17122 14762.1 10396.2 1441.7 1.25993e+07 7284.99 1.67936e+07 7044.7 6.30784e+06 5805.39 1.67936e+07 42934.8 5776.39 1.67936e+07 3998.07 1.67936e+07 837504 1.18196e+06 8.15251e+06 3.15981e+07

mku-defineThenMatch

build_id build_number pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem pi_basic_mt_virtual_cft^ Commit latency factor tpcc_virtual_cft^ tpcc_sgx_cft^ tpcc_sgx_cft_mem 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^ 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 hist_sgx_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 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)^
78096 20231030.17 27893.3 2.30851e+07 81840.1 0.79445 17194 5579.98 8.59996e+07 44053.3 47782.2 54072.1 4419.3 17126.9 19565.3 17237.1 14848.8 9796.07 13976.7 1.88908e+07 14090.7 1.05021e+07 15439.4 1.25993e+07 42124.5 1420.6 1.25993e+07 6810.64 1.88908e+07 6867.9 6.30784e+06 5767.01 1.67936e+07 5463.94 1.67936e+07 3987.71 1.67936e+07 837642 1.17927e+06 8.14959e+06 3.12997e+07
78126 20231031.9 28021.9 2.30851e+07 79378.1 0.77204 17264.8 5589.07 8.59996e+07 45791.2 47204.5 54799.1 4441.1 17249.7 19287.5 17301 14632.7 9842.4 14121.4 1.67936e+07 14201.4 1.05021e+07 15614 1.46964e+07 43510.3 1435.8 1.25993e+07 6844.51 1.88908e+07 6966.9 6.30784e+06 5785.2 1.67936e+07 5743.19 1.67936e+07 3999.15 1.67936e+07 837540 1.18078e+06 8.13528e+06 3.17988e+07
78141 20231031.14 27901.8 2.51822e+07 81783.8 0.836525 17284.2 5581.84 8.59996e+07 45641.4 46669.4 54951.7 4392.5 17149.3 19331.9 17488 14929.5 9799.34 14017.3 1.67936e+07 14155.3 1.05021e+07 15524.4 1.46964e+07 45411.2 1431.7 1.25993e+07 6888.81 1.67936e+07 7091.3 6.30784e+06 5771.59 1.67936e+07 5486.15 1.67936e+07 4009.25 1.67936e+07 832584 1.18358e+06 8.13367e+06 3.09272e+07

images

auto-merge was automatically disabled October 31, 2023 15:41

Rebase failed

@lemmy lemmy merged commit 6e0ba3a into main Oct 31, 2023
31 checks passed
@lemmy lemmy deleted the mku-defineThenMatch branch October 31, 2023 15:51
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

@heidihoward heidihoward heidihoward approved these changes

Assignees
No one assigned
Labels
tla TLA+ specifications
Projects
None yet
Milestone
TLA+ Trace Validation (Consensus)
Development

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