Хочу анонсировать инструмент, который я разработал. Инструмент называется 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 €!»
Честно скажу, я в этой области не особо силён. Поэтому с радостью выслушаю любые предложения по улучшению лицензии. Был бы очень признателен.
Здравствуйте, remark, Вы писали:
R>>>Буду рад услышать любые отзывы, замечания и предложения. А>>Андронный коллайдер? R>Хм... Это замечание или предложение?
ИМХО звучит также устрошающе
Здравствуйте, Alxndr, Вы писали:
R>>Буду рад услышать любые отзывы, замечания и предложения.
A>Мелкая придирка: сабж в исходном коде повсеместно. A>Неудобно читать редакторами, в которых табуляция не равна 4м пробелам.
Здравствуйте, remark, Вы писали:
R>Готов ответить на любые вопросы, связанные с инструментом, в этом топике или здесь:
Прошу прощение за дурацкий вопрос , но на скорую руку никак не найду, c++ 98 — Win32 Api код с помощью этой библиотеки можно проверять ?
Здравствуйте, dip_2000, Вы писали:
R>>Готов ответить на любые вопросы, связанные с инструментом, в этом топике или здесь: _>Прошу прощение за дурацкий вопрос , но на скорую руку никак не найду, c++ 98 — Win32 Api код с помощью этой библиотеки можно проверять ?
В целом — можно. Зависит от того, какие именно функции из Win32 Api используются. В данный момент поддерживаются не все. Но некоторые модификации в код надо внести в любом случае.
Вот здесь можно посмотреть пример тестирования алгоритма под Win32 Api, который использует Event'ы и Semaphore'ы: http://groups.google.ru/group/comp.programming.threads/msg/30c2ec41c4d498a2
Здравствуйте, remark, Вы писали:
R>В целом — можно. Зависит от того, какие именно функции из Win32 Api используются. В данный момент поддерживаются не все. Но некоторые модификации в код надо внести в любом случае.
в код тестируемый или в код библиотеки ?
Планируется ли развитие библиотеки в этом направлении ?
Здравствуйте, dip_2000, Вы писали:
R>>В целом — можно. Зависит от того, какие именно функции из Win32 Api используются. В данный момент поддерживаются не все. Но некоторые модификации в код надо внести в любом случае.
_>в код тестируемый или в код библиотеки ?
В тестируемый.
_>Планируется ли развитие библиотеки в этом направлении ?
Да, планируется. В смысле поддержки WaitForMultipleObjects, SignalObjectAndWait и т.д.
R>>std::atomic<int> x;
R>>x($).fetch_add(1);
R>>// или просто
R>>x($) += 1;
R>>
LD>Извините за дурацкий вопрос. LD>Что значает символ $ в этом коде?
Это вспомогательная конструкция для сбора отладочной информации (имя файла, номер строки, имя функции). $ — это макрос. () — это вызов operator() у объекта.
Здравствуйте, remark, Вы писали:
R>Это вспомогательная конструкция для сбора отладочной информации (имя файла, номер строки, имя функции). $ — это макрос. () — это вызов operator() у объекта.
Я просто сначала подумал, что $ это что-то из следующего стандарта C++, или что это имеет какое-то отношение к многопочности.
Спасибо за ответ.
Здравствуйте, remark, Вы писали:
R>Хочу анонсировать инструмент, который я разработал. Инструмент называется 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).
Основная доработка релиза — это поддержка верификации Java/CLI (aka .NET) алгоритмов (но это всё ещё С++ библиотека).
Поддержка заключается в слудущем.
— Поддержка GC. Т.е. просто выделяем память и забываем. GC решает некоторые проблемы, связанные с lock-free алгоритмами, — безопасное освобождение памяти и ABA-проблема. Режим GC можно использовать и при верификации С++ алгоритмов — просто определите макрос RL_GC.
— Поддержка Java и CLI моделей памяти. Т.е. более сильный барьер памяти и более сильные атомарные операции. Так же для Java происходит автоматичесий эмит барьера памяти между volatile сохранением и volatile загрузкой.
— Поддержка основных Java и CLI API, связанных с синхронизацией.
Для CLI это — rl::nvolatile<> эмулирует volatile переменные, rl::nvar<> эмулирует обычные переменные. Interlocked операции доступны в пространстве имён rl::Interlocked (например, rl::Interlocked::CompareExchange()). Так же доступны rl::Thread::MemoryBarrier(), rl::Thread::VolatileRead(), rl::Thread::VolatileWrite() and rl::Thread::SpinWait().
Для Java доступны соотв. rl::jvolatile<>, rl::jvar<>, rl::AtomicInteger and rl::AtomicLong.
Однако богатые библиотеки поддержки Java/CLI (такие как ConcurrentQueue и т.д.) не эмулируются. Тем не менее можно использовать мьютексы, переменные условной синхронизации, семафоры и события из API С++, POSIX или Windows.
Так же надо отметить следующий момент. В Java/CLI фактически нет таких вещей как гонки (data races) и неинициализированные переменные. Это вынуждает просто отключить некоторые типы автоматически детектируемых ошибок (гонки и достпы к неинициализированным переменным). С т.з. верификации алгоритмов — это плохо. Однако в Java/CLI режимах по-прежнему можно использовать rl::var<>, по-сути это вновь позволит автоматически детектировать упомянутые типы ошибок. Т.е. если Вы уверены, что доступ к какой-то переменной должен быть только в "однопоточном стиле" (например, все доступы защищены мьютексом), то для такой переменной можно использовать rl::var<>.
По-прежнему R>Буду рад услышать любые отзывы, замечания и предложения.
Здравствуйте, remark, Вы писали:
R>Я выложил версию 1.2 Relacy Race Detector. Можно скачать здесь: R>http://groups.google.com/group/relacy/files
R>Основная доработка релиза — это поддержка верификации Java/CLI (aka .NET) алгоритмов (но это всё ещё С++ библиотека).
Здравствуйте, Кодт, Вы писали:
R>>Хочу анонсировать инструмент, который я разработал. Инструмент называется Relacy Race Detector. Это — верификатор алгоритмов синхронизации для расслабленных моделей памяти (в особенности C++0x).
К>Статью для журнала не хочешь написать?
Когда придёт время, возможно, напишу. Сейчас — нет. По нескольким причинам.
Во-первых, библиотека сейчас в очень активном развитии. Плюс часть старых интерфейсов пока меняется.
Во-вторых, сама модель памяти C++0x пока не до конца зафиксирована. Ещё возможно что-то измениться по отношению к барьерам памяти. Плюс я сам же практически убедил Hans Boehm и Peter Dimov внести некоторые изменения в правила но отношению к взаимодействию барьеров памяти и атомарных операций: http://groups.google.com/group/comp.programming.threads/msg/d2cb5e1f98bf0afa
И возможно удастся убедить внести ещё изменения по отношению к барьерам памяти: http://groups.google.com/group/comp.programming.threads/msg/07c810b38be80bbb
Это всё придётся отражать и в Relacy. Ну и там всякие мелочи, типа за последний месяц, например, переименовали все упоминания 'swap' в атомарной библиотеки на 'exchange'
В-третьих, у библиотеки такого плана не предполагается очень большого числа пользователей. Т.е. это не ширпотреб, в некотором смысле. Хотя, конечно, по-моему мнению, библиотекой могло бы пользоваться значительно больше разработчиков, чем будет. Тем не менее, как видишь, пока за неделю никто активного интереса тут не проявил, и со мной тоже никто с rsdn не связывался касательно библиотеки.
remark пишет: > > К>Статью для журнала не хочешь написать? > > > Когда придёт время, возможно, напишу. Сейчас — нет.
И зря. А потом обновишь статью. (и реклама и объяснения на пальцах и ...)
> В-третьих, у библиотеки такого плана не предполагается очень большого > числа пользователей. Т.е. это не ширпотреб, в некотором смысле. Хотя, > конечно, по-моему мнению, библиотекой могло бы пользоваться значительно > больше разработчиков, чем будет. Тем не менее, как видишь, пока за > неделю никто активного интереса тут не проявил, и со мной тоже никто с > rsdn не связывался касательно библиотеки.
Ну необязательно же всем писать, особенно если по сути нечего сказать.
Библиотека интересна. Например, я, будет время, попробую. Думаю многие
также.
В nondigit символа нет, но MSVC зараза переваривает
People who are more than casually interested in computers should have at least some idea of what the underlying hardware is like. Otherwise the programs they write will be pretty weird (c) D.Knuth
Известно что любой измерительный инструмент вносит собственные возмущения в измерямый процесс.
Вопрос состоит в следующем: возможны ли такого рода возмущения и какие?
Ну т.е. false positives нет — это как я понимаю методологически, но что-то мне говорит что они в принципе
возможны самим фактом добаления инструмента в процесс. Или я ошибаюсь?
Здравствуйте, c-smile, Вы писали:
CS>Известно что любой измерительный инструмент вносит собственные возмущения в измерямый процесс. CS>Вопрос состоит в следующем: возможны ли такого рода возмущения и какие?
CS>Ну т.е. false positives нет — это как я понимаю методологически, но что-то мне говорит что они в принципе CS>возможны самим фактом добаления инструмента в процесс. Или я ошибаюсь?
false positives (т.е. когда библиотека выдаёт ошибку, которой на самом деле нет) в данном контексте не сильно страшны, т.к. после ручного анализа будет видно, что это false positive, и ошибку в библиотеке можно будет исправить. Теоретически, и до сего момента практически, все false positives можно исправить, т.е. у библиотеки достаточно информации, что точно сказать, есть тут, например, data race или нет.
false negatives (т.е. когда библиотека не выдаёт ошибку, которая на самом деле есть) тут, конечно, очень неприятны. Основной их источник может быть или ошибка в библиотеке, либо что я пока намеренно не реализовывал поддержку детектирования каких-то ситуаций. Ну тут я могу только посоветовать, для обеспечения собственной уверенности, вначале сделать ряд тестов, что бы убедиться "собственными глазами", что библиотека находит ошибку в тесте с ошибкой, и не находит ошибок в тесте без ошибок (кстати нетривиальные тесты можно отправить мне, что бы я их включил в набор юнит-тестов).
Что касается именно каких-то принципиальных "возмущений", которые не связаны с ошибками в библиотеке... сложно сказать... на данный момент я ничего такого не вижу. Можно так, ты говоришь какую-то гипотезу относительно того какое "возмущение" возможно, тогда я точно говорю, возможно оно или нет.
Здравствуйте, c-smile, Вы писали:
CS>false positives нет — это как я понимаю методологически, но что-то мне говорит что они в принципе CS>возможны самим фактом добаления инструмента в процесс. Или я ошибаюсь?
Измеряемого процесса как такового и нет, это же симулятор. Ошибки могут быть только методологические, за счёт неверной эмуляции объектов синхронизации, но это исправимо.
People who are more than casually interested in computers should have at least some idea of what the underlying hardware is like. Otherwise the programs they write will be pretty weird (c) D.Knuth
Здравствуйте, gear nuke, Вы писали:
GN>Здравствуйте, c-smile, Вы писали:
CS>>false positives нет — это как я понимаю методологически, но что-то мне говорит что они в принципе CS>>возможны самим фактом добаления инструмента в процесс. Или я ошибаюсь?
GN>Измеряемого процесса как такового и нет, это же симулятор. Ошибки могут быть только методологические, за счёт неверной эмуляции объектов синхронизации, но это исправимо.
Ну в принципе, да. Ничего не выполняется, и я ничего не измеряю. Работа программы проактивно симулируется.