无法对分布式协议做单元测试，但可以做模型检验
分布式缺陷在部署后修复成本高昂。模型检验能让你在写下第一行实现代码之前就发现它们。以下是如何使用 TLA+ 做到这一点。
你无法对分布式协议做单元测试。单元测试在一台机器上以一个顺序运行一个进程。而你的协议在五台机器上以十个进程、以你无法控制的顺序运行。这两种现实之间的鸿沟，正是缺陷藏身之处。 模型检验弥合了这一鸿沟。它穷举协议可能到达的每一种状态的所有可能交错。如果存在两条副本不一致的路径、存在领导者选举陷入死锁的路径、或存在…
protocol-design
1 post