Changing index into Configurations in MCccfraft.tla

[heidihoward]

I believe that there is currently an issue in MCccfraft.tla where the first configuration in Configurations is ignored. Currently, the initial configuration is any subset of servers and then the next configuration is the 2nd set of servers in Configurations and so on.

I'm not sure yet if this is the best fix (verse using a separate initial state in MCccfraft.tla). I think this is simplest fix so the best for now

This PR is related to (but separate from) #5778

[ghost]

tla-mcconfigs@77905 aka 20231025.60 vs main ewma over 20 builds from 77080 to 77900

Click to see table

main

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^	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	tpcc_virtual_cft^	ls_jwt_sgx_cft^	ls_jwt_sgx_cft_mem	pi_ls_jwt_sgx_cft^	pi_ls_jwt_sgx_cft_mem	ls_virtual_cft^	pi_ls_virtual_cft^	pi_basic_virtual_cft^	ls_js_sgx_cft^	ls_js_sgx_cft_mem	pi_basic_js_virtual_cft^	ls_full_js_sgx_cft^	ls_full_js_sgx_cft_mem	ls_jwt_virtual_cft^	pi_ls_jwt_virtual_cft^	ls_js_virtual_cft^	ls_js_jwt_sgx_cft^	ls_js_jwt_sgx_cft_mem	ls_full_js_virtual_cft^	ls_js_jwt_virtual_cft^	hist_sgx_cft^	RB put (/s)^	CHAMP put (/s)^	RB get (/s)^	CHAMP get (/s)^
77080	20231011.6	28231.3	2.30851e+07	0.805739	5614.98	8.59996e+07	77100.4	14016.4	1.67936e+07	14058.7	1.05021e+07	15607.1	1.25993e+07	1435.6	1.25993e+07	17356.8	6865.39	1.88908e+07	6917	6.30784e+06	45541.3	47443.3	53459.3	5768.86	1.67936e+07	4480.6	5749.11	1.67936e+07	17192.9	19626.7	16932.3	3974.5	1.67936e+07	16704.5	9841.59	44338.6	839572	1.1863e+06	8.14557e+06	3.07489e+07
77087	20231011.8	27891.2	2.51822e+07	0.821071	5620.28	8.59996e+07	83135	14043.4	1.88908e+07	14129.4	1.05021e+07	15619	1.46964e+07	1427.7	1.25993e+07	17648.9	6872.29	1.67936e+07	7079.7	6.30784e+06	45716.6	48214.1	53475.5	5780.82	1.67936e+07	4431.6	5765.08	1.67936e+07	17316.9	19004.2	17758.2	3974.44	1.67936e+07	16880.7	9849.81	40652.5	827510	1.16961e+06	8.14036e+06	3.30899e+07
77124	20231011.20	27859.9	2.51822e+07	0.810686	5576.3	8.59996e+07	81677.3	13934.9	1.88908e+07	14029.2	1.05021e+07	15421.8	1.25993e+07	1419.9	1.25993e+07	17272.2	6782.48	1.67936e+07	7028.9	6.30784e+06	45763.1	48479	54961.6	5759.88	1.67936e+07	4431	5495.58	1.88908e+07	17497.2	19917.1	17216.9	3980.45	1.67936e+07	16806.9	9875.23	42920	829281	1.17704e+06	8.02253e+06	3.09324e+07
77138	20231011.24	27788.7	2.51822e+07	0.817166	5505.15	8.59996e+07	79701.7	13944.3	1.88908e+07	14007.9	1.05021e+07	15414.3	1.46964e+07	1420.9	1.25993e+07	17450.2	6826.31	1.88908e+07	6933.7	6.30784e+06	43714.5	47439	54645.3	5805.03	1.67936e+07	4386.8	5491.25	1.67936e+07	16999.7	19561.8	17388.6	3992.65	1.67936e+07	14746.3	9915	39122	838714	1.18152e+06	8.09934e+06	3.09754e+07
77148	20231012.2	28066.3	2.51822e+07	0.806977	5622.22	8.59996e+07	88890.3	14012.7	1.88908e+07	14136.8	1.05021e+07	15607.9	1.25993e+07	1437.4	1.25993e+07	17218.1	6885.22	1.88908e+07	6981.9	6.30784e+06	46048.4	48655.6	55217	5813.57	1.67936e+07	4449.2	5723.57	1.88908e+07	17077.4	19720.8	17064.5	4000.45	1.67936e+07	15135.1	9799.03	45326.3	828634	1.17897e+06	8.14758e+06	3.07383e+07
77236	20231016.5	27858.7	2.51822e+07	0.79596	5620.83	8.59996e+07	59377	13995.4	1.88908e+07	14108.1	1.05021e+07	15609.7	1.46964e+07	1442	1.25993e+07	17148.6	6827.74	1.67936e+07	7065.1	6.30784e+06	45783.9	48719.4	54902.8	5817.83	1.67936e+07	4441	5743.02	1.67936e+07	17077.1	18804.1	17198.3	4006.32	1.67936e+07	15291.6	9993.77	44154.4	838342	1.17813e+06	8.15154e+06	3.18804e+07
77284	20231016.20	27801.1	2.30851e+07	0.800376	5523.42	8.59996e+07	76928.2	13858.5	1.88908e+07	14093.4	1.05021e+07	15419	1.46964e+07	1423.4	1.05021e+07	17222.7	6815.4	1.88908e+07	6872.8	6.30784e+06	45566.9	48808.1	54701.8	5802.5	1.67936e+07	4442.5	5472.72	1.67936e+07	17018.1	19157.5	17650.8	3973.37	1.67936e+07	14639.8	9852.83	43502.1	833609	1.17767e+06	8.15537e+06	3.06513e+07
77294	20231016.23	27413.6	2.51822e+07	0.822085	5504.43	8.59996e+07	84572	14028.1	1.88908e+07	14087.6	1.05021e+07	15527	1.46964e+07	1420.2	1.05021e+07	17297.3	6819.85	1.88908e+07	6931.4	6.30784e+06	45995.1	48594.2	53897	5754.38	1.67936e+07	4439.9	5710.32	1.67936e+07	17262.3	19125.2	17406.6	3992.44	1.67936e+07	14896.4	9812.12	41300	823461	1.17985e+06	8.1493e+06	3.05375e+07
77306	20231017.4	27907.4	2.30851e+07	0.806546	5649.91	8.59996e+07	60982.9	13997.7	1.88908e+07	14120.3	1.05021e+07	15513.7	1.46964e+07	1427.4	1.25993e+07	17275.1	6895.99	1.67936e+07	6972.2	6.30784e+06	46102.1	47686.9	53983.1	5811.89	1.67936e+07	4424.7	5778.4	1.67936e+07	17066.2	19713	14599.9	4010.44	1.67936e+07	14833.6	9890.99	45776.1	832093	1.181e+06	8.15615e+06	3.10764e+07
77410	20231019.5	27911.2	2.30851e+07	0.79845	5633.52	8.59996e+07	89839.8	14034.4	1.88908e+07	14172.6	1.05021e+07	15641.4	1.25993e+07	1439.9	1.25993e+07	17335.1	6838.11	1.67936e+07	7046.5	6.30784e+06	43709	47970.1	54598	5772.37	1.67936e+07	4449.7	5751.39	1.67936e+07	17103.2	19628.2	14821.2	4007.97	1.67936e+07	14920.8	9802.6	42755.2	840034	1.18128e+06	8.17441e+06	3.06839e+07
77459	20231020.5	27942.3	2.51822e+07	0.806882	5609.6	8.59996e+07	83682.7	14027.3	1.88908e+07	14086.4	1.05021e+07	15436.7	1.46964e+07	1431.9	1.25993e+07	17271.7	6873.38	1.88908e+07	6974.5	6.30784e+06	45556.9	48282.6	53165.7	5805.89	1.67936e+07	4426.2	5491.04	1.67936e+07	17066.3	17662.5	16990.3	3972.9	1.67936e+07	14844.7	9889.88	42113.3	830635	1.18094e+06	8.16668e+06	3.0923e+07
77461	20231020.6	27968.8	2.30851e+07	0.797578	5645.01	8.59996e+07	86522.6	13956.1	1.88908e+07	14152	1.05021e+07	15499.4	1.46964e+07	1437.7	1.25993e+07	17246.7	7235.96	1.67936e+07	7078.7	6.30784e+06	45887.8	48453.6	54176.2	5801.29	1.67936e+07	4426.2	5742.38	1.67936e+07	17079.1	19435.2	15003.7	3995.17	1.67936e+07	14699.8	9770.09	43030.2	825201	1.1798e+06	8.16489e+06	3.14443e+07
77485	20231020.14	27955.5	2.51822e+07	0.827982	5614.45	8.59996e+07	67488.2	14042.3	1.67936e+07	14155.3	1.05021e+07	15587	1.46964e+07	1441.5	1.25993e+07	17203.3	7220.81	1.67936e+07	6925.4	6.30784e+06	45720.2	47505.9	52771.4	5824.33	1.67936e+07	4441	5745.31	1.67936e+07	17168.5	19652.2	16950.7	3980.22	1.67936e+07	14720	9771.33	46913.9	831368	1.1798e+06	8.12782e+06	3.08955e+07
77532	20231020.31	27967.5	2.51822e+07	0.835073	5614.22	8.59996e+07	60943.5	14001.1	1.88908e+07	14174.9	1.05021e+07	15520.9	1.46964e+07	1429.6	1.25993e+07	17092.6	7252.76	1.67936e+07	7086.5	6.30784e+06	43713.6	47796.6	52609.1	5806.4	1.67936e+07	4332.3	5491.29	1.67936e+07	17195.4	19336.7	17022.6	4001.82	1.67936e+07	14750.8	10188.5	40351.5	833120	1.18235e+06	8.17343e+06	3.12829e+07
77555	20231023.5	28238.2	2.51822e+07	0.816011	5639.66	8.59996e+07	74767.3	14029.3	1.88908e+07	14118.1	1.05021e+07	15640.2	1.46964e+07	1432.7	1.25993e+07	17264.2	7273.33	1.67936e+07	6953.5	6.30784e+06	45924.9	47674	53843.3	5781.01	1.67936e+07	4365.2	5742.5	1.67936e+07	17152.3	19152.3	17286.3	3995.51	1.67936e+07	14910.6	10169.6	43068.6	829052	1.18151e+06	8.148e+06	3.09408e+07
77584	20231023.15	27775.2	2.51822e+07	0.839543	5525.06	8.59996e+07	63643	13936	1.88908e+07	13990.4	1.05021e+07	15424.6	1.46964e+07	1427	1.25993e+07	17237.3	6853.5	1.88908e+07	6881.2	6.30784e+06	43785.4	47940.2	54114.3	5758.93	1.67936e+07	4430	5762.09	1.67936e+07	17010.7	19396.4	17307.2	3983.52	1.67936e+07	14810.6	9823.55	42679.4	825381	1.18095e+06	8.16893e+06	3.13159e+07
77665	20231024.10	28077.5	2.30851e+07	0.782853	5565	8.59996e+07	71956.1	13918.6	1.88908e+07	14015.8	1.05021e+07	15439.4	1.46964e+07	1417.5	1.25993e+07	17332.4	6827.52	1.88908e+07	6933.8	6.30784e+06	43627.5	47460.4	55764.1	5759.87	1.67936e+07	4480.7	5778.73	1.67936e+07	16984.5	19600.5	17210.4	3994.77	1.67936e+07	15032.4	9934.79	42277.7	837727	1.17659e+06	8.1335e+06	3.08424e+07
77722	20231024.29	28002.9	2.51822e+07	0.808583	5477.83	8.59996e+07	68825.6	13980.7	1.88908e+07	14011.7	1.05021e+07	15103.3	1.46964e+07	1409.7	1.25993e+07	17482.9	6842.46	1.88908e+07	6811.8	6.30784e+06	43910	47389.3	55105.8	5772.89	1.67936e+07	4422.3	5489.45	1.67936e+07	16897.2	19100.4	17082.1	4013.18	1.67936e+07	15051.5	9901.25	43837.6	824014	1.17985e+06	8.16421e+06	3.03628e+07
77856	20231025.44	27880.1	2.30851e+07	0.830072	5666.89	8.59996e+07	84849.8	14118.2	1.88908e+07	14176.7	1.05021e+07	15508.7	1.46964e+07	1425.1	1.25993e+07	17303.7	7259.6	1.67936e+07	6931.4	6.30784e+06	45783	47925.3	54083.6	5816.26	1.67936e+07	4428.6	5714.88	1.67936e+07	17130.6	18998.8	17531.7	3996.87	1.67936e+07	14906.9	9965.7	44821	832615	1.17692e+06	8.17447e+06	3.1229e+07
77900	20231025.59	27968.9	2.30851e+07	0.816541	5546.67	8.59996e+07	81852.5	13948.6	1.88908e+07	14105.4	1.05021e+07	15469.3	1.46964e+07	1430.1	1.25993e+07	17281.4	6806.65	1.88908e+07	6880.7	6.30784e+06	45862.6	47692.2	54378.7	5770.88	1.67936e+07	4430.3	5488.27	1.88908e+07	17128.6	18994.4	17211.3	3990.38	1.67936e+07	14724.7	9880.77	42489.7	839143	1.18218e+06	8.15475e+06	3.09642e+07

tla-mcconfigs

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	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^	pi_basic_mt_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)^
77864	20231025.45	27992.3	2.51822e+07	0.799767	5526.61	8.59996e+07	17210.2	45699	47677.9	13930.1	1.88908e+07	54408.3	14024.5	1.05021e+07	15293.4	1.46964e+07	4425	17131.3	19133.6	87720.8	17213.6	14722	1410.9	1.25993e+07	10397.2	6838.29	1.88908e+07	6834.5	6.30784e+06	5803.3	1.67936e+07	5482.64	1.67936e+07	41553.2	3978.87	1.67936e+07	834732	1.18253e+06	8.14505e+06	3.11986e+07
77905	20231025.60	28048.4	2.51822e+07	0.795069	5555.8	8.59996e+07	17320.6	44146.2	48326.9	14015.7	1.88908e+07	54675.7	14110.5	1.05021e+07	15461.1	1.25993e+07	4426	17393.6	19066.5	76257.8	17379.4	14855.2	1426.7	1.25993e+07	10150.1	6837.44	1.88908e+07	6877.6	6.30784e+06	5755.07	1.67936e+07	5488.12	1.67936e+07	43752.2	3990.54	1.67936e+07	825976	1.17768e+06	8.15277e+06	3.07304e+07

[heidihoward]

This change which should slow down the exhaustive model checking, is making MCccfraftWithReconfig.cfg faster for reasons which are not obvious to me. https://github.com/microsoft/CCF/actions/runs/6641887323/job/18045392763#step:6:59

[heidihoward]

Mystery solved, I needed to increase the ViewLimit to allow all three reconfigurations

[lemmy]

Can we remove reconfigurationCount and constraint the number of reconfigurations with MaxTermLimit and leave picking the next config to CHOOSE c \in SUBSET Servers : c \notin {previous configs inferred from committed log}?

[heidihoward]

Can we remove reconfigurationCount and constraint the number of reconfigurations with MaxTermLimit and leave picking the next config to CHOOSE c \in SUBSET Servers : c \notin {previous configs inferred from committed log}?

Yes, I believe we can. I'll try this refactor in a separate PR