Stateright:一个用于实现分布式系统的模型检查器

在当今的云计算时代,分布式系统已成为构建大规模应用不可或缺的基础设施。然而,正确实现分布式算法一直是一个极具挑战性的任务。像Paxos和Raft这样的共识协议,由于网络设备导致的固有不确定性(如消息重排序),其正确实现尤其困难。为了应对这一挑战,Stateright应运而生。

Stateright简介

Stateright是一个用Rust语言编写的Actor库和模型检查器,旨在简化分布式系统的实现和验证过程。它提供了以下核心功能:

嵌入式模型检查器:可以系统地枚举所有可能的系统行为。
交互式UI:用于探索系统行为。
轻量级Actor运行时:可以在真实网络上运行实现的系统。
线性一致性测试器:可以在模型检查器中运行,提供比Jepsen等类似解决方案更全面的测试覆盖。

Stateright Explorer screenshot

Stateright的主要特性

Stateright包含一个通用的模型检查器,提供以下功能:

通过"always"属性进行不变量检查
通过"sometimes"属性进行非平凡性检查
通过"eventually"属性进行活性检查(实验性/不完整)
用于交互式探索状态空间的Web浏览器UI
线性一致性和顺序一致性测试器
支持对称性归约以减少状态空间

Stateright的Actor系统特性包括:

可以在"真实世界"中执行Actor的运行时
用于有损/无损、重复/非重复网络的模型,能够捕获Actor消息历史以检查Actor系统是否符合预期的一致性模型
用于模型检查的可插拔网络语义,允许在更少的假设(如"有损无序重复")和更多的假设(加速模型检查;如"无损有序")之间进行选择
可选的网络适配器,为一对Actor之间的消息提供无损非重复有序的虚拟通道

与其他Actor库相比,Stateright使您能够正式验证实现的正确性。与TLA+的TLC等模型检查器相比,使用Stateright实现的系统无需用其他语言重新实现即可在真实网络上运行。

快速入门

要开始使用Stateright,可以按照以下步骤操作:

阅读《使用Stateright构建分布式系统》一书,这是最全面的入门资料。
观看视频介绍,快速了解Stateright的主要概念。
查阅详细的API文档。
加入Stateright Discord服务器获取问答和其他反馈。

示例

Stateright包含多个示例,如单决策Paxos集群和抽象的两阶段提交模型。

通过传递checkCLI参数,可以使每个示例使用Stateright的模型检查器进行自验证:

# 具有3个资源管理器的两阶段提交
cargo run --release --example 2pc check 3
# 具有3个客户端的Paxos集群
cargo run --release --example paxos check 3
# 具有3个客户端的单副本(非复制)寄存器
cargo run --release --example single-copy-register check 3
# 具有2个客户端的可线性化分布式寄存器(ABD算法),假设Actor之间有序通道
cargo run --release --example linearizable-register check 2 ordered

传递exploreCLI参数会使每个示例在本地3000端口启动Stateright Explorer Web UI,允许您浏览系统行为:

cargo run --release --example 2pc explore
cargo run --release --example paxos explore
cargo run --release --example single-copy-register explore
cargo run --release --example linearizable-register explore

对于利用Actor功能的示例,传递spawnCLI参数将使用包含的运行时生成Actor,通过UDP传输JSON消息:

cargo run --release --example paxos spawn
cargo run --release --example single-copy-register spawn
cargo run --release --example linearizable-register spawn

bench.sh脚本使用各种设置运行所有示例,用于基准测试对库的更改的性能影响:

./bench.sh

贡献

欢迎贡献!请fork库,将更改推送到您的fork,然后发送拉取请求。除非在拉取请求中另有明确说明,否则所有贡献均在MIT许可下共享。

结语

Stateright为构建和验证分布式系统提供了强大的工具集。通过结合模型检查、可视化探索和实际运行时,它帮助开发人员克服了分布式算法实现中的许多固有挑战。无论您是在设计新的分布式协议,还是试图验证现有系统的正确性,Stateright都能为您提供宝贵的支持。随着分布式系统在现代计算架构中的重要性日益提升,像Stateright这样的工具将在确保这些系统的可靠性和正确性方面发挥越来越重要的作用。