如何验证无锁算法？

Question

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

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

Answer 1

你一定要试试Spin模型检查器.

您使用名为Promela的简单C语言编写类似程序的模型,Spin内部转换为状态机.模型可以包含多个并行进程.

然后Spin会检查每个进程的指令的每个可能的交错,无论你想要测试什么条件 - 通常,没有竞争条件,没有死锁等.大多数这些测试都可以使用assert()语句轻松编写.如果有任何可能的执行序列违反断言,则打印出序列,否则您将获得"全清除".

(实际上,它使用了更加高级和更快的算法来实现这一点,但这就是效果.默认情况下,会检查所有可访问的程序状态.)

这是一个令人难以置信的计划,它赢得了2001年ACM系统软件奖(其他获奖者包括Unix,Postscript,Apache,TeX).我开始非常快速地使用它,并且在几天内能够实现MPI功能的模型MPI_Isend()和MPI_Irecv()Promela.Spin 在一段并行代码中发现了一些棘手的竞争条件,我将其转换为Promela进行测试.

Answer 2

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仅限标头)并运行可执行文件:

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内存模型,如果你遇到这种情况的话.