无日志动态重配置协议的设计与分析

基于复制状态机模型的分布式复制系统已成为现代数据库系统基础且普遍的存在。为在故障下确保可用性，这些系统必须能通过动态重配置用健康节点动态替换失效节点。MongoDB是一种文档导向数据库，其分布式复制机制派生自Raft协议。本文中，我们提出MongoRaftReconfig，一种用于MongoDB复制系统的新型动态重配置协议。MongoRaftReconfig采用无日志方法管理配置状态，并将配置变更处理与主数据库操作日志解耦。该协议设计受先前MongoDB中存在的非安全遗留重配置机制重设计时所面临工程约束的影响。我们提供了MongoRaftReconfig的安全性证明及TLA+形式化规范。据我们所知，这是首个已发布的基于Raft系统的重配置协议安全性证明与形式化规范。我们还给出了在有限协议实例上模型检验其安全属性的结果。最后，我们讨论了MongoRaftReconfig的概念新颖性，它如何被理解为Raft单服务器重配置算法的优化与泛化版本，并给出了其优化如何为重配置提供性能收益的实验评估。