Spin is indeed excellent, but also consider Relacy Race Detector by Dmitriy V'jukov. It is purpose-built for verifying concurrent algorithms including non-blocking (wait-/lock-free) algorithms. It's open source and liberally licensed.
Relacy provides POSIX and Windows synchronization primitives (mutexes, condition variables, semaphores, CriticalSections, win32 events, Interlocked*, etc), so your actual C++ implementation can be fed to Relacy for verification. No need to develop a separate model of your algorithm as with Promela and Spin.
Relacy provides C++0x std::atomic (explicit memory ordering for the win!) so you can use pre-processor #defines to select between Relacy's implementation and your own platform specific atomic implementation (tbb::atomic, boost::atomic, etc).
Scheduling is controllable: random, context-bound, and full search (all possible interleavings) available.
Here's an example Relacy program. A few things to note:
- The
$ is a Relacy macro that records execution information.
rl::var<T> flags "normal" (non-atomic) variables that also need to be considered as part of the verification.
The code:
#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>();
}
Compile with your normal compiler (Relacy is header-only) and run the executable:
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)
Recent versions of Relacy also provide Java and CLI memory models if you're into that sort of thing.
