分布式系统的正确性验证方法
分布式系统的正确性验证方法
1. Jepsen框架
Jepsen是一个开源的分布式一致性验证框架，可用于验证分布式数据库、分布式消息队列、分布式协调系统。Jepsen探索特定故障模式下分布式系统是否满足一致性。Jepsen框架是一个Clojure程序库，Clojure是一门运行在JVM上的解释型的类Lisp语言。Jepsen测试程序是一个Clojure程序，它使用Jepsen框架来构建一个分布式系统，对其执行一系列操作，并验证这些操作的历史记录是否有意义。它还可以生成性能和可用性图，帮助描述系统如何响应不同故障。
Jepsen测试程序在Control
node上运行，使用SSH登录到一些DB node，在其上部署并启动相应的DB进程，DB进程组成待测试的分布式系统。测试开始后，Control node创建一组Client进程，每个Client都有自己的分布式系统客户端。Generator产生每个Client执行的operation，Client进程使用其客户端将operation应用于待测试的分布式系统。每个operation的开始和结束以及操作结果记录在历史记录中。同时，一个特殊的Client进程Nemesis将故障引入系统，其operation也来自Generator。测试结束后，DB将停止并卸载。Checker分析历史记录是否正确，并可生成报告、图表等。Checker在分析时可使用一个定义系统行为的Model。
2. 形式化的TLA+
TLA+是Leslie B. Lamport老爷子提出的分布式系统形式化验证方法。目前已知的，AWS的DynamoDB和微软的CosmosDB支持部分TLA+形式化验证。