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

Attempt to fix the simulation #5939

Merged
merged 5 commits into from
Jan 19, 2024

Conversation

achamayou
Copy link
Member

@achamayou achamayou commented Jan 18, 2024

With #5922, the simulation has much better coverage, and is now hitting invariants that are not clearly useful as we try to reconcile the impl and the spec. This is an attempt to drop enough to get back to a working CI without making unreasonable changes.

@achamayou achamayou requested a review from a team as a code owner January 18, 2024 16:18
@lemmy lemmy added the tla TLA+ specifications label Jan 18, 2024
@ccf-bot
Copy link
Collaborator

ccf-bot commented Jan 19, 2024

relax_simulation_invariants@80551 aka 20240119.5 vs main ewma over 16 builds from 80229 to 80541

Click to see table

main

build_id build_number 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)^ pi_basic_mt_sgx_cft^ pi_basic_mt_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 pi_basic_mt_virtual_cft^ tpcc_virtual_cft^ ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ pi_basic_js_virtual_cft^ tlc_sim_traces tlc_sim_levelmean ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_js_virtual_cft^ ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^
80229 20240111.14 0.812835 5619.7 8.59996e+07 14056.2 1.67936e+07 14196 1.05021e+07 15573.5 1.46964e+07 1437.6 1.25993e+07 7262.24 1.88908e+07 7029.5 6.30784e+06 5814.66 1.67936e+07 5765.08 1.67936e+07 4000.28 1.67936e+07 48116.8 831651 1.18093e+06 8.1541e+06 3.07406e+07 27955.9 2.30851e+07 6 77678 213 5.77852e+06 201 5.0742e+06 81578.4 17111.2 50602.2 58236.4 61854.1 4607.9 3780 403 20912.3 22219.8 17649.9 17429.6 11592.6
80242 20240111.19 0.773804 5676 8.59996e+07 14015 1.88908e+07 14125.8 1.05021e+07 15610 1.46964e+07 1432.2 1.25993e+07 7227.55 1.67936e+07 6931.1 6.30784e+06 5774.13 1.67936e+07 5743.01 1.67936e+07 4011.12 1.67936e+07 45142.8 824477 1.18539e+06 8.15543e+06 3.07813e+07 28203.5 2.51822e+07 6 77678 230 5.84821e+06 205 5.08533e+06 80254.5 17179.2 52816.7 57165.1 61509 4575.6 3496 403 20626.3 22255.9 17614.7 17469.5 11706.6
80252 20240111.22 0.803418 5642.83 8.80968e+07 14130.4 1.88908e+07 14169.5 1.05021e+07 15696.8 1.25993e+07 1432.8 1.25993e+07 7272.8 1.67936e+07 7093.3 6.30784e+06 5808.84 1.67936e+07 5757.11 1.67936e+07 4009.22 1.67936e+07 44845.1 830304 1.17589e+06 8.14596e+06 3.22312e+07 28090.5 2.51822e+07 6 77678 224 5.84821e+06 203 5.08533e+06 96022.6 17226.9 55861.6 58346.8 62303.6 4613.1 3419 403 20686.4 21550.3 17526.7 17350.6 11800.7
80271 20240111.29 0.813292 5499.35 8.59996e+07 14036.4 1.88908e+07 14118.3 1.05021e+07 15562.4 1.25993e+07 1431 1.25993e+07 7241.94 1.67936e+07 7039.7 6.30784e+06 5815.33 1.67936e+07 5734.66 1.88908e+07 3971.63 1.67936e+07 42971.6 831724 1.17891e+06 8.148e+06 3.07129e+07 27607.9 2.30851e+07 6 77678 237 5.84821e+06 243 5.73663e+06 83752.5 17133.9 55981.5 58573.4 62651.1 4605.8 3610 403 20476.2 22162.1 20610.2 17402.2 11766.9
80281 20240111.33 0.807376 5593.57 8.59996e+07 14056.4 1.88908e+07 14156.9 1.05021e+07 15553.7 1.46964e+07 1429.4 1.25993e+07 7262.76 1.67936e+07 6942.1 6.30784e+06 5813.13 1.67936e+07 5740.59 1.88908e+07 3977.86 1.67936e+07 47590.2 832607 1.18047e+06 8.15371e+06 3.07388e+07 27775 2.30851e+07 6 77678 229 5.84821e+06 252 5.73663e+06 85969.9 17787.9 55910.9 57744.4 62780 4629.4 3492 403 20614.3 21886.1 20606 17743.7 11816.4
80292 20240112.1 0.799609 5616.54 8.59996e+07 14086 1.88908e+07 14203.3 1.05021e+07 15647.6 1.25993e+07 1431 1.25993e+07 7203.91 1.67936e+07 6980.4 6.30784e+06 5771.83 1.67936e+07 5724.94 1.67936e+07 4001.42 1.67936e+07 40504.9 839107 1.17402e+06 8.13535e+06 3.10106e+07 28064.6 2.51822e+07 6 77678 237 5.84821e+06 254 5.73663e+06 99762.3 17167.1 55981.2 58058.2 62225.6 4625.2 3744 403 20836.9 22032.3 17710.9 17417.6 11589
80302 20240112.6 0.825414 5106.83 8.80968e+07 14005.8 1.88908e+07 13959.4 1.05021e+07 15214.7 1.46964e+07 1411 1.25993e+07 6814.37 1.88908e+07 6972 6.30784e+06 5806.03 1.67936e+07 5435.01 1.67936e+07 3989.3 1.67936e+07 39672.7 824006 1.17846e+06 8.13987e+06 3.0784e+07 28172.9 2.51822e+07 6 77678 231 5.84821e+06 255 5.73663e+06 96165 17642.7 53235 57617.6 61515.4 4588.4 3477 403 21122.8 21902.4 17823 17557.4 11576.2
80310 20240112.9 0.777512 5489.82 8.59996e+07 13961.1 1.88908e+07 14164.5 1.05021e+07 15557.3 1.25993e+07 1433 1.25993e+07 6791.51 1.67936e+07 7052.7 6.30784e+06 5819.48 1.67936e+07 5501.69 1.88908e+07 4013.78 1.67936e+07 45888.2 830922 1.1812e+06 8.13473e+06 3.09768e+07 28180.1 2.51822e+07 6 77678 232 5.84821e+06 249 5.73663e+06 77692.7 17237.7 56197.8 58912.6 63019.4 4550.4 3659 403 20668.2 22383.9 17474.6 17666.4 11810
80334 20240112.19 0.79401 5651.76 8.59996e+07 14082.7 1.88908e+07 14160.5 1.05021e+07 15748.6 1.25993e+07 1438 1.05021e+07 7274 1.67936e+07 7082 6.30784e+06 5786 1.67936e+07 5772.55 1.67936e+07 3980.36 1.67936e+07 45690 837432 1.17733e+06 8.15598e+06 3.19346e+07 28026.5 2.30851e+07 6 77678 232 5.84821e+06 240 5.73663e+06 79466.5 17347.6 55964.3 58284.9 63911.7 4653.1 3411 403 20253.8 22174.9 20908.6 17454 11706.5
80350 20240115.1 0.853383 5630.48 8.59996e+07 14122.2 1.67936e+07 14226.6 1.05021e+07 15704.8 1.46964e+07 1442 1.25993e+07 6843.32 1.88908e+07 6951.2 6.30784e+06 5813.52 1.67936e+07 5717.31 1.67936e+07 4007.06 1.67936e+07 45570.6 823989 1.17933e+06 8.13451e+06 3.08573e+07 27987.3 2.30851e+07 6 77678 234 5.84821e+06 248 5.73663e+06 74596 17262.3 56150.7 58512 61481.1 4619.2 3205 403 20893.6 21478.6 18112.5 17519.1 11680.7
80369 20240115.9 0.785847 5581.66 8.59996e+07 14041.8 1.88908e+07 14189.5 1.05021e+07 15718.9 1.25993e+07 1431.1 1.25993e+07 7259.6 1.67936e+07 7015.5 6.30784e+06 5819.81 1.67936e+07 5730.37 1.67936e+07 3986.19 1.67936e+07 45423.4 832130 1.17982e+06 8.14071e+06 3.07609e+07 28127.3 2.51822e+07 6 77678 228 5.6478e+06 245 5.46091e+06 74738.4 17146.4 55979.2 57713.4 61785.9 4644.3 3537 403 20685.7 22112.6 20644.4 17590 11860.7
80375 20240115.11 0.78028 5675.59 8.59996e+07 14077.4 1.88908e+07 14180.4 1.05021e+07 15568.1 1.46964e+07 1422.9 1.25993e+07 6829.18 1.67936e+07 6931 6.30784e+06 5758.09 1.67936e+07 5765.08 1.88908e+07 3992.89 1.67936e+07 45478.6 837280 1.17885e+06 8.1554e+06 3.10826e+07 28189.2 2.51822e+07 6 77678 218 5.6478e+06 235 5.46091e+06 78120.6 17816.3 55863.6 57285.3 61472.1 4630.6 3483 403 21139.8 21564.3 17347.6 17435.6 11696.8
80425 20240117.3 0.806812 5590.92 8.59996e+07 14033 1.88908e+07 14137.2 1.05021e+07 15607.1 1.46964e+07 1431.2 1.25993e+07 7220.81 1.67936e+07 6958.9 6.30784e+06 5812.83 1.67936e+07 5482.91 1.67936e+07 4002.85 1.67936e+07 45852.5 833254 1.17849e+06 8.12834e+06 3.05571e+07 27907.1 2.51822e+07 6 77678 947 2.53976e+07 677 1.594e+07 82946.7 17182.2 52999.7 57154.3 62316.7 4633.8 38100 401 20811.4 22429.1 20786.7 17507.5 11723.3
80453 20240118.2 0.786115 5600.57 8.59996e+07 14013 1.88908e+07 14170.8 1.05021e+07 15581.1 1.25993e+07 1433.9 1.25993e+07 7235.96 1.88908e+07 7136.5 6.30784e+06 5808.65 1.67936e+07 5494.33 1.67936e+07 3998.52 1.67936e+07 43064.8 830418 1.18005e+06 8.13509e+06 3.07291e+07 28245.5 2.51822e+07 6 77678 967 2.53976e+07 661 1.594e+07 86598.2 17175.3 52887.1 57977.4 61711.4 4601.7 37791 392 21160.5 21121.1 17754 17667.3 11680.2
80538 20240118.37 0.806333 5648.14 8.59996e+07 14079.2 1.67936e+07 14119.8 1.05021e+07 15673.6 1.46964e+07 1438.2 1.25993e+07 6847.53 1.67936e+07 6972.4 6.30784e+06 5826.08 1.67936e+07 5497.74 1.88908e+07 4001.88 1.67936e+07 48080.6 835309 1.18231e+06 8.1516e+06 3.09525e+07 27799 2.51822e+07 6 77678 958 2.53976e+07 638 1.594e+07 93220.8 17271.6 55942.8 57911.9 62487.4 4622.8 39215 398 20683.8 22215.3 20722.2 17538.8 11874.3
80541 20240119.2 0.811699 5602.96 8.59996e+07 14077.8 1.88908e+07 14159.5 1.05021e+07 15654.8 1.25993e+07 1430.8 1.25993e+07 7242.25 1.67936e+07 7010.3 6.30784e+06 5763.86 1.67936e+07 5496.46 1.88908e+07 4007.17 1.67936e+07 42754.5 826787 1.18274e+06 8.15576e+06 3.08253e+07 27789.1 2.30851e+07 6 77678 938 2.53976e+07 663 1.594e+07 69040.3 17285.9 55852.9 57476.2 62218.5 4594.9 39508 394 20770.3 21123.8 20607.2 17556.2 11829.2

relax_simulation_invariants

build_id build_number Commit latency factor 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_basic_js_virtual_cft^ pi_ls_sgx_cft^ pi_ls_sgx_cft_mem pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem ls_jwt_virtual_cft^ pi_basic_sgx_cft^ pi_basic_sgx_cft_mem pi_ls_jwt_virtual_cft^ ls_js_virtual_cft^ ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^ pi_basic_mt_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)^ 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 tlc_sim_traces tlc_sim_levelmean
80551 20240119.5 0.829403 5611.8 8.59996e+07 17311.7 53388.3 57863 61931.4 14021.7 1.88908e+07 4624 14169.1 1.05021e+07 28178.9 2.51822e+07 20334.5 15592.8 1.46964e+07 22092.6 20630.9 17495.1 11715.1 77343.6 1434.2 1.25993e+07 7229.51 1.67936e+07 6999.9 6.30784e+06 5801.64 1.67936e+07 43605.8 5489.52 1.67936e+07 4007 1.67936e+07 836880 1.18311e+06 8.14489e+06 3.07554e+07 6 77678 963 2.53976e+07 697 1.594e+07 53950 396

images

@achamayou achamayou merged commit de6f63a into microsoft:main Jan 19, 2024
25 checks passed
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.

None yet

4 participants