9
腾讯PaxosStore中共识算法的验证
source link: https://zhuanlan.zhihu.com/p/85864733
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
腾讯PaxosStore中共识算法的验证
分布式算法，分布式系统
[2020.11.08]
- 近期完成了基于TLA-PS的证明，并且已经更新到官方案例中。正在进行EagerVoting和Voting 的精化关系的形式化规约与验证。
- 论文全文已经在《软件学报》发表。
微信背后的高可用存储系统PaxosStore中，使用了Paxos算法。PaxosStore系统的论文中只给出了算法的实现，并未深入讨论其正确性。
Jianjun Zheng, Qian Lin, Jiatao Xu, Cheng Wei, Chuwei Zeng, Pingan Yang, and Yunfan Zhang. 2017. PaxosStore: high-availability storage made practical in WeChat.Proc. VLDB Endow.10, 12 (August 2017), 1730-1741. DOI: https://doi.org/10.14778/3137765.3137778.
为此，我们使用TLA+对PaxosStore中的Paxos实现（我们称为TPaxos）进行了形式化规约与验证。
- 规约的代码和model checking结果见我们的github项目：TPaxos的TLA+规约与验证 。
- 我们的这个案例被TLA+的官方案例项目merge进去了：在TLA+官方案例项目中的链接。
- 相关的论文投往了软件学报的一个专刊，未来正式定稿了会发布出来。
验证过程中，我们采用了精化技术（参考了Lamport的做法），将TPaxos这一新的变体，“挂在”精化树上。未来我们希望：i）所有Paxos变体都能厘清关系，挂在一棵精化树上，实现增量式地高效验证，ii）对既有变体的原理理解地更深，iii）能够有效地指导新变体的开发。
此外，目前主要还是对设计（算法伪码这一层次）在验证，未来我们希望能够走到（至少更接近）代码层。
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK