Finding bugs in Raft implementations

摘要

Antithesis 团队在多个开源 Raft 实现（包括 HashiCorp Raft、Aeron Cluster、OpenRaft、MicroRaft）中发现了违反状态机安全性的 bug。他们使用简单的 Chain of Blocks 工作负载和确定性模拟环境，通过故障注入和随机输入，在一小时内就能复现数据分歧。文章详细分析了 HashiCorp Raft 中的三个 bug（一个安全性、两个活性），其中一个根因是异步心跳处理与主线程的竞态条件。作者强调正式规范不等于代码正确，测试可以很简单，并批评了分布式系统测试中的'习得性无助'。