26

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

注意：如果你知道一种方法来证明一个点（例如只证明它对 ABA 问题是安全的）或者我没有提到的问题，那么无论如何都要发布解决方案。在最坏的情况下，每种方法都可以轮流进行，以充分验证它。

4

5 回答 5

21

您绝对应该尝试使用Spin 模型检查器。

你用一种叫做 Promela 的简单的类 C 语言编写类似程序的模型，Spin 在内部将其翻译成状态机。一个模型可以包含多个并行进程。

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

（嗯，实际上它使用了一种更漂亮、更快的算法来完成这个，但这就是效果。默认情况下，所有可达的程序状态都会被检查。）

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

于 2010-01-15T14:05:19.673 回答
8

Spin 确实很棒，但也可以考虑Dmitriy V'jukov 的Relacy Race Detector。它专门用于验证并发算法，包括非阻塞（等待/无锁）算法。它是开源的并且获得了自由许可。

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

Relacy 提供了 C++0x std::atomic（显式内存排序），因此您可以使用预处理器#defines在 Relacy 的实现和您自己的平台特定原子实现（tbb::atomic、boost::atomic等）之间进行选择。

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

这是一个 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 仅是头文件）并运行可执行文件：

结构race_test
数据竞赛
迭代次数：8

执行历史：
[0] 0: atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0: store, value=0, 在race_test::before, test.cpp(15)
[2] 0: store, value=1, 在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：原子负载，value=1，order=relaxed，在race_test::thread，test.cpp(28)
[5] 1: store, value=0, 在race_test::thread, test.cpp(29)
[6] 1: 在race_test::thread, test.cpp(29)中检测到数据竞争

线程 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, 在race_test::before, test.cpp(15)
[2] 0: store, value=1, 在race_test::thread, test.cpp(23)
[3] 0: atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)

线程1：
[4] 1：原子负载，value=1，order=relaxed，在race_test::thread，test.cpp(28)
[5] 1: store, value=0, 在race_test::thread, test.cpp(29)
[6] 1: 在race_test::thread, test.cpp(29)中检测到数据竞争

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

于 2010-02-02T11:29:52.873 回答
4

我不知道您使用的是什么平台或语言——但在 .Net 平台上有一个名为Chess的 Microsoft Research 项目，它看起来很有希望帮助我们这些做多线程组件的人——包括无锁。

请注意，我没有大量使用它。

它的工作原理（粗略的解释）通过以最紧密的方式显式地交错线程来实际迫使你的错误进入野外。它还分析代码以发现常见错误和不良模式 - 类似于代码分析。

过去，我还构建了相关代码的特殊版本（通过#if 块等），添加了额外的状态跟踪信息；然后我可以在单元测试中深入了解计数、版本等。

这样做的问题是编写代码需要更多时间，而且你不能总是在不改变已经存在的代码的底层结构的情况下添加这种东西。

于 2010-01-15T13:46:43.070 回答
4

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

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

于 2010-01-15T13:54:12.380 回答
4

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

但是请注意，VCC 是一个验证器，而不是一个错误搜索工具；您必须对代码进行大量注释才能对其进行验证，并且学习曲线可能有点陡峭。另请注意，它假定顺序一致性（与大多数工具一样）。

顺便说一句，同行评审不是验证并发算法（甚至是顺序算法）的好方法。名人在重要期刊上发表并发算法的历史由来已久，但几年后才发现错误。

于 2013-11-05T09:42:40.673 回答