[ANN] Верификатор алгоритмов синхронизации
От: remark Россия http://www.1024cores.net/
Дата: 19.08.08 22:10
Оценка: 491 (33) +1
Хочу анонсировать инструмент, который я разработал. Инструмент называется Relacy Race Detector. Это — верификатор алгоритмов синхронизации для расслабленных моделей памяти (в особенности C++0x). Инструмент предназначен для тестирования как традиционных mutex-based алгоритмов (основанных на mutex, condition_variable, semaphore, event), так и lock-free алгоритмов (основанных на С++0х std::atomic<> и std::atomic_thread_fence), а так же для смешанных алгоритмов. Relacy точно моделирует расслабленную ISO C++0x модель памяти (relaxed, acquire, release, acq_rel, seq_cst атомарные операции и барьеры памяти), но может так же использовться и для верификации алгоритмов для других моделей памяти (x86, PPC, Java, CLI).

Физически инструмент представляет из себя С++ header-only библиотеку для юнит-тестирования многопоточного кода. Вначале Вы описываете юнит-тест (т.е. код выполняемый разными потоками). Потом, опционально, размещаете локальные ассерты, описываете глобальные инварианты, описываете код, выполняемый до и после основных потоков. Далее запускаете юнит-тест на исполнение (симуляцию). Relacy точно моделирует выполнение различных интерливингов (interleaving) потоков на расслабленной модели памяти, и одновременно проводит исчерпывающий анализ на предмет следующих типов ошибок: гонки (data race, type-1 и type-2 согласно С++0х), обращения к освобожденной памяти, двойные освобождения памяти, утечки памяти, утечки ресурсов, доступы к неинициализированным переменным, тупики (deadlock), активные тупики (livelock), некорректное использование API (рекурсия на нерекурсивном мьютексе, попытка изменить разделяемый доступ к мьютексу на эксклюзивный и т.д.), а так же нарушения пользовательских ассертов и инвариантов. Если тест проваливается Relacy выводит подробную историю выполнения, которая ведёт к ошибке.

Ещё некоторые моменты.
У инструмента отсутствуют ложные срабатывания (false positive), т.е. любая обнаруженная ошибка есть нарушение либо C++0x, либо POSIX, либо WinAPI.
Есть возможность использовать один из трёх планировщиков (scheduler). Random планировщик исследует заданное кол-во случайных интерливингов потоков, хорошо подходит для первоначального тестирования. Full search планировщик систематически исследует пространство состояний программы, предназначен для финального тестирования, время работы может быть очень велико. Context bound планировщик систематически исследует интересное подмножество состояний программы, даёт хороший компромисс между временем работы и степенью покрытия. Full search и Context bound планировщики являются справедливыми (fair), т.е. могут верифицировать формально не завершающиеся (non-terminating) алгоритмы.
Значительное кол-во ошибок детектируется автоматически, без необходимости указания каких-либо ассёртов или инвариантов.
Моделируются такие детали как ложные провалы (spurious failure) операции compare_exchange, ложные провалы операции try_lock для std::mutex, ложные пробуждения (spurious wake-ups) на std::condition_variable (и pthread_cond) и т.д. В истории выполнения выводятся такие детали как возникновение ABA-проблемы.
С некоторыми усилиями возможно тестирование Java и CLI алгоритмов.

Помимо своего прямого назначения (тестирования алгоритмов), инструмент может так же применяться для ознакомления/изучения расслабленной модели памяти и библиотеки атомарных операция С++0х, т.к. может опровергать или подтверждать какие-либо гипотезы относительно работоспособности того или иного кода, а так же указывать на конкретную причину неработоспособности.

В отдельных сообщениях приведу несколько примеров использования.

Поддерживаемые платформы. MSVC 7/8/9, Windows 2k (32bit) и выше. gcc 3.4 и выше, Linux (32bit).

Relacy Race Detector может свободно использоваться для (1) разработки некоммерческого программного обеспечения с открытым исходным кодом, (2) научных работ с публикуемыми, не патентуемыми результатами, (3) образовательных целей, (4) частного некоммерческого использования. По остальным случаям, пожалуйста, обращайтесь лично.

Скачать исходный код можно здесь (содержит ряд примеров):
http://groups.google.ru/group/relacy/files

Ещё некоторая информация (краткое руководство, примеры и т.д.):
http://groups.google.ru/group/relacy/web

Готов ответить на любые вопросы, связанные с инструментом, в этом топике или здесь:
http://groups.google.ru/group/relacy/topics

Буду рад услышать любые отзывы, замечания и предложения.

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re: lock-free пример
От: remark Россия http://www.1024cores.net/
Дата: 19.08.08 22:25
Оценка:
Небольшой пример теста для 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

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re: lock-based пример
От: remark Россия http://www.1024cores.net/
Дата: 19.08.08 23:57
Оценка:
Небольшой пример некой гипотетической бизнес-логики, отвечающей за хранение списка лицевых счетов, и осуществляющей переводы сумм с одного л/с на другой. Пример записан сразу в виде, пригодном для тестирования Relacy, но я думаю, что не составит труда представить, как код выглядел с использованием pthread API.
Так же в коде сразу присутствуют исправления допущенных ошибок (закомментированы), дабы впоследствие не сбивались номера строк.

1:#include "stdafx.h"
2:#include "../../relacy/relacy_std.hpp"
3:
4:class business_logic
5:{
6:public:
7:    typedef unsigned account_id_t;
8:    typedef double balance_t;
9:
10:    business_logic()
11:    {
12:        rl::pthread_rwlock_init(&accounts_guard, 0, $);
13:    }
14:
15:    ~business_logic()
16:    {
17:        rl::pthread_rwlock_destroy(&accounts_guard, $);
18:    }
19:
20:    bool add_account(account_id_t acc_id, balance_t balance)
21:    {
22:        rl::pthread_rwlock_wrlock(&accounts_guard, $);
23:        if (accounts.find(acc_id) != accounts.end())
24:        {
25:            rl::pthread_rwlock_unlock(&accounts_guard, $);
26:            return false;
27:        }
28:        accounts[acc_id].balance = balance;
29:        rl::pthread_rwlock_unlock(&accounts_guard, $);
30:        return true;
31:    }
32:
33:    bool transfer_balance(account_id_t acc_id1, account_id_t acc_id2, balance_t amount)
34:    {
35:        //if (acc_id1 == acc_id2)
36:        //    return true;
37:        rl::pthread_rwlock_rdlock(&accounts_guard, $);
38:        if (accounts.find(acc_id1) == accounts.end()
39:            || accounts.find(acc_id2) == accounts.end())
40:        {
41:            rl::pthread_rwlock_unlock(&accounts_guard, $);
42:            return false;
43:        }
44:        account_info& acc1 = accounts[acc_id1];
45:        account_info& acc2 = accounts[acc_id2];
46:        //if (acc_id1 > acc_id2)
47:        {
48:            rl::pthread_mutex_lock(&acc1.mtx, $);
49:            rl::pthread_mutex_lock(&acc2.mtx, $);
50:        }
51:        //else
52:        //{
53:        //    rl::pthread_mutex_lock(&acc2.mtx, $);
54:        //    rl::pthread_mutex_lock(&acc1.mtx, $);
55:        //}
56:        rl::pthread_rwlock_unlock(&accounts_guard, $);
57:
58:        acc1.balance -= amount;
59:        acc2.balance += amount;
60:
61:        rl::pthread_mutex_unlock(&acc1.mtx, $);
62:        rl::pthread_mutex_unlock(&acc2.mtx, $);
63:        return true;
64:    }
65:
66:private:
67:    struct account_info
68:    {
69:        balance_t balance;
70:        rl::pthread_mutex_t mtx;
71:
72:        account_info()
73:            : balance()
74:        {
75:            rl::pthread_mutex_init(&mtx, 0, $);
76:        }
77:
78:        account_info(account_info const& acc)
79:            : balance(acc.balance)
80:        {
81:            rl::pthread_mutex_init(&mtx, 0, $);
82:        }
83:
84:        ~account_info()
85:        {
86:            rl::pthread_mutex_destroy(&mtx, $);
87:        }
88:    };
89:
90:    typedef std::map<account_id_t, account_info> account_map_t;
91:    account_map_t accounts;
92:    rl::pthread_rwlock_t accounts_guard;
93:};
94:
95:struct business_logic_test : rl::test_suite<business_logic_test, 2>
96:{
97:    business_logic bl;
98:
99:    static size_t const account_count = 4;
100:
101:    void before()
102:    {
103:        for (size_t i = 0; i != account_count; ++i)
104:        {
105:            bool rv = bl.add_account(i, i * 10.0);
106:            RL_ASSERT(rv);
107:        }
108:    }
109:
110:    void thread(unsigned /*index*/)
111:    {
112:        business_logic::account_id_t acc1 = rl::rand(account_count);
113:        business_logic::account_id_t acc2 = rl::rand(account_count);
114:        bool rv = bl.transfer_balance(acc1, acc2, 1.0);
115:        RL_ASSERT(rv);
116:    }
117:};
118:
119:int main()
120:{    
121:    rl::simulate<business_logic_test>();
122:}
123:


При запуске теста Relacy детектирует рекурсивный захват нерекурсивного мьютекса. Из анализа истории выполнения видно, что рекурсивный захват происходит в строчках 48 и 49, т.е. когда номера л/с совпадают.

struct business_logic_test
RECURSION ON NON-RECURSIVE MUTEX
iteration: 3

execution history:
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [0] 1: [CTOR BEGIN]
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [1] 1: [CTOR END]
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [2] 1: [BEFORE BEGIN]
..\peterson.cpp(22) : [3] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [4] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [5] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [6] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [7] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [8] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [9] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [10] 1: <00358008> mutex: exclusive unlock
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [11] 1: [BEFORE END]
..\peterson.cpp(37) : [12] 0: <00358008> mutex: shared lock
..\peterson.cpp(37) : [13] 1: <00358008> mutex: shared lock
..\peterson.cpp(48) : [14] 0: <00357E88> mutex: exclusive lock
..\peterson.cpp(49) : [15] 0: <00357F48> mutex: exclusive lock
..\peterson.cpp(56) : [16] 0: <00358008> mutex: shared unlock
..\peterson.cpp(48) : [17] 1: <00357F08> mutex: exclusive lock
..\peterson.cpp(49) : [18] 1: <00357F08> mutex: recursive exclusive lock
..\peterson.cpp(49) : [19] 1: RECURSION ON NON-RECURSIVE MUTEX

thread 0:
..\peterson.cpp(37) : [12] 0: <00358008> mutex: shared lock
..\peterson.cpp(48) : [14] 0: <00357E88> mutex: exclusive lock
..\peterson.cpp(49) : [15] 0: <00357F48> mutex: exclusive lock
..\peterson.cpp(56) : [16] 0: <00358008> mutex: shared unlock

thread 1:
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [0] 1: [CTOR BEGIN]
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [1] 1: [CTOR END]
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [2] 1: [BEFORE BEGIN]
..\peterson.cpp(22) : [3] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [4] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [5] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [6] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [7] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [8] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [9] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [10] 1: <00358008> mutex: exclusive unlock
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [11] 1: [BEFORE END]
..\peterson.cpp(37) : [13] 1: <00358008> mutex: shared lock
..\peterson.cpp(48) : [17] 1: <00357F08> mutex: exclusive lock
..\peterson.cpp(49) : [18] 1: <00357F08> mutex: recursive exclusive lock
..\peterson.cpp(49) : [19] 1: RECURSION ON NON-RECURSIVE MUTEX



Хорошо, раскомментируем строчки:
35:        if (acc_id1 == acc_id2)
36:            return true;


Теперь Relacy выводит следующее. Из истории выполнения видно, что происходит дедлок, т.к. первый поток вначале захватывает мьютекс 00357E88, и потом пытается захватить мьютекс 00357EC8; а второй поток вначале захватывает мьютекс 00357EC8, а потом пытается захватить мьютекс 00357E88.

struct business_logic_test
DEADLOCK (deadlock detected)
iteration: 135

execution history:
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [0] 1: [CTOR BEGIN]
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [1] 1: [CTOR END]
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [2] 1: [BEFORE BEGIN]
..\peterson.cpp(22) : [3] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [4] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [5] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [6] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [7] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [8] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [9] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [10] 1: <00358008> mutex: exclusive unlock
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [11] 1: [BEFORE END]
..\peterson.cpp(37) : [12] 1: <00358008> mutex: shared lock
..\peterson.cpp(37) : [13] 0: <00358008> mutex: shared lock
..\peterson.cpp(48) : [14] 1: <00357EC8> mutex: exclusive lock
..\peterson.cpp(48) : [15] 0: <00357E88> mutex: exclusive lock
..\peterson.cpp(49) : [16] 1: <00357E88> mutex: blocking
..\peterson.cpp(49) : [17] 1: blocking current thread
..\peterson.cpp(49) : [18] 0: <00357EC8> mutex: blocking
..\peterson.cpp(49) : [19] 0: blocking current thread
..\peterson.cpp(49) : [20] 0: DEADLOCK (deadlock detected)

thread 0:
..\peterson.cpp(37) : [13] 0: <00358008> mutex: shared lock
..\peterson.cpp(48) : [15] 0: <00357E88> mutex: exclusive lock
..\peterson.cpp(49) : [18] 0: <00357EC8> mutex: blocking
..\peterson.cpp(49) : [19] 0: blocking current thread
..\peterson.cpp(49) : [20] 0: DEADLOCK (deadlock detected)

thread 1:
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [0] 1: [CTOR BEGIN]
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [1] 1: [CTOR END]
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [2] 1: [BEFORE BEGIN]
..\peterson.cpp(22) : [3] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [4] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [5] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [6] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [7] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [8] 1: <00358008> mutex: exclusive unlock
..\peterson.cpp(22) : [9] 1: <00358008> mutex: exclusive lock
..\peterson.cpp(29) : [10] 1: <00358008> mutex: exclusive unlock
c:\root\relacy_1_0\rrd\relacy\context.hpp(385) : [11] 1: [BEFORE END]
..\peterson.cpp(37) : [12] 1: <00358008> mutex: shared lock
..\peterson.cpp(48) : [14] 1: <00357EC8> mutex: exclusive lock
..\peterson.cpp(49) : [16] 1: <00357E88> mutex: blocking
..\peterson.cpp(49) : [17] 1: blocking current thread



Хорошо, раскомментируем строчки, которые отвечают за правильный захват мьютексов:
46:        if (acc_id1 > acc_id2)
47:        {
48:            rl::pthread_mutex_lock(&acc1.mtx, $);
49:            rl::pthread_mutex_lock(&acc2.mtx, $);
50:        }
51:        else
52:        {
53:            rl::pthread_mutex_lock(&acc2.mtx, $);
54:            rl::pthread_mutex_lock(&acc1.mtx, $);
55:        }


Запускаем — тест успешно пройден!

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re: ещё несколько примеров
От: remark Россия http://www.1024cores.net/
Дата: 20.08.08 00:05
Оценка:
Здесь пример верификации самопального condition variable на основе примитивов Win API — semaphore и event. Relacy с легкостью детектировала тонкую ошибку, связанную с семантикой пробуждения на condition variable, которая может приводить к deadlock'ам в программе, и о которой автор ничего не подозревал, использовал алгоритм значительное время, и был уверен, что он полностью корректный:
http://groups.google.ru/group/comp.programming.threads/msg/30c2ec41c4d498a2

Здесь пример верификации блокирующей single-producer/single-consumer очереди сообщений. Relacy детектирует ошибку, которая может приводить к безвременному засыпанию consumer'а:
http://groups.google.ru/group/comp.programming.threads/msg/71eae0808af7e0ed

Здесь пример multi-producer/multi-consumer lock-free stack:
http://groups.google.ru/group/relacy/web/smr-example

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re: [ANN] Верификатор алгоритмов синхронизации
От: Pavel Dvorkin Россия  
Дата: 20.08.08 05:41
Оценка:
Здравствуйте, remark, Вы писали:

R>Хочу анонсировать инструмент, который я разработал. Инструмент называется Relacy Race Detector. Это — верификатор алгоритмов синхронизации для расслабленных моделей памяти (в особенности C++0x). Инструмент предназначен для тестирования как традиционных mutex-based алгоритмов (основанных на mutex, condition_variable, semaphore, event)


Поддерживается ли проверка на критических секциях ?
With best regards
Pavel Dvorkin
Re: [ANN] Верификатор алгоритмов синхронизации
От: Кодт Россия  
Дата: 20.08.08 07:10
Оценка:
Здравствуйте, remark, Вы писали:

R>Хочу анонсировать инструмент, который я разработал. Инструмент называется Relacy Race Detector. Это — верификатор алгоритмов синхронизации для расслабленных моделей памяти (в особенности C++0x).


Статью для журнала не хочешь написать?
Перекуём баги на фичи!
Re[2]: [ANN] Верификатор алгоритмов синхронизации
От: remark Россия http://www.1024cores.net/
Дата: 20.08.08 07:47
Оценка:
Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Здравствуйте, remark, Вы писали:


R>>Хочу анонсировать инструмент, который я разработал. Инструмент называется Relacy Race Detector. Это — верификатор алгоритмов синхронизации для расслабленных моделей памяти (в особенности C++0x). Инструмент предназначен для тестирования как традиционных mutex-based алгоритмов (основанных на mutex, condition_variable, semaphore, event)


PD>Поддерживается ли проверка на критических секциях ?


Да, вот пример, который использует pthread_mutex и pthread_rwlock:
http://gzip.rsdn.ru/forum/message/3068695.1.aspx
Автор: remark
Дата: 20.08.08

Имеются аналогичные обёртки и для InitializeCriticalSection.

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re: [ANN] Верификатор алгоритмов синхронизации
От: Alexander G Украина  
Дата: 20.08.08 08:24
Оценка:
Здравствуйте, remark,

Так нельзя ?

include <relacy/relacy_std.hpp>

// template parameter '2' is number of threads
struct race_test : rl::test_suite<race_test, 2>
{
  rl::var<volatile long> i; // или rl::atomic ?

  // executed in single thread before main thread function
  void before()
  {
    i($) = 0;
  }

  // main thread function
  void thread(unsigned thread_index)
  {
    ::InterlockedIncrement(&(i($)));
  }

  // 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>();
}
Русский военный корабль идёт ко дну!
Re[2]: [ANN] Верификатор алгоритмов синхронизации
От: remark Россия http://www.1024cores.net/
Дата: 20.08.08 08:32
Оценка:
Здравствуйте, Alexander G, Вы писали:

AG> rl::var<volatile long> i; // или rl::atomic ?

AG> ::InterlockedIncrement(&(i($)));


Нет, так нельзя. Оно не будет работать, как предполагается.
Атомарные операции производятся с помощью методов класса std::atomic<>:

std::atomic<int> x;
x($).fetch_add(1);
// или просто
x($) += 1;



Хотя в принципе в будущем я собираюсь сделать для C# обёртки вида:
rl::cli_var<int> x;
Interlocked.Increment(x, $);


Для WinAPI InterlockedXXX пока сильной необходимости делать обёртки не было.

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re[3]: [ANN] Верификатор алгоритмов синхронизации
От: Pavel Dvorkin Россия  
Дата: 20.08.08 08:34
Оценка:
Здравствуйте, remark, Вы писали:

R>Да, вот пример, который использует pthread_mutex и pthread_rwlock:

R>http://gzip.rsdn.ru/forum/message/3068695.1.aspx
Автор: remark
Дата: 20.08.08

R>Имеются аналогичные обёртки и для InitializeCriticalSection.

Я бы с удовольствием попробовал, как раз имею дело с таким проектом. Проблема в одном — проект на чистом С, да еще с прямым подключением MYSQL, а там такая либа, что хоть плачь Если будет время, попытаюсь собрать.
With best regards
Pavel Dvorkin
Re[3]: [ANN] Верификатор алгоритмов синхронизации
От: Alexander G Украина  
Дата: 20.08.08 08:48
Оценка:
Здравствуйте, remark, Вы писали:

R>Нет, так нельзя. Оно не будет работать, как предполагается.

R>Атомарные операции производятся с помощью методов класса std::atomic<>:

Это класс С++0х, который не может быть сейчас реализован на InterlockedXxx даже для LONG ?

R>Для WinAPI InterlockedXXX пока сильной необходимости делать обёртки не было.


Другие средства WinAPI, вроде InterlockedPushEntrySList, EnterCriticalSection и WaitForMultipleObjects тоже не нужны ?

Что произойдёт при дедлоке или ливлоке, зависание или вывод сообщения об ошибке ?
Русский военный корабль идёт ко дну!
Re[4]: [ANN] Верификатор алгоритмов синхронизации
От: remark Россия http://www.1024cores.net/
Дата: 20.08.08 08:50
Оценка:
Здравствуйте, Pavel Dvorkin, Вы писали:

R>>Да, вот пример, который использует pthread_mutex и pthread_rwlock:

R>>http://gzip.rsdn.ru/forum/message/3068695.1.aspx
Автор: remark
Дата: 20.08.08

R>>Имеются аналогичные обёртки и для InitializeCriticalSection.

PD>Я бы с удовольствием попробовал, как раз имею дело с таким проектом. Проблема в одном — проект на чистом С, да еще с прямым подключением MYSQL, а там такая либа, что хоть плачь Если будет время, попытаюсь собрать.


Тут есть 2 момента.
Первый, тестируемый алгоритм можно переписать для тестирования. Т.е. ничего не мешает иметь проект на С, и несколько юнит-тестов отдельным проектом на С++. Я даже применял Relacy для тестирования алгоритмов, изначально написанных на C#. Т.е. уверенность в работоспособности сложного и критичного алгоритма синхронизации может стоить некоторой дополнительной работы.
Второй, с помощью тонкой прослойки из макросов скорее всего можно будет тестировать и сам продакшн-код, даже если он на С. Примерно как-то так:
#ifndef RL_TEST
#  define MY_VOLATILE_VAR(T) T volatile
#  define MY_INTERLOCKED_INC(x) InterlockedIncrement(&x)
#else
#  define MY_VOLATILE_VAR(T) rl::atomic<T>
#  define MY_INTERLOCKED_INC(x) (x($).fetch_add(1) + 1)
#endif

Это так же снимет вопрос с необходимостью везде писать "($)".

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re[4]: [ANN] Верификатор алгоритмов синхронизации
От: remark Россия http://www.1024cores.net/
Дата: 20.08.08 08:59
Оценка:
Здравствуйте, Alexander G, Вы писали:

R>>Нет, так нельзя. Оно не будет работать, как предполагается.

R>>Атомарные операции производятся с помощью методов класса std::atomic<>:

AG>Это класс С++0х, который не может быть сейчас реализован на InterlockedXxx даже для LONG ?



Тут дело не в реализации через InterlockedXxx. Фактически Relacy не выполняет код, она симулирует выполнение. Т.е. объект std::atomic<>, помимо текущего значения, содержит значительный объем вспомогательной информации, которая включает ряд предыдущих значений, ряд векторных часов, ряд флагов и т.д. Соотв. методы std::atomic<> не просто меняют значение, они производят значительный объем расчетов и проверок, связанных с изменением или чтением переменной.


R>>Для WinAPI InterlockedXXX пока сильной необходимости делать обёртки не было.


AG>Другие средства WinAPI, вроде InterlockedPushEntrySList, EnterCriticalSection и WaitForMultipleObjects тоже не нужны ?


На данный момент из Win API поддерживаются API, связанные с CriticalSection, SRWLock, Semaphore, Event, ConditionVariable, WaitForSingleObject.
InterlockedPushEntrySList, WaitForMultipleObjects, SignalObjectAndWait пока не поддерживаются. Всё зависит от востребованности и заинтересованности.


AG>Что произойдёт при дедлоке или ливлоке, зависание или вывод сообщения об ошибке ?


Вывод сообщения и детальной истории выполнения, которая привела к дедлоку или ливлоку.
Например смотри здесь:
http://gzip.rsdn.ru/forum/message/3068695.1.aspx
Автор: remark
Дата: 20.08.08

Там есть пример детектирования дедлока.

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re: [ANN] Верификатор алгоритмов синхронизации
От: jazzer Россия Skype: enerjazzer
Дата: 20.08.08 10:53
Оценка:
Здравствуйте, remark, Вы писали:

Эх, я б потестил, да весь мой софт коммерческий, нельзя по твоей лицензии
jazzer (Skype: enerjazzer) Ночная тема для RSDN
Автор: jazzer
Дата: 26.11.09

You will always get what you always got
  If you always do  what you always did
Re[2]: [ANN] Верификатор алгоритмов синхронизации
От: eao197 Беларусь http://eao197.blogspot.com
Дата: 20.08.08 11:07
Оценка:
Здравствуйте, jazzer, Вы писали:

J>Эх, я б потестил, да весь мой софт коммерческий, нельзя по твоей лицензии


Для коммерческого софта у Димы своя лицензия. Так что обращайся напрямую к нему -- вопрос, я думаю, решится положительно.


SObjectizer: <микро>Агентно-ориентированное программирование на C++.
Re[2]: Лицензия
От: Roman Odaisky Украина  
Дата: 20.08.08 11:28
Оценка: 16 (1)
Здравствуйте, jazzer, Вы писали:

J>Эх, я б потестил, да весь мой софт коммерческий, нельзя по твоей лицензии :crash:


Ну проблем-то. Напиши сам себе библиотеку на условиях лицензии MIT, проверь ее детектором, благо условия RRD это позволяют, потом включи ее в свой коммерческий продукт, благо условия MIT это позволяют.

Вообще, лицензия крайне странная. Во-первых, прав ли я в том, что лицензия не может регулировать, для чего используется продукт, а только условия распространения производных работ?

Во-вторых, хитрый разработчик пожадничает, загрузит верификатор и применит по назначению, исправит найденные ошибки и удалит верификатор, и автору ничего не достанется :-)

Вывод: лицензию надо сильно переделать, сразу видно, что DVINAL. И где-нибудь большими буквами написать: «Проверю ваш проект на отсутствие гонок и пр.! Недорого, каких-то 50 000 €!»
До последнего не верил в пирамиду Лебедева.
Re[3]: [ANN] Верификатор алгоритмов синхронизации
От: remark Россия http://www.1024cores.net/
Дата: 20.08.08 11:37
Оценка:
Здравствуйте, eao197, Вы писали:

J>>Эх, я б потестил, да весь мой софт коммерческий, нельзя по твоей лицензии


E>Для коммерческого софта у Димы своя лицензия. Так что обращайся напрямую к нему -- вопрос, я думаю, решится положительно.


Совершенно верно.
Для начала могу дать trail лицензию для ознакомления.



1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re: [ANN] Верификатор алгоритмов синхронизации
От: Аноним  
Дата: 20.08.08 11:46
Оценка:
Здравствуйте, remark, Вы писали:

R>Буду рад услышать любые отзывы, замечания и предложения.

Андронный коллайдер?
Re[3]: Лицензия
От: remark Россия http://www.1024cores.net/
Дата: 20.08.08 11:51
Оценка:
Здравствуйте, Roman Odaisky, Вы писали:

J>>Эх, я б потестил, да весь мой софт коммерческий, нельзя по твоей лицензии


RO>Ну проблем-то. Напиши сам себе библиотеку на условиях лицензии MIT, проверь ее детектором, благо условия RRD это позволяют, потом включи ее в свой коммерческий продукт, благо условия MIT это позволяют.



А как формально/юридически отличать такую ситуацию от следующей? Человек честно использует RRD для разработки опен-сорц библиотеки. А через какое-то время использует накопленный опыт и проверенные алгоритмы в своих коммерческих разработках. Тут вроде как всё чисто, никакого жульничества.


RO>Вообще, лицензия крайне странная. Во-первых, прав ли я в том, что лицензия не может регулировать, для чего используется продукт, а только условия распространения производных работ?



В смысле? Что вообще лицензии не могут этого регулировать? Или что эта конкретная лицензия не регулирует?


RO>Во-вторых, хитрый разработчик пожадничает, загрузит верификатор и применит по назначению, исправит найденные ошибки и удалит верификатор, и автору ничего не достанется



С хитрым (особенно русским) разработчиком вообще сложно совладать. Особенно если скачать можно свободно. И нет никакой возможности защитить продукт, т.к. это просто библиотека с исходными кодами.


RO>Вывод: лицензию надо сильно переделать, сразу видно, что DVINAL. И где-нибудь большими буквами написать: «Проверю ваш проект на отсутствие гонок и пр.! Недорого, каких-то 50 000 €!»



Честно скажу, я в этой области не особо силён. Поэтому с радостью выслушаю любые предложения по улучшению лицензии. Был бы очень признателен.

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Re[2]: [ANN] Верификатор алгоритмов синхронизации
От: remark Россия http://www.1024cores.net/
Дата: 20.08.08 11:54
Оценка:
Здравствуйте, Аноним, Вы писали:

R>>Буду рад услышать любые отзывы, замечания и предложения.


А>Андронный коллайдер?


Хм... Это замечание или предложение?

1024cores &mdash; all about multithreading, multicore, concurrency, parallelism, lock-free algorithms
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.