Design and Analysis of a Logless Dynamic Reconfiguration Protocol
Design and Analysis of a Logless Dynamic Reconfiguration Protocol
复制标题
无日志动态重配置协议的设计与分析
DOI：
10.4230/lipics.opodis.2021.26
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
S. Tripakis
中科院分区：
文献类型：
--
作者：
William Schultz;Siyuan Zhou;Ian Dardik;S. Tripakis
基于复制状态机模型的分布式复制系统作为现代数据库系统的基础已经变得无处不在。为了确保出现故障时的可用性，这些系统必须能够通过动态重新配置将故障节点动态替换为健康节点。MongoDB是一个面向文档的数据库，具有从RAFT协议派生的分布式复制机制。本文提出了一种适用于MongoDB复制系统的动态重构协议--MongoRaftResources。MongoRaft562利用LOGLISH方法来管理配置状态，并将配置更改的处理与主数据库操作日志分离。该协议的设计受到了工程约束的影响，当时试图重新设计MongoDB中以前存在的不安全的、遗留的重新配置机制。我们给出了一个MongoRaft重构的安全性证明，并给出了TLA+的形式化规范。据我们所知，这是第一个发表的基于浮筏系统的重新配置协议的安全证明和正式规范。我们还给出了有限个协议实例上的模型检测结果及其安全性质。最后，我们讨论了MongoRaftResources的概念创新，如何将其理解为RAFT单服务器重构算法的优化和推广版本，并给出了它的优化如何为重构提供性能优势的实验评估。
Distributed replication systems based on the replicated state machine model have become ubiquitous as the foundation of modern database systems. To ensure availability in the presence of faults, these systems must be able to dynamically replace failed nodes with healthy ones via dynamic reconfiguration. MongoDB is a document oriented database with a distributed replication mechanism derived from the Raft protocol. In this paper, we present MongoRaftReconfig, a novel dynamic reconfiguration protocol for the MongoDB replication system. MongoRaftReconfig utilizes a logless approach to managing configuration state and decouples the processing of configuration changes from the main database operation log. The protocol's design was influenced by engineering constraints faced when attempting to redesign an unsafe, legacy reconfiguration mechanism that existed previously in MongoDB. We provide a safety proof of MongoRaftReconfig, along with a formal specification in TLA+. To our knowledge, this is the first published safety proof and formal specification of a reconfiguration protocol for a Raft-based system. We also present results from model checking its safety properties on finite protocol instances. Finally, we discuss the conceptual novelties of MongoRaftReconfig, how it can be understood as an optimized and generalized version of the single server reconfiguration algorithm of Raft, and present an experimental evaluation of how its optimizations can provide performance benefits for reconfigurations.