This repository contains a TLA+ formal specification of MongoRaftReconfig, a novel logless dynamic reconfiguration protocol designed for and implemented in the MongoDB distributed replication system. It also includes a formally stated inductive invariant for establishing its high level safety properties along with a machine checked TLAPS safety proof.
The overall reconfiguration protocol is defined in the MongoRaftReconfig TLA+ specification. The protocol is formally described as the composition of two subprotocols:
- MongoStaticRaft: the static MongoDB replication protocol
- MongoLoglessDynamicRaft: the protocol for managing reconfiguration
Note that the specifications are written at a deliberately high level of abstraction, ignoring some lower level details of the protocol and system model. In practice, we have found this abstraction level most useful for understanding and communicating the essential behaviors and safety characteristics of the protocol, while also serving to make automated verification via model checking more feasible.
Safety properties of finite instances of MongoRaftReconfig can be verified using the TLC model checker. To check a model, you can execute the following:
./modelcheck.sh <config_file> <spec_name> <tlc_worker_count>
This will save the results of the execution, along with auxiliary information about the run, into a timestamped file in tlc-results. For example, to verify safety properties of MongoRaftReconfig and MongoLoglessDynamicRaft with 4 TLC workers, you can run the following commands:
# Check MongoRaftReconfig.
./modelcheck.sh models/MCMongoRaftReconfig-4Servers-L2-T3-CV3.cfg MCMongoRaftReconfig 4
# Check MongoLoglessDynamicRaft.
./modelcheck.sh models/MCMongoLoglessDynamicRaft-5Servers-T4-CV4.cfg MCMongoLoglessDynamicRaft 4These models impose state constraints on both protocols to make the reachable state space finite. Complete verification time, however, will vary depending on the speed of your local machine.
TLAPS proofs of the safety properties of MongoRaftReconfig are provided in the proofs sub-directory. This includes a formal inductive invariant for establishing safety. Information on how to inspect and check these proofs using the TLA+ proof system is provided in the README present in the proofs sub-directory.