algorithm - 如何验证无锁算法？

Question

从理论上讲，至少应该可以对无锁算法进行暴力验证(函数调用相交的组合只有这么多)。是否有任何工具或形式推理过程可用于实际证明无锁算法是正确的(理想情况下它还应该能够检查竞争条件和 ABA 问题)？

注意:如果您知道一种方法来证明一个点(例如，只证明它是安全的 ABA 问题)或我没有提到的问题，那么无论如何都要发布解决方案。在最坏的情况下，每个方法都可以依次做，以充分验证。

Answer 1

你绝对应该试试 Spin model checker .

您使用称为 Promela 的简单类 C 语言编写类程序模型，Spin 在内部将其转换为状态机。一个模型可以包含多个并行进程。

然后 Spin 所做的是检查来自每个进程的所有可能的指令交错您想要测试的任何条件——通常是，没有竞争条件，没有死锁等。大多数这些测试都可以使用 assert() 语句轻松编写。如果有任何可能的执行顺序违反断言，则打印出该顺序，否则您将获得“全部清除”。

(好吧，实际上它使用了更奇特和更快的算法来完成此操作，但这就是效果。默认情况下，检查所有可到达的程序状态。)

这是一个不可思议的程序，它赢得了 2001 年 ACM System Software Award (其他获胜者包括 Unix、Postscript、Apache、TeX)。我很快就开始使用它，几天后就能够在 Promela 中实现 MPI 函数 MPI_Isend() 和 MPI_Irecv() 的模型。 Spin 在我转换到 Promela 进行测试的一段并行代码中发现了几个棘手竞争条件。