We present two abstractions for designing modular state machine replication (SMR) protocols: trees and turtles. A tree captures the set of possible state machine histories, while a turtle represents a subprotocol that tries to find agreement in this tree. We showcase the applicability of these abstractions by constructing crash-tolerant SMR protocols out of abstract tree turtles and providing examples of tree turtle implementations. The modularity of tree turtles allows a generic approach for adding a leader for liveness. We expect that these abstractions will simplify reasoning and formal verification of SMR protocols as well as facilitate innovation in protocol designs.

翻译：我们提出了两种用于设计模块化状态机复制（SMR）协议的抽象：树与龟。树捕捉了可能的状态机历史集合，而龟则代表试图在该树中达成一致性的子协议。我们通过基于抽象树龟构建容错型SMR协议，并提供树龟实现的示例，展示了这些抽象的可应用性。树龟的模块化特性支持通过通用方式引入领导者以实现活性。我们预期，这些抽象将有助于简化SMR协议的推理与形式化验证，并推动协议设计的创新。