CCF icon indicating copy to clipboard operation
CCF copied to clipboard

Published 20 hours ago • verified publisher icon microsoft

Fixing TLA+ specifications

Open heidihoward opened this issue 3 years ago • 1 comments

Currently, the function of this PR is to improve visibility of the ongoing work on the TLA+ specifications. It is not yet ready to be reviewed/merged.

This PR will fix the current TLA+ specifications and will bring them closer to the current codebase of CCF's consensus protocol.

This will likely include the following:

Deduplicating the two specifications

  • [x] Merge the two specifications into one. Currently, there is one with reconfiguration and one without, however they have diverged in other ways and are difficult to maintain/test. We can instead use different TLC configurations to check the same specification both with and without reconfiguration. Merging the specifications will involve starting with the reconfiguration specification and copying changes over from the other specification before deletion.

Checking the existing TLC+ specification in TLC

  • [x] Document and patch any bugs
    • [x] The specs were using LastLogTermin leader election logic & MoreUpToDateCorrectInv invariant instead of LastCommittableTerm.
    • [x] CommittedLogDecrease logic did not allow the same log entry to be committed twice by different leaders. This is in fact safe as long as the log entries are the same.
    • [x] A leader should not update its commitIndex until it has replicated a signature in its current term - see https://github.com/microsoft/CCF/issues/3950. This is not an issue in the TLA+ atm as there are currently no heartbeat AppendEntries but it should be patched anyway
    • [x] TLA+ specs and CCF codebase was using quorums across configurations instead of in each configuration for leader election - see https://github.com/microsoft/CCF/issues/3837 and https://github.com/microsoft/CCF/issues/3948
  • [ ] Updating the docs to reflect the latest version of TLC used to check the specs
  • [ ] Adding new logged_runs

Reduce the state space and make it quicker to model check

  • [x] Investigate enabling symmetry by default
  • [ ] Reduce the number of states by removing any extra state, such as candidateVars and leaderVars for non candidates/leaders
  • [ ] Replace arbitrary reconfigurations with a list of reconfigurations to check - also useful to stop a node being removed and added back again

Add more invariants to verify correctness of the specification

  • [x] Add TypeOK invariant to check type safety
  • [x] Add debugging invariants which are designed to produce counter-examples to check that useful states are being reached

Make the TLA+ specification more similar to the current codebase

  • [ ] Update NACK handling to reflect the CCF logic for determine which log entries the leader should sent next
  • [ ] Change appendEntries action so that a leader can send multiple entries at once
  • [ ] Change appendEntries action so that a leader can send a heartbeat with no new log entries
  • [x] Implement CheckQuourm - add an action allowing a leader to choose to step down in the current term - see https://github.com/microsoft/CCF/pull/3865

General tidying up

  • [x] Minor reformatting, fixing typos, adding more documentation
  • [ ] Consolidate docs into a single page here
  • [ ] Update docs to reflect the fact that there is now only one core specification with multiple configurations
  • [x] Remove dummy values from signature transactions
  • [ ] Adding a some tables/graphs to illustrate how long it will take to check various configurations

This PR will make way for future PRs on the TLA+ specs. This changes are currently out-of-scope for this PR but may include:

  • Check the specs with the Apalache model checker as well as TLC
  • Addition of inductive invariants (and check induction with Apalache)
  • Prove inductive invariants using TLAPS
  • Addition of temporal properties and changing the specs to support liveness - These specs currently only check for safety.
  • Addition of action invariants to check properties such as monotonicity of currentTerm or commitIndex
  • Extend specifications to cover more aspects of CCF. Could include:
    • 2-phase reconfiguration
    • Disaster recovery (DR)
    • Snapshotting
    • BFT
  • Add support/instructions for running the specs using PlusPy
  • Wrappers which run the specification with different numbers of servers, e.g. 1, 3 and 5 servers
  • Bonus scripts to automate model checking many configurations
  • Expand specification to explicitly include clients.
    • Add logic for sending early responses with transaction ID
    • Support checking the status of transactions by ID
  • Update spec with future changes to CCF's consensus protocol such as PreVote - see https://github.com/microsoft/CCF/issues/2577
  • Update docs to describe how to use the TLA+ VSCode plugin to check these specs
  • Reformat next state relation for complete coverage checking - currently some actions are missed by the coverage checking

heidihoward avatar Jun 21 '22 14:06 heidihoward

tla-combine-specs@51123 aka 20221011.8 vs main ewma over 20 builds from 50750 to 51108

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 tpcc_sgx_cft^ tpcc_sgx_cft_mem ls_js_virtual_cft^ ls_js_virtual_cft_mem ls_sgx_cft^ ls_sgx_cft_mem ls_full_js_virtual_cft^ ls_full_js_virtual_cft_mem ls_jwt_sgx_cft^ ls_jwt_sgx_cft_mem ls_js_sgx_cft^ ls_js_sgx_cft_mem ls_js_jwt_virtual_cft^ ls_js_jwt_virtual_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)^
50750 20221005.2 10995.9 0 42222.6 0 10390.3 0 6425.91 8.40213e+07 4411.31 0 19878 1.6126e+07 3702.47 0 5602.38 1.56017e+07 2495.03 1.2456e+07 3361.3 0 24517.4 2156.45 9.31027e+06 1934.01 9.31027e+06 896628 1.37902e+06 9.29215e+06 3.58669e+07
50769 20221005.9 11479.8 0 42187.6 0 10099.3 0 6336.03 8.37592e+07 4775.02 0 19590.3 1.6126e+07 3871.36 0 5561.84 1.53396e+07 2556.91 9.83456e+06 3396.49 0 24441 2087.49 9.57242e+06 1932.5 9.31027e+06 906390 1.372e+06 9.27952e+06 3.59298e+07
50778 20221005.12 10740.1 0 40915.2 0 9954.33 0 6251.58 8.24484e+07 4611.91 0 19490.6 1.63882e+07 3703.39 0 5554.05 1.53396e+07 2473.42 1.00967e+07 3377.88 0 24277.1 2076.35 9.31027e+06 1917.35 9.31027e+06 904554 1.38444e+06 9.16331e+06 3.57417e+07
50792 20221005.18 11798.2 0 41437.3 0 10270 0 6282.01 8.37592e+07 4675.05 0 19199.8 1.6126e+07 3560.85 0 5599.88 1.56017e+07 2552.23 1.00967e+07 3487.7 0 26504.4 2122.44 9.57242e+06 1928.84 9.31027e+06 901454 1.35549e+06 9.20437e+06 3.58675e+07
50825 20221005.30 11066.8 0 43698.5 0 10655.7 0 6228.44 8.74292e+07 4658.34 0 19719.2 1.63882e+07 3695.34 0 5611.1 1.58639e+07 2604.78 9.83456e+06 3374.99 0 25744.1 2119.9 9.31027e+06 1938.39 9.04813e+06 872522 1.38023e+06 9.24601e+06 3.58663e+07
50850 20221006.2 11348 0 40797.1 0 10676 0 6229.21 8.27106e+07 4688.94 0 19754.9 1.66503e+07 3696.51 0 5579.31 1.53396e+07 2564.65 9.83456e+06 3384.5 0 25559.2 2109.84 9.31027e+06 1931.02 9.04813e+06 881004 1.37856e+06 9.23763e+06 3.58663e+07
50874 20221006.11 11531.7 0 44439.2 0 10249.9 0 6294.18 8.66428e+07 4619.46 0 19492.6 1.69124e+07 3646.48 0 5217.43 1.53396e+07 2536.76 1.00967e+07 3384.72 0 27370.2 2114.04 1.32424e+07 2006.22 9.04813e+06 894982 1.37182e+06 9.25436e+06 3.58036e+07
50933 20221006.28 10998.8 0 40651.3 0 10803.1 0 5890.25 8.32349e+07 4648.81 0 19537.4 1.6126e+07 3646.89 0 5546.49 1.56017e+07 2420.2 9.57242e+06 3371.18 0 25695.2 2099.96 9.57242e+06 1870.37 9.04813e+06 910257 1.37145e+06 9.32176e+06 3.56794e+07
50956 20221006.36 11200.8 0 43280.1 0 10641.9 0 5869.76 8.27106e+07 4322.64 0 19647 1.66503e+07 3504.67 0 5636.79 1.6126e+07 2480.09 9.57242e+06 3255.79 0 21597.6 2027.12 9.04813e+06 1877.18 9.04813e+06 889551 1.36072e+06 9.21273e+06 3.54325e+07
50972 20221006.42 10821.2 0 41526.4 0 10027.1 0 5917.45 8.32349e+07 4574.86 0 19779.4 1.58639e+07 3536.17 0 5562.98 1.53396e+07 2521.1 9.57242e+06 3237.04 0 24266.6 2068.4 9.31027e+06 1909.31 9.04813e+06 911390 1.37044e+06 9.10218e+06 3.56174e+07
50980 20221007.2 10868.3 0 41467.3 0 10087.3 0 6218.71 8.3497e+07 4356.33 0 19358.1 1.6126e+07 3414 0 5621.58 1.56017e+07 2426.73 9.57242e+06 3236.18 0 25864.8 2031.2 9.57242e+06 1874.24 9.04813e+06 901443 1.34745e+06 9.24184e+06 3.58669e+07
51011 20221007.12 11187.7 0 40597.2 0 10412.8 0 6235.86 8.37592e+07 4314.43 0 19821 1.69124e+07 3399.11 0 5548.36 1.56017e+07 2523.87 9.57242e+06 3294.19 0 25389.5 2059.07 9.31027e+06 1906.84 9.04813e+06 875619 1.37458e+06 9.04985e+06 3.58669e+07
51025 20221007.17 11467.1 0 41236.5 0 10121.7 0 6310.28 8.32349e+07 4527.82 0 19793.5 1.71746e+07 3615.67 0 5621.17 1.53396e+07 2419.48 9.83456e+06 3274.8 0 24578.3 2063.54 9.57242e+06 1918.97 9.04813e+06 895804 1.35574e+06 9.19615e+06 3.56174e+07
51036 20221007.21 11072.4 0 42141.6 0 10163.2 0 6290.72 8.24484e+07 4412.54 0 19773.6 1.6126e+07 3630.63 0 5628.41 1.58639e+07 2415 9.57242e+06 3431.49 0 25969.5 2058.22 9.31027e+06 1874.55 9.04813e+06 905347 1.36952e+06 9.19206e+06 3.56788e+07
51053 20221010.2 11798 0 42227.8 0 10245.4 0 6305.13 8.29727e+07 4300.08 0 19794.7 1.69124e+07 3599.97 0 5606.72 1.53396e+07 2531.31 9.57242e+06 3431.49 0 30481.2 2067.16 9.31027e+06 1956.25 9.31027e+06 906832 1.35853e+06 9.20445e+06 3.55556e+07
51060 20221010.5 11225.8 0 40998.7 0 10243.7 0 5735.1 8.3497e+07 4262.26 0 19764 1.6126e+07 3544.72 0 5607.19 1.6126e+07 2441.86 1.14074e+07 3369.34 0 26450.9 2106.7 9.04813e+06 1955.23 9.04813e+06 925351 1.35297e+06 9.16327e+06 3.56174e+07
51070 20221010.9 10742 0 42747.9 0 10320.7 0 6480.7 8.29727e+07 4674.44 0 19954.2 1.66503e+07 3571.41 0 5627.41 1.53396e+07 2553.85 9.57242e+06 3396.5 0 28907 2111.12 9.31027e+06 1947.45 9.04813e+06 912656 1.38126e+06 9.15921e+06 3.58669e+07
51073 20221010.10 11037.5 0 42007.3 0 10311.2 0 6238.01 8.37592e+07 4644.78 0 19572.5 1.6126e+07 3545.97 0 5580.73 1.56017e+07 2371.74 9.83456e+06 3330.9 0 28710.5 2032.18 9.31027e+06 1870.01 9.04813e+06 886611 1.35065e+06 9.07391e+06 3.53097e+07
51085 20221010.15 11316.8 0 42993.9 0 10336.3 0 6167.23 8.29727e+07 4529.17 0 19214.9 1.71746e+07 3535.49 0 5530.5 1.53396e+07 2368.9 9.83456e+06 3433.88 0 29176.9 2037.46 9.04813e+06 1876.41 9.04813e+06 892875 1.3806e+06 9.45954e+06 3.63766e+07
51108 20221011.2 11535.3 0 39052.9 0 10195.2 0 6323.44 8.32349e+07 4591.11 0 19655.7 1.6126e+07 3519.27 0 5603.65 1.56017e+07 2423.14 9.57242e+06 3402.86 0 30358.8 2041.8 9.31027e+06 1873.74 9.57242e+06 887882 1.37735e+06 9.15913e+06 3.58669e+07

tla-combine-specs

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)^
50880 20221006.13 11576.3 0 44257.5 0 10413.1 0 4785.18 0 3763.03 0 3416.62 0 23353.9 6520.05 8.32349e+07 19947.4 1.6126e+07 5484.98 1.58639e+07 2554.41 1.00967e+07 2120.63 9.57242e+06 1931.44 8.78598e+06 892569 1.37201e+06 9.3945e+06 3.64413e+07
50971 20221006.41 10817.9 0 41197 0 10006.9 0 4321 0 3554.77 0 3202.91 0 24130.1 6273.67 8.3497e+07 19548.9 1.6126e+07 5571.66 1.56017e+07 2431.39 9.57242e+06 2065.77 9.04813e+06 1883.47 9.04813e+06 895881 1.37163e+06 9.30478e+06 3.56794e+07
51021 20221007.15 11457.6 0 41708.8 0 10354.2 0 4247.28 0 3454.23 0 3326.87 0 27731 6284.79 8.32349e+07 19556.8 1.63882e+07 5541.88 1.53396e+07 2518.56 9.57242e+06 2025.67 1.2456e+07 1863.81 9.31027e+06 908319 1.36687e+06 9.20859e+06 3.58663e+07
51035 20221007.20 10945.7 0 40801.8 0 10195.8 0 4594.01 0 3523.87 0 3412.51 0 25087.1 7200.19 8.3497e+07 19584.9 1.63882e+07 5522.98 1.56017e+07 2423.27 9.57242e+06 1996.28 9.57242e+06 1873.77 9.04813e+06 909367 1.36962e+06 9.3858e+06 3.56794e+07
51123 20221011.8 11030.2 0 43671 0 10535.5 0 4559.45 0 3456.75 0 3347.09 0 28204.4 7311.06 8.32349e+07 19495.1 1.6126e+07 5638.11 1.56017e+07 2421.05 9.57242e+06 2101.45 9.57242e+06 1876.4 9.04813e+06 909689 1.3768e+06 9.21684e+06 3.58663e+07

images

ccf-bot avatar Jun 21 '22 14:06 ccf-bot

https://github.com/microsoft/CCF/discussions/4264 documents future changes we might want to make to the TLA+ specs but are beyond scope for this PR

heidihoward avatar Oct 10 '22 08:10 heidihoward