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: 14107
Venue: VLDB
Year: 2025
Pagerank: 5.1725247e-05
Overall Rank: 10,787 | 25.03%
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
18	A Critique of ANSI SQL Isolation Levels	1995	SIGMOD	0.00059344857
57	Calvin: Fast Distributed Transactions for Partitioned Database Systems	2012	SIGMOD	0.00040347584
142	Megastore: Providing Scalable, Highly Available Storage for Interactive Services	2011	CIDR	0.00029935122
219	CockroachDB: The Resilient Geo-Distributed SQL Database	2020	SIGMOD	0.00024561689
244	Serializable Isolation for Snapshot Databases	2008	SIGMOD	0.00023702075
301	TiDB: A Raft-based HTAP Database	2020	VLDB	0.00022033345
1,111	Elle: Inferring Isolation Anomalies from Experimental Observations	2021	VLDB	0.00012210503
1,498	Amazon Aurora: On Avoiding Distributed Consensus for I/Os, Commits, and Membership Changes	2018	SIGMOD	0.00010657884
2,330	What Are We Doing With Our Lives? Nobody Cares About Our Concurrency Control Research	2017	SIGMOD	8.8209052e-05
3,384	Implementation of Cluster-wide Logical Clock and Causal Consistency in MongoDB	2019	SIGMOD	7.5295883e-05
4,456	Tunable Consistency in MongoDB	2019	VLDB	6.7490937e-05
7,352	eXtreme Modelling in Practice	2020	VLDB	5.6947508e-05

Semantically Similar Papers

Overall Rank	Paper	Year	Venue	Pagerank
13,044	Specification and Verification of Abstract Database Types	1984	PODS	5.1725247e-05
14,346	Transactions Modeling	1982	SIGMOD	-
5,128	Cooperative Transaction Hierarchies: A Transaction Model to Support Design Applications	1990	VLDB	6.4173474e-05
12,895	Ensuring Transaction Atomicity in Multidatabase Systems	1992	PODS	5.1725247e-05
6,863	Ensuring Relaxed Atomicity for Flexible Transactions in Multidatabase Systems	1994	SIGMOD	5.8190903e-05
13,934	Correctness in General Configurations of Transactional Components	1999	PODS	-
3,384	Implementation of Cluster-wide Logical Clock and Causal Consistency in MongoDB	2019	SIGMOD	7.5295883e-05
4,456	Tunable Consistency in MongoDB	2019	VLDB	6.7490937e-05
7,165	Adapting TPC-C Benchmark to Measure Performance of Multi-Document Transactions in MongoDB	2019	VLDB	5.7419998e-05
7,352	eXtreme Modelling in Practice	2020	VLDB	5.6947508e-05