2026-07-24T09:35:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14863 2024-03-06T10:55:02Z ddc:004 open_access

Brief Announcement: Design and Verification of a Logless Dynamic Reconfiguration Protocol in MongoDB Replication Schultz, William Zhou, Siyuan Tripakis, Stavros Reconfiguration Consensus State Machine Replication We introduce a novel dynamic reconfiguration protocol for the MongoDB replication system that extends and generalizes the single server reconfiguration protocol of the Raft consensus algorithm. Our protocol decouples the processing of configuration changes from the main database operation log, which allows reconfigurations to proceed in cases when the main log is prevented from processing new operations. Additionally, this decoupling allows for configuration state to be managed by a logless replicated state machine, storing only the latest version of the configuration and avoiding the complexities of a log-based protocol. We present a formal specification of the protocol in TLA+, initial verification results of model checking its safety properties, and an experimental evaluation of how reconfigurations are able to quickly restore a system to healthy operation when node failures have stalled the main operation log. This announcement is a short version and the full paper is available at [Schultz et al., 2021]. Schloss Dagstuhl – Leibniz-Zentrum für Informatik William Schultz and Siyuan Zhou and Stavros Tripakis 2021 Is Part Of LIPIcs, Volume 209, 35th International Symposium on Distributed Computing (DISC 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.DISC.2021.61 urn:nbn:de:0030-drops-148636 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021.61 eng https://creativecommons.org/licenses/by/4.0/legalcode