Небольшой пример теста для single-producer/single-consumer lock-free очереди сообщений.

1:#include "stdafx.h"
2:#include "../../relacy/relacy_std.hpp"
3:
4:template<typename T>
5:class nonblocking_spsc_queue
6:{
7:public:
8:    nonblocking_spsc_queue()
9:    {
10:        node* n = RL_NEW node ();
11:        head($) = n;
12:        tail($) = n;
13:    }
14:
15:    ~nonblocking_spsc_queue()
16:    {
17:        RL_ASSERT(head($) == tail($));
18:        RL_DELETE((node*)head($));
19:    }
20:
21:    void enqueue(T data)
22:    {
23:        node* n = RL_NEW node (data);
24:        head($)->next($).store(n, std::memory_order_release); 
25:        head($) = n;
26:    }
27:
28:    bool dequeue(T& data)
29:    {
30:        node* t = tail($);
31:        node* n = t->next($).load(std::memory_order_acquire);
32:        if (0 == n)
33:            return false;
34:        data = n->data($);
35:        RL_DELETE(t);
36:        tail($) = n;
37:        return true;
38:    }
39:
40:private:
41:    struct node
42:    {
43:        std::atomic<node*> next;
44:        rl::var<T> data;
45:
46:        node(T data = T())
47:            : next(0)
48:            , data(data)
49:        {}
50:    };
51:
52:    rl::var<node*> head;
53:    rl::var<node*> tail;
54:};
55:
56:struct nonblocking_spsc_queue_test : rl::test_suite<nonblocking_spsc_queue_test, 2>
57:{
58:    nonblocking_spsc_queue<int> q;
59:
60:    void thread(unsigned thread_index)
61:    {
62:        if (0 == thread_index)
63:        {
64:            q.enqueue(11);
65:        }
66:        else
67:        {
68:            int data = 0;
69:            while (false == q.dequeue(data))
70:            {}
71:            RL_ASSERT(11 == data);
72:        }
73:    }
74:};
75:
76:int main()
77:{
78:    rl::simulate<nonblocking_spsc_queue_test>();
79:}
80:

Данный тест проходит успешно.
Теперь попробуем заменить, например, в функции enqueue() строчку:

24:        head($)->next($).store(n, std::memory_order_release);

на:

24:        head($)->next($).store(n, std::memory_order_relaxed);

После запуска измененного теста Relacy выводит (вначале идёт общая история выполнения, далее история выполнения отдельно для каждого потока):

struct nonblocking_spsc_queue_test
DATA RACE (data race detected)
iteration: 1

execution history:
[0] 1: [CTOR BEGIN], in rl::context_impl<struct nonblocking_spsc_queue_test,class rl::random_scheduler<2> >::fiber_proc_impl, context.hpp(385)
[1] 1: memory allocation: addr=00353B28, size=52, in nonblocking_spsc_queue<int>::nonblocking_spsc_queue, spsc_queue.cpp(10)
[2] 1: <003539A0> store, value=00353B28, in nonblocking_spsc_queue<int>::nonblocking_spsc_queue, spsc_queue.cpp(11)
[3] 1: <003539B0> store, value=00353B28, in nonblocking_spsc_queue<int>::nonblocking_spsc_queue, spsc_queue.cpp(12)
[4] 1: [CTOR END], in rl::context_impl<struct nonblocking_spsc_queue_test,class rl::random_scheduler<2> >::fiber_proc_impl, context.hpp(385)
[5] 1: [BEFORE BEGIN], in rl::context_impl<struct nonblocking_spsc_queue_test,class rl::random_scheduler<2> >::fiber_proc_impl, context.hpp(385)
[6] 1: [BEFORE END], in rl::context_impl<struct nonblocking_spsc_queue_test,class rl::random_scheduler<2> >::fiber_proc_impl, context.hpp(385)
[7] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[8] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[9] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[10] 0: memory allocation: addr=0035BD98, size=52, in nonblocking_spsc_queue<int>::enqueue, spsc_queue.cpp(23)
[11] 0: <003539A0> load, value=00353B28, in nonblocking_spsc_queue<int>::enqueue, spsc_queue.cpp(24)
[12] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[13] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[14] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[15] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[16] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[17] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[18] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[19] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[20] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[21] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[22] 0: <00353B28> atomic store, value=0035BD98, (prev value=00000000), order=relaxed, in nonblocking_spsc_queue<int>::enqueue, spsc_queue.cpp(24)
[23] 0: <003539A0> store, value=0035BD98, in nonblocking_spsc_queue<int>::enqueue, spsc_queue.cpp(25)
[24] 1: <00353B28> atomic load, value=00000000 [NOT CURRENT], order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[25] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[26] 1: <00353B28> atomic load, value=0035BD98, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[27] 1: <0035BDBC> load, value=0, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(34)
[28] 1: DATA RACE (data race detected), in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(34)

thread 0:
[10] 0: memory allocation: addr=0035BD98, size=52, in nonblocking_spsc_queue<int>::enqueue, spsc_queue.cpp(23)
[11] 0: <003539A0> load, value=00353B28, in nonblocking_spsc_queue<int>::enqueue, spsc_queue.cpp(24)
[22] 0: <00353B28> atomic store, value=0035BD98, (prev value=00000000), order=relaxed, in nonblocking_spsc_queue<int>::enqueue, spsc_queue.cpp(24)
[23] 0: <003539A0> store, value=0035BD98, in nonblocking_spsc_queue<int>::enqueue, spsc_queue.cpp(25)

thread 1:
[0] 1: [CTOR BEGIN], in rl::context_impl<struct nonblocking_spsc_queue_test,class rl::random_scheduler<2> >::fiber_proc_impl, context.hpp(385)
[1] 1: memory allocation: addr=00353B28, size=52, in nonblocking_spsc_queue<int>::nonblocking_spsc_queue, spsc_queue.cpp(10)
[2] 1: <003539A0> store, value=00353B28, in nonblocking_spsc_queue<int>::nonblocking_spsc_queue, spsc_queue.cpp(11)
[3] 1: <003539B0> store, value=00353B28, in nonblocking_spsc_queue<int>::nonblocking_spsc_queue, spsc_queue.cpp(12)
[4] 1: [CTOR END], in rl::context_impl<struct nonblocking_spsc_queue_test,class rl::random_scheduler<2> >::fiber_proc_impl, context.hpp(385)
[5] 1: [BEFORE BEGIN], in rl::context_impl<struct nonblocking_spsc_queue_test,class rl::random_scheduler<2> >::fiber_proc_impl, context.hpp(385)
[6] 1: [BEFORE END], in rl::context_impl<struct nonblocking_spsc_queue_test,class rl::random_scheduler<2> >::fiber_proc_impl, context.hpp(385)
[7] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[8] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[9] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[12] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[13] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[14] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[15] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[16] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[17] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[18] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[19] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[20] 1: <00353B28> atomic load, value=00000000, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[21] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[24] 1: <00353B28> atomic load, value=00000000 [NOT CURRENT], order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[25] 1: <003539B0> load, value=00353B28, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(30)
[26] 1: <00353B28> atomic load, value=0035BD98, order=acquire, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(31)
[27] 1: <0035BDBC> load, value=0, in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(34)
[28] 1: DATA RACE (data race detected), in nonblocking_spsc_queue<int>::dequeue, spsc_queue.cpp(34)

Т.е. инструмент автоматически детектировал гонку сигналов (data race) в строчке 34, при считывании переменной node::data