树与龟：状态机复制协议的模块化抽象
分布式、并行与集群计算
2023-05-09 v2
摘要
我们提出两种用于设计模块化状态机复制（SMR）协议的抽象：树与龟。树刻画了可能的状态机历史集合，而龟代表一种试图在该树中达成一致的子协议。我们通过由抽象树龟构建崩溃容错 SMR 协议并提供树龟实现的示例，展示了这些抽象的适用性。树龟也可被扩展以具备拜占庭容错（BFT）能力。树龟的模块化特性提供了一种用于添加领导者以保证活性的通用方法。我们期望这些抽象将简化 SMR 协议的推理与形式化验证，并促进协议设计的创新。
引用
@article{arxiv.2304.07850,
title = {Trees and Turtles: Modular Abstractions for State Machine Replication Protocols},
author = {Natalie Neamtu and Haobin Ni and Robbert van Renesse},
journal= {arXiv preprint arXiv:2304.07850},
year = {2023}
}
备注
Full version of the paper published in PaPoC '23, including full proofs and discussion of BFT protocols