Improve TLA+ specification

[heidihoward]

CCF currently has a TLA+ specification that can be model checked using TLC. It would be great to do more with this specification in the future. Here is a list of ideas (small, medium & large) that might be worth considering:

Small

• Add action invariants to check properties such as monotonicity of currentTerm or commitIndex
• Add Github actions check the TLA+ specification - This is now supported
• Add wrappers that model check the specification with different configuration e.g. numbers of servers, e.g. 1, 3 and 5 servers
• Update specification with future changes to CCF's consensus protocol such as PreVote - Raft extensions for omission faults #2577
• Update docs to describe how to use the TLA+ VSCode plugin to check the specification
• Add a GitHub action to check the formatting/syntax of the .tla and .cfg files
• Reformat the next state relation in the TLA+ specification for complete coverage checking by TLC - currently some actions are missed by the coverage checking
• Check the specification for a range of configurations and store the output for future analysis. This will require some cloud storage as the files will be too large to be added to this repository.
• Add some tables/graphs to illustrate how long it will take to check various configurations
• Change the appendEntries action so that a leader can send multiple entries at once and so that a leader can send a heartbeat with no new log entries
• Update NACK handling to reflect the CCF logic for determine which log entries the leader should sent next
• All message are currently held in a one large set, this makes it difficult to read traces. Messages could be abstracted and divided into sets for each sender and receiver pair. This would make it easier to read and could help with future changes, for instance, ordered message delivery
• More user-friendly trace exploration, e.g. https://github.com/japgolly/tla2json
• Update variable names in spec to match implementation in raft.h. Also, adopt a naming convention to distinguish model checking state from real system state.

Medium

• Support symbolic execution of the specification (bounded model checking) with the Apalache model checker. Currently the only supported model checker is TLC.
• Add inductive invariants (and check these inductive invariants with Apalache)
  • Inductive invariant for Raft using Apalache dranov/raft-tla#1
• Add temporal properties and changing the spec to support liveness. These spec currently only check for safety.
  • https://github.com/Vanlightly/raft-tlaplus/blob/main/specifications/standard-raft/Raft.tla
• Create a more high-level specification that abstracts from some aspects of ccfraft.tla and vanilla raft.tla
  • https://github.com/muenchnerkindl/AbstractRaft/blob/main/AbstractRaft/tla/AbstractRaft.tla
  • https://github.com/will62794/endive/blob/ind-tree/benchmarks/AbstractStaticRaft.tla
  • https://github.com/will62794/raft-by-refinement/blob/master/RaftAbstractStatic.tla
• Extend specification to cover more aspects of CCF. This could include:
  • Disaster recovery (DR)
  • Snapshotting
  • Forwarding logic & session consistency Maintaining session consistency in the presence of forwarding #4401
• Expand specification to explicitly include clients:
  • Add logic for sending early responses with transaction ID
  • Support checking the status of transactions by ID
  • Add forwarding logic
  • Add read-only transactions
• Develop a trace checker which can take a trace of CCF "in the wild" and check that it is a valid behaviour according to the TLA+ specification. This could help keep the source code and specification in sync.
  • Consensus trace validation #5057

Large

• Formal proof of inductive invariants using TLAPS

Some things we considered but decided against (at least for now):

• Add support for running the specification using PlusPy
  • This has been replaced by support for simulation
• Reduce the number of states by removing any extra state (or ignore this state using symmetry/projection/views) , such as:
  • candidateVars and leaderVars for non candidates/leaders, and
  • artificial state that is used only for model checking, like ReconfigurationCount, messagesSent, commitsNotified, votesRequested, clientRequests, committedLog & committedLogConflict
  • messages which will be ignored by the receiver because their term is too small
• Add instruction for checking the specification using cloud-based distributed TLC

(Note that some of these items where originally listed in #3965)