无法对分布式协议做单元测试，但可以做模型检验
分布式缺陷在部署后修复成本高昂。模型检验能让你在写下第一行实现代码之前就发现它们。以下是如何使用 TLA+ 做到这一点。
你无法对分布式协议做单元测试。单元测试在一台机器上以一个顺序运行一个进程。而你的协议在五台机器上以十个进程、以你无法控制的顺序运行。这两种现实之间的鸿沟，正是缺陷藏身之处。 模型检验弥合了这一鸿沟。它穷举协议可能到达的每一种状态的所有可能交错。如果存在两条副本不一致的路径、存在领导者选举陷入死锁的路径、或存在…
2 posts
分布式缺陷在部署后修复成本高昂。模型检验能让你在写下第一行实现代码之前就发现它们。以下是如何使用 TLA+ 做到这一点。
你无法对分布式协议做单元测试。单元测试在一台机器上以一个顺序运行一个进程。而你的协议在五台机器上以十个进程、以你无法控制的顺序运行。这两种现实之间的鸿沟，正是缺陷藏身之处。 模型检验弥合了这一鸿沟。它穷举协议可能到达的每一种状态的所有可能交错。如果存在两条副本不一致的路径、存在领导者选举陷入死锁的路径、或存在…
Crash-only 软件将每一次失败视为崩溃，将每一次启动视为恢复。对于 Web 服务来说，这意味着删除你的关闭逻辑，并设计出能在 kill -9 下存活的状态。
你的 Web 服务有一个关闭处理器。它会刷写缓冲区、关闭连接、写入检查点。也许你曾经测试过一次。在生产环境中，它可能只在每年一次的有计划部署时才会运行。其余时间，你的服务死于 OOM kill、节点驱逐、断电，或是超时后被 SIGKILL 的部署。 Crash-only…