如何验证无锁算法？

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

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

1> j_random_hac..：

---

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

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

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

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

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

---

旋转效果很好.但是请注意,虽然学习曲线比使用PVS或Isabelle(定理证明)要陡峭得多,但它仍然相当棘手.要真正使用SPIN,您通常需要减少状态空间; 这意味着添加限制验证的假设,您还需要知道首先要查找的内容.尽管如此,旋转是一个非常坚固且相对简单的工具,只要你不期待任何魔法.

---

哦,不要忘记记忆障碍; spin(AFAIK)假设所有写入都是原子的并且立即可见,您需要单独推断内存屏障(这对于低锁或无锁技术通常是必需的)

2> sstock..：

---

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 标记"正常"(非原子)变量,也需要被视为验证的一部分.

代码:

#include 

// template parameter '2' is number of threads
struct race_test : rl::test_suite
{
    std::atomic a;
    rl::var 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();
}

使用普通编译器进行编译(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内存模型,如果你遇到这种情况的话.