如何证明像 multipaxos 这样的共识实现是正确的？
how to prove a consensus implementation like multipaxos is right?
我想证明我的multi-paxos实现是正确的。有没有有效的例子供我测试？或者可以有一些其他的方法来说服别人我的实现是正确的。
我试图找到一些包含示例的论文，但大多数论文只是指定了算法。
您无法通过示例或测试来证明任何事情。你只能通过证明来证明一些事情。
所以，为了证明你的multi-paxos实现是正确的，你需要先写下严格的数学规范说明什么是"right"，然后证明你的实现满足这个规格。
Elastic 是 Elasticsearch 背后的公司，希望加强他们是否存在设计错误。他们在 GitHub here 上构建了所有算法的 TLA+ 模型，证明这些算法具有安全性。然后他们需要检查他们的代码没有偏离模型。他们写了一篇关于以这种方式查找和修复旧错误的博客。这种方法可以防止设计错误，因为您知道您的预期实现是正确的。然后你必须担心佣金错误，这是你的代码偏离模型的实现错误。显然，这是一项非常重要的工作投资，比实际编写您正在验证的代码要多得多。
相比之下，如果您查看 Google 上关于使用 Paxos 的著名 google 胖纸，他们没有使用正式证明。他们通过注入随机消息丢失和崩溃的测试进行压力测试很长时间，以期消除错误。然后你没有证据证明它是正确的，只有一些证据表明在数千小时的崩溃和网络错误模拟中没有观察到错误。这种建立信心的练习对于编写实现的单个人来说是可行的，并且 运行。
Kyle Kingsbury 的 Jepson 项目展示了他如何发现和证明其他人的实现中的错误。他仔细研究了人们声称的安全属性，然后设计了一个测试客户端，并 运行 在 vms 上安装系统并注入网络分区、消息丢失和崩溃。然后，他有一个检查器检查所有测试客户端看到的所有响应，以查找不一致之处。他在很多系统中发现了很多错误。所以公司现在聘请他来寻找错误。如果他发现 none，这并不是没有错误的证明，只是让人们更有信心（通常会发现错误！）。聘请编写开源检查器的人花几个月时间尝试检查您的代码是一项重大投资。 Kyle 教授面对面的培训课程，向您展示如何 运行 他的开源软件，并且您练习在代码中查找旧版本 sql 数据库中的错误。我参加了这门课程，我强烈推荐它。
在编写您自己的实现的情况下，问题在于您将花费多少精力。 Paxos 被证明是正确的，在实现困难的地方是你需要添加到核心算法以构建实用系统的所有现实世界的东西。举例来说，您可能会遇到节点在一段时间无法访问后如何赶上的错误。 运行ning 实验的方法可以长时间模拟大量错误，验证所有节点保持不变，并且没有客户端看到不稳定的状态，这可能是最可行的。检查所有节点是否都经历了相同的状态是微不足道的。证明没有客户端观察到节点从未进入的状态更难编码。您可以使用 Knassos，这是 Kyle 用 Clojure 编写的开源检查器。
终于有华盛顿大学的在线课程了，代码在 GitHub called DSLabs where students must write there own Paxos implementation in a project that links to the universities opensource checker that will check inconsistencies seen by clients during simulated network errors and crashes. As it is all opensource you can use it to check your own implementation. You can read a comsci paper about it titled Teaching rigorous distributed systems with efficient model checking。 DSLabs 是用 Java 编写的，因此如果不是用 jvm 语言编写的，插入您自己的实现可能不会那么容易。然后你可以让 Java 调用其他语言的任何其他进程 运行ning 所以理论上你可以编写一个 Java shim 来调用你的实现 运行ning在另一个过程中。
更新：人们可能会对这篇论文感兴趣，其中提到证明算法正确的成本需要人年，并且可能比它证明的代码大十倍https://blog.acolyer.org/2019/11/13/scaling-symbolic-evaluation-serval/
我想证明我的multi-paxos实现是正确的。有没有有效的例子供我测试？或者可以有一些其他的方法来说服别人我的实现是正确的。
我试图找到一些包含示例的论文，但大多数论文只是指定了算法。
您无法通过示例或测试来证明任何事情。你只能通过证明来证明一些事情。
所以，为了证明你的multi-paxos实现是正确的，你需要先写下严格的数学规范说明什么是"right"，然后证明你的实现满足这个规格。
Elastic 是 Elasticsearch 背后的公司，希望加强他们是否存在设计错误。他们在 GitHub here 上构建了所有算法的 TLA+ 模型，证明这些算法具有安全性。然后他们需要检查他们的代码没有偏离模型。他们写了一篇关于以这种方式查找和修复旧错误的博客。这种方法可以防止设计错误，因为您知道您的预期实现是正确的。然后你必须担心佣金错误，这是你的代码偏离模型的实现错误。显然，这是一项非常重要的工作投资，比实际编写您正在验证的代码要多得多。
相比之下，如果您查看 Google 上关于使用 Paxos 的著名 google 胖纸，他们没有使用正式证明。他们通过注入随机消息丢失和崩溃的测试进行压力测试很长时间，以期消除错误。然后你没有证据证明它是正确的，只有一些证据表明在数千小时的崩溃和网络错误模拟中没有观察到错误。这种建立信心的练习对于编写实现的单个人来说是可行的，并且 运行。
Kyle Kingsbury 的 Jepson 项目展示了他如何发现和证明其他人的实现中的错误。他仔细研究了人们声称的安全属性，然后设计了一个测试客户端，并 运行 在 vms 上安装系统并注入网络分区、消息丢失和崩溃。然后，他有一个检查器检查所有测试客户端看到的所有响应，以查找不一致之处。他在很多系统中发现了很多错误。所以公司现在聘请他来寻找错误。如果他发现 none，这并不是没有错误的证明，只是让人们更有信心（通常会发现错误！）。聘请编写开源检查器的人花几个月时间尝试检查您的代码是一项重大投资。 Kyle 教授面对面的培训课程，向您展示如何 运行 他的开源软件，并且您练习在代码中查找旧版本 sql 数据库中的错误。我参加了这门课程，我强烈推荐它。
在编写您自己的实现的情况下，问题在于您将花费多少精力。 Paxos 被证明是正确的，在实现困难的地方是你需要添加到核心算法以构建实用系统的所有现实世界的东西。举例来说，您可能会遇到节点在一段时间无法访问后如何赶上的错误。 运行ning 实验的方法可以长时间模拟大量错误，验证所有节点保持不变，并且没有客户端看到不稳定的状态，这可能是最可行的。检查所有节点是否都经历了相同的状态是微不足道的。证明没有客户端观察到节点从未进入的状态更难编码。您可以使用 Knassos，这是 Kyle 用 Clojure 编写的开源检查器。
终于有华盛顿大学的在线课程了，代码在 GitHub called DSLabs where students must write there own Paxos implementation in a project that links to the universities opensource checker that will check inconsistencies seen by clients during simulated network errors and crashes. As it is all opensource you can use it to check your own implementation. You can read a comsci paper about it titled Teaching rigorous distributed systems with efficient model checking。 DSLabs 是用 Java 编写的，因此如果不是用 jvm 语言编写的，插入您自己的实现可能不会那么容易。然后你可以让 Java 调用其他语言的任何其他进程 运行ning 所以理论上你可以编写一个 Java shim 来调用你的实现 运行ning在另一个过程中。
更新：人们可能会对这篇论文感兴趣，其中提到证明算法正确的成本需要人年，并且可能比它证明的代码大十倍https://blog.acolyer.org/2019/11/13/scaling-symbolic-evaluation-serval/