Adore: atomic distributed objects with certified reconfiguration
Adore: atomic distributed objects with certified reconfiguration
复制标题
Adore：具有经过认证的重新配置的原子分布式对象
DOI：
10.1145/3519939.3523444
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Shao, Zhong
中科院分区：
文献类型：
--
作者：
Honoré, Wolf;Shin, Ji-Yong;Kim, Jieung;Shao, Zhong
找到正确的抽象对于推理复杂系统（如Paxos和Raft等分布式协议）至关重要。尽管最近在这一领域进行了大量令人印象深刻的验证工作，但我们认为过去的分布式状态建模方法对于协议级推理并不理想：它们要么隐藏了重要的细节，要么从网络中泄露了太多的复杂性。作为证据，我们观察到，几乎所有的人都避免了复杂的，但重要的问题的重新配置。重新配置的主要挑战在于它如何与协议的核心安全不变量交互。为了处理这种增加的复杂性，我们引入了Adore模型，其新颖的抽象状态隐藏了网络级通信，同时捕获了已提交和未提交状态之间的依赖关系，以及选举法定人数等元数据。它包括对通用重新配置命令的一流支持，可以使用各种实现实例化该命令。在此模型下，重构和核心协议之间的微妙的相互作用变得清晰，并与此洞察，我们完成了第一个机械化的安全性证明的可重构共识协议。
Finding the right abstraction is critical for reasoning about complex systems such as distributed protocols like Paxos and Raft. Despite a recent abundance of impressive verification work in this area, we claim the ways that past efforts model distributed state are not ideal for protocol-level reasoning: they either hide important details, or leak too much complexity from the network. As evidence we observe that nearly all of them avoid the complex, but important issue of reconfiguration. Reconfiguration's primary challenge lies in how it interacts with a protocol's core safety invariants. To handle this increased complexity, we introduce the Adore model, whose novel abstract state hides network-level communications while capturing dependencies between committed and uncommitted states, as well as metadata like election quorums. It includes first-class support for a generic reconfiguration command that can be instantiated with a variety of implementations. Under this model, the subtle interactions between reconfiguration and the core protocol become clear, and with this insight we completed the first mechanized proof of safety of a reconfigurable consensus protocol.
登录
查看更多内容
无日志动态重配置协议的设计与分析
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
使用 CSPEC 中的移动器验证并发软件
DOI：
--
发表时间：
2018
期刊：
USENIX Symposium on Operating Systems Design and Implementation
影响因子：
--
作者：
Tej Chajed;Frans Kaashoek;Mit Csail;Microsoft Butler Lampson;Nickolai Zeldovich;M. Kaashoek;Microsoft Research
通讯作者：
Microsoft Research
DOI：
10.1145/3497775.3503688
发表时间：
2022
期刊：
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
影响因子：
--
作者：
Schultz, William;Dardik, Ian;Tripakis, Stavros
通讯作者：
Tripakis, Stavros
影响因子：
--
作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
通讯作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
DOI：
--
发表时间：
2020
期刊：
FMBC@CAV
影响因子：
--
作者：
Helin Sahinturk;S. Turhan;Selvi Ozlem Can;Ali Abbas Ylmaz;A. Uysalel
通讯作者：
A. Uysalel