如何验证无锁算法？

Question

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

笔记：如果你知道一种方法来证明一个观点（例如只是证明它对于 ABA 问题是安全的）或我没有提到的问题，然后无论如何发布解决方案。在最坏的情况下，可以依次执行每种方法来充分验证它。

Answer 1

您一定要试试旋模型检验。

您写在称为PROMELA一个简单的类C语言，其自旋内部转换成一个状态机的程序类似的模型。模型可以包含多个并行的进程。

什么旋转，然后做的是检查对于任何条件下你想要的每个流程说明每一个可能的交错测试 - 通常情况下，没有竞争条件，从自由死锁等多数这些测试可以使用assert()语句随便写。如果有违反断言任何可能的执行序列，该序列被打印出来，否则你被给予“全清除”。

（好吧，实际上它使用了很多发烧友和更快的算法来做到这一点，但是这是有效果的。默认情况下，所有可到达的程序状态进行检查。）

这是一个的难以置信的程序，它获得了2001年 ACM系统软件奖（其他获奖者包括UNIX，后记，阿帕奇，特）。我得到了非常迅速地开始使用它，并在一两天能实现的MPI函数MPI_Isend()和MPI_Irecv()在PROMELA的模型。自旋发现一对夫妇的棘手竞态条件中的并行代码的一个段I转换对面PROMELA用于测试。

Answer 2

Spin 确实很优秀，但也要考虑 继电器竞赛检测器 作者：德米特里·维尤科夫。它专为验证并发算法而设计，包括非阻塞（等待/无锁）算法。它是开源的并且获得自由许可。

Relacy 提供 POSIX 和 Windows 同步原语（互斥体、条件变量、信号量、CriticalSections、win32 事件、Interlocked* 等），因此您的实际 C++ 实现可以馈送到 Relacy 进行验证。无需像 Promela 和 Spin 那样开发单独的算法模型。

Relacy 提供 C++0x std::atomic （显式内存排序以获得胜利！）因此您可以使用预处理器 #defines 在 Relacy 的实现和您自己的平台特定原子实现之间进行选择（待定::原子, 增强::原子, ， ETC）。

调度可控：提供随机、上下文绑定和完整搜索（所有可能的交错）。

这是一个 Relacy 程序示例。有几点需要注意：

• 这 $ 是一个记录执行信息的Relacy宏。
• rl::var<T> 标记也需要被视为验证一部分的“正常”（非原子）变量。

代码：

#include <relacy/relacy_std.hpp>

// template parameter '2' is number of threads
struct race_test : rl::test_suite<race_test, 2>
{
    std::atomic<int> a;
    rl::var<int> x;

    // executed in single thread before main thread function
    void before()
    {
        a($) = 0;
        x($) = 0;
    }

    // main thread function
    void thread(unsigned thread_index)
    {
        if (0 == thread_index)
        {
            x($) = 1;
            a($).store(1, rl::memory_order_relaxed);
        }
        else
        {
            if (1 == a($).load(rl::memory_order_relaxed))
                x($) = 2;
        }
    }

    // executed in single thread after main thread function
    void after()
    {
    }

    // executed in single thread after every 'visible' action in main threads
    // disallowed to modify any state
    void invariant()
    {
    }
};

int main()
{
    rl::simulate<race_test>();
}

使用普通编译器进行编译（Relacy 仅包含头文件）并运行可执行文件：

struct race_test
DATA RACE
iteration: 8

execution history:
[0] 0:  atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0:  store, value=0, in race_test::before, test.cpp(15)
[2] 0:  store, value=1, in race_test::thread, test.cpp(23)
[3] 0:  atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)
[4] 1:  atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)
[5] 1:  store, value=0, in race_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

thread 0:
[0] 0:  atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0:  store, value=0, in race_test::before, test.cpp(15)
[2] 0:  store, value=1, in race_test::thread, test.cpp(23)
[3] 0:  atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)

thread 1:
[4] 1:  atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)
[5] 1:  store, value=0, in race_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

如果您喜欢的话，最新版本的 Relacy 还提供 Java 和 CLI 内存模型。

Answer 3

数据竞争检测是一个 NP 难题 [Netzer&Miller 1990]

我听说过 Lockset 和 DJit+ 工具（它们 教它 在 CDP 课程中）。尝试阅读幻灯片，并用谷歌搜索它们引用的内容。它包含一些有趣的信息。

Answer 4

我不知道你使用的是什么平台或语言 - 但在.NET平台上有一个叫做的这是在寻找帮助那些美国做的多线程组件非常有前途的国际象棋 - 包括无锁

。

我没有用它，数额巨大，脑海。

它的工作原理（原油解释）在最紧密的方式实际上迫使你的虫子到野外明确交织线程。报告还分析了代码，以查找常见的错误和糟糕的模式 - 类似于代码分析

在过去，我还内置有问题的代码的特殊版本（通过＃如果块等）的添加额外的状态跟踪信息;计数，版本等，我可以然后浸渍到一个单元测试中。

但问题是，它需要更多的时间来写你的代码，你不能随时添加这种东西不改变这种已经存在的代码的底层结构。

Answer 5

如果你想真正验证无锁码（而不是详尽测试一个小实例），你可以使用VCC（ http://vcc.codeplex.com ），并发C代码演绎验证它已被用来验证一些有趣的无锁的算法（使用危险指针例如无锁列表和可调整大小的散列表，乐观事务多版本处理，MMU虚拟化，各种同步原语，等等）。它模块化验证，并已被用于验证的工业代码非平凡块（约20KLOC最多）。

请注意，然而，VCC是验证者，而不是bug狩猎工具;你将不得不做你的代码进行实质性的注释得到它来验证，和学习曲线可以有点陡峭。还需要注意的是它假定顺序一致性（如大多数工具）。

顺便说一句，同行评审不是验证并发算法（或甚至连续的一个）的好方法。有著名的人在重要期刊上发表并发算法的悠久历史，只有有虫子年后发现的。