Move simulation to ADO too, and shorten the length of its run to not delay PRs

[achamayou]

Re-group raft simulation with the model checking on ADO, and shorten run, 50 minutes it too long for the current CI.

[heidihoward]

@achamayou I cannot see any edits to shorten the runs

[achamayou]

@achamayou I cannot see any edits to shorten the runs

Thank you for spotting that this hadn't been done right!

[lemmy]

I do not recommend shortening the traces, i.e., changing the -depth parameter beyond 250. From observations, simulation has found issues such as violations of QuorumLogInv because it explores the state space where the system has seen "more" activity such as several client requests, more than a few votes, messages being lost, ... (once simulation found a long counterexample, human insight can help shorten it).

Perhaps, spec simulation should be completely decoupled from our PR builder, or, if shortened, a new long-running (hours?) simulation should run every night.

[achamayou]

I do not recommend shortening the traces, i.e., changing the -depth parameter beyond 250. From observations, simulation has found issues such as violations of QuorumLogInv because it explores the state space where the system has seen "more" activity such as several client requests, more than a few votes, messages being lost, ... (once simulation found a long counterexample, human insight can help shorten it).

They're back to where they were (https://github.com/microsoft/CCF/pull/5827/files#diff-ebe20cacfdab2c7f426ccfec227825fae1a34bb8f01fb8248ba83bfb5319c6dcR22), I just misunderstood what the parameter did.

Perhaps, spec simulation should be completely decoupled from our PR builder, or, if shortened, a new long-running (hours?) simulation should run every night.

The Daily Build does that (ASAN etc), so that's where we would put it. What's the best way to parametrise timeout out of the file?

[lemmy]

Perhaps, spec simulation should be completely decoupled from our PR builder, or, if shortened, a new long-running (hours?) simulation should run every night.

The Daily Build does that (ASAN etc), so that's where we would put it. What's the best way to parametrise timeout out of the file?

TLCSet("exit", TLCGet("duration") > atoi(IOEnv.YOUR_TIMEOUT))

[ghost]

move_sim_to_ado_and_shorten_run@78663 aka 20231110.27 vs main ewma over 20 builds from 78284 to 78639

Click to see table

main

build_id	build_number	pi_basic_mt_sgx_cft^	pi_basic_mt_sgx_cft_mem	pi_basic_mt_virtual_cft^	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_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)^	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
78284	20231102.4	27902.1	2.30851e+07	74128.5	0.775601	5607	8.59996e+07	17090	43810.2	47171.4	53039.6	14039.4	1.88908e+07	4380.6	14144.7	1.05021e+07	15534.3	1.46964e+07	16902.4	19632.5	14945.6	14982	10242.7	1433.6	1.25993e+07	6870.67	1.88908e+07	7007.8	6.30784e+06	5753.55	1.67936e+07	40950.5	5431.34	1.67936e+07	3982.9	1.67936e+07	830357	1.18333e+06	8.13473e+06	3.08373e+07	nan	nan	nan	nan	nan	nan
78305	20231102.12	27661.5	2.30851e+07	88216.8	0.78799	5520.15	8.59996e+07	17322.6	45645.4	48989.3	53847.3	14034	1.88908e+07	4386.2	14105	1.05021e+07	15532.4	1.25993e+07	17291.3	19701.3	17082.4	14871.8	10051.9	1421.1	1.25993e+07	6844.95	1.88908e+07	7082.4	6.30784e+06	5797.56	1.67936e+07	40964.4	5725.47	1.88908e+07	4001.42	1.67936e+07	822024	1.17786e+06	8.15592e+06	3.10807e+07	nan	nan	nan	nan	nan	nan
78319	20231102.17	27989.4	2.30851e+07	83397.2	0.793434	5616.9	8.59996e+07	17142.8	45692.3	48014.1	53896.9	13956	1.88908e+07	4359.7	14087.7	1.05021e+07	15500.2	1.46964e+07	17057.3	19245.9	17127.5	14800.7	10296.3	1432	1.25993e+07	6839.82	1.67936e+07	6924.1	6.30784e+06	5801.1	1.67936e+07	45008.6	5739.65	1.67936e+07	3972.71	1.67936e+07	834976	1.18569e+06	8.12273e+06	3.07789e+07	nan	nan	nan	nan	nan	nan
78358	20231103.3	27874.4	2.51822e+07	73888.9	0.80868	5613.85	8.59996e+07	17311.7	43799.2	48061.9	53988.3	14024	1.88908e+07	4395.8	14173.7	1.05021e+07	15658	1.46964e+07	17328	19780	17379.4	14648.9	10273.9	1431	1.25993e+07	6848.6	1.88908e+07	6936	6.30784e+06	5795.98	1.67936e+07	45285.7	5450.88	1.67936e+07	3999.15	1.67936e+07	829705	1.18299e+06	8.14787e+06	3.0569e+07	nan	nan	nan	nan	nan	nan
78365	20231103.6	28034	2.30851e+07	72764.7	0.787105	5629.97	8.59996e+07	17440.6	45729.3	48139.6	54762.3	14078.6	1.88908e+07	4342.9	14064.8	1.05021e+07	15659.9	1.25993e+07	17317.7	19576	15085.7	14683.7	9954.18	1424	1.25993e+07	6812	1.67936e+07	6988	6.30784e+06	5761.67	1.67936e+07	43491.4	5755.45	1.67936e+07	3977.18	1.67936e+07	829913	1.18447e+06	8.14194e+06	3.07286e+07	nan	nan	nan	nan	nan	nan
78372	20231103.8	27795.9	2.30851e+07	90924.9	0.811727	5578.73	8.59996e+07	17281.7	45628	48368.5	53990.3	13977.9	1.88908e+07	4355.3	14087	1.05021e+07	15549.8	1.25993e+07	17137.4	19422.4	14922.2	14674.6	10171.6	1424.7	1.25993e+07	6788.55	1.88908e+07	6925.3	6.30784e+06	5793.13	1.67936e+07	44113	5490.55	1.88908e+07	3975.67	1.67936e+07	838885	1.18174e+06	8.15439e+06	3.16504e+07	nan	nan	nan	nan	nan	nan
78384	20231103.12	27988.7	2.30851e+07	74382.9	0.802159	5517.44	8.59996e+07	17108.5	43878.6	47871.9	52246	13977	1.88908e+07	4407.6	14136.3	1.05021e+07	15467.4	1.46964e+07	17039.1	19823.6	17407.9	14732.2	10283.4	1436.3	1.05021e+07	6845.18	1.88908e+07	6873	6.30784e+06	5794.5	1.67936e+07	45856.3	5481.25	1.67936e+07	3986.29	1.67936e+07	827005	1.1842e+06	8.15429e+06	3.09913e+07	nan	nan	nan	nan	nan	nan
78407	20231103.18	28323.1	2.30851e+07	59381.6	0.797156	5591.14	8.59996e+07	17161.2	43521.6	46519.9	53186.1	13982.6	1.88908e+07	4343	14162.3	1.05021e+07	15482.2	1.25993e+07	16972	19625.2	14970	14529.4	10096.1	1429.7	1.25993e+07	6854.13	1.67936e+07	7087.8	6.30784e+06	5753.69	1.67936e+07	40541.7	5469.17	1.67936e+07	3986.36	1.67936e+07	829355	1.18365e+06	8.17382e+06	3.16191e+07	nan	nan	nan	nan	nan	nan
78430	20231106.1	27904	2.30851e+07	75314.2	0.785044	5655.91	8.59996e+07	17142.7	45699	47880.3	54141.9	14049.4	1.88908e+07	4390.8	14103.2	1.05021e+07	15592	1.46964e+07	17165.6	19773.4	15067.1	14805.8	10259.9	1438.6	1.05021e+07	6904.68	1.88908e+07	7080.2	6.30784e+06	5768.13	1.67936e+07	45223.5	5444.99	1.67936e+07	4003.81	1.67936e+07	830876	1.1802e+06	8.13838e+06	3.08745e+07	nan	nan	nan	nan	nan	nan
78447	20231107.4	27883.9	2.30851e+07	63226	0.803997	5657.58	8.59996e+07	17233.7	43850.9	46545.8	53892.3	14082.8	1.67936e+07	4342.9	14226.4	1.05021e+07	15619.5	1.46964e+07	16914.1	19725.8	17400.6	14863.8	10109.8	1439.7	1.25993e+07	7269.63	1.67936e+07	7062.6	6.30784e+06	5804.83	1.67936e+07	43312.1	5742.73	1.67936e+07	3981.14	1.67936e+07	834561	1.18331e+06	8.16776e+06	3.07268e+07	nan	nan	nan	nan	nan	nan
78486	20231107.16	27770.8	2.51822e+07	87344	0.801874	5617.84	8.59996e+07	17279.4	43772.2	47733.8	54072.7	14085.9	1.88908e+07	4379	14206.9	1.05021e+07	15610.5	1.46964e+07	16987.8	19100.7	15027.3	14993.4	10303.6	1438	1.25993e+07	6857.21	1.88908e+07	6977.6	6.30784e+06	5803.25	1.67936e+07	44144	5736.63	1.67936e+07	3971.58	1.67936e+07	838496	1.18042e+06	8.15371e+06	2.9949e+07	131	1.97092e+06	nan	nan	nan	nan
78494	20231108.1	27924.2	2.51822e+07	80711.6	0.78468	5532.27	8.59996e+07	17313.3	45642.2	47648.1	54269.5	13978.1	1.67936e+07	4387.4	14115.2	1.05021e+07	15527.7	1.25993e+07	17062.1	19037.5	15166.2	15030.2	10352.8	1433.1	1.25993e+07	6857.9	1.88908e+07	6971.4	6.30784e+06	5796.65	1.67936e+07	41476.9	5489.21	1.67936e+07	3996.02	1.67936e+07	804898	1.17648e+06	8.09413e+06	3.07706e+07	124	1.97092e+06	nan	nan	nan	nan
78534	20231108.16	27940.7	2.51822e+07	71362	0.814001	5508.65	8.59996e+07	17305.2	43733.1	47228.6	53728.9	14045.8	1.67936e+07	4372.2	14093.1	1.05021e+07	15472.9	1.46964e+07	17222.8	19593.2	14958.9	14561.2	10207.8	1417.5	1.25993e+07	6760.42	1.67936e+07	7034.2	6.30784e+06	5797.13	1.67936e+07	43059	5482.75	1.67936e+07	3994.88	1.67936e+07	834726	1.17855e+06	8.17421e+06	3.284e+07	127	1.97092e+06	412	1.17179e+07	229	5.94846e+06
78546	20231108.20	27842.3	2.30851e+07	70955	0.803831	5562.49	8.59996e+07	17193.3	45583.3	47085.4	53757.4	13953.9	1.88908e+07	4369.1	13971.1	1.05021e+07	15327	1.46964e+07	17214.2	19185.4	17445.6	14796.9	10162.5	1401.6	1.25993e+07	6825.09	1.88908e+07	6884.7	6.30784e+06	5756.81	1.67936e+07	43053.4	5462.49	1.67936e+07	3947.94	1.67936e+07	834314	1.17795e+06	8.1518e+06	3.07434e+07	132	1.97092e+06	423	1.17179e+07	222	5.94846e+06
78558	20231108.24	27852.3	2.30851e+07	87493	0.791062	5555.81	8.59996e+07	17037.4	43865.1	47170	52802.9	14017.9	1.88908e+07	4353.3	14164.4	1.05021e+07	15546.1	1.46964e+07	17050	18865.8	17186.9	14777.5	10241.2	1433.9	1.25993e+07	6787.99	1.67936e+07	6940.2	6.30784e+06	5809.33	1.67936e+07	41786.3	5447.34	1.67936e+07	3968.11	1.67936e+07	834125	1.18208e+06	8.1247e+06	3.0595e+07	120	1.97092e+06	398	1.17179e+07	224	5.94846e+06
78568	20231109.3	27939.1	2.51822e+07	87721.9	0.799269	5598.12	8.59996e+07	17264.6	43783.2	47435.4	53481.3	14087.6	1.88908e+07	4385.9	14194.3	1.05021e+07	15680	1.46964e+07	17091	19520.6	14848.6	14708.1	10132.6	1434.2	1.25993e+07	7226.55	1.67936e+07	7100.8	6.30784e+06	5793.83	1.67936e+07	44947.9	5483.14	1.67936e+07	3971.48	1.67936e+07	834758	1.18204e+06	8.14421e+06	3.08257e+07	139	1.97092e+06	428	1.17179e+07	238	5.94846e+06
78597	20231110.2	28119.2	2.51822e+07	89644	0.820217	5574.8	8.59996e+07	17438.9	45782.2	48199	54129.5	14024.1	1.88908e+07	4406.4	14119.9	1.05021e+07	15507.8	1.46964e+07	17319.5	19699.8	14922.9	14864.4	10196.3	1421.1	1.25993e+07	7248.55	1.67936e+07	7079.1	6.30784e+06	5793.81	1.67936e+07	45165.9	5494.3	1.67936e+07	3999.09	1.67936e+07	835013	1.18481e+06	8.14223e+06	3.07975e+07	124	1.97092e+06	410	1.17179e+07	227	5.94846e+06
78603	20231110.5	28155.1	2.30851e+07	73387.6	0.800484	5580.74	8.59996e+07	17135.5	43772.8	47530.3	54447	14024.5	1.88908e+07	4438.1	14134.4	1.05021e+07	15453.5	1.46964e+07	17217.2	19690.9	17424.3	15192.4	10204.5	1435.7	1.25993e+07	7234.68	1.67936e+07	6947	6.30784e+06	5801.75	1.67936e+07	38563.2	5489.21	1.67936e+07	4002.28	1.67936e+07	834638	1.17761e+06	8.0415e+06	3.07975e+07	122	1.97092e+06	414	1.17179e+07	227	5.94846e+06
78616	20231110.10	27789.4	2.51822e+07	80935.3	0.803176	5620.57	8.59996e+07	17222.8	43599.4	47949.9	53841.8	14024.6	1.88908e+07	4400.4	14178.4	1.05021e+07	15586.9	1.25993e+07	17024.2	19096.7	15032.3	14891.5	10161.5	1421.1	1.25993e+07	6883.97	1.88908e+07	7094.6	6.30784e+06	5767.02	1.67936e+07	43058	5739.27	1.67936e+07	3985.71	1.67936e+07	835116	1.18152e+06	8.15241e+06	3.07646e+07	124	1.97092e+06	411	1.17179e+07	227	5.94846e+06
78639	20231110.19	27614.7	2.30851e+07	69445.7	0.781922	5627.55	8.59996e+07	17359.9	45728.6	48073.9	54500.8	14013.2	1.88908e+07	4431.6	14116.4	1.05021e+07	15570.1	1.46964e+07	17027.1	19186.5	17302.6	14918.9	10196.6	1433.9	1.25993e+07	6786.6	1.88908e+07	7029.2	6.30784e+06	5799.06	1.67936e+07	43277.5	5444.62	1.67936e+07	3992.6	1.67936e+07	825457	1.18272e+06	8.08601e+06	3.06931e+07	113	1.97092e+06	378	1.15766e+07	210	5.93588e+06

move_sim_to_ado_and_shorten_run

build_id	build_number	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_sgx_cft^	pi_basic_mt_sgx_cft_mem	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	tpcc_virtual_cft^	hist_sgx_cft^	ls_virtual_cft^	RB put (/s)^	CHAMP put (/s)^	RB get (/s)^	CHAMP get (/s)^	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^	pi_basic_mt_virtual_cft^	ls_full_js_virtual_cft^	ls_js_jwt_virtual_cft^	tlc_sim_traces	tlc_sim_levelmean
78658	20231110.25	119	1.97092e+06	385	1.15766e+07	219	5.93588e+06	27768.2	2.30851e+07	0.790426	5520.32	8.59996e+07	13957.9	1.88908e+07	14149.2	1.05021e+07	15440.5	1.25993e+07	1433.7	1.25993e+07	6803.59	1.67936e+07	6911.3	6.30784e+06	5798.72	1.67936e+07	5481.82	1.67936e+07	3984.31	1.67936e+07	17114.7	45079.2	43614.1	832639	1.18153e+06	8.15131e+06	3.08202e+07	47501.9	53680.8	4359	17129	19496.2	17350.5	88607.5	14733.3	10209.7	nan	nan
78663	20231110.27	115	1.97092e+06	368	1.15766e+07	214	5.93588e+06	28131.1	2.30851e+07	0.811127	5595.84	8.59996e+07	14031.2	1.67936e+07	14169.4	1.05021e+07	15563.8	1.46964e+07	1426.4	1.25993e+07	6879.24	1.88908e+07	7003.1	6.30784e+06	5810.37	1.67936e+07	5464.26	1.67936e+07	4001.19	1.67936e+07	17236.9	44884.9	45387.4	828814	1.18225e+06	8.13496e+06	3.07914e+07	42145	49644.3	4286.6	17151.5	18562.2	17358.3	78241	14946.5	10171	2395	403