Relacy Race Detector

Relacy Race Detector is a tool for efficient execution of unit-tests for synchronization algorithms written in C++0x.

Every user thread is represented as a fiber (ucontext). Every time only one fiber is running, and special scheduler controls interleaving between fibers.

With random scheduler it just executes numerous amount of various interleavings between threads. With full search scheduler or context-bound scheduler it systematically executes all possible interleavings between threads. While executing particular interleaving it makes exhaustive verification of various aspects of execution (races, accesses to freed memory etc).

If no errors found then verification terminates when particular number of interleavings are verified (for random scheduler), or when all possible interleavings are verified (for full search scheduler). If error is found then tool outputs execution history which leads to error and terminates.

Physically Relacy Race Detector is a header-only library for C++98.

Features

- Relaxed ISO C++0x Memory Model. Relaxed/acquire/release/acq_rel/seq_cst memory operations. The only non-supported feature is memory_order_consume, it's simulated with memory_order_acquire.
- Exhaustive automatic error checking (including ABA detection).
- Full-fledged atomics library (with spurious failures in compare_exchange()).
- Memory fences.
- Arbitrary number of threads.
- Detailed execution history for failed tests.
- No false positives.
- Before/after/invariant functions for test suites.

Detectable Errors

- Race condition (type 1 and type 2, according to ISO C++0x)
- Access to uninitialized variable
- Access to freed memory
- Double free
- Memory leak
- Deadlock
- Livelock
- User assert failed
- User invariant failed

Supported Platforms

MSVC 7/8/9, Windows 2000 and above, 32-bit
GCC 3.4 and above, Linux, 32-bit

Tutorial

1. Add

#include <relacy/relacy_std.hpp>

2. For atomic variables use type std::atomic<T>:

std::atomic<void*> head;

3. For usual non-atomic variables use type rl::var<T>:

rl::var<int> data;

Such vars will be checked for races and included into trace.

4. All accesses to std::atomic<T> and rl::var<T> variables postfix with '($)':

std::atomic<void*> head;

rl::var<int> data;

head($).store(0);

data($) = head($).load();

5. Strictly thread-private variables use can leave as-is:

for (int i = 0; i != 10; ++i)

Such vars will be NOT checked for races NOR included into trace. But they will accelerate verification.

6. Describe test-suite: number of threads, thread function, before/after/invariant functions. See example below.

7. Place asserts:

int x = g($).load();

RL_ASSERT(x > 0);

8. Start verification:

rl::simulate<test_suite_t>();

Complete example

#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>();

}

Output

struct race_test

DATA RACE

iteration: 8

execution history:

[0] 0: <00366538> atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)

[1] 0: <0036655C> store, value=0, in race_test::before, test.cpp(15)

[2] 0: <0036655C> store, value=1, in race_test::thread, test.cpp(23)

[3] 0: <00366538> atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)

[4] 1: <00366538> atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)

[5] 1: <0036655C> store, value=0, in race_test::thread, test.cpp(29)

[6] 1: data race detected, in race_test::thread, test.cpp(29)

thread 0: