Skip to content

SYSTEM Cited by 2 sources

RaftMongo.tla

Overview

RaftMongo.tla is the MongoDB-specific TLA+ spec of how servers in a MongoDB replica set learn the commit point — the logical timestamp of the newest majority-replicated write. It models MongoDB's Raft-like consensus protocol, but focused specifically on commit-point propagation rather than leader election.

Source: RaftMongo.tla on GitHub.

What it models

A replica-set deployment (typically three servers) with:

  1. Leader election — one server is leader; others are followers.
  2. Log replication — clients send writes to the leader, which appends to its log with a monotonically-increasing logical timestamp.
  3. Follower catch-up — followers replicate the leader's log asynchronously; tell the leader how up-to-date they are.
  4. Commit point tracking — leader keeps the commit point: the logical timestamp of the newest majority-replicated write.
  5. Failure + recovery — leaders + followers crash; messages are lost; new leaders are elected; uncommitted writes are rolled back.

Invariants it checks

Two stated properties (Source: sources/2025-06-02-mongodb-conformance-checking-at-mongodb-testing-that-our-code-matches-our-tla-specs):

  • Safety — no committed write is ever lost. (A write with timestamp ≤ commit point remains in every majority of future server states.)
  • Liveness — all servers eventually learn the newest commit point.

Role in the 2020 conformance-checking experiment

MongoDB's 2020 attempt to conformance-check the production MongoDB server's C++ implementation against RaftMongo.tla via trace-checking failed after 10 weeks. Three named reasons — all three mapped to choices made in the spec, not the checker:

  1. Multithreaded-state snapshotting expensive. RaftMongo.tla models the protocol at state-variable granularity; the C++ server has fine-grained locking. Capturing all state variables atomically took a month of instrumentation work.

  2. Abstraction mismatch. RaftMongo.tla is focused on commit-point propagation and deliberately simplifies leader handoff to a single atomic action (old leader steps down + new leader steps up in one step). The real server steps the old leader down first, then steps the new leader up. Davis and Schvimer tried to paper over this in the Python trace translator:

We tried to paper over the difference with some post-processing in our Python script, but it never worked. By the end of the project, we decided we should have backtracked, making our spec much more complex and realistic, but we'd run out of time.

  1. Spec-specific setup didn't generalise. 10 weeks of instrumentation for one spec → starting over for the next one.

What a conformance-friendly version would look like

Davis's 2025 retrospective: a spec co-designed with the implementation (see patterns/extreme-modelling) would either model leader handoff at the same granularity the impl does (two distinct actions), or the impl would have been written to do the leader handoff atomically. Either way, the abstraction gap that killed trace-checking wouldn't exist.

Every post-2020 successful conformance-checking system Davis surveys (Mocket, SandTable, Multi-Grained Zookeeper, Confidential Consortium Framework) wrote new specs designed to match their target implementations — rather than retrofitting conformance onto an old abstract spec like RaftMongo.tla.

Seen in

Last updated · 200 distilled / 1,178 read