从理论上讲，至少应该可以强行验证无锁算法（只有很多相交的函数调用组合）。是否有任何工具或正式推理过程可用来证明无锁算法是正确的（理想情况下，它也应该能够检查比赛条件和ABA问题）？
In theory, it should be possible to at least brute force a verification of a lock-free algorithm (there are only so many combinations of function calls intersecting). Are there any tools or formal reasoning processes available to actually prove that a lock-free algorithm is correct (ideally it should also be able to check for race conditions and the ABA problem as well)?
注意：如果您知道一种方法来证明一个观点（例如，仅证明它可以解决ABA问题是安全的）或我没有提到的问题，则无论如何都要发布解决方案。在最坏的情况下，可以依次执行每种方法以对其进行完全验证。
Note: If you know a way to just prove one point (e.g. only prove that it is safe from the ABA problem) or a problem I haven't mentioned then post the solution anyway. In the worst case scenario, each method can be done in turn to fully verify it.
推荐答案您绝对应该尝试旋转模型检查器。
您编写了一个程序一种简单的类似于C的语言（称为Promela）中的类似模型，Spin在内部将其转换为状态机。一个模型可以包含多个并行流程。
You write a program-like model in a simple C-like language called Promela, which Spin internally translates into a state machine. A model can contain multiple parallel processes.
Spin然后执行的操作是检查每个条件下所有可能的指令交织您想要测试-通常情况下，没有竞争条件，没有死锁，等等。大多数测试可以使用 assert（）语句轻松编写。如果存在任何可能违反断言的执行序列，则会打印出该序列，否则将为您提供全部清除。
What Spin then does is check every possible interleaving of instructions from each process for whatever conditions you want to test -- typically, absence of race conditions, freedom from deadlocks etc. Most of these tests can be easily written using assert() statements. If there is any possible execution sequence that violates an assertion, the sequence is printed out, otherwise you are given the "all-clear".
（嗯，实际上
这是一个令人难以置信的程序，它赢得了2001年的 ACM系统软件奖（其他获奖者包括Unix，Postscript ，Apache，TeX）。我很快就开始使用它，几天之内就可以实现MPI函数的模型 MPI_Isend（）和 MPI_Irecv（）在Promela中。 Spin在我转换为Promela进行测试的并行代码的一部分中发现了几个 tricky 竞争条件。
This is an incredible program, it won the 2001 ACM System Software Award (other winners include Unix, Postscript, Apache, TeX). I got started using it very quickly, and in a couple of days was able to implement models of the MPI functions MPI_Isend() and MPI_Irecv() in Promela. Spin found a couple of tricky race conditions in one segment of parallel code I converted across to Promela for testing.
更多推荐
如何验证无锁算法？
发布评论