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