Design and Modular Verification of Distributed Transactions in MongoDB

Summary: Modular formal specification of MongoDB’s distributed multi-document transactions and its interface to WiredTiger, enabling verification of protocol correctness while isolating layer-specific concurrency/timestamping concerns. Uses explicit-state model checking to auto-generate tests that validate WiredTiger’s conformance to the storage contract and to formally analyze permissiveness (concurrency optimality). (summarized by gpt-5-mini on Feb 09 2026)

Paper ID: 14106
Venue: VLDB
Year: 2025
Pagerank: 4.1945683e-05
Overall Rank: 10,781 | 25.00%
DOI: 10.14778/3750601.3750626

Incoming Non-self Citations Over Time

No non-self incoming citations found for this paper in this database.

Authors

1. William Schultz
2. Murat Demirbas

Incoming Citations (Sorted by Pagerank)

Showing 0 of 0 citing papers.

Rank	Citing Paper	Year	Venue	Pagerank

Outgoing Citations (Sorted by Pagerank)

Showing 12 of 12 cited papers.

Citations counted here include only citations to other VLDB/SIGMOD/CIDR/PODS papers in this database.

Rank	Cited Paper	Year	Venue	Pagerank
23	A Critique of ANSI SQL Isolation Levels	1995	SIGMOD	0.00083894938
122	Calvin: Fast Distributed Transactions for Partitioned Database Systems	2012	SIGMOD	0.00045316749
189	Megastore: Providing Scalable, Highly Available Storage for Interactive Services	2011	CIDR	0.00035925334
349	Serializable Isolation for Snapshot Databases	2008	SIGMOD	0.00026440605
390	CockroachDB: The Resilient Geo-Distributed SQL Database	2020	SIGMOD	0.00024607299
488	TiDB: A Raft-based HTAP Database	2020	VLDB	0.000220409
1,227	Elle: Inferring Isolation Anomalies from Experimental Observations	2021	VLDB	0.00013170695
1,984	Amazon Aurora: On Avoiding Distributed Consensus for I/Os, Commits, and Membership Changes	2018	SIGMOD	9.8607096e-05
2,601	What Are We Doing With Our Lives? Nobody Cares About Our Concurrency Control Research	2017	SIGMOD	8.468229e-05
3,672	Implementation of Cluster-wide Logical Clock and Causal Consistency in MongoDB	2019	SIGMOD	6.8558714e-05
4,347	Tunable Consistency in MongoDB	2019	VLDB	6.269146e-05
7,423	eXtreme Modelling in Practice	2020	VLDB	4.7339251e-05

Semantically Similar Papers

Overall Rank	Paper	Year	Venue	Pagerank
13,033	Specification and Verification of Abstract Database Types	1984	PODS	4.1945683e-05
14,332	Transactions Modeling	1982	SIGMOD	-
4,912	Cooperative Transaction Hierarchies: A Transaction Model to Support Design Applications	1990	VLDB	5.8321169e-05
12,885	Ensuring Transaction Atomicity in Multidatabase Systems	1992	PODS	4.1945683e-05
6,028	Ensuring Relaxed Atomicity for Flexible Transactions in Multidatabase Systems	1994	SIGMOD	5.2415551e-05
13,920	Correctness in General Configurations of Transactional Components	1999	PODS	-
3,672	Implementation of Cluster-wide Logical Clock and Causal Consistency in MongoDB	2019	SIGMOD	6.8558714e-05
4,347	Tunable Consistency in MongoDB	2019	VLDB	6.269146e-05
6,636	Adapting TPC-C Benchmark to Measure Performance of Multi-Document Transactions in MongoDB	2019	VLDB	4.9820843e-05
7,423	eXtreme Modelling in Practice	2020	VLDB	4.7339251e-05