我想证明我对multi-paxos的实现是正确的。有什么有效的例子可供我测试吗？或者可以有其他一些方法来说服其他人我的实现是正确的。
我试图找到一些包含示例的论文，但大多数论文只是指定了算法。
问问题
252 次
2 回答
5
Elasticsearch 背后的公司希望加强他们是否存在设计错误。他们在GitHub 上构建了所有算法的 TLA+ 模型，证明这些算法可以带来安全性。然后他们需要检查他们的代码没有偏离模型。他们写了一篇关于以这种方式查找和修复旧错误的博客。这种方法可以防止设计错误，因为您知道您的预期实现是正确的。然后你必须担心佣金错误，这是你的代码偏离模型的实现错误。显然，这是一项非常重要的工作投资，远远大于实际编写您要证明的代码。
相比之下，如果你看一下著名的 google chubby 论文，关于在 Google 使用 Paxos，他们没有使用正式的证明。他们在很长一段时间内通过注入随机消息丢失和崩溃的测试进行压力测试，以期摆脱错误。然后，您没有证据证明它是正确的，只有一些证据表明在数千小时的崩溃和网络错误模拟中没有观察到错误。这种建立信心的练习是可行的，一个编写实现的人可以设置和运行。
Kyle Kingsbury 的 Jepson 项目展示了他如何在其他人的实现中发现和证明错误。他仔细研究了人们声称的安全属性，然后设计了一个测试客户端，在虚拟机上运行系统并注入网络分区、消息丢失和崩溃。然后，他有一个检查器来检查所有测试客户看到的所有响应，以寻找不一致的地方。他在很多系统中发现了很多错误。所以公司现在雇佣他来寻找错误。如果他没有发现任何错误，则不能证明没有错误，只是让人们感到更加自信（并且通常会发现错误！）。聘请编写开源检查器的人花费几个月的时间来尝试修复您的代码是一项重大投资。Kyle 教授面对面的培训课程，向您展示如何运行他的开源软件，并练习在旧版本的 sql 数据库中查找错误的代码。我参加了这门课程，我强烈推荐它。
在编写您自己的实现的情况下，这是您将花费多少精力的问题。Paxos 被证明是正确的，在实现困难的地方是您需要添加到核心算法以创建实用系统的所有现实世界的东西。举例来说，您可能有一个错误，即节点在一段时间无法访问后如何赶上。运行长时间模拟大量错误的实验方法，验证所有节点保持不变，并且没有客户端看到不稳定状态，这可能是最可行的。检查所有节点是否都经历了相同的状态是微不足道的。证明没有客户端观察到节点从未进入的状态更难编码。您可以使用Knassos，它是 Kyle 用 Clojure 编写的开源检查器。
最后，华盛顿大学有一个在线课程，在GitHub 上有一个名为 DSLabs的代码，学生必须在一个项目中编写自己的 Paxos 实现，该项目链接到大学的开源检查器，该检查器将检查客户在模拟网络错误和崩溃期间看到的不一致。由于它都是开源的，您可以使用它来检查您自己的实现。你可以阅读一篇 comsci 论文，标题为通过有效的模型检查来教授严格的分布式系统. DSLabs 是用 Java 编写的，因此如果不是用 jvm 语言编写的，插入您自己的实现可能不会那么容易。然后，您可以再次让 Java 调用以其他语言运行的任何其他进程，因此理论上您可以编写一个 Java shim 调用在另一个进程中运行的实现。
更新：人们可能对这篇论文感兴趣，该论文提到证明算法正确的成本需要人数年，并且可能比它证明的代码大十倍https://blog.acolyer.org/2019/11/13/缩放符号评估服务/
于 2019-08-13T20:33:47.633 回答
0
您无法通过示例或测试来证明任何事情。你只能通过证明来证明某事。
所以，为了证明你的 multi-paxos 实现是正确的，你需要先写下一个严格的数学规范，说明什么是“正确”，然后证明你的实现符合这个规范。
于 2019-08-12T13:33:38.057 回答