Another subset of small improvements of TLA+ specification listed in #4264

[lemmy]

The previous PR squashed all commits when merged into main. The commits in this PR are independent of each other. I'd suggest keeping the individual commits when merging.

[heidihoward]

The previous PR squashed all commits when merged into main. The commits in this PR are independent of each other. I'd suggest keeping the individual commits when merging.

Thanks for highlighting this. Squashing commits is the default for this repo. We try to aim for small incremental PRs (but sometimes fail, as demonstrated by yours truly with https://github.com/microsoft/CCF/pull/3965).

@achamayou Is this something we easily modify on a per PR basis? or what workaround would you suggest? Markus's commit messages include useful context on the changes made.

[lemmy]

FYI: The motivation to extract/refactor what are essentially hardwired state constraints is strategically enabling simulation, liveness checking, bounded model-checking, and proofs. Also, a true state constraint causes a 2x slowdown in TLC because the state constraint is expensive to evaluate, and the number of generated goes up significantly (see https://github.com/lemmy/CCF/tree/mku-gh4264-3).

[heidihoward]

Thanks for highlighting this. Squashing commits is the default for this repo. We try to aim for small incremental PRs (but sometimes fail, as demonstrated by yours truly with #3965).

@achamayou Is this something we easily modify on a per PR basis? or what workaround would you suggest? Markus's commit messages include useful context on the changes made.

I discussed this with the team this morning and there is a preference for squashing for consistency with the other commits to main. The workflow for reviewing code history is to use git praise to go to the PR and then review the PR description/comments/commits for a more fine-grained explanation.

This approach (along with a few other things) makes more sense for the production code than it does for the TLA+ spec. One solution is to put the TLA+ spec into a separate repo, but the idea behind having the spec live alongside the production code is to try to keep them both in sync (and maybe even enforce this one day with trace checking CI)

[achamayou]

@lemmy adding to what @heidihoward has said: we can enable "Rebase and merge" as a choice when merging, and you/we/whoever merges this PR could make use of that. It's not our preference in general, but if you feel strongly about it, we'll do it :)

[lemmy]

I have a few more commits pending that depend on the current commits in this PR. Do you want me to push those into this or open more PRs?

[heidihoward]

Opening seperate PRs is preferable if that's ok with you

[heidihoward]

/azp run

[azure-pipelines[bot]]

Azure Pipelines successfully started running 2 pipeline(s).

[ccf-bot]

mku-gh4264-2@52623 aka 20221031.29 vs main ewma over 20 builds from 52062 to 52542

Click to see table

main | build_id | build_number | tpcc_virtual_cft^ | tpcc_virtual_cft_mem | ls_virtual_cft^ | ls_virtual_cft_mem | ls_jwt_virtual_cft^ | ls_jwt_virtual_cft_mem | ls_js_virtual_cft^ | ls_js_virtual_cft_mem | ls_full_js_virtual_cft^ | ls_full_js_virtual_cft_mem | ls_js_jwt_virtual_cft^ | ls_js_jwt_virtual_cft_mem | hist_sgx_cft^ | tpcc_sgx_cft^ | tpcc_sgx_cft_mem | ls_sgx_cft^ | ls_sgx_cft_mem | ls_jwt_sgx_cft^ | 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 | RB put (/s)^ | CHAMP put (/s)^ | RB get (/s)^ | CHAMP get (/s)^ | |-----------:|:---------------|--------------------:|-----------------------:|------------------:|---------------------:|----------------------:|-------------------------:|---------------------:|------------------------:|--------------------------:|-----------------------------:|-------------------------:|----------------------------:|----------------:|----------------:|-------------------:|--------------:|-----------------:|------------------:|---------------------:|-----------------:|--------------------:|----------------------:|-------------------------:|---------------------:|------------------------:|---------------:|------------------:|---------------:|------------------:| | 52062 | 20221025.1 | 10867.9 | 0 | 43201.8 | 0 | 10139.3 | 0 | 4325.6 | 0 | 3455.55 | 0 | 3413.03 | 0 | 28088.8 | 5619.86 | 8.29727e+07 | 17763.6 | 1.6126e+07 | 6027.95 | 1.56017e+07 | 2351.98 | 9.31027e+06 | 1976.69 | 9.31027e+06 | 1924.45 | 9.04813e+06 | 908070 | 1.35376e+06 | 9.20019e+06 | 3.47702e+07 | | 52148 | 20221025.38 | 11063.7 | 0 | 40818 | 0 | 10463.8 | 0 | 4339.26 | 0 | 3383.05 | 0 | 3229.84 | 0 | 28238.2 | 5718.6 | 8.29727e+07 | 17753.4 | 1.6126e+07 | 6044.86 | 1.58639e+07 | 2358.53 | 9.57242e+06 | 1979.66 | 9.57242e+06 | 1921.17 | 9.04813e+06 | 888304 | 1.37246e+06 | 9.46824e+06 | 3.58036e+07 | | 52163 | 20221025.43 | 11038.1 | 0 | 41761.6 | 0 | 10179 | 0 | 4350.36 | 0 | 3469.75 | 0 | 3335.97 | 0 | 28399.5 | 5600.9 | 8.32349e+07 | 17696.9 | 1.66503e+07 | 6085.06 | 1.56017e+07 | 2358.74 | 9.83456e+06 | 1983.17 | 9.57242e+06 | 1889.35 | 9.31027e+06 | 903435 | 1.38201e+06 | 9.39881e+06 | 3.62478e+07 | | 52174 | 20221025.47 | 11133.2 | 0 | 43517.8 | 0 | 10340.2 | 0 | 4330.74 | 0 | 3411.3 | 0 | 3218.81 | 0 | 27570.9 | 5689.44 | 8.32349e+07 | 17535.4 | 1.63882e+07 | 6022.79 | 1.58639e+07 | 2412.92 | 9.57242e+06 | 1918.01 | 9.83456e+06 | 1919.16 | 9.31027e+06 | 914116 | 1.40687e+06 | 9.30901e+06 | 3.61831e+07 | | 52195 | 20221026.2 | 11554.9 | 0 | 41858.6 | 0 | 10139.1 | 0 | 4270.16 | 0 | 3340.51 | 0 | 3053.82 | 0 | 27354.3 | 5681.17 | 8.3497e+07 | 17589.3 | 1.66503e+07 | 6028.17 | 1.53396e+07 | 2370.68 | 9.57242e+06 | 1984.11 | 9.57242e+06 | 1963.27 | 9.04813e+06 | 903111 | 1.34426e+06 | 9.21269e+06 | 3.58042e+07 | | 52214 | 20221026.8 | 11377 | 0 | 43249 | 0 | 10217.2 | 0 | 4275.83 | 0 | 3312.68 | 0 | 3029.65 | 0 | 23651.4 | 5602.67 | 8.27106e+07 | 17410.9 | 1.6126e+07 | 6036.44 | 1.53396e+07 | 2364.04 | 9.57242e+06 | 1979.57 | 9.31027e+06 | 1879.58 | 9.04813e+06 | 884697 | 1.3768e+06 | 9.30055e+06 | 3.57411e+07 | | 52321 | 20221026.31 | 10453 | 0 | 38970.4 | 0 | 10294.1 | 0 | 4251.76 | 0 | 3285.73 | 0 | 3177.25 | 0 | 27773.5 | 5580.3 | 8.27106e+07 | 15985.1 | 1.63882e+07 | 5350.9 | 1.50774e+07 | 2045.31 | 8.78598e+06 | 1683.25 | 8.78598e+06 | 1609.17 | 7.99955e+06 | 832968 | 1.18137e+06 | 8.17226e+06 | 3.08369e+07 | | 52328 | 20221026.34 | 10406.6 | 0 | 42425.6 | 0 | 10133.3 | 0 | 4210.29 | 0 | 3311.42 | 0 | 3102.98 | 0 | 26285.5 | 5539.42 | 8.29727e+07 | 16169.2 | 1.63882e+07 | 5419.9 | 1.53396e+07 | 2044.22 | 8.78598e+06 | 1698.7 | 9.04813e+06 | 1633.03 | 7.99955e+06 | 837046 | 1.17644e+06 | 8.1554e+06 | 3.08299e+07 | | 52354 | 20221026.44 | 10994.5 | 0 | 43307.1 | 0 | 10571.3 | 0 | 4305.09 | 0 | 3401.98 | 0 | 3203.79 | 0 | 29508.5 | 5613.1 | 8.32349e+07 | 16113.1 | 1.63882e+07 | 5476.42 | 1.50774e+07 | 2037.63 | 8.78598e+06 | 1699.13 | 8.52384e+06 | 1613.01 | 7.99955e+06 | 841627 | 1.17455e+06 | 8.11629e+06 | 3.18141e+07 | | 52361 | 20221027.2 | 11278.3 | 0 | 42344.7 | 0 | 10238.3 | 0 | 4462.95 | 0 | 3416.97 | 0 | 3359.41 | 0 | 24552.5 | 5624.01 | 8.29727e+07 | 16270 | 1.63882e+07 | 5511.84 | 1.50774e+07 | 2106.3 | 8.78598e+06 | 1695.12 | 8.78598e+06 | 1627.48 | 8.2617e+06 | 786062 | 1.17803e+06 | 8.13531e+06 | 3.08229e+07 | | 52379 | 20221027.8 | 10670.5 | 0 | 41077.2 | 0 | 9739 | 0 | 4216.82 | 0 | 3525.8 | 0 | 3227.53 | 0 | 22220.2 | 5581.03 | 8.27106e+07 | 16078.2 | 1.6126e+07 | 5503.73 | 1.53396e+07 | 2074.76 | 9.31027e+06 | 1696.53 | 8.78598e+06 | 1634.42 | 7.99955e+06 | 833507 | 1.18032e+06 | 8.17509e+06 | 3.07203e+07 | | 52399 | 20221027.15 | 10627.3 | 0 | 39767.1 | 0 | 10549.9 | 0 | 4254.08 | 0 | 3344.72 | 0 | 3247.66 | 0 | 24358.2 | 5548.85 | 8.29727e+07 | 16077.7 | 1.63882e+07 | 5485.35 | 1.53396e+07 | 2048.86 | 8.52384e+06 | 1680.39 | 8.78598e+06 | 1635.04 | 8.2617e+06 | 834019 | 1.17717e+06 | 8.1553e+06 | 3.07854e+07 | | 52405 | 20221027.17 | 10335.5 | 0 | 39075.6 | 0 | 9752.7 | 0 | 4231.41 | 0 | 3536.45 | 0 | 3192.94 | 0 | 23452.7 | 5608.57 | 8.27106e+07 | 16344.9 | 1.6126e+07 | 5562.37 | 1.58639e+07 | 2063.86 | 9.31027e+06 | 1690.84 | 8.52384e+06 | 1617.92 | 7.99955e+06 | 838816 | 1.17836e+06 | 8.154e+06 | 3.07896e+07 | | 52417 | 20221027.21 | 11201.8 | 0 | 40626.7 | 0 | 10661.6 | 0 | 4317.76 | 0 | 3419.76 | 0 | 3268.04 | 0 | 24057.8 | 5488.35 | 8.32349e+07 | 16047.7 | 1.63882e+07 | 5461.25 | 1.56017e+07 | 2041.66 | 9.04813e+06 | 1675.77 | 8.52384e+06 | 1604.46 | 7.73741e+06 | 818448 | 1.17821e+06 | 8.14499e+06 | 3.07535e+07 | | 52450 | 20221027.36 | 11209.9 | 0 | 39970 | 0 | 10115.7 | 0 | 4332.35 | 0 | 3518.27 | 0 | 3367.28 | 0 | 28711.9 | 5653.36 | 8.45456e+07 | 16833.6 | 1.71746e+07 | 6089.56 | 1.53396e+07 | 2341.41 | 9.83456e+06 | 1971.75 | 9.31027e+06 | 1906.04 | 9.04813e+06 | 905548 | 1.34515e+06 | 9.2879e+06 | 3.53097e+07 | | 52457 | 20221028.1 | 11177.8 | 0 | 40727.3 | 0 | 10101.5 | 0 | 4382.02 | 0 | 3440.65 | 0 | 3174.64 | 0 | 28786.6 | 5647.7 | 8.3497e+07 | 17338.3 | 1.71746e+07 | 6080.41 | 1.58639e+07 | 2368.58 | 9.31027e+06 | 1944.24 | 9.31027e+06 | 1919.89 | 9.04813e+06 | 903075 | 1.36953e+06 | 9.23354e+06 | 3.55556e+07 | | 52481 | 20221028.11 | 11055.9 | 0 | 40501.3 | 0 | 10172.4 | 0 | 4280.41 | 0 | 3449.25 | 0 | 3080.9 | 0 | 23372.9 | 5667.16 | 8.27106e+07 | 17370.1 | 1.66503e+07 | 6046.24 | 1.53396e+07 | 2319.49 | 9.57242e+06 | 1984.44 | 9.57242e+06 | 1916.44 | 9.04813e+06 | 906671 | 1.37044e+06 | 9.17966e+06 | 3.57417e+07 | | 52513 | 20221028.24 | 10988.1 | 0 | 41192.4 | 0 | 10370.2 | 0 | 4321.82 | 0 | 3446.62 | 0 | 3193.77 | 0 | 28825.8 | 5617.3 | 8.29727e+07 | 17318.8 | 1.69124e+07 | 6079.54 | 1.56017e+07 | 2356.67 | 9.83456e+06 | 1971.67 | 1.19317e+07 | 1953.53 | 9.31027e+06 | 920528 | 1.38753e+06 | 9.3303e+06 | 3.47113e+07 | | 52529 | 20221031.1 | 11317.6 | 0 | 42713.1 | 0 | 10189.6 | 0 | 4384.6 | 0 | 3465.19 | 0 | 3239.39 | 0 | 28320.2 | 5554.34 | 8.32349e+07 | 17385.6 | 1.6126e+07 | 5952.21 | 1.53396e+07 | 2353.33 | 9.83456e+06 | 1949.8 | 9.57242e+06 | 1887.19 | 9.04813e+06 | 889422 | 1.38191e+06 | 9.39441e+06 | 3.58036e+07 | | 52542 | 20221031.6 | 11057.3 | 0 | 40617.7 | 0 | 9983.96 | 0 | 4282.55 | 0 | 3477.62 | 0 | 3205.73 | 0 | 22787.8 | 5640.13 | 8.32349e+07 | 17419.4 | 1.63882e+07 | 5984.67 | 1.56017e+07 | 2359.4 | 9.83456e+06 | 1982.98 | 9.57242e+06 | 1915.42 | 9.31027e+06 | 886345 | 1.36215e+06 | 9.24184e+06 | 3.58036e+07 | mku-gh4264-2 | build_id | build_number | tpcc_virtual_cft^ | tpcc_virtual_cft_mem | ls_virtual_cft^ | ls_virtual_cft_mem | ls_jwt_virtual_cft^ | ls_jwt_virtual_cft_mem | ls_js_virtual_cft^ | ls_js_virtual_cft_mem | ls_full_js_virtual_cft^ | ls_full_js_virtual_cft_mem | ls_js_jwt_virtual_cft^ | ls_js_jwt_virtual_cft_mem | hist_sgx_cft^ | tpcc_sgx_cft^ | tpcc_sgx_cft_mem | ls_sgx_cft^ | ls_sgx_cft_mem | ls_jwt_sgx_cft^ | 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 | RB put (/s)^ | CHAMP put (/s)^ | RB get (/s)^ | CHAMP get (/s)^ | |-----------:|:---------------|--------------------:|-----------------------:|------------------:|---------------------:|----------------------:|-------------------------:|---------------------:|------------------------:|--------------------------:|-----------------------------:|-------------------------:|----------------------------:|----------------:|----------------:|-------------------:|--------------:|-----------------:|------------------:|---------------------:|-----------------:|--------------------:|----------------------:|-------------------------:|---------------------:|------------------------:|---------------:|------------------:|---------------:|------------------:| | 52527 | 20221029.1 | 10809.7 | 0 | 41772.3 | 0 | 10168.5 | 0 | 4329.24 | 0 | 3424.83 | 0 | 3347.23 | 0 | 27704 | 5804.18 | 8.3497e+07 | 17539.8 | 1.58639e+07 | 6027.48 | 1.56017e+07 | 2349.51 | 9.57242e+06 | 1979.66 | 1.19317e+07 | 1922.29 | 9.31027e+06 | 883629 | 1.37081e+06 | 9.27532e+06 | 3.59298e+07 | | 52623 | 20221031.29 | 11290.6 | 0 | 42335.2 | 0 | 10233 | 0 | 4295.2 | 0 | 3494.78 | 0 | 3254.54 | 0 | 23788.7 | 5126.29 | 8.27106e+07 | 15538.2 | 1.63882e+07 | 5362.48 | 1.53396e+07 | 2025.85 | 8.52384e+06 | 1670.43 | 8.78598e+06 | 1591.88 | 7.99955e+06 | 830242 | 1.18069e+06 | 8.16909e+06 | 3.07688e+07 |

[heidihoward]

/azp run

[azure-pipelines[bot]]

Azure Pipelines successfully started running 1 pipeline(s), but failed to run 1 pipeline(s).

[heidihoward]

This PR is ready to be merged (the failure in daily is unrelated)