consensus - 如何证明像 multipaxos 这样的共识实现是正确的？

Question

我想证明我对multi-paxos的实现是正确的。有没有有效的例子供我测试？或者可以有一些其他方法来说服其他人我的实现是正确的。

我试图找到一些包含示例的论文，但大多数论文只是指定了算法。

Answer 1

Elastic 是 Elasticsearch 背后的公司，想要加强对他们是否存在设计错误的控制。他们在 GitHub here 上构建了所​​有算法的 TLA+ 模型证明算法导致安全。然后他们需要检查他们的代码没有偏离模型。他们写了一篇关于以这种方式查找和修复旧错误的博客。这种方法可以防止设计错误，因为您知道您的预期实现是正确的。然后你必须担心佣金错误，这是你的代码偏离模型的实现错误。显然，这是一项非常重要的工作投资，比实际编写您正在验证的代码要多得多。

相比之下，如果您查看著名的关于在 Google 使用 Paxos 的 google chubby 论文，他们没有使用正式证明。他们通过注入(inject)随机消息丢失和崩溃的测试进行压力测试很长时间，以期消除错误。然后你没有证据证明它是正确的，只有一些证据表明在数千小时的崩溃和网络错误模拟中没有观察到错误。这种建立信心的练习是可行的，一个编写实现的人就可以设置和运行。

Kyle Kingsbury 的 Jepson 项目展示了他如何发现和证明其他人的实现中的错误。他仔细研究了人们声称的安全属性，然后设计了一个测试客户端，并在 vms 上运行系统并注入(inject)网络分区、消息丢失和崩溃。然后，他有一个检查器检查所有测试客户端看到的所有响应，以查找不一致之处。他在很多系统中发现了很多错误。所以公司现在聘请他来寻找错误。如果他什么也没找到，那不是没有错误的证明，只是让人们更有信心(通常会发现错误!)。聘请编写开源检查器的人花几个月时间尝试检查您的代码是一项重大投资。 Kyle 亲自教授培训类(class)，向您展示如何运行他的开源软件，并在代码中练习在旧版本的 sql 数据库中查找错误。我参加了这门类(class)，我强烈推荐它。

在编写您自己的实现的情况下，问题在于您将花费多少精力。 Paxos 被证明是正确的，在实现困难的地方是你需要添加到核心算法以构建实用系统的所有现实世界的东西。举例来说，您可能会遇到节点在一段时间无法访问后如何 catch 的错误。运行实验的方法可以长时间模拟大量错误，验证所有节点保持不变，并且没有客户端看到不稳定的状态，这可能是最可行的。检查所有节点是否都经历了相同的状态是微不足道的。证明没有客户端观察到节点从未进入的状态更难编码。您可以使用 Knassos这是 Kyle 用 Clojure 编写的开源检查器。

最后还有华盛顿大学的在线类(class)，代码在 GitHub called DSLabs 上学生必须在一个链接到大学开源检查器的项目中编写自己的 Paxos 实现，该检查器将检查客户端在模拟网络错误和崩溃期间看到的不一致情况。由于它都是开源的，您可以使用它来检查您自己的实现。您可以阅读一篇关于它的 comsci 论文，标题为 Teaching rigorous distributed systems with efficient model checking . DSLabs 是用 Java 编写的，因此如果不是用 jvm 语言编写的，插入您自己的实现可能不会那么容易。然后，您可以再次让 Java 调用以其他语言运行的任何其他进程，因此理论上您可以编写一个 Java 填充程序来调用您在另一个进程中运行的实现。

更新:人们可能会对这篇论文感兴趣，这篇论文提到证明算法正确的成本需要人年，并且可能比它证明的代码大十倍 https://blog.acolyer.org/2019/11/13/scaling-symbolic-evaluation-serval/