TechPrufer
Sign inGet started

Blogs›MongoDB›Model-Based Verification of Storage Engine

Model-Based Verification of Storage Engine

Model-Based Verification of Storage Engine

5
posts
2025–2026

Introduced model-based verification to formally check the conformance of the WiredTiger storage engine implementation against an abstract specification of its semantics. This approach leverages a TLA+ specification of the storage engine interface and uses a modified TLC model checker to generate tens of thousands of API call test cases, ensuring the implementation matches the contract relied upon by the distributed transactions protocol. The process achieved high test coverage for a small model. This post details the extensive dogfooding of MongoDB 8.0 Release Candidates on internal production systems, including critical systems like Evergreen's CI infrastructure. This process uncovered and fixed critical bugs, such as a segfault related to malformed TTL index specifications during primary election and an inefficiency in query execution leading to increased index scans. These findings led to improvements in automated testing coverage and demonstrated the reliability of MongoDB 8.0.

2026

Towards Model-based Verification of a Key-Value Storage Engine

2/27/2026

Developed a tool for automatically checking conformance between the WiredTiger implementation and an abstract storage specification. Utilized a modified TLC model checker to generate a complete graph of reachable states for the storage component specification and computed path coverings to create individual test cases. This resulted in the generation and execution of 87,143 test cases for a small, finite model, verifying WiredTiger's semantics against the abstract model.

2025

Carrying Complexity, Delivering Agility

9/25/2025

Details the application of formal methods to replication and failover protocols, including logless reconfiguration and multi-shard transaction protocols, using TLA+ to model core logic and verify invariants like terms blocking stale primaries, monotonic versions preventing forks, majority votes stopping minority splits, and the oplog-commit rule ensuring durability. It also highlights the use of automated model-based techniques for testing the WiredTiger storage interface and assessing concurrency maximization within isolation levels.

Rapid Prototyping a Safe, Logless Reconfiguration Protocol for MongoDB with TLA+

7/2/2025

Details the process of formally modeling the legacy gossip-based reconfiguration protocol in TLA+, characterizing its bugs with a model checker, and iteratively developing modifications to lead to a safe, logless reconfiguration protocol design. Explores single-node changes and their limitations, and demonstrates how TLA+ and TLC were used to discover and fix safety issues, ultimately accelerating design and delivery timelines while maintaining a high correctness bar.

Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs

6/2/2025

Details the application of trace-checking to the MongoDB server's replication protocol. Describes the workflow: running randomized tests, collecting execution traces, translating traces to TLA+, and checking conformance with TLC. Explains the Python script used to reconstruct system state and generate TLA+ traces, and provides an example of state transition logging for a leader election scenario.

MongoDB 8.0: Eating Our Own Dog Food

3/3/2025

This post details the dogfooding of MongoDB 8.0 Release Candidates on internal production systems, specifically the Evergreen CI system's Amboy and main replica sets. It describes the discovery and resolution of a critical bug (SERVER-94487) causing primary election crashes due to malformed TTL index specifications with strengthened validation checks. It also highlights the identification of an inefficiency in query execution leading to a 5x increase in index scans and documents scanned after an upgrade, which was addressed by improving automated testing coverage. The post emphasizes the proactive identification and fixing of issues before customer release.