Spin действительно превосходен, но также рассмотрим 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, если вы в такой ситуации.