Хочу анонсировать инструмент, который я разработал. Инструмент называется 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

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