建模重要性：使用建模工具发现Paxos实现中的一个错误 - brooker
source link: https://www.jdon.com/57598
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
在过去的几周里，我一直在学习优秀的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+ 等语言的重要原因。它们不仅是指定、检查和建模算法的好方法，而且还是传达它们的好方法。如果您使用分布式算法，我强烈建议您选择其中一种语言。
Recommend
-
25
现状 早在行业刚开始的那个时期，安全岗位基本只有两种，WEB安全工程师和网络安全工程师，回忆一下近几年企业出现的风险事件、大多是安全工程师围绕应用安全漏洞，以及如何在漏洞攻与防之间进行技术博弈。普遍受限于当时年代对...
-
7
Brooker Group将向DeFi和Dapp初创公司投资近5000万美元 • 11 小时前 碳链价值A...
-
11
使用业务能力方法实现DDD战略建模 - pulse将大型复杂系统模块化为更小、更易于管理的部分是很好的最佳实践，不仅可以降低每个部分的认知负担，还可以实现团队独立性和操作弹性。棘手的一点是如何划定边界？为整个系统建立一个稳定和可持续的结构。基于有...
-
9
使用用户故事映射实现领域建模 - pulse在构建业务关键型软件时，像领域驱动设计这样的实践是把一个重要的焦点放在IT和领域专家协作上。此外许多公司还看到了与客户更亲密的关系，更好地了解他们的愿望和需求，从而建立更忠诚的客户群的必要性。这就是服务设计、...
-
3
幽默视频：业务建模的重要性从需求到代码的直接拷贝，无建模，没有在问题空间和解决方案空间之间的迭代过程，没有DDD设计的样子（点击下面图片）： 另外：以程序员的认知理解实现的业务应用系统：
-
3
在 .NET 中使用有限状态机实现工作流建模 希望这篇文章...
-
3
数据发现对数据治理的重要性-51CTO.COM 数据发现对数据治理的重要性 作者：何威风 2022-06-09 00:03:44 数据发现系统确保数据是可搜索的。就像在 Google 中输入搜索词一样，完善的数...
-
9
Black Mirror creator Charlie Brooker on AI, tech, and creativity
-
5
使用 Structurizr 实现企业范围建模的项目 这里有一个使用Structurizr进行企业建模的方法的例子，其中自顶向下的系统景观图是自动...
-
4
使用知识图实现领域知识建模与测试 知识图成为现代软件工程实践的基石。知识图是...
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK