Хочу анонсировать инструмент, который я разработал. Инструмент называется 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) частного некоммерческого использования. По остальным случаям, пожалуйста, обращайтесь лично.
Небольшой пример некой гипотетической бизнес-логики, отвечающей за хранение списка лицевых счетов, и осуществляющей переводы сумм с одного л/с на другой. Пример записан сразу в виде, пригодном для тестирования Relacy, но я думаю, что не составит труда представить, как код выглядел с использованием pthread API.
Так же в коде сразу присутствуют исправления допущенных ошибок (закомментированы), дабы впоследствие не сбивались номера строк.
При запуске теста Relacy детектирует рекурсивный захват нерекурсивного мьютекса. Из анализа истории выполнения видно, что рекурсивный захват происходит в строчках 48 и 49, т.е. когда номера л/с совпадают.
struct business_logic_test
RECURSION ON NON-RECURSIVE MUTEX
iteration: 3
Теперь Relacy выводит следующее. Из истории выполнения видно, что происходит дедлок, т.к. первый поток вначале захватывает мьютекс 00357E88, и потом пытается захватить мьютекс 00357EC8; а второй поток вначале захватывает мьютекс 00357EC8, а потом пытается захватить мьютекс 00357E88.
Здесь пример верификации самопального condition variable на основе примитивов Win API — semaphore и event. Relacy с легкостью детектировала тонкую ошибку, связанную с семантикой пробуждения на condition variable, которая может приводить к deadlock'ам в программе, и о которой автор ничего не подозревал, использовал алгоритм значительное время, и был уверен, что он полностью корректный: http://groups.google.ru/group/comp.programming.threads/msg/30c2ec41c4d498a2
Здравствуйте, remark, Вы писали:
R>Хочу анонсировать инструмент, который я разработал. Инструмент называется Relacy Race Detector. Это — верификатор алгоритмов синхронизации для расслабленных моделей памяти (в особенности C++0x). Инструмент предназначен для тестирования как традиционных mutex-based алгоритмов (основанных на mutex, condition_variable, semaphore, event)
Поддерживается ли проверка на критических секциях ?
Здравствуйте, remark, Вы писали:
R>Хочу анонсировать инструмент, который я разработал. Инструмент называется Relacy Race Detector. Это — верификатор алгоритмов синхронизации для расслабленных моделей памяти (в особенности C++0x).
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Здравствуйте, remark, Вы писали:
R>>Хочу анонсировать инструмент, который я разработал. Инструмент называется Relacy Race Detector. Это — верификатор алгоритмов синхронизации для расслабленных моделей памяти (в особенности C++0x). Инструмент предназначен для тестирования как традиционных mutex-based алгоритмов (основанных на mutex, condition_variable, semaphore, event)
PD>Поддерживается ли проверка на критических секциях ?
include <relacy/relacy_std.hpp>
// template parameter '2' is number of threadsstruct race_test : rl::test_suite<race_test, 2>
{
rl::var<volatile long> i; // или rl::atomic ?
// executed in single thread before main thread functionvoid before()
{
i($) = 0;
}
// main thread functionvoid thread(unsigned thread_index)
{
::InterlockedIncrement(&(i($)));
}
// executed in single thread after main thread functionvoid after()
{
}
// executed in single thread after every 'visible' action in main threads
// disallowed to modify any statevoid invariant()
{
}
};
int main()
{
rl::simulate<race_test>();
}
R>Имеются аналогичные обёртки и для InitializeCriticalSection.
Я бы с удовольствием попробовал, как раз имею дело с таким проектом. Проблема в одном — проект на чистом С, да еще с прямым подключением MYSQL, а там такая либа, что хоть плачь Если будет время, попытаюсь собрать.
Здравствуйте, remark, Вы писали:
R>Нет, так нельзя. Оно не будет работать, как предполагается. R>Атомарные операции производятся с помощью методов класса std::atomic<>:
Это класс С++0х, который не может быть сейчас реализован на InterlockedXxx даже для LONG ?
R>Для WinAPI InterlockedXXX пока сильной необходимости делать обёртки не было.
Другие средства WinAPI, вроде InterlockedPushEntrySList, EnterCriticalSection и WaitForMultipleObjects тоже не нужны ?
Что произойдёт при дедлоке или ливлоке, зависание или вывод сообщения об ошибке ?
R>>Имеются аналогичные обёртки и для InitializeCriticalSection.
PD>Я бы с удовольствием попробовал, как раз имею дело с таким проектом. Проблема в одном — проект на чистом С, да еще с прямым подключением MYSQL, а там такая либа, что хоть плачь Если будет время, попытаюсь собрать.
Тут есть 2 момента.
Первый, тестируемый алгоритм можно переписать для тестирования. Т.е. ничего не мешает иметь проект на С, и несколько юнит-тестов отдельным проектом на С++. Я даже применял Relacy для тестирования алгоритмов, изначально написанных на C#. Т.е. уверенность в работоспособности сложного и критичного алгоритма синхронизации может стоить некоторой дополнительной работы.
Второй, с помощью тонкой прослойки из макросов скорее всего можно будет тестировать и сам продакшн-код, даже если он на С. Примерно как-то так:
Здравствуйте, Alexander G, Вы писали:
R>>Нет, так нельзя. Оно не будет работать, как предполагается. R>>Атомарные операции производятся с помощью методов класса std::atomic<>:
AG>Это класс С++0х, который не может быть сейчас реализован на InterlockedXxx даже для LONG ?
Тут дело не в реализации через InterlockedXxx. Фактически Relacy не выполняет код, она симулирует выполнение. Т.е. объект std::atomic<>, помимо текущего значения, содержит значительный объем вспомогательной информации, которая включает ряд предыдущих значений, ряд векторных часов, ряд флагов и т.д. Соотв. методы std::atomic<> не просто меняют значение, они производят значительный объем расчетов и проверок, связанных с изменением или чтением переменной.
R>>Для WinAPI InterlockedXXX пока сильной необходимости делать обёртки не было.
AG>Другие средства WinAPI, вроде InterlockedPushEntrySList, EnterCriticalSection и WaitForMultipleObjects тоже не нужны ?
На данный момент из Win API поддерживаются API, связанные с CriticalSection, SRWLock, Semaphore, Event, ConditionVariable, WaitForSingleObject.
InterlockedPushEntrySList, WaitForMultipleObjects, SignalObjectAndWait пока не поддерживаются. Всё зависит от востребованности и заинтересованности.
AG>Что произойдёт при дедлоке или ливлоке, зависание или вывод сообщения об ошибке ?
Здравствуйте, jazzer, Вы писали:
J>Эх, я б потестил, да весь мой софт коммерческий, нельзя по твоей лицензии :crash:
Ну проблем-то. Напиши сам себе библиотеку на условиях лицензии MIT, проверь ее детектором, благо условия RRD это позволяют, потом включи ее в свой коммерческий продукт, благо условия MIT это позволяют.
Вообще, лицензия крайне странная. Во-первых, прав ли я в том, что лицензия не может регулировать, для чего используется продукт, а только условия распространения производных работ?
Во-вторых, хитрый разработчик пожадничает, загрузит верификатор и применит по назначению, исправит найденные ошибки и удалит верификатор, и автору ничего не достанется :-)
Вывод: лицензию надо сильно переделать, сразу видно, что DVINAL. И где-нибудь большими буквами написать: «Проверю ваш проект на отсутствие гонок и пр.! Недорого, каких-то 50 000 €!»
Здравствуйте, eao197, Вы писали:
J>>Эх, я б потестил, да весь мой софт коммерческий, нельзя по твоей лицензии
E>Для коммерческого софта у Димы своя лицензия. Так что обращайся напрямую к нему -- вопрос, я думаю, решится положительно.
Совершенно верно.
Для начала могу дать trail лицензию для ознакомления.
Здравствуйте, Roman Odaisky, Вы писали:
J>>Эх, я б потестил, да весь мой софт коммерческий, нельзя по твоей лицензии
RO>Ну проблем-то. Напиши сам себе библиотеку на условиях лицензии MIT, проверь ее детектором, благо условия RRD это позволяют, потом включи ее в свой коммерческий продукт, благо условия MIT это позволяют.
А как формально/юридически отличать такую ситуацию от следующей? Человек честно использует RRD для разработки опен-сорц библиотеки. А через какое-то время использует накопленный опыт и проверенные алгоритмы в своих коммерческих разработках. Тут вроде как всё чисто, никакого жульничества.
RO>Вообще, лицензия крайне странная. Во-первых, прав ли я в том, что лицензия не может регулировать, для чего используется продукт, а только условия распространения производных работ?
В смысле? Что вообще лицензии не могут этого регулировать? Или что эта конкретная лицензия не регулирует?
RO>Во-вторых, хитрый разработчик пожадничает, загрузит верификатор и применит по назначению, исправит найденные ошибки и удалит верификатор, и автору ничего не достанется
С хитрым (особенно русским) разработчиком вообще сложно совладать. Особенно если скачать можно свободно. И нет никакой возможности защитить продукт, т.к. это просто библиотека с исходными кодами.
RO>Вывод: лицензию надо сильно переделать, сразу видно, что DVINAL. И где-нибудь большими буквами написать: «Проверю ваш проект на отсутствие гонок и пр.! Недорого, каких-то 50 000 €!»
Честно скажу, я в этой области не особо силён. Поэтому с радостью выслушаю любые предложения по улучшению лицензии. Был бы очень признателен.