在过去的几周里，我一直在学习优秀的P 编程语言，一种用于建模和指定分布式系统的语言。我在 P 中做的第一件事就是实现 Paxos——一种我很熟悉的算法，有很多微妙的失败模式，而且很容易出错。
为了测试 P 的模型检查器，我特意按照Paxos Made Simple 中的描述实现了一个有缺陷的 Paxos 版本，模型检查器发现Paxos实现出现错误。
我向一位同事提到了这一点，他说他们从未听说过这个错误。我认为它应该更广为人知，所以我想我应该写下来：
问题不在于Paxos算法本身，而在于论文中的描述。Michael Deardeuff 向我指出了这个错误，并将它写在可能是有史以来最好的 Stack Overflow问答中 。
事实证明这是因为 Paxos Made Simple 的文本中有两个歧义。首先，关于接受（第二）阶段的接受者的选择（来自 Paxos Made Simple）：
如果提议者从大多数接受者那里收到对其准备请求（编号为 n）的响应，那么它会向这些接受者中的每一个发送接受请求，以获得编号为 n 且值为 v 的提议，其中 v 是最高的值 -在响应中编号的提案，或者如果响应没有报告提案，则为任何值。
如果您按照本声明的内容，将接受消息发送给响应您的第一阶段消息的接受者，那么问题就不会发生。不幸的是，这也使得算法在实践中不太稳健。幸运的是，还有另一种可能的修复方法。再次，来自Michael的回答：
通过接受一个值，该节点还承诺不接受较早的值。
Lamport 在 Paxos Made Simple 中没有这么说。相反，他说：
如果接受者收到对编号为 n 的提案的接受请求，则它接受该提案，除非它已经响应了编号大于 n 的准备请求。
Leslie Lamport 是我的技术写作英雄之一。我重读了他的一些论文，比如时间逻辑有什么好处？有时只是因为我喜欢它们的书写方式。指出这种歧义并不是批评他的写作，而是提醒您即使在文本中对相对简单的分布式协议进行清晰的描述也是多么困难。正如兰波特本人所说：
散文不是精确描述算法的方式。
这就是为什么我如此喜欢 P 和 TLA+ 等语言的重要原因。它们不仅是指定、检查和建模算法的好方法，而且还是传达它们的好方法。如果您使用分布式算法，我强烈建议您选择其中一种语言。