TV for startup followed by join

[achamayou]

Matches, except sent_idx/nextIdx, but I claim we want to look at that separately, as suggested in #5895.

[lemmy]

I'll switch to Codespaces to get the debugger on Monday.

Remember to add -DTLA-Library=.. to "Tlaplus › Java: Options" in VSCode.

[ghost]

startup_2nodes@80082 aka 20240109.26 vs main ewma over 20 builds from 79809 to 80055

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	ls_js_sgx_cft^	ls_js_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	tpcc_virtual_cft^	ls_full_js_sgx_cft^	ls_full_js_sgx_cft_mem	ls_virtual_cft^	pi_ls_virtual_cft^	ls_js_jwt_sgx_cft^	ls_js_jwt_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^	ls_full_js_virtual_cft^	hist_sgx_cft^	ls_js_jwt_virtual_cft^	RB put (/s)^	CHAMP put (/s)^	RB get (/s)^	CHAMP get (/s)^	tlc_sim_traces	tlc_sim_levelmean	pi_basic_mt_virtual_cft^
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	5809.21	1.67936e+07	6	86496	427	1.2541e+07	241	6.31473e+06	17426.2	5725.47	1.88908e+07	52688.3	56487.3	4000.63	1.67936e+07	62076.8	4588.5	20938.1	21383.1	17806.2	17373.5	39813.8	11613.7	838128	1.18558e+06	8.15241e+06	3.07577e+07	2304	403	89517.2
79821	20240102.7	0.812237	28223.4	2.30851e+07	5591.2	8.59996e+07	14003.1	1.88908e+07	14188.3	1.05021e+07	15498.1	1.46964e+07	1429.2	1.25993e+07	7246.07	1.67936e+07	6934.2	6.30784e+06	5809.09	1.67936e+07	7	86496	446	1.2541e+07	237	6.31473e+06	17312.2	5478.56	1.67936e+07	53352.6	57235.7	4007.06	1.67936e+07	62129.2	4590.4	21078.7	22285.6	20842.2	17429	40366	11612.2	832255	1.17903e+06	8.15355e+06	3.03592e+07	2331	403	100850
79832	20240102.10	0.780568	27705.2	2.51822e+07	5592.62	8.59996e+07	14075.6	1.88908e+07	14247	1.05021e+07	15580.2	1.46964e+07	1429.8	1.25993e+07	6842.56	1.67936e+07	7079.5	6.30784e+06	5781.21	1.67936e+07	6	86496	424	1.2541e+07	245	6.31473e+06	17247.1	5767.74	1.67936e+07	52935.7	56910	3982.1	1.67936e+07	62683.8	4647.1	20739.3	20193.9	20729.9	17575.8	42743.5	11690.8	823735	1.18304e+06	8.15511e+06	3.0778e+07	2301	403	90345.4
79836	20240103.1	0.8277	28173	2.51822e+07	5617.23	8.59996e+07	14088.9	1.88908e+07	14246.2	1.05021e+07	15684.4	1.46964e+07	1430.6	1.25993e+07	7262.76	1.67936e+07	6980.2	6.30784e+06	5814.99	1.67936e+07	6	86496	417	1.2541e+07	238	6.31473e+06	17163.7	5465.89	1.88908e+07	52985.4	57238.7	3973.9	1.67936e+07	62511.8	4622.6	20776.5	21693.9	20385	17974.8	43365.4	11889.2	827987	1.18005e+06	8.16857e+06	3.13533e+07	2109	403	68113.2
79850	20240104.1	0.774183	28107.5	2.51822e+07	5647.78	8.59996e+07	14069.1	1.88908e+07	14203.3	1.05021e+07	15616.9	1.25993e+07	1430.7	1.25993e+07	7263.29	1.67936e+07	7142	6.30784e+06	5808.21	1.67936e+07	6	86496	447	1.2541e+07	239	6.31473e+06	17222.5	5739.03	1.88908e+07	53076.9	56886.7	4019.28	1.67936e+07	62583	4618.3	20820.4	21956.8	17246.1	17545.1	45361.8	11727	833007	1.17531e+06	8.1401e+06	3.07056e+07	2277	403	88847.3
79858	20240104.5	0.762951	28151.4	2.30851e+07	5612.73	8.59996e+07	14105.1	1.88908e+07	14237.6	1.05021e+07	15657.2	1.46964e+07	1437	1.05021e+07	7259.07	1.88908e+07	6983.6	6.30784e+06	5791.47	1.67936e+07	6	86496	420	1.2541e+07	238	6.31473e+06	17237.2	5734.66	1.67936e+07	53156.1	56700.3	4001.19	1.67936e+07	62251.6	4624.7	20802.9	22305.5	17912	17600.9	46312.7	12005.6	832473	1.18246e+06	8.14589e+06	3.0464e+07	2357	403	72092.6
79876	20240104.10	0.770841	27983.2	2.51822e+07	5617.52	8.59996e+07	14034.5	1.67936e+07	14165.8	1.05021e+07	15592.9	1.25993e+07	1427.3	1.25993e+07	7241.98	1.67936e+07	6915.4	6.30784e+06	5771.22	1.67936e+07	6	86496	429	1.2541e+07	234	6.31473e+06	17196.9	5737.28	1.67936e+07	53164.5	56410.8	3985.63	1.67936e+07	62397	4645.9	20949.8	22178.9	17324.7	17551.5	40222.9	11659.7	829045	1.18083e+06	8.15014e+06	3.10298e+07	2315	403	82253.2
79893	20240105.3	0.770387	28242.6	2.30851e+07	5619.63	8.59996e+07	14091.5	1.88908e+07	14247.6	1.05021e+07	15674.3	1.25993e+07	1436.8	1.25993e+07	7241.21	1.67936e+07	7028.1	6.30784e+06	5776.46	1.67936e+07	6	86496	438	1.2541e+07	234	6.31473e+06	17195.7	5739.53	1.67936e+07	53109.3	56423.9	4001.54	1.67936e+07	61913.6	4637.7	21053.6	21897.2	17479.2	17489.6	41192.1	11786.3	834184	1.18333e+06	8.13454e+06	3.07928e+07	2312	403	79459.2
79901	20240105.6	0.804442	28134.7	2.51822e+07	5625.32	8.59996e+07	14099	1.88908e+07	14266.8	1.05021e+07	15657.8	1.46964e+07	1428.6	1.25993e+07	6896.08	1.67936e+07	7033.2	6.30784e+06	5807.41	1.67936e+07	6	86496	445	1.2541e+07	240	6.31473e+06	17253.5	5744.67	1.88908e+07	52754.9	54886.9	4003.65	1.67936e+07	61431.1	4615.1	20971.5	21889.5	17410.2	17219.9	42166	11532.7	837682	1.17356e+06	8.14881e+06	3.18111e+07	2258	403	96416.1
79920	20240105.14	0.804667	28090.3	2.51822e+07	5642.82	8.59996e+07	14097.8	1.88908e+07	14249.7	1.05021e+07	15643	1.46964e+07	1426.1	1.25993e+07	6883.92	1.88908e+07	6976.3	6.30784e+06	5819.57	1.67936e+07	6	86496	434	1.2541e+07	235	6.31473e+06	17195.4	5767.4	1.67936e+07	53484.4	56927.5	3983.21	1.67936e+07	63034.1	4635.9	20600.9	21708	20208.9	17600.9	42864.9	11868.5	816929	1.18007e+06	8.14615e+06	3.06564e+07	2325	403	72389.5
79931	20240105.18	0.830304	28155.9	2.51822e+07	5572.38	8.59996e+07	14067.9	1.67936e+07	14143.9	1.05021e+07	15609.5	1.25993e+07	1433	1.25993e+07	6844.24	1.67936e+07	6937.8	6.30784e+06	5775.62	1.67936e+07	6	86496	436	1.2541e+07	236	6.31473e+06	17203.8	5454.13	1.67936e+07	53081	57491.7	3990.64	1.67936e+07	63657.6	4644.3	20979.1	21753.3	20837.9	17426.7	41115.6	11781.2	835630	1.17185e+06	8.15319e+06	3.14385e+07	2224	403	78451.8
79937	20240105.20	0.788583	28053.5	2.51822e+07	5577.35	8.59996e+07	14052.4	1.88908e+07	14109.9	1.05021e+07	15547.2	1.46964e+07	1435.2	1.25993e+07	7233.07	1.67936e+07	6844.1	6.30784e+06	5802.33	1.67936e+07	6	77678	366	1.14441e+07	223	5.86578e+06	17208.8	5491.67	1.67936e+07	56022.5	56925.6	3998.46	1.67936e+07	63903.6	4666.7	20742.8	21552.2	20961.9	17614	47083.7	11908.4	832419	1.18053e+06	8.15387e+06	3.21896e+07	2256	403	85420.8
79954	20240108.2	0.811783	28237	2.30851e+07	5591.06	8.59996e+07	14064.6	1.88908e+07	14197.4	1.05021e+07	15540.4	1.46964e+07	1431.6	1.25993e+07	7263.29	1.67936e+07	7083.5	6.30784e+06	5819.68	1.67936e+07	6	77678	393	1.14441e+07	225	5.86578e+06	17316.8	5772.06	1.67936e+07	53076.6	55248.3	4006.27	1.67936e+07	60320.6	4528.2	20993.9	21334.7	17858.4	17621.1	41219.2	11538.3	823934	1.18456e+06	8.13305e+06	3.08225e+07	2191	403	99047.8
79961	20240108.5	0.812651	27925.4	2.51822e+07	5643.13	8.59996e+07	14080.8	1.67936e+07	14230.5	1.05021e+07	15627.5	1.25993e+07	1428.6	1.25993e+07	7265.93	1.67936e+07	6978.2	6.30784e+06	5819.84	1.67936e+07	5	77678	377	1.14441e+07	219	5.86578e+06	17247.2	5491.66	1.88908e+07	53409.5	56958	3978.52	1.67936e+07	63490.4	4632.7	20797.7	22702.5	20869.2	17815.9	43913.1	11888.8	834677	1.17721e+06	8.13573e+06	3.1303e+07	2280	403	85416
79989	20240108.17	0.812918	28271	2.51822e+07	5581.25	8.59996e+07	14031.6	1.67936e+07	14136.4	1.05021e+07	15523.6	1.46964e+07	1415.9	1.25993e+07	7249.22	1.67936e+07	6933.6	6.30784e+06	5811.81	1.67936e+07	6	77678	392	1.14441e+07	220	5.87421e+06	17262.7	5488.58	1.67936e+07	52887.3	55918.4	3984.32	1.67936e+07	62745.3	4610.5	20923.3	22286.1	20921.3	17621.5	45321.3	11740.7	831008	1.18097e+06	8.15374e+06	3.08415e+07	2380	403	78403.9
80001	20240108.22	0.786976	28214.4	2.30851e+07	5635.92	8.59996e+07	14107	1.67936e+07	14229	1.05021e+07	15650.3	1.25993e+07	1429.2	1.05021e+07	7261.71	1.67936e+07	7084.9	6.30784e+06	5822.41	1.67936e+07	6	77678	147	3.90715e+06	144	3.83177e+06	17220.1	5738.66	1.67936e+07	52740.1	56590.9	3986.1	1.67936e+07	62501.5	4637.4	20710.5	21594.5	20773	17397.2	45877	11679.9	835642	1.18258e+06	8.17072e+06	3.06881e+07	2749	403	82485.2
80019	20240109.2	0.779573	27799.4	2.51822e+07	5541.95	8.59996e+07	13996.1	1.88908e+07	14114.4	1.05021e+07	15421.9	1.25993e+07	1423.3	1.25993e+07	6843.67	1.67936e+07	6964.2	6.30784e+06	5808.73	1.67936e+07	5	77678	150	3.90715e+06	149	3.83177e+06	17676.2	5734.06	1.67936e+07	53244.4	56053.5	4019.09	1.67936e+07	61572.3	4586.7	20734.2	22425.5	17371.7	17383.5	40846.9	11766.6	840733	1.17962e+06	8.12931e+06	3.06812e+07	2587	403	92062.2
80028	20240109.6	0.773671	28077.7	2.51822e+07	5668.81	8.59996e+07	14080.8	1.88908e+07	14176.2	1.05021e+07	15684.6	1.46964e+07	1435.3	1.25993e+07	6914.02	1.88908e+07	7048.5	6.30784e+06	5802.22	1.67936e+07	5	77678	150	3.90715e+06	146	3.83177e+06	17211.9	5766.41	1.67936e+07	53026.8	58109.1	3999.26	1.67936e+07	61402.2	4691.4	20760.8	22245	20537.9	17634	43293	11758.4	830215	1.18604e+06	8.15176e+06	3.07125e+07	2686	403	80572.2
80038	20240109.10	0.804995	27757.8	2.30851e+07	5590.07	8.59996e+07	14106.5	1.88908e+07	14170.6	1.05021e+07	15627.6	1.25993e+07	1424.9	1.25993e+07	6806.45	1.67936e+07	7055.6	6.30784e+06	5772.08	1.67936e+07	6	77678	148	3.90715e+06	149	3.83177e+06	17787.8	5731.73	1.67936e+07	52786.7	56588	3997.66	1.67936e+07	62017.1	4618.3	21127.5	22348.4	20872.7	17348.9	46610.2	11716.9	793924	1.17586e+06	8.15647e+06	3.07947e+07	2762	403	82244.9
80055	20240109.17	0.801944	28125.3	2.51822e+07	5553.42	8.59996e+07	14011.9	1.88908e+07	14117.8	1.05021e+07	15653.4	1.25993e+07	1440.5	1.25993e+07	6840.17	1.88908e+07	6906.2	6.30784e+06	5773.25	1.67936e+07	6	77678	150	3.90715e+06	150	3.83177e+06	17168	5487.83	1.88908e+07	53353.8	56983.3	3992.89	1.67936e+07	62914.7	4671.7	20784.1	21676.9	20551.7	17667.4	45493	11750.6	839102	1.17961e+06	8.13667e+06	3.07457e+07	2683	403	83110

startup_2nodes

build_id	build_number	pi_basic_mt_virtual_cft^	Commit latency factor	pi_basic_mt_sgx_cft^	pi_basic_mt_sgx_cft_mem	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_sgx_cft^	ls_sgx_cft_mem	ls_jwt_virtual_cft^	pi_ls_sgx_cft^	pi_ls_sgx_cft_mem	pi_ls_jwt_virtual_cft^	pi_basic_sgx_cft^	pi_basic_sgx_cft_mem	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	hist_sgx_cft^	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)^	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
80015	20240108.27	82300.4	0.792547	28224.6	2.51822e+07	17258.1	5620.61	8.59996e+07	53151.2	56885.7	61085.3	4584	14040.6	1.67936e+07	21024.6	14165.3	1.05021e+07	21330.1	15548.7	1.46964e+07	17449.9	17434	11797.8	1426.1	1.25993e+07	7245.62	1.67936e+07	6971.6	6.30784e+06	47179.9	5773.39	1.67936e+07	5728.07	1.88908e+07	3976.52	1.67936e+07	824537	1.18001e+06	8.12673e+06	3.06339e+07	6	77678	206	5.77852e+06	186	5.0742e+06	4315	403
80073	20240109.22	85928.1	0.785064	28024.7	2.51822e+07	17294	5635.3	8.59996e+07	55628.6	57912.9	62454.8	4681.7	14061.6	1.88908e+07	20749.9	14170.4	1.05021e+07	22122.4	15649	1.25993e+07	21017.4	17631.6	11866.3	1431.9	1.25993e+07	6830.36	1.67936e+07	7192.7	6.30784e+06	45890.7	5803.98	1.67936e+07	5725.92	1.67936e+07	4010.09	1.67936e+07	829332	1.17806e+06	8.15563e+06	3.07129e+07	6	77678	213	5.77852e+06	194	5.0742e+06	4398	403
80082	20240109.26	67563	0.784084	27948.9	2.30851e+07	17738.2	5602.98	8.59996e+07	52888.2	56207.9	62223.6	4658.8	14037.9	1.67936e+07	20908.4	14191	1.05021e+07	21850.3	15587.4	1.46964e+07	20654.4	17319.5	11681.1	1424.5	1.25993e+07	7207.28	1.88908e+07	6979.7	6.30784e+06	44586.3	5809.95	1.67936e+07	5505.68	1.67936e+07	3992.39	1.67936e+07	828280	1.17495e+06	8.14839e+06	3.01776e+07	6	77678	207	5.77852e+06	193	5.0742e+06	3424	403

[achamayou]

So the change to UpdateTerm to transition None to Follower has broken the MC/Sim, because we do not restrict the sending of AppendEntries: a leader can send AEs to any node, even those not in configuration. This is of course not what the implementation does, and cause LogConfigurationConsistentInv to break.