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

Recreating longer counterexamples such as those coming out of the simulator is significantly faster when deserialized from TLC's binary format as opposed to the textual record in TTrace.tla. #5761

Merged
merged 2 commits into from
Oct 23, 2023

Conversation

lemmy
Copy link
Contributor

@lemmy lemmy commented Oct 23, 2023

nt

…ulator is significantly faster when deserialized from TLC's binary format as opposed to the textual record in TTrace.tla.
@lemmy lemmy added the tla TLA+ specifications label Oct 23, 2023
@lemmy lemmy requested a review from a team October 23, 2023 20:05
@lemmy lemmy enabled auto-merge (squash) October 23, 2023 20:05
@ghost
Copy link

ghost commented Oct 23, 2023

mku-ciIncludeBinaryTrace@77639 aka 20231023.34 vs main ewma over 20 builds from 76994 to 77584

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_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^ ls_full_js_virtual_cft^ pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem ls_js_jwt_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_full_js_sgx_cft^ ls_full_js_sgx_cft_mem hist_sgx_cft^ ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^
76994 20231009.5 27792.2 2.30851e+07 0.799524 88389.5 5591.29 8.59996e+07 17106.4 45848 48779.1 53666.3 13986.8 1.88908e+07 14144 1.05021e+07 15585.3 1.25993e+07 4397.6 17242 19596.7 16914.5 16715.5 1431.3 1.25993e+07 9855.69 6852.61 1.67936e+07 6940.5 6.30784e+06 5808.48 1.67936e+07 5783.34 1.67936e+07 44311.9 3987.05 1.67936e+07 831717 1.18619e+06 8.15293e+06 3.07093e+07
77015 20231010.4 27777.8 2.30851e+07 0.83228 62049.7 5592.78 8.59996e+07 17372.9 45785.1 48171.9 53651.8 14023.3 1.88908e+07 14107 1.05021e+07 15597.5 1.25993e+07 4441.2 17407.2 19739.4 17105.5 16857.9 1436 1.25993e+07 9954.93 6898.77 1.88908e+07 7117.8 6.30784e+06 5804.14 1.67936e+07 5786.43 1.67936e+07 41221.6 4016.78 1.67936e+07 825345 1.18742e+06 8.12844e+06 3.06711e+07
77052 20231010.17 27851.7 2.51822e+07 0.805827 87071.8 5614.03 8.59996e+07 17123.9 45707.2 48521.1 53548.8 14004.1 1.88908e+07 14072.2 1.05021e+07 15532.7 1.25993e+07 4435.4 17238.9 19725.4 17064.9 16932.1 1434.8 1.25993e+07 9900.42 6879.16 1.88908e+07 6931.4 6.30784e+06 5811.67 1.67936e+07 5725.25 1.88908e+07 39661.9 3978.87 1.67936e+07 835356 1.17508e+06 8.12795e+06 3.02453e+07
77065 20231010.21 27866.2 2.51822e+07 0.805254 76791.9 5593.79 8.59996e+07 17453.5 45981.3 47639.7 53782.5 13984.2 1.88908e+07 14076.6 1.05021e+07 15457.8 1.46964e+07 4471.3 17159.7 19727 17221.9 16835.2 1431.7 1.25993e+07 9888.21 6839.77 1.67936e+07 6882.8 6.30784e+06 5802.59 1.67936e+07 5713.9 1.67936e+07 47354.4 3982.91 1.67936e+07 831464 1.17023e+06 8.14609e+06 3.06028e+07
77080 20231011.6 28231.3 2.30851e+07 0.805739 77100.4 5614.98 8.59996e+07 17356.8 45541.3 47443.3 53459.3 14016.4 1.67936e+07 14058.7 1.05021e+07 15607.1 1.25993e+07 4480.6 17192.9 19626.7 16932.3 16704.5 1435.6 1.25993e+07 9841.59 6865.39 1.88908e+07 6917 6.30784e+06 5768.86 1.67936e+07 5749.11 1.67936e+07 44338.6 3974.5 1.67936e+07 839572 1.1863e+06 8.14557e+06 3.07489e+07
77087 20231011.8 27891.2 2.51822e+07 0.821071 83135 5620.28 8.59996e+07 17648.9 45716.6 48214.1 53475.5 14043.4 1.88908e+07 14129.4 1.05021e+07 15619 1.46964e+07 4431.6 17316.9 19004.2 17758.2 16880.7 1427.7 1.25993e+07 9849.81 6872.29 1.67936e+07 7079.7 6.30784e+06 5780.82 1.67936e+07 5765.08 1.67936e+07 40652.5 3974.44 1.67936e+07 827510 1.16961e+06 8.14036e+06 3.30899e+07
77124 20231011.20 27859.9 2.51822e+07 0.810686 81677.3 5576.3 8.59996e+07 17272.2 45763.1 48479 54961.6 13934.9 1.88908e+07 14029.2 1.05021e+07 15421.8 1.25993e+07 4431 17497.2 19917.1 17216.9 16806.9 1419.9 1.25993e+07 9875.23 6782.48 1.67936e+07 7028.9 6.30784e+06 5759.88 1.67936e+07 5495.58 1.88908e+07 42920 3980.45 1.67936e+07 829281 1.17704e+06 8.02253e+06 3.09324e+07
77138 20231011.24 27788.7 2.51822e+07 0.817166 79701.7 5505.15 8.59996e+07 17450.2 43714.5 47439 54645.3 13944.3 1.88908e+07 14007.9 1.05021e+07 15414.3 1.46964e+07 4386.8 16999.7 19561.8 17388.6 14746.3 1420.9 1.25993e+07 9915 6826.31 1.88908e+07 6933.7 6.30784e+06 5805.03 1.67936e+07 5491.25 1.67936e+07 39122 3992.65 1.67936e+07 838714 1.18152e+06 8.09934e+06 3.09754e+07
77148 20231012.2 28066.3 2.51822e+07 0.806977 88890.3 5622.22 8.59996e+07 17218.1 46048.4 48655.6 55217 14012.7 1.88908e+07 14136.8 1.05021e+07 15607.9 1.25993e+07 4449.2 17077.4 19720.8 17064.5 15135.1 1437.4 1.25993e+07 9799.03 6885.22 1.88908e+07 6981.9 6.30784e+06 5813.57 1.67936e+07 5723.57 1.88908e+07 45326.3 4000.45 1.67936e+07 828634 1.17897e+06 8.14758e+06 3.07383e+07
77236 20231016.5 27858.7 2.51822e+07 0.79596 59377 5620.83 8.59996e+07 17148.6 45783.9 48719.4 54902.8 13995.4 1.88908e+07 14108.1 1.05021e+07 15609.7 1.46964e+07 4441 17077.1 18804.1 17198.3 15291.6 1442 1.25993e+07 9993.77 6827.74 1.67936e+07 7065.1 6.30784e+06 5817.83 1.67936e+07 5743.02 1.67936e+07 44154.4 4006.32 1.67936e+07 838342 1.17813e+06 8.15154e+06 3.18804e+07
77284 20231016.20 27801.1 2.30851e+07 0.800376 76928.2 5523.42 8.59996e+07 17222.7 45566.9 48808.1 54701.8 13858.5 1.88908e+07 14093.4 1.05021e+07 15419 1.46964e+07 4442.5 17018.1 19157.5 17650.8 14639.8 1423.4 1.05021e+07 9852.83 6815.4 1.88908e+07 6872.8 6.30784e+06 5802.5 1.67936e+07 5472.72 1.67936e+07 43502.1 3973.37 1.67936e+07 833609 1.17767e+06 8.15537e+06 3.06513e+07
77294 20231016.23 27413.6 2.51822e+07 0.822085 84572 5504.43 8.59996e+07 17297.3 45995.1 48594.2 53897 14028.1 1.88908e+07 14087.6 1.05021e+07 15527 1.46964e+07 4439.9 17262.3 19125.2 17406.6 14896.4 1420.2 1.05021e+07 9812.12 6819.85 1.88908e+07 6931.4 6.30784e+06 5754.38 1.67936e+07 5710.32 1.67936e+07 41300 3992.44 1.67936e+07 823461 1.17985e+06 8.1493e+06 3.05375e+07
77306 20231017.4 27907.4 2.30851e+07 0.806546 60982.9 5649.91 8.59996e+07 17275.1 46102.1 47686.9 53983.1 13997.7 1.88908e+07 14120.3 1.05021e+07 15513.7 1.46964e+07 4424.7 17066.2 19713 14599.9 14833.6 1427.4 1.25993e+07 9890.99 6895.99 1.67936e+07 6972.2 6.30784e+06 5811.89 1.67936e+07 5778.4 1.67936e+07 45776.1 4010.44 1.67936e+07 832093 1.181e+06 8.15615e+06 3.10764e+07
77410 20231019.5 27911.2 2.30851e+07 0.79845 89839.8 5633.52 8.59996e+07 17335.1 43709 47970.1 54598 14034.4 1.88908e+07 14172.6 1.05021e+07 15641.4 1.25993e+07 4449.7 17103.2 19628.2 14821.2 14920.8 1439.9 1.25993e+07 9802.6 6838.11 1.67936e+07 7046.5 6.30784e+06 5772.37 1.67936e+07 5751.39 1.67936e+07 42755.2 4007.97 1.67936e+07 840034 1.18128e+06 8.17441e+06 3.06839e+07
77459 20231020.5 27942.3 2.51822e+07 0.806882 83682.7 5609.6 8.59996e+07 17271.7 45556.9 48282.6 53165.7 14027.3 1.88908e+07 14086.4 1.05021e+07 15436.7 1.46964e+07 4426.2 17066.3 17662.5 16990.3 14844.7 1431.9 1.25993e+07 9889.88 6873.38 1.88908e+07 6974.5 6.30784e+06 5805.89 1.67936e+07 5491.04 1.67936e+07 42113.3 3972.9 1.67936e+07 830635 1.18094e+06 8.16668e+06 3.0923e+07
77461 20231020.6 27968.8 2.30851e+07 0.797578 86522.6 5645.01 8.59996e+07 17246.7 45887.8 48453.6 54176.2 13956.1 1.88908e+07 14152 1.05021e+07 15499.4 1.46964e+07 4426.2 17079.1 19435.2 15003.7 14699.8 1437.7 1.25993e+07 9770.09 7235.96 1.67936e+07 7078.7 6.30784e+06 5801.29 1.67936e+07 5742.38 1.67936e+07 43030.2 3995.17 1.67936e+07 825201 1.1798e+06 8.16489e+06 3.14443e+07
77485 20231020.14 27955.5 2.51822e+07 0.827982 67488.2 5614.45 8.59996e+07 17203.3 45720.2 47505.9 52771.4 14042.3 1.67936e+07 14155.3 1.05021e+07 15587 1.46964e+07 4441 17168.5 19652.2 16950.7 14720 1441.5 1.25993e+07 9771.33 7220.81 1.67936e+07 6925.4 6.30784e+06 5824.33 1.67936e+07 5745.31 1.67936e+07 46913.9 3980.22 1.67936e+07 831368 1.1798e+06 8.12782e+06 3.08955e+07
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 15520.9 1.46964e+07 4332.3 17195.4 19336.7 17022.6 14750.8 1429.6 1.25993e+07 10188.5 7252.76 1.67936e+07 7086.5 6.30784e+06 5806.4 1.67936e+07 5491.29 1.67936e+07 40351.5 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 15640.2 1.46964e+07 4365.2 17152.3 19152.3 17286.3 14910.6 1432.7 1.25993e+07 10169.6 7273.33 1.67936e+07 6953.5 6.30784e+06 5781.01 1.67936e+07 5742.5 1.67936e+07 43068.6 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 15424.6 1.46964e+07 4430 17010.7 19396.4 17307.2 14810.6 1427 1.25993e+07 9823.55 6853.5 1.88908e+07 6881.2 6.30784e+06 5758.93 1.67936e+07 5762.09 1.67936e+07 42679.4 3983.52 1.67936e+07 825381 1.18095e+06 8.16893e+06 3.13159e+07

mku-ciIncludeBinaryTrace

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^ tpcc_virtual_cft^ ls_virtual_cft^ pi_ls_virtual_cft^ ls_sgx_cft^ ls_sgx_cft_mem pi_basic_virtual_cft^ pi_ls_sgx_cft^ pi_ls_sgx_cft_mem 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^ ls_full_js_virtual_cft^ pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem ls_js_jwt_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_full_js_sgx_cft^ ls_full_js_sgx_cft_mem hist_sgx_cft^ ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^
77633 20231023.32 27903.7 2.30851e+07 0.788091 5585.47 8.59996e+07 79165.4 17365.1 45886.6 48003.3 14049.3 1.88908e+07 53949.4 14149 1.05021e+07 15609.2 1.25993e+07 4461.2 17160.7 19943 17400.6 14769.1 1436.1 1.25993e+07 9951.85 6872.98 1.88908e+07 6936.6 6.30784e+06 5806.93 1.67936e+07 5781.98 1.67936e+07 40587.8 3980.96 1.67936e+07 829629 1.17933e+06 8.14657e+06 3.26099e+07
77639 20231023.34 28069.8 2.30851e+07 0.804338 5622.94 8.59996e+07 74960.1 17091.9 43785.7 47082.1 14063.6 1.88908e+07 55321.3 14190.8 1.05021e+07 15667.5 1.25993e+07 4378.1 17071.3 19518.3 17273.6 14968.2 1435 1.25993e+07 9946.18 6861.11 1.88908e+07 7003.9 6.30784e+06 5817.91 1.67936e+07 5745.9 1.67936e+07 43566 3999.49 1.67936e+07 832809 1.17968e+06 8.1337e+06 3.06973e+07

images

@lemmy lemmy merged commit 499f170 into main Oct 23, 2023
21 checks passed
@lemmy lemmy deleted the mku-ciIncludeBinaryTrace branch October 23, 2023 21:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
tla TLA+ specifications
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants