如何验证无锁算法？

Question

如何验证无锁算法？

algorithmverificationlock-free

28

理论上，至少可以通过暴力破解来验证无锁算法（函数调用的组合只有那么多种）。是否有工具或形式化推理过程可用于实际证明无锁算法的正确性（最好还能检查竞争条件和ABA问题）？

注意：如果您知道一种仅验证一点（例如仅验证其免受ABA问题的影响）或我未提及的问题的方法，则仍然可以发布解决方案。在最坏的情况下，每种方法都可以按顺序执行以完全验证它。

- Grant Peters

1

通过状态转换图正式地实现。 - jldupont

目前硬件不支持进行这样的检查，只有在可以以某种方式同步运行多个CPU指令，从而实现确定性竞争时才能进行这样的检查。当前的硬件无法做到这一点。 - Pop Catalin

1

@Pop：你不需要特殊的硬件来证明一个算法不会锁死。 - jldupont

3

发布算法并让尽可能多的人查看。这并不能证明正确性，但希望第N个眼睛能发现一些你没有考虑到的边角情况。 - Nikolai Fetissov

我同意 - 同行评审是救星！ - Andras Zoltan

@Pop 我认为具有记录-重放功能的虚拟机可以帮助确定性地实现竞态条件。尽管它还没有完全开发出来...但我猜现在它是开源的了... - peeyush

5个回答

8

Spin确实很优秀，但也要考虑Dmitriy V'jukov的Relacy Race Detector。它专门用于验证包括非阻塞(wait-/lock-free)算法在内的并发算法。它是开源的并且授权宽松。

Relacy提供POSIX和Windows同步原语（互斥量、条件变量、信号量、CriticalSection、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: 原子存储，值=0，（先前值=0），顺序=seq_cst，在race_test::before，test.cpp(14)
[1] 0: 存储，值=0，在race_test::before，test.cpp(15)
[2] 0: 存储，值=1，在race_test::thread，test.cpp(23)
[3] 0: 原子存储，值=1，（先前值=0），顺序=relaxed，在race_test::thread，test.cpp(24)
[4] 1: 原子加载，值=1，顺序=relaxed，在race_test::thread，test.cpp(28)
[5] 1: 存储，值=0，在race_test::thread，test.cpp(29)
[6] 1: 检测到数据竞争，在race_test::thread，test.cpp(29)
线程0：
[0] 0: 原子存储，值=0，（先前值=0），顺序=seq_cst，在race_test::before，test.cpp(14)
[1] 0: 存储，值=0，在race_test::before，test.cpp(15)
[2] 0: 存储，值=1，在race_test::thread，test.cpp(23)
[3] 0: 原子存储，值=1，（先前值=0），顺序=relaxed，在race_test::thread，test.cpp(24)
线程1：
[4] 1: 原子加载，值=1，顺序=relaxed，在race_test::thread，test.cpp(28)
[5] 1: 存储，值=0，在race_test::thread，test.cpp(29)
[6] 1: 检测到数据竞争，在race_test::thread，test.cpp(29)

如果您需要Java和CLI内存模型的话，最近版本的Relacy也提供了这些。

- sstock

看起来很不错，我也得试一试。 - Grant Peters

1

看起来非常不错！顺便说一下，它现在已经迁移到http://www.1024cores.net/home/relacy-race-detector。 - j_random_hacker

4

我不知道你使用的平台或语言是什么 - 但在 .Net 平台上有一个名为 Chess 的微软研究项目，它在帮助我们做多线程组件（包括无锁）方面非常有前途。

我没有大量使用过它。

它的工作原理（简单解释）是通过明确地交错线程，以尽可能紧密的方式来强制将错误暴露到外部。它还分析代码以查找常见的错误和不良模式 - 类似于代码分析。

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

问题在于编写代码需要更多的时间，并且您不能总是在不改变已有代码的基础结构的情况下添加此类内容。

- Andras Zoltan

+1，非常有趣，特别是它的非侵入性。但是这条评论：http://channel9.msdn.com/shows/Going+Deep/CHESS-An-Automated-Concurrency-Testing-Tool/?CommentID=448235 表示它（尚）不考虑任意指令之间的抢占。因此，你放置的锁/互斥量等越少，Chess 在查找错误方面做得越差——如果你的多线程代码根本没有锁，Chess 就什么也发现不了。 - j_random_hacker

是的，这是一个雄心勃勃的项目，还有很长的路要走 - 我喜欢当前的最新版本号：v0.1.30626.0。显然，在发布v1.0之前，他们还有很多工作要做！ - Andras Zoltan

1

我发现了这个页面：http://www.projectbentley.com/work/chess/lockfreequeue.php#test1，是由一个一直在玩CHESS（抱歉，忍不住要说！）的人尝试检测无锁错误。他发现将某些东西标记为volatile会使其正确地检测到无锁错误。但这并不意味着它适用于所有无锁内容。但我们可以看到，在这种情况下，您可能需要更改某些变量的声明为“volatile”，并使用#if...#endif进行“测试”构建。 - Andras Zoltan

很好，他们为.NET程序实现了“volatile”“标记”。虽然我不使用.NET，但我认为如果有一种方法可以说服编译器在不到处编写的情况下将所有变量都设为volatile就会很好。 - j_random_hacker

我同意——在 .Net 中，易变性（volatility）是框架设计者不赞成的。我们的交错操作需要对一个对象进行'ref'，会引发编译器警告，因为把'ref'用于易变值被视为靠不住。我希望 .Net 有更低级别的API来进行交错读/写操作和内存屏障（不要让我开始谈SIMD！）——我并不确信我们的交错操作是否会转化为相应的CPU指令，我认为它们利用了Windows的API。 - Andras Zoltan

@Andras：是的，interlocked API 中的 ref/volatile 警告很不幸。上次我研究 .NET interlocked 操作实现时，它们似乎都在内部使用 compare-exchange（顺便说一下，Win32 版本确实编译成了正确的 CPU 指令），这是正确的但对于像 fetch-and-add 这样的操作来说是次优的（可以通过单个硬件指令完成，而无需循环，尽管可能具有潜在的高延迟）。 - Cameron

4

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

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

- Anna

看起来很有趣，但是从浏览Powerpoint来看，似乎两个工具都不能做出任何保证，因为它们只检查调度程序给出的任何指令序列，而不是像Spin和Chess那样检查所有可能的序列。此外，你有这些工具的链接吗？ - j_random_hacker

2

在大学里他们只教你理论，哈哈 :). 不过我找到了原始的锁定集论文：http://www.cs.washington.edu/homes/tom/pubs/eraser.pdf。虽然我不记得在课程中玩过这些工具...嗯... 它们可能只是为了论文目的而进行的大学级别实现。在这种情况下，我认为也许我应该完全删除我的评论。 - Anna

我意识到这将是一个NP问题，这就是为什么我提到了蛮力算法的原因。尽管测试越复杂（操作/输入组合更多），测试所有可能的序列所需的时间就越长，但仍然有可能进行彻底的测试。 - Grant Peters

请不要删除这个有用的回答！ :) - j_random_hacker

3

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

然而，需要注意的是，VCC是一个验证器，而不是漏洞寻找工具；您必须对代码进行大量注释才能使其验证，并且学习曲线可能会有点陡峭。还请注意，它假设顺序一致性（与大多数工具一样）。

顺便说一句，同行评审不是验证并发算法（甚至连顺序算法都不是）的好方法。长期以来，许多著名人士在重要期刊上发布并发算法，只有在几年后才发现了错误。

- user2949652

看起来很有趣，这正是我希望找到的东西（我从来不喜欢同行评审这种东西，因为很容易忽略复杂的问题，或者认为验证一个部分意味着可以假定另一个部分是正确的）。 - Grant Peters

实际上，如果你在无锁并发编程方面很有纪律性，同行评审可以对其产生积极的影响。你必须认真对待对象不变量，并且对于可线性化的数据结构，你必须非常明确地指出操作“似乎”发生的位置。 - user2949652

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- j_random_hacker · Accepted Answer

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

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

接下来Spin会检查每个进程中指令的所有可能交错组合，并根据您想测试的任何条件进行检查，通常是检查是否存在竞争条件或死锁等问题。大多数这样的测试都可以通过使用assert()语句轻松编写。如果存在任何可能违反断言的执行序列，这些序列会被打印出来，否则您将收到“全清”的消息。

（实际上，它使用了更高级和更快速的算法来完成此操作，但这是效果。默认情况下，将检查所有可达的程序状态。）

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