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

Minor refactorings #5880

Merged
merged 5 commits into from
Jan 2, 2024
Merged

Minor refactorings #5880

merged 5 commits into from
Jan 2, 2024

Conversation

lemmy
Copy link
Contributor

@lemmy lemmy commented Dec 22, 2023

  • Show value of newConfiguration parameter of ChangeConfigurationInt in traces
  • Add DebugInvUpToDepth invariant to SIMccfraft to quickly generate a trace of length N by passing N to TLC's -depth cli.

Related to #5875

@lemmy lemmy added the tla TLA+ specifications label Dec 22, 2023
@lemmy lemmy requested a review from a team December 22, 2023 15:47
@lemmy lemmy enabled auto-merge (rebase) December 22, 2023 15:48
@ghost
Copy link

ghost commented Dec 22, 2023

mku-minor@79826 aka 20240102.8 vs main ewma over 20 builds from 79519 to 79809

Click to see table

main

build_id build_number Commit latency factor pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem 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 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 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 tpcc_virtual_cft^ ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ pi_basic_js_virtual_cft^ ls_jwt_virtual_cft^ hist_sgx_cft^ pi_ls_jwt_virtual_cft^ ls_js_virtual_cft^ RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^ ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^ tlc_sim_traces tlc_sim_levelmean pi_basic_mt_virtual_cft^
79519 20231218.10 0.798259 28034.3 2.30851e+07 5649.04 8.59996e+07 14073.9 1.67936e+07 14131.2 1.05021e+07 15680.1 1.25993e+07 1434.1 1.25993e+07 7257.49 1.67936e+07 6926.8 6.30784e+06 6 86496 442 1.2541e+07 234 6.31473e+06 5796.44 1.67936e+07 5496.59 1.88908e+07 4000.63 1.67936e+07 17354 53225.5 57562.6 63172.6 4571.7 20561.7 43611.9 22192.6 20824.9 839283 1.18148e+06 8.14091e+06 3.13836e+07 17639.3 11774 2266 403 88022.4
79527 20231218.12 0.804365 27882.3 2.51822e+07 5652.5 8.59996e+07 14054.9 1.88908e+07 14156.8 1.05021e+07 15651.7 1.25993e+07 1434.7 1.25993e+07 7256.84 1.67936e+07 6931.3 6.30784e+06 6 86496 432 1.2541e+07 234 6.31473e+06 5812.28 1.67936e+07 5490.43 1.67936e+07 3970.69 1.67936e+07 17343.5 53109.2 56861.5 63383 4615.7 20975.3 41214.1 21199 17583.3 832631 1.18361e+06 8.16366e+06 3.09979e+07 17621.2 10246.3 2415 403 87764.2
79542 20231218.17 0.804376 28109.4 2.51822e+07 5515.18 8.59996e+07 14007.3 1.88908e+07 14094.4 1.05021e+07 15548.3 1.25993e+07 1421.3 1.25993e+07 6831.17 1.67936e+07 6933.8 6.30784e+06 6 86496 444 1.2541e+07 240 6.31473e+06 5752.49 1.67936e+07 5482.48 1.67936e+07 3989.6 1.67936e+07 16839.2 53015.6 56723.7 62722.4 4557.8 20754.6 43143.5 21126.9 17414.4 844389 1.17243e+06 8.14447e+06 3.0803e+07 17483.6 11568.2 2402 403 69097.4
79567 20231219.3 0.795646 28206.2 2.51822e+07 5611.75 8.59996e+07 14063.6 1.67936e+07 14157.8 1.05021e+07 15638.2 1.46964e+07 1436.2 1.25993e+07 7272.8 1.67936e+07 6997.9 6.30784e+06 6 86496 430 1.2541e+07 233 6.31473e+06 5800.99 1.67936e+07 5722.19 1.88908e+07 3967.94 1.67936e+07 17368.8 55627.2 56626.1 62713.3 4630.4 20932.7 41599.6 21734.4 17750.5 833208 1.18146e+06 8.13641e+06 3.33991e+07 17590.3 11679.7 2184 403 81521.8
79588 20231219.11 0.814283 27802.7 2.30851e+07 5611.96 8.59996e+07 14052.5 1.88908e+07 14207.7 1.05021e+07 15610.1 1.25993e+07 1427.9 1.25993e+07 7239.63 1.67936e+07 6934.5 6.30784e+06 6 86496 423 1.2541e+07 242 6.31473e+06 5752.75 1.67936e+07 5730.57 1.88908e+07 3975.98 1.67936e+07 17317.5 53109.2 56478.3 58259.5 4621.8 20778.6 45838.7 21632.8 20842.2 828389 1.18457e+06 8.13215e+06 3.19566e+07 17459.4 11668.3 2351 403 74190.4
79604 20231219.15 0.806726 28041.5 2.51822e+07 5652.29 8.59996e+07 14034.6 1.88908e+07 14150.8 1.05021e+07 15632 1.25993e+07 1432.3 1.25993e+07 6876.9 1.67936e+07 6919.6 6.30784e+06 6 86496 433 1.2541e+07 240 6.31473e+06 5771.57 1.67936e+07 5738.72 1.67936e+07 3971.34 1.67936e+07 17471.7 53128.4 57049.3 63174.4 4649.5 20576.8 46717.2 21778 17665.7 832710 1.17881e+06 8.16395e+06 3.10661e+07 17429 11721.7 2346 403 98705.3
79611 20231219.17 0.822773 27994.7 2.51822e+07 5549.24 8.59996e+07 13991.6 1.67936e+07 14084.8 1.05021e+07 15528.8 1.46964e+07 1416.9 1.25993e+07 6888.13 1.88908e+07 6885 6.30784e+06 6 86496 426 1.2541e+07 241 6.31473e+06 5798.46 1.67936e+07 5454.42 1.67936e+07 3798.13 1.67936e+07 17836.6 53012.7 56994.3 62802.2 4503.5 20997.7 41541.3 22145.9 17826.8 828514 1.18511e+06 8.1358e+06 3.07457e+07 17670.9 11664.7 2317 403 75455.9
79621 20231219.21 0.803674 28144.4 2.30851e+07 5601.6 8.59996e+07 14042.2 1.88908e+07 14177.8 1.05021e+07 15554.8 1.46964e+07 1432 1.25993e+07 7253.97 1.67936e+07 7080.6 6.30784e+06 6 86496 437 1.2541e+07 240 6.31473e+06 5766.9 1.67936e+07 5722.58 1.88908e+07 3975.88 1.67936e+07 17287.3 53077 57174.2 62510.9 4571.8 20976.3 46184.1 21635.7 20794.6 833718 1.18439e+06 8.13399e+06 3.09543e+07 17422.7 11721.6 2504 403 81290.5
79642 20231220.4 0.797657 28505.5 2.30851e+07 5574.1 8.59996e+07 14035.2 1.88908e+07 14152.9 1.05021e+07 15669.3 1.25993e+07 1429.7 1.25993e+07 7246.97 1.67936e+07 6980.1 6.30784e+06 7 86496 433 1.2541e+07 237 6.31473e+06 5800.86 1.67936e+07 5459.1 1.67936e+07 3976.44 1.67936e+07 17262.1 52978.3 56536.1 62672 4577 20696.7 45331.4 22254.4 17598.7 831359 1.18546e+06 8.17402e+06 3.07023e+07 17574.9 11711.9 2205 403 83188.6
79649 20231220.6 0.790672 27856.5 2.30851e+07 5633.93 8.59996e+07 14086.3 1.67936e+07 14136.7 1.05021e+07 15662.2 1.25993e+07 1425.4 1.25993e+07 7271.74 1.67936e+07 7090.8 6.30784e+06 7 86496 431 1.2541e+07 241 6.31473e+06 5802.52 1.67936e+07 5719.34 1.67936e+07 3999.03 1.67936e+07 17057.1 52924.1 55935 60678.1 4551.7 21063.8 43239.8 21328.3 17352 831415 1.17087e+06 8.14998e+06 3.04395e+07 17391.2 11532 2422 403 98341.7
79678 20231220.18 0.791999 28217.3 2.51822e+07 5558.58 8.59996e+07 14061.7 1.88908e+07 14133.4 1.05021e+07 15598 1.25993e+07 1437.1 1.25993e+07 6906.58 1.88908e+07 6985.7 6.30784e+06 6 86496 431 1.2541e+07 236 6.31473e+06 5794.4 1.67936e+07 5731.37 1.67936e+07 3993.12 1.67936e+07 17425.3 52743.3 56074.6 61667.5 4603.9 21027.1 47191.7 22116.6 17741.1 837557 1.18345e+06 8.11176e+06 3.06298e+07 17275.2 11597.5 2274 403 70893.4
79693 20231221.3 0.825277 27963.8 2.51822e+07 5633.86 8.59996e+07 14089 1.88908e+07 14143.4 1.05021e+07 15608.7 1.46964e+07 1418.7 1.25993e+07 7243.3 1.67936e+07 6931.6 6.30784e+06 6 86496 443 1.2541e+07 240 6.31473e+06 5760.75 1.67936e+07 5475.1 1.67936e+07 3977.28 1.67936e+07 17281.9 53233.4 57492.4 62214.5 4570.5 20675.4 43951.7 21741.5 17380 810554 1.17945e+06 8.1552e+06 3.0712e+07 17681.7 11860.3 2247 403 73753.8
79707 20231222.3 0.812946 28028.2 2.30851e+07 5620.72 8.59996e+07 14007.1 1.67936e+07 14111.8 1.05021e+07 15564.3 1.46964e+07 1429.5 1.25993e+07 6869.23 1.88908e+07 7085 6.30784e+06 7 86496 433 1.2541e+07 243 6.31473e+06 5786 1.67936e+07 5731.94 1.67936e+07 3996.47 1.67936e+07 17192.9 52990.6 58113.2 62042.6 4644.1 20983.2 44675.9 22005.6 20798.9 840758 1.17882e+06 8.1646e+06 3.06982e+07 17660.2 11716.6 2385 403 86154.2
79724 20231225.2 0.835919 28166.4 2.30851e+07 5619.85 8.59996e+07 14035.1 1.67936e+07 14190.5 1.05021e+07 15651.5 1.25993e+07 1440.9 1.25993e+07 7241.84 1.67936e+07 6978.6 6.30784e+06 7 86496 436 1.2541e+07 237 6.31473e+06 5808 1.67936e+07 5474.82 1.88908e+07 3994.32 1.67936e+07 17292.1 52861.9 56705.4 61889.5 4601.8 20650.7 46135.5 21723.1 17483.2 834644 1.1791e+06 8.14888e+06 3.27303e+07 17588.3 11783.8 2316 403 74118.7
79739 20231226.3 0.830636 28205.8 2.51822e+07 5613.09 8.59996e+07 14076 1.88908e+07 14178.4 1.05021e+07 15658.8 1.25993e+07 1443.1 1.25993e+07 7268.57 1.67936e+07 6983.8 6.30784e+06 6 86496 428 1.2541e+07 244 6.31473e+06 5759.16 1.67936e+07 5489.93 1.88908e+07 3983.36 1.67936e+07 17368.3 52752.6 56752.4 62271.2 4587.3 21018.1 47038.4 22055.1 17838.1 824513 1.17359e+06 8.14881e+06 3.08443e+07 17531.8 11814.9 2478 403 70865.4
79750 20231227.1 0.818602 27885.2 2.51822e+07 5599.89 8.59996e+07 14026.9 1.67936e+07 14100 1.05021e+07 15563.2 1.25993e+07 1425.9 1.25993e+07 6848.41 1.67936e+07 6932.3 6.30784e+06 6 86496 430 1.2541e+07 242 6.31473e+06 5796.65 1.67936e+07 5448.92 1.67936e+07 3976.43 1.67936e+07 17400.9 53080.8 56737.9 61924.4 4624.8 20931.4 45579.1 18203 20610 838072 1.18283e+06 8.15446e+06 3.07475e+07 17300.9 11921.8 2258 403 87959.6
79764 20231228.1 0.785802 28069.2 2.30851e+07 5579.3 8.59996e+07 14013.7 1.88908e+07 14133.7 1.05021e+07 15558.2 1.25993e+07 1426 1.25993e+07 6801.15 1.67936e+07 7035 6.30784e+06 6 86496 434 1.2541e+07 235 6.31473e+06 5760.56 1.67936e+07 5478.71 1.67936e+07 3992.59 1.67936e+07 17482.4 52691.7 56538.7 62169.5 4606.1 21182.6 47564.7 22162.1 17804.6 832827 1.17369e+06 8.16737e+06 3.1373e+07 17513 11666.7 2144 403 100210
79781 20231229.2 0.801636 27896.7 2.51822e+07 5589.66 8.59996e+07 14027.6 1.88908e+07 14166.7 1.05021e+07 15567.2 1.46964e+07 1425.2 1.25993e+07 6793.52 1.67936e+07 7078.9 6.30784e+06 6 86496 436 1.2541e+07 240 6.31473e+06 5797.56 1.67936e+07 5483.48 1.67936e+07 3993.74 1.67936e+07 17379.6 53058 56634.4 62290.7 4544.7 21324.7 40847.4 22159.2 17388.8 834593 1.18035e+06 8.15979e+06 3.07217e+07 17492.5 11838.8 2181 403 70323.6
79795 20240101.3 0.78501 28203.3 2.51822e+07 5573.08 8.59996e+07 14058.6 1.88908e+07 14075.3 1.05021e+07 15400.4 1.25993e+07 1433.5 1.25993e+07 6907.22 1.88908e+07 6981.9 6.30784e+06 7 86496 437 1.2541e+07 244 6.31473e+06 5797.99 1.67936e+07 5721.54 1.67936e+07 3992.77 1.67936e+07 17464.7 53125.1 57116.7 61313 4568.7 20746.1 45491.3 22281.6 17744.9 828138 1.18098e+06 8.16847e+06 3.08021e+07 17841.4 11654.5 2254 403 88523
79809 20240102.3 0.818907 27998 2.51822e+07 5582.58 8.59996e+07 14069 1.88908e+07 14207.7 1.05021e+07 15632.9 1.46964e+07 1438 1.25993e+07 7254.86 1.67936e+07 6979.5 6.30784e+06 6 86496 427 1.2541e+07 241 6.31473e+06 5809.21 1.67936e+07 5725.47 1.88908e+07 4000.63 1.67936e+07 17426.2 52688.3 56487.3 62076.8 4588.5 20938.1 39813.8 21383.1 17806.2 838128 1.18558e+06 8.15241e+06 3.07577e+07 17373.5 11613.7 2304 403 89517.2

mku-minor

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_sgx_cft^ ls_sgx_cft_mem pi_ls_sgx_cft^ pi_ls_sgx_cft_mem ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_sgx_cft^ pi_basic_sgx_cft_mem pi_basic_virtual_cft^ 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 ls_js_jwt_virtual_cft^ 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 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 RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^ tlc_sim_traces tlc_sim_levelmean
79718 20231222.6 28003 2.51822e+07 0.811476 5666.93 8.59996e+07 74540.2 17376.4 14039.6 1.88908e+07 14154.9 1.05021e+07 53144.1 56828.5 15653.7 1.25993e+07 62430.7 4626.9 21174.7 22314 17603.9 1439.2 1.25993e+07 17661.1 7216.67 1.67936e+07 11683.3 6991.9 6.30784e+06 5768.48 1.67936e+07 5487.8 1.88908e+07 45748.3 3980.23 1.67936e+07 6 86496 427 1.2541e+07 239 6.31473e+06 838694 1.1804e+06 8.13292e+06 3.08699e+07 2360 403
79721 20231222.7 27824.4 2.30851e+07 0.812365 5608.94 8.59996e+07 81579.6 17442.8 14068.1 1.67936e+07 14194 1.05021e+07 53130.5 58634.5 15660.3 1.25993e+07 63035.7 4642.7 21000.8 21840.7 20433 1428.7 1.25993e+07 17397.2 7227.36 1.67936e+07 11893 6975.2 6.30784e+06 5807.49 1.67936e+07 5492.94 1.67936e+07 48297.3 3997.9 1.67936e+07 6 86496 432 1.2541e+07 237 6.31473e+06 835460 1.17836e+06 8.14959e+06 3.10915e+07 2383 403
79826 20240102.8 28130.6 2.30851e+07 0.846978 5671.69 8.59996e+07 84763 17223.2 14168.9 1.88908e+07 14240.6 1.05021e+07 52668.5 48207.9 15767 1.25993e+07 59995.7 4593.7 20726 22179.3 17602.1 1441.7 1.25993e+07 17565.4 7289.07 1.67936e+07 11663 7089.3 6.30784e+06 5822.03 1.67936e+07 5732.85 1.67936e+07 44581.2 4012.64 1.67936e+07 6 86496 437 1.2541e+07 238 6.31473e+06 834990 1.18239e+06 8.14683e+06 3.16005e+07 2436 403

images

@lemmy lemmy merged commit 58a8177 into main Jan 2, 2024
29 checks passed
@lemmy lemmy deleted the mku-minor branch January 2, 2024 17:50
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