topic Checking Against Other Memory Models (x86, PPC, Java, CLI) in Intel® Moderncode for Parallel Architectures

Synchronization Algorithm Verificator for C++0x

Dmitry_Vyukov — Sun, 03 Aug 2008 07:54:57 GMT

I want to announce tool called Relacy Race Detector, which I've developed. It's synchronization algorithm verificator for C++0x's relaxed memory model. The tool is implemented in the form of header-only library for C++03, which can be used for efficient execution of unit-tests for synchronization algorithms. The tool executes unit-test many times under control of special scheduler, on every execution scheduler models different interleaving between threads, at the same time every execution is exhaustively analyzed for data races, accesses to freed memory, failed assertions 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 detailed execution history which leads to error and terminates.

The tool was designed for verification of algorithms like memory management, memory reclamation for lock-free algorithms, multithreaded containers (queues, stacks, maps), mutexes, eventcounts and so on.

My personal subjective feeling to date is that tool is capable of finding extremely subtle algorithmic errors, memory fence placement errors and memory fence type errors within a second. And after error is detected error fixing is relatively trivial, because one has detailed execution history which leads to error.

Main features:

- Relaxed ISO C++0x Memory Model. Relaxed/acquire/release/acq_rel/seq_cst memory operations and fences. 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()).

- Arbitrary number of threads.

- Detailed execution history for failed tests.

- Before/after/invariant functions for test suites.

- No false positives.

Types of detectable errors:

- Race condition (according to ISO C++0x definition)

- Access to uninitialized variable

- Access to freed memory

- Double free

- Memory leak

- Deadlock

- Livelock

- User assert failed

- User invariant failed

You can get some more information (tutorial, examples etc) here:

http://groups.google.com/group/relacy/web

And here is dedicated news group/discussion forum:

http://groups.google.com/group/relacy/topics

If you want to get a copy of the tool, please, contact me via dvyukov@gmail.com.

Any feedback, comments, suggestions are welcome.

Relacy Race Detector is free for open-source, non-commercial development; research with non-patented, published results; educational purposes; home/private usage. Please contact me (dvyukov@gmail.com) about other usages.

--------------------------------------------------------

Here is quick example.

Code of unit-test:

#include

// template parameter '2' is number of threads

struct race_test : rl::test_suite

    std::atomic a;

    rl::var 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)

            // code executed by first thread

            x($) = 1;

            a($).store(1, rl::memory_order_relaxed);

        else

            // code executed by second thread

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

    // start simulation

    rl::simulate();

And here is output of the tool:

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 rac e_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

thread 0:
[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)

thread 1:
[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)

--------------------------------------------------------

Dmitriy V'jukov

Checking Against Other Memory Models (x86, PPC, Java, CLI)

Dmitry_Vyukov — Sun, 03 Aug 2008 12:25:37 GMT

Q: Can I use Relacy Race Detector to check my algo againts other that C++0x memory models (x86, PPC, Java, CLI)?

A Yes, you can. Fortunately, C++0x memory model is very relaxaed, so for the main part it's a "superset" of basically any other memory model. You just have to define "binding" between your target memory model and C++0x memory model.

Let's create such binding, for example, for x86 memory model:
- plain load operation is always "acquire" (i.e. memory_order_acquire)
- plain store operation is always "release" (i.e. memory_order_release)
- atomic RMW operation is always sequentially consistent (i.e. memory_order_seq_cst)
- mfence instruction is std::atomic_thread_fence(memory_order_seq_cst)
That is all. You can create such bindings for other hardware memory models you are interested in (PPC, Itatium, SPARC etc).

And you can define such binding to other abstract memory model, like Java MM. Let's see:
- plain load is "relaxed" (i.e. memory_order_relaxed)
- plain store is "relaxed" (i.e. memory_order_relaxed)
- volatile load is "acquire" (i.e. memory_order_acquire)
- volatile store operation is "release" (i.e. memory_order_release)
- atomic RMW operation is always sequentially consistent (i.e. memory_order_seq_cst)
But here are some caveats. First, you have to emulate work of GC, i.e. put all allocated memory to special list, and free all allocated memory in test_suite::after(). Second, you have to manually emit sequentially consistent memory fence between every volatile store and volatile load. Third, you have to manually initialize all variables to default value (0). Fourth, there is no such thing as data race, so you have to define all variables as std::atomic, this will effectively disable data race detection mechanizm. Well, actually you can use rl::var variables, if you know that there must be no concurrent accesses to variable, this will enable some automatic error detection wrt data races.
Sounds not very cool... So I'm going to add built-in support for Java and CLI. Then user would have to define something like RL_JAVA_MODE/RL_CLI_MODE, and get all those things out-of-the-box. But yes, it still will be C++ library. What do you think?

Dmitriy V'jukov

Relacy v1.1

Dmitry_Vyukov — Fri, 15 Aug 2008 18:31:36 GMT

I want to announce release 1.1 of Relacy Race Detector.

First of all, now you can freely DOWNLOAD latest version of Relacy
Race Detector DIRECTLY FROM WEB:
http://groups.google.com/group/relacy/files

Main change in release 1.1 is support for standard synchronization
primitives:
1. mutex (std::mutex, pthread_mutex_init, InitializeCriticalSection)
2. rw_mutex (pthread_rwlock_init, InitializeSRWLock)
3. condition variable (std::condition_variable,
std::condition_variable_any, pthread_cond_init,
InitializeConditionVariable)
4. semaphore (sem_init, CreateSemaphore)
5. event (CreateEvent)

Now you can test more traditional "mutex-based" algorithms (i.e. no
lock-free), and Relacy still will detect data races, deadlocks,
livelocks, resource leaks, incorrect usage of API etc.
Also you can test mixed lock-based/lock-free algorithms. For example
fast-path is lock-free, and slow-path is mutex-based.
For examples see 'spsc_queue' example in distributive, it uses
std::mutex and std::condition_variable as well as lock-free fast-path.
And following manual implementation of condition_variable via Win
API's CreateEvent and CreateSemaphore:
http://groups.google.com/group/comp.programming.threads/msg/30c2ec41c4d498a2

Also I add RL_DEBUGBREAK_ON_ASSERT and RL_MSVC_OUTPUT options. And
initial_state/final_state parameters. See details here:
http://groups.google.com/group/relacy/web/advanced-moments

Dmitriy V'jukov