Formal verification of a distributed dynamic reconfiguration protocol
Formal verification of a distributed dynamic reconfiguration protocol
复制标题
分布式动态重配置协议的形式化验证
DOI：
10.1145/3497775.3503688
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Tripakis, Stavros
中科院分区：
文献类型：
--
作者：
Schultz, William;Dardik, Ian;Tripakis, Stavros
本文给出了mongoraftreconfig（一种分布式动态重配置协议）的正式的、机器检查的TLA+安全性证明。mongoraftreconfig是为MongoDB设计和实现的，MongoDB是一个分布式数据库，其复制协议派生自Raft共识算法。我们提出了一个用TLA+形式化的mongoraftreconfig的归纳不变量，并使用TLA+证明系统（TLAPS）进行了形式化证明。我们还对mongoraftreconfig的两个关键安全属性（LeaderCompletenessandStateMachineSafety）进行了正式的TLAPS证明。据我们所知，这是基于Raft复制系统的动态重构协议的第一个机器检查归纳不变量和安全证明。
We present a formal, machine checked TLA+ safety proof ofMongoRaftReconfig, a distributed dynamic reconfiguration protocol.MongoRaftReconfigwas designed for and implemented in MongoDB, a distributed database whose replication protocol is derived from the Raft consensus algorithm. We present an inductive invariant forMongoRaftReconfigthat 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 ofMongoRaftReconfig,LeaderCompletenessandStateMachineSafety. 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.
登录
查看更多内容
无日志动态重配置协议的设计与分析
DOI：
10.4230/lipics.opodis.2021.26
发表时间：
2021
期刊：
Proceedings of the 27th ACM Symposium on Operating Systems Principles
影响因子：
--
作者：
William Schultz;Siyuan Zhou;Ian Dardik;S. Tripakis
通讯作者：
S. Tripakis
MongoDB 中基于拉取共识的容错复制
DOI：
--
发表时间：
2021
期刊：
Symposium on Networked Systems Design and Implementation
影响因子：
--
作者：
Siyuan Zhou;Shuai Mu
通讯作者：
Shuai Mu
使用 TLC 检查电感不变性
DOI：
--
发表时间：
2018
期刊：
影响因子：
--
作者：
L. Lamport
通讯作者：
L. Lamport
论平等主义Paxos的正确性
影响因子：
0.5
作者：
P. Sutra
通讯作者：
P. Sutra
DOI：
10.1007/978-3-540-75560-9_13
发表时间：
2007-10
期刊：
--
影响因子：
--
作者：
Richard Bonichon;David Delahaye;Damien Doligez
通讯作者：
Richard Bonichon;David Delahaye;Damien Doligez