{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:21:17Z","timestamp":1784830877313,"version":"3.55.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"12","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. VLDB Endow."],"published-print":{"date-parts":[[2025,8]]},"abstract":"<jats:p>\n            MongoDB's distributed multi-document transactions protocol was designed and developed incrementally, building on WiredTiger, an existing single node multi-version storage engine that provided snapshot isolated key-value storage. This layered approach required meticulous management of concurrency control and timestamping mechanisms across system layers, complicated by intricate component interactions and a large evolving codebase. In this paper, we describe our experience using\n            <jats:italic toggle=\"yes\">modular<\/jats:italic>\n            formal specification techniques to address this challenge. Our approach formally specifies the distributed transactions protocol and its interface with the underlying storage layer, allowing us to verify high level protocol properties while also formalizing the contract between these two components. This modular approach also enables an automated, model-based verification technique for testing conformance of the WiredTiger storage implementation to this interface. We use an explicit state model checker to automatically generate test cases from our storage model, which are then executed against the storage implementation, ensuring the implementation matches the interface relied upon by the transactions protocol. Our work highlights the value of formal modeling not only for verifying high-level protocol correctness but also for precisely defining and validating interactions with lower-level system components in an automated way. Beyond verifying key isolation properties, our specification also enabled us to formally analyze\n            <jats:italic toggle=\"yes\">permissiveness-<\/jats:italic>\n            -how well the protocol maximizes concurrency within a given isolation level-a property not previously examined.\n          <\/jats:p>","DOI":"10.14778\/3750601.3750626","type":"journal-article","created":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T13:38:05Z","timestamp":1758029885000},"page":"5045-5058","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Design and Modular Verification of Distributed Transactions in MongoDB"],"prefix":"10.14778","volume":"18","author":[{"given":"William","family":"Schultz","sequence":"first","affiliation":[{"name":"MongoDB Research, New York, New York"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Murat","family":"Demirbas","sequence":"additional","affiliation":[{"name":"MongoDB Research, New York, New York"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,9,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/888672"},{"key":"e_1_2_1_4_1","volume-title":"Porcupine: A fast linearizability checker in Go. https:\/\/github.com\/anishathalye\/porcupine.","author":"Athalye Anish","year":"2017","unstructured":"Anish Athalye. 2017. Porcupine: A fast linearizability checker in Go. https:\/\/github.com\/anishathalye\/porcupine."},{"key":"e_1_2_1_5_1","volume-title":"Highly Available Storage for Interactive Services. In Conference on Innovative Data Systems Research (CIDR)","author":"Baker Jason","year":"2011","unstructured":"Jason Baker, Chris Bond, James C. Corbett, JJ Furman, Andrey Khorlin, James Larson, Jean-Michel Leon, Yawei Li, Alexander Lloyd, and Vadim Yushprakh. 2011. Megastore: Providing Scalable, Highly Available Storage for Interactive Services. In Conference on Innovative Data Systems Research (CIDR) (Asilomar, California). 223\u2013234."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/223784.223785"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/568271.223785"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the ACM on Programming Languages 5, OOPSLA","author":"Biswas Ranadeep","year":"2021","unstructured":"Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, and Akash Lal. 2021. MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels. Proceedings of the ACM on Programming Languages 5, OOPSLA (2021), 1\u201327."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1620585.1620587"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.58"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"E. M. Clarke E. A. Emerson S. Jha and A. P. Sistla. 1998. Symmetry reductions in model checking. In Computer Aided Verification Alan J. Hu and Moshe Y. Vardi (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 147\u2013158.","DOI":"10.1007\/BFb0028741"},{"key":"e_1_2_1_12_1","unstructured":"Confluent. 2018. Hardening Kafka Replication. Online. https:\/\/www.confluent.io\/kafka-summit-sf18\/hardening-kafka-replication\/ Accessed: 2025-01-14."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation","author":"Corbett James C.","year":"2012","unstructured":"James C. Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, J. J. Furman, Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, Wilson Hsieh, Sebastian Kanthak, Eugene Kogan, Hongyi Li, Alexander Lloyd, Sergey Melnik, David Mwaura, David Nagle, Sean Quinlan, Rajesh Rao, Lindsay Rolig, Yasushi Saito, Michal Szymaniak, Christopher Taylor, Ruth Wang, and Dale Woodford. 2012. Spanner: Google's globally-distributed database. In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation (Hollywood, CA, USA) (OSDI'12). USENIX Association, USA, 251\u2013264."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087801.3087802"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556924"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.14778\/3397230.3397233"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462184"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276529"},{"key":"e_1_2_1_19_1","volume-title":"Kayfabe: Model-based Program Testing with TLC. In TLA+ Conference. https:\/\/conf.tlapl.us\/2020\/11-Star_Dorminey-Kayfabe_Model_based_program_testing_with_TLC.pdf","author":"Dorminey Star","year":"2020","unstructured":"Star Dorminey. 2020. Kayfabe: Model-based Program Testing with TLC. In TLA+ Conference. https:\/\/conf.tlapl.us\/2020\/11-Star_Dorminey-Kayfabe_Model_based_program_testing_with_TLC.pdf"},{"key":"e_1_2_1_20_1","volume-title":"Chardonnay: Fast and General Datacenter Transactions for On-Disk Databases. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)","author":"Eldeeb Tamer","year":"2023","unstructured":"Tamer Eldeeb, Xincheng Xie, Philip A. Bernstein, Asaf Cidon, and Junfeng Yang. 2023. Chardonnay: Fast and General Datacenter Transactions for On-Disk Databases. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23). USENIX Association, Boston, MA, 343\u2013360. https:\/\/www.usenix.org\/conference\/osdi23\/presentation\/eldeeb"},{"key":"e_1_2_1_21_1","volume-title":"Fauna: Distributed Serverless Database. https:\/\/fauna.com\/ Accessed: 2025-03-11.","year":"2025","unstructured":"Fauna. 2025. Fauna: Distributed Serverless Database. https:\/\/fauna.com\/ Accessed: 2025-03-11."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1031570.1031573"},{"key":"e_1_2_1_23_1","volume-title":"Permissiveness in Transactional Memories","author":"Guerraoui Rachid","unstructured":"Rachid Guerraoui, Thomas A. Henzinger, and Vasu Singh. 2008. Permissiveness in Transactional Memories. In Distributed Computing, Gadi Taubenfeld (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 305\u2013319."},{"key":"e_1_2_1_24_1","unstructured":"Aric Hagberg Pieter Swart and Daniel S Chult. 2008. Exploring network structure dynamics and function using NetworkX. Technical Report. Los Alamos National Lab.(LANL) Los Alamos NM (United States)."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/602902.602931"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.14778\/3415478.3415535"},{"issue":"0","key":"e_1_2_1_27_1","first-page":"34","article-title":"Jepsen","volume":"8","year":"2024","unstructured":"Jepsen. 2024. Jepsen: MySQL 8.0.34. https:\/\/jepsen.io\/analyses\/mysql-8.0.34 Accessed: 2024-11-15.","journal-title":"MySQL"},{"issue":"5","key":"e_1_2_1_28_1","first-page":"4","article-title":"Jepsen","volume":"2","author":"Kingsbury Kyle","year":"2019","unstructured":"Kyle Kingsbury. 2019. Jepsen: FaunaDB 2.5.4. https:\/\/jepsen.io\/analyses\/faunadb-2.5.4 Accessed: 2024-02-04.","journal-title":"FaunaDB"},{"key":"e_1_2_1_29_1","unstructured":"Kyle Kingsbury. 2024. Jepsen 15: What Even Are Transactions? https:\/\/www.youtube.com\/watch?v=ecZp6cWhDjg Accessed: 2025-02-04."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.14778\/3430915.3430918"},{"key":"e_1_2_1_31_1","volume-title":"Hermitage: Testing the I in ACID. https:\/\/martin.kleppmann.com\/2014\/11\/25\/hermitage-testing-the-i-in-acid.html Accessed: 2025-02-04.","author":"Kleppmann Martin","year":"2014","unstructured":"Martin Kleppmann. 2014. Hermitage: Testing the I in ACID. https:\/\/martin.kleppmann.com\/2014\/11\/25\/hermitage-testing-the-i-in-acid.html Accessed: 2025-02-04."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465351.2465363"},{"key":"e_1_2_1_33_1","volume-title":"Principles of Distributed Systems, Marcos K","author":"Kulkarni Sandeep S.","unstructured":"Sandeep S. Kulkarni, Murat Demirbas, Deepak Madappa, Bharadwaj Avva, and Marcelo Leone. 2014. Logical Physical Clocks. In Principles of Distributed Systems, Marcos K. Aguilera, Leonardo Querzoni, and Marc Shapiro (Eds.). Springer International Publishing, Cham, 17\u201332."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133373.1133382"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685086"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1979.234213"},{"key":"e_1_2_1_39_1","volume-title":"Verifying transactional consistency of mongodb. arXiv preprint arXiv:2111.14946","author":"Ouyang Hongrong","year":"2021","unstructured":"Hongrong Ouyang, Hengfeng Wei, Yu Huang, Haixiang Li, and Anqun Pan. 2021. Verifying transactional consistency of mongodb. arXiv preprint arXiv:2111.14946 (2021)."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360600"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3056096"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1924943.1924961"},{"key":"e_1_2_1_43_1","volume-title":"Spectacle: Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+. https:\/\/github.com\/will62794\/spectacle.","author":"Schultz William","year":"2024","unstructured":"William Schultz. 2024. Spectacle: Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+. https:\/\/github.com\/will62794\/spectacle."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.14778\/3352063.3352125"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503688"},{"key":"e_1_2_1_46_1","unstructured":"William Schultz and Murat Demirbas. 2025. MongoDB distributed transactions protocol specifications. https:\/\/github.com\/mongodb-labs\/vldb25-dist-txns."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67220-1_4"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043592"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318464.3386134"},{"key":"e_1_2_1_50_1","volume-title":"Cobra: Making Transactional Key-Value Stores Verifiably Serializable. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Tan Cheng","year":"2020","unstructured":"Cheng Tan, Changgeng Zhao, Shuai Mu, and Michael Walfish. 2020. Cobra: Making Transactional Key-Value Stores Verifiably Serializable. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 63\u201380. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/tan"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3627703.3650077"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213836.2213838"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3299869.3314049"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.456"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196937"},{"key":"e_1_2_1_56_1","unstructured":"WiredTiger. 2024. WiredTiger. https:\/\/github.com\/wiredtiger\/wiredtiger"},{"key":"e_1_2_1_57_1","volume-title":"MODIST: Transparent Model Checking of Unmodified Distributed Systems. In 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI 09)","author":"Yang Junfeng","year":"2009","unstructured":"Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou. 2009. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI 09). USENIX Association, Boston, MA. https:\/\/www.usenix.org\/conference\/nsdi-09\/modist-transparent-model-checking-unmodified-distributed-systems"},{"key":"e_1_2_1_58_1","unstructured":"Yuan Yu. 2002. Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor. In Proceedings of the 3rd IEEE International Workshop on Microprocessor Test and Verification (MTV '02) (proceedings of the 3rd ieee international workshop on microprocessor test and verification (mtv '02) ed.). Institute of Electrical and Electronics Engineers Inc. https:\/\/www.microsoft.com\/en-us\/research\/publication\/using-formal-specifications-to-monitor-and-guide-simulation-verifying-the-cache-coherence-engine-of-the-alpha-21364-microprocessor\/"},{"key":"e_1_2_1_59_1","volume-title":"Model Checking TLA+ Specifications","author":"Yu Yuan","unstructured":"Yuan Yu, Panagiotis Manolios, and Leslie Lamport. 1999. Model Checking TLA+ Specifications. In Correct Hardware Design and Verification Methods, Laurence Pierre and Thomas Kropf (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 54\u201366."},{"key":"e_1_2_1_60_1","unstructured":"Yugabyte. 2025. YugabyteDB - Distributed SQL Database. https:\/\/github.com\/yugabyte\/yugabyte-db Accessed: 2025-03-13."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815404"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3552326.3567492"},{"key":"e_1_2_1_63_1","volume-title":"Fault-Tolerant Replication with Pull-Based Consensus in MongoDB. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Zhou Siyuan","year":"2021","unstructured":"Siyuan Zhou and Shuai Mu. 2021. Fault-Tolerant Replication with Pull-Based Consensus in MongoDB. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 687\u2013703. https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/zhou"}],"container-title":["Proceedings of the VLDB Endowment"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.14778\/3750601.3750626","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T13:42:06Z","timestamp":1758030126000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.14778\/3750601.3750626"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8]]},"references-count":63,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2025,8]]}},"alternative-id":["10.14778\/3750601.3750626"],"URL":"https:\/\/doi.org\/10.14778\/3750601.3750626","relation":{},"ISSN":["2150-8097"],"issn-type":[{"value":"2150-8097","type":"print"}],"subject":[],"published":{"date-parts":[[2025,8]]},"assertion":[{"value":"2025-09-16","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}