We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and implemented in MongoDB, a distributed database whose replication protocol is derived from the Raft consensus algorithm. We present an inductive invariant for MongoRaftReconfig that is formalized in TLA+ and formally proved using the TLA+ proof system (TLAPS). We also present a formal TLAPS proof of two key safety properties of MongoRaftReconfig, LeaderCompleteness and StateMachineSafety. To our knowledge, these are the first machine checked inductive invariant and safety proof of a dynamic reconfiguration protocol for a Raft based replication system.
翻译：我们提出了一个经过机器检查的关于MongoRaftReconfig(一个分布式动态重组协议)的正式TLA+安全证明。MongoDB设计并实施了MongoRaft Reconfig。MongoDB是一个分布式数据库,其复制协议来自Raft共识算法。我们为MongoRaftReconfig提供了一种诱导性进化剂,在TLA+中正式确立,并使用TLA+验证系统(TLAPS)正式证明。我们还为MongoRaftReconfig、Conflead Conflig、Confleteness和StateMachineSafety的两个主要安全属性提供了正式的TLAPS证明。据我们所知,这是对基于Raft的复制系统的动态重组协议的首个测试机的导导不动性磁性和安全证明。
相关内容
微信扫码咨询专知VIP会员