Интервью с Дмитрием Вьюковым - автором инструмента Relacy Race Detector (RRD) для верификации параллельных приложений. В статье вы узнаете об истории создания RRD, его основных возможностях, а также о некоторых других аналогичных инструментах и их отличии от RRD.
Поддержка VivaMP была прекращена в 2014 году. По всем возникшим вопросам вы можете обратиться в нашу поддержку.
Вашему вниманию предлагается интервью с автором верификатора Relacy Race Detector (RRD) для тестирования многопоточных алгоритмов. В интервью обсуждаются перспективы использования RRD и других инструментов для проверки параллельных приложений и смежные темы.
Вопросы задает (вопросы будут выделены жирным текстом):
Карпов Андрей Николаевич. Один из основателей компании "Системы программной верификации", занимается разработкой инструментов для статического анализа исходного кода. Участвует в развитии инструментов Viva64 и VivaMP для тестирования 64-битных и параллельных приложений. Поддерживает открытую библиотеку VivaCore, предназначенную для разбора (парсинга) Си/Си++ кода.
На вопросы отвечает:
Вьюков Дмитрий Сергеевич. Разработчик высокопроизводительного программного обеспечения на Си/Си++ в области клиент/серверных систем и сетевых серверов. В свободное время увлекается разработкой инновационных алгоритмов синхронизации, разработкой моделей программирования для многоядерных процессоров и систем верификации многопоточного кода. Автор инструмента Relacy Race Detector (RRD).
В меру своих сил я занимаюсь всем, что связано с многопоточностью и параллелизмом: масштабируемыми алгоритмами синхронизации, моделями программирования для многоядерных процессоров, верификацией многопоточного кода и так далее. Свои разработки касательно алгоритмов синхронизации я публикую в группе Scalable Synchronization Algorithms. Так же я разработал и поддерживаю инструмент верификации многопоточного кода Relacy Race Detector (RRD).
RRD появился достаточно спонтанно. Предпосылок для его создания было три.
Первая - я занимаюсь разработкой алгоритмов синхронизации, а тестирование и локализация ошибок в них - очень и очень серьёзная проблема: ошибки проявляются очень редко или вообще не проявляются на некоторых компьютерах (допустим на компьютерах с менее чем 4-мя процессорами, или на компьютерах с некоторой версией операционной системы). А если ошибка всё-таки регулярно проявляется, то часто бывает очень сложно понять истинную первопричину ошибки (в какой момент и что именно начинает идти "не так"). Это породило мысль, что неплохо было бы иметь какие-то "инструменты" для решения проблемы.
Вторая предпосылка - за время работы с алгоритмами синхронизации накопился некоторый багаж приёмов, которые я применял для тестирования и локализации ошибок. Один из основных - это вставка в код программы большого количества примерно таких строчек:
if ((rand() % 1000) == 0) Sleep (rand() % 10);
и последующее стресс-тестирование работы программы. Этот приём позволяет добиться выполнения значительно большего количества различных чередований (interleaving) потоков. Собственно это, по большому счёту, и является основным принципом работы RRD.
Третьей предпосылкой явилось то, что в какой-то момент я, наконец, понял, как можно собрать все мои приёмы в автоматический инструмент тестирования, как можно простым способом проводить необходимое инструментирование программы, и как при этом можно обеспечить высокую эффективность работы инструмента. Дальше было дело техники - первый рабочий прототип (который реально обнаружил одну специально внесённую ошибку в простой алгоритм) появился в тот же день ближе к ночи. Хотя, конечно, доведение RRD до более-менее пригодного для реальной работы вида заняло значительно больше времени.
RRD является средством динамической верификации без запоминания состояний. Он предназначен, прежде всего, для тестирования многопоточных алгоритмов (алгоритмов синхронизации, многопоточных структур данных и так далее). Для пользователя работа с RRD выглядит примерно следующим образом. Вначале реализуется тестируемый алгоритм. Реализация может быть выражена через примитивы синхронизации C++09, POSIX threads (pthread), Win32 API, C#/.NET, Java. Однако необходимо использовать указанные API не напрямую, а через "обёртки", предоставляемые RRD; синтаксис практически идентичен, однако имеются некоторые отличия. Когда тестируемый алгоритм реализован, необходимо реализовать один или несколько юнит-тестов (unit test) для алгоритма. Далее можно запускать их на исполнение, при этом RRD позаботится об эффективном исполнении тестов, то есть будет проверено как можно больше различных чередований (interleaving) потоков. Во время исполнения каждого чередования RRD будет делать множество различных проверок корректности алгоритма, включая как пользовательские утверждения (asserts) и инварианты (invariants), так и базовые встроенные проверки - гонки (data races), обращения к освобожденной памяти, двойные освобождения памяти, утечки памяти, взаимные блокировки (deadlocks), активные блокировки (livelocks), некорректные использования API (например, рекурсивный захват нерекурсивного мьютекса), и другие. При обнаружении ошибки RRD выведет подробную историю исполнения, которая привела к ошибке. Имея на руках такую историю, локализация ошибки становится делом техники (история содержит такие детали как отклонения от последовательно согласованного (sequentially consistent) порядка, инстансы ABA проблемы, ложные пробуждения на условных переменных (condition variable) и т.д.).
Большое количество встроенных проверок и пристрастность, с которой RRD их проводит, позволяют во многих случаях не делать в тесте вообще никаких пользовательских проверок. Например, если мы тестируем reader-writer мьютекс, то достаточно лишь создать несколько потоков, которые будут захватывать мьютекс на чтение и считывать какую-то переменную, и несколько потоков, которые захватывают мьютекс для записи и изменяют эту же переменную. Если алгоритм мьютекса не обеспечивает взаимного исключения, то автоматически будет обнаружена гонка на защищаемой переменной; если алгоритм может входить во взаимную блокировку или активную блокировку, то RRD тоже обнаруживает это автоматически. Однако если мы тестируем очередь типа производитель-потребитель (producer-consumer), и очередь должна обеспечивать FIFO порядок сообщений, то такую проверку придётся запрограммировать вручную.
Теперь немного о внутреннем устройстве RRD, и об используемых алгоритмах. RRD инструментирует все обращения к переменным, примитивам синхронизации и API вызовам. Это даёт возможность встроить в них все необходимые проверки, а так же возможность полностью управлять переключением потоков. RRD содержит 3 планировщика потоков (выбор планировщика производится при запуске теста).
Самый простой планировщик - это так называемый случайный планировщик (random scheduler), после каждого элементарного действия программы (обращении к переменной, примитиву синхронизации, API вызову) планировщик выбирает случайный поток и переключает управление на него. Этот планировщик хорош для первоначального тестирования алгоритма, т.к. он не даёт исчерпывающей проверки, но зато работает очень быстро.
Второй планировщик производит полный систематический перебор всех возможных чередований потоков (full search scheduler), однако его недостаток в очень длительном времени верификации, на практике его целесообразно применять только для небольших тестов.
Последний, третий, планировщик самый интересный и полезный - это так называемый планировщик с ограничением на количество переключений потоков (context bound scheduler). Он производит систематический перебор чередования потоков, однако при этом проверяет только чередования, в которых общее количество добровольных переключений потоков не больше некоторого заданного числа. За счёт этого он даёт очень хороший компромисс между качеством проверки и временем работы. Так же следует отметить, что все планировщики являются справедливыми (fair), это даёт возможность тестировать формально не терминирующие алгоритмы, т.е. алгоритмы, содержащие циклы, которые могут повторяться потенциально неограниченное число раз.
RRD может свободно использоваться для некоммерческой разработки с открытыми исходными кодами, для образовательных целей, для академических разработок с непатентуемыми результатами, а так же для персонального некоммерческого использования. Для всех остальных применений RRD является платным. Хотя возможно рассмотрение частных случаев; например, я имел некоторые предварительные беседы касательно предоставления специальных лицензий для разработки ядра Linux (там есть некоторые скользкие моменты, касающиеся патентованных алгоритмов и коммерциализации), а так же для разработки Intel Threading Building Blocks (который распространяется под двойной лицензией, одна из которых коммерческая).
Основной ресурс, посвященный RRD расположен по адресу:
https://groups.google.com/forum/#!forum/relacy
Там можно скачать последнюю версию библиотеки, найти некоторые материалы по RRD, а так же задавать вопросы. Дистрибутив RRD включает ряд примеров, которые могут помочь освоить RRD.
Да, конечно, до создания RRD я смотрел на множество средств верификации (Intel Thread Checker, Chord, Zing, Spin, RacerX, CheckFence, Sober, Coverity Thread Analyzer, CHESS, KISS, PreFast, Prefix, FxCop) в надежде найти то, что нужно для моих целей. Однако большинство инструментов рассчитаны, так сказать, на разработчиков конечных прикладных программ, а не на разработчиков алгоритмов синхронизации и библиотек поддержки параллелизма. Ни один из инструментов не даёт того уровня детализации и точности моделирования свободного доступа к памяти (Relaxed Memory Order) [*], который был необходим мне. Образно, если упомянутые средства могут верифицировать программу, использующую OpenMP, то RRD может верифицировать саму реализацию OpenMP.
[*] Примечание. Свободный доступ к памяти (Relaxed Memory Order, RMO) - метод работы с памятью, когда процессор использует все средства кэширования и динамического переупорядочения команд, и не пытается обеспечить никаких требований к упорядоченности выборки и сохранению операндов в основной памяти. Иногда такой режим называют "расслабленная модель памяти".
Сразу оговорюсь, что с большинством инструментов я не знакомился практически (установка, запуск примеров, применение в собственных проектах). Я знакомился с ними поверхностно, так как из общих описаний мне становилось понятно, что это не то, что мне нужно; и дальше знакомиться не имело смысла. Поэтому я, наверное, не смогу рассказать много интересного для конечных пользователей, но тем не менее...
Могу рассказать про инструмент Spin, который несколько приближается по свойствам к RRD, и я знаю, что он использовался для верификации некоторых алгоритмов синхронизации для ядра Linux и для Threading Building Blocks. Spin - это, наверное, самый старый и основательный инструмент такого рода, его корни уходят в начало 80-ых годов, по нему написан ряд книг, и, что очень приятно, он активно развивается и по сей день. Spin включает множество вариантов проверки - динамическая проверка с запоминанием состояний, без запоминания, полная проверка модели программы, не полная проверка модели программы (для очень больших программ) и так дадее, всего и не перечесть. Компилятор Promela (язык, используемый Spin) и верификатор (Protocol ANalyser, pan в терминологии Spin) имеют множество ключей, управляющих различными аспектами работы (режим проверки, степень детализации вывода, лимит памяти и так далее), так же имеется несколько GUI оболочек. Одним словом, если вам понадобится что-то особенное, скорее всего, это уже есть в Spin.
Сам процесс работы со Spin схож с RRD - описывается тест на специальном языке Promela (a PRocess MEta LAnguage), далее компилируете его, на выходе получается исходный файл на языке С, который надо скомпилировать С компилятором, что бы получить верификатор. Далее запускаете верификатор, и при обнаружении ошибки он создаёт файл с подробным описанием ошибки и истории выполнения. Потом из этого файла можно сгенерировать Postscript файл для просмотра, или использовать для "проигрывания" истории выполнения. Как видно процесс работы со Spin несколько сложнее, чем с RRD, ну что ж, статус обязывает :).
Возникает закономерный вопрос - чем же меня не устроил Spin? Во-первых, это специальный язык Promela для описания тестов; с одной стороны это кажется не таким уж и принципиальным моментом, но с другой стороны я иногда ловлю себя на том, что мне лень делать даже то минимальное инструментирование кода, которое требуется для RRD. Да и переписывая программу вручную на другой язык, мы рискуем протестировать не совсем то, что хотели. Во-вторых, это последовательно согласованная (sequentially consistent) модель памяти; тут уже ничего не сказать в защиту Spin - поддержка свободного доступа к памяти ("расслабленной модели памяти") просто необходима для верификатора алгоритмов синхронизации. В-третьих, это отсутствие встроенной поддержки для таких специфических вещей как вызовы Win32 API WaitForMultipleObjects() или SignalObjectAndWait(), или ложные пробуждения на condition variable POSIX, или ожидания с таймаутами, и так далее. Совокупность этих факторов в итоге заставила меня отвернуться от Spin.
Тем не менее, ещё раз подчеркну, что инструмент очень и очень достойный. Основной сайт проекта - http://spinroot.com/ .
Вот простой пример, в котором реализуется взаимное исключение на основе спин-мьютекса (первый пример я приведу в синтаксисе C++09, а второй в синтаксисе RRD, что бы показать различия):
std::atomic<int> mutex;
int data;
void thread1()
{
// простой спин-мьютекс
while (mutex.exchange(1, std::memory_order_acquire))
std::this_thread::yield();
data = 1;
mutex.store(0, std::memory_order_release);
}
void thread2()
{
// простой спин-мьютекс
while (mutex.exchange(1, std::memory_order_acquire))
std::this_thread::yield();
data = 2;
mutex.store(0, std::memory_order_relaxed);
}В этом примере содержится так называемая гонка второго типа (data race type 2). Гонки типа 2 характеризуются тем, что конфликтующие доступы к проблемной переменной не являются смежными ни в одном чередовании потоков; тем не менее, они конфликтуют из-за возможного переупорядочивания обращений к памяти при свободном доступе. RRD обнаружит эту гонку и покажет в результирующей истории исполнения какие именно переупорядочивания имели место.
Вот несколько более сложный пример - lock-free stack (уже записанный в синтаксисе RRD; основное пространство имён, используемое RRD - "rl", так же обратите внимание на требуемое инструментирование кода в виде "($)"):
struct node
{
rl::atomic<node*> next;
rl::var<void*> data;
};
struct stack
{
rl::atomic<node*> head;
};
void push(stack* s, void* data)
{
node* n = RL_NEW(node);
n->data($) = data;
node* next = s->head($).load(rl::memory_order_relaxed);
for (;;)
{
n->next($).store(next, rl::memory_order_relaxed);
if (s->head($).compare_exchange_weak(
next, n, rl::memory_order_release))
break;
}
}
void* pop(stack* s)
{
node* n = s->head($).load(rl::memory_order_relaxed);
for (;;)
{
if (0 == n)
return 0;
node* next = n->next($).load(rl::memory_order_relaxed);
if (s->head($).compare_exchange_weak(
n, next, rl::memory_order_acquire))
break;
}
void* data = n->data($);
RL_DELETE(n);
return data;
}И вот юнит-тест для RRD:
// шаблонный параметр "2" задаёт кол-во потоков в тесте
struct test : rl::test_suite<test, 2>
{
stack s;
// выполняется в одном потоке
// перед исполнением основной функции потоков
void before()
{
s.head($) = 0;
}
// основная функция потоков
void thread(unsigned /*thread_index*/)
{
push(&s, (void*)1);
void* data = pop(&s);
RL_ASSERT(data == (void*)1);
}
};
int main()
{
rl::simulate<test>();
}Если мы запустим программу, то увидим следующий вывод (я убрал историю выполнения отдельных потоков; первая цифра в строчке является глобальным порядковым номером операции - для сопоставления с историей выполнения отдельных потоков, вторая цифра - номер потока):
struct test
ACCESS TO FREED MEMORY (access to freed memory)
iteration: 2
execution history:
[0] 1: [BEFORE BEGIN]
[1] 1: <0023DEA0> atomic store, value=00000000,
(prev value=00000000), order=seq_cst, in test::before, main.cpp(70)
[2] 1: [BEFORE END]
[3] 1: memory allocation: addr=0023CB78, size=52,
in push, main.cpp(34)
[4] 1: <0023CB9C> store, value=00000001, in push, main.cpp(35)
[5] 1: <0023DEA0> atomic load, value=00000000, order=relaxed,
in push, main.cpp(36)
[6] 0: memory allocation: addr=0023CE80, size=52,
in push, main.cpp(34)
[7] 0: <0023CEA4> store, value=00000001, in push, main.cpp(35)
[8] 1: <0023CB78> atomic store, value=00000000, (prev value=00000000),
order=relaxed, in push, main.cpp(39)
[9] 0: <0023DEA0> atomic load, value=00000000, order=relaxed,
in push, main.cpp(36)
[10] 0: <0023CE80> atomic store, value=00000000,
(prev value=00000000), order=relaxed, in push, main.cpp(39)
[11] 1: <0023DEA0> CAS fail [SPURIOUSLY] orig=00000000,
cmp=00000000, xchg=0023CB78, order=release, in push, main.cpp(40)
[12] 0: <0023DEA0> CAS succ orig=00000000, cmp=00000000,
xchg=0023CE80, order=release, in push, main.cpp(40)
[13] 1: <0023CB78> atomic store, value=00000000,
(prev value=00000000), order=relaxed, in push, main.cpp(39)
[14] 0: <0023DEA0> atomic load, value=0023CE80, order=relaxed,
in pop, main.cpp(47)
[15] 1: <0023DEA0> CAS fail orig=0023CE80, cmp=00000000,
xchg=0023CB78, order=release, in push, main.cpp(40)
[16] 1: <0023CB78> atomic store, value=0023CE80,
(prev value=00000000), order=relaxed, in push, main.cpp(39)
[17] 0: <0023CE80> atomic load, value=00000000, order=relaxed,
in pop, main.cpp(52)
[18] 1: <0023DEA0> CAS succ orig=0023CE80, cmp=0023CE80,
xchg=0023CB78, order=release, in push, main.cpp(40)
[19] 1: <0023DEA0> atomic load, value=0023CB78, order=relaxed,
in pop, main.cpp(47)
[20] 0: <0023DEA0> CAS fail orig=0023CB78, cmp=0023CE80,
xchg=00000000, order=acquire, in pop, main.cpp(53)
[21] 1: <0023CB78> atomic load, value=0023CE80, order=relaxed,
in pop, main.cpp(52)
[22] 1: <0023DEA0> CAS succ orig=0023CB78, cmp=0023CB78,
xchg=0023CE80, order=acquire, in pop, main.cpp(53)
[23] 1: <0023CB9C> load, value=00000001, in pop, main.cpp(56)
[24] 1: memory deallocation: addr=0023CB78, in pop, main.cpp(57)
[25] 0: ACCESS TO FREED MEMORY (access to freed memory),
in pop, main.cpp(52)Из вывода мы видим, что при проверке второго чередования потоков RRD обнаружил обращение к освобожденной памяти. Из анализа истории можно понять, что поток 1 снимает элемент со стека и освобождает его, после этого поток 0 обращается к этому элементу.
Я думаю, что тут Вы немного лукавите, говоря, что OpenMP используется малым количеством разработчиком. Конечно, всё относительно; но я думаю, что буду недалек от истины, сказав, что OpenMP - самая распространённая в промышленном коде библиотека поддержки параллелизма. Во-первых, это - относительно старое и проверенное средство, поддерживаемое множеством коммерческих и некоммерческих организаций, с множеством независимых реализаций. Во-вторых, оно достаточно простое и хорошо решает свою задачу.
Ну и естественно я, как разработчик собственного средства верификации многопоточного кода, считаю такие инструменты очень актуальными и необходимыми; особенно сейчас, когда у каждого из нас на рабочем столе стоит компьютер с многоядерным процессором. Исходя из этих двух вещей, VivaMP - просто незаменимое средство для начинающих в области параллельного программирования разработчиков. Но VivaMP будет так же полезен и более опытным разработчикам, так как никто не застрахован как от "глупых" ошибок (невнимательность, copy-paste), так и от "умных". А VivaMP всегда будет "прикрывать тыл" своей беспристрастностью и вычислительной мощью. Я знаю не мало примеров, когда многопоточный код, разработанный в том числе и экспертами, и просмотренный не одной парой глаз, работал годами, но потом в нём всё же обнаруживались серьёзные ошибки, которые приводили к зависаниям и падениям. Значительная часть этих ошибок была или могла бы быть обнаружена средствами верификации, такими как VivaMP.
Касательно технической стороны вопроса, VivaMP - это средство статической верификации. И что мне очень нравится в статической верификации так это то, что не нужно писать юнит-тесты; инструмент проверяет целевой код сам по себе. И вопрос даже не столько в необходимости написать некоторый объём дополнительного кода, сколько в том, что это - опять же человеческий фактор. Разработчик должен определить, какие именно тесты необходимы, как именно они должны работать и так далее; и качество проверки напрямую будет зависеть от качества юнит-тестов. При использовании VivaMP такой проблемы нет, есть только проверяемый код и инструмент. Я считаю, что это очень сильное свойство.
Идея была в устранении необходимости ручного инструментирования кода. Т.е. написать собственный препроцессор кода на основе библиотеки VivaCore, что бы он вставлял в нужные места все эти пресловутые "($)", а пользователь мог тестировать непосредственно свой "боевой" код. Однако после предпроектных исследований выяснилось, что это потребует затрат достаточно существенных ресурсов, поэтому от этой идеи, к сожалению, пришлось отказаться.
Планов у меня всегда много :). На сайте RRD можно видеть TODO/Feature List, в котором я отражаю свои планы и идеи касательно дальнейшего развития RRD. Из наиболее существенных и интересных доработок можно отметить поддержку локального хранилища потоков (TSS/TLS) с обёртками для POSIX и Win32, поддержку UNIX сигналов и различных типов аппаратных прерываний, оптимизация алгоритма полного перебора состояний программы (partial-order reductions) и распараллеливание работы библиотеки, периодическое сохранение состояния в контрольных точках, определение "мёртвого" (не тестируемого) кода, моделирование характеристик программы, касающихся производительности и масштабируемости. Однако в данный момент развитие библиотеки, так сказать, demand-driven, т.е. движется нуждами пользователей. Поэтому буду рад услышать отзывы, мысли и идеи читателей по этому поводу.
Про параллельные технологии можно сказать всё то же, что и про любую другую новую технологию - больше экспериментируйте; пробуйте решать простые задачи - смотрите что получается, а что нет, пробуйте ещё; выдвигайте гипотезы - проверяйте их, выдвигайте новые гипотезы и так далее. Только практика и обратная связь может сделать Вас - профессионалом. Ну и, конечно, "не брезгайте" средствами автоматической верификации кода, это как эксперт всегда стоящий за спиной и приглядывающий за вами. Естественно можно обойтись и без таких средств, ну уж как минимум они сэкономят вам массу времени.
Спасибо. Желаю Вам и нашим читателям успехов в их разработках.
Еще раз хотим поблагодарить Дмитрия за интересную беседу и рассказ об инструментах верификации параллельных приложений. В конце статьи в библиографическом списке читатели могут познакомиться со списком ресурсов посвященных RRD и ряду других инструментов схожей направленности.