Введение 3
Цели и задачи работы 4
Глава 1. Обзор предметной области 5
1.1. Используемые понятия 5
1.2. Существующие подобные инструменты 8
Глава 2. Реализация верификатора 9
2.1. Пользовательский интерфейс 9
2.2. Архитектура верификатора 10
2.3. Интерфейс Task 12
2.4. Выбор корутин для реализации Task 13
2.5. Реализация корутин 15
2.6. Генерация прерываний в целевых методах 17
2.7. Реализация примитивов синхронизации 18
2.8. Задачи планировщика 21
2.9. Случаный планировщик 22
2.10. ModelCheck планировщик 24
Глава 3. Применение верификатора 27
3.1. Неатомарный счетчик 27
3.2. Lock-free очередь 1 28
3.3. Lock-free очередь из библиотеки корутин 29
3.4. RWM буффер из библиотеки корутин 32
Выводы 33
Заключение 34
Список литературы 35
Сейчас трудно представить производительный серверный код, написанный без использования конкурентности, параллелизма, или же смеси этих
двух подходов. Абстракция конкурентности означает, что исполняемые функции чередуются, передавая поток исполнения друг другу тем или иным способом. Для реализации этой абстракции в современных языках программирования используются легкие потоки, называемые файберами или корутинами
[1].
Язык C++ используется для написания высокопроизводительного кода.
Корутины, как концепция языка, появились в 20-м его стандарте [2]. Однако,
предоставляется лишь минимальный набор операций, не предполагающий их
использование в сыром виде: нет неблокирующих примитивов синхронизаци,
планировщика.
В одной из команд компании «ВКонтакте» написали библиотеку на
базе корутин из C++, которая призвана решить описанные выше проблемы. В
нее вошли как упомянутые примитивы синхронизации: мьютексы, условные
переменные, так и lock-free очереди, наборы буфферов.
Планировщик библиотеки исполняет корутины в нескольких системных потоках, поэтому для синхронизации и обмена данными между ними используются многопоточные структуры данных. Для них написано множество
модульных и интеграционных тестов, запускающихся в том числе под санитайзером [3]. Однако, такие тесты не могут гарантировать, что проверяемые
структуры данных обладают свойствами корректности, потому что каждый
такой тест проверяет лишь одно конкретное исполнение из большого пространства. Кроме того, даже большое количество запусков может не помочь
обнаружить проблемые исполнения, потому что поведение многопоточного
кода может сильно зависеть от текущего состояния системы.
Требуемым свойством корректности является линеаризуемость [4]. Кроме того, в библиотеке используются дуальные структуры данных, и линеаризуемость может быть расширена для проверки в том числе их корректности
[5].
Так как нами не было найдено открытого инструмента для проверки
3C++ кода на линеаризуемость, то было решено разработать его самостоятельно. Кроме того, разрабатываемый инструмент должен быть способен работать
с кодом произвольных многопоточных структур данных, чтобы быть применимым в модульных тестах других приложений и библиотек.
Несмотря на то, что разработанного функционала хватает для базовой
проверки структур на линеаризуемость, встраивания в модульные тесты существующих библиотек, достижения целей текущей работы, трудно назвать
верификатор законченным. Поэтому необходимо упомянуть список возможных доработок:
1. Добавить возможность распараллеливания проверки историй. В данный
момент используется лишь одно ядро. Распараллеливание приведет к
существенному ускорению, так как генерация историй может быть произведена независимо.
2. Добавить возможность указания степени параллельности методов, чтобы можно было протестировать не только multi-producer multi-consumer
очереди, но и варианты с одним consumer, одним producer.
343. Добавить минимизацию найденной нелинеаризуемой истории исполнения. Таким образом, можно упростить отладку.
4. Добавить отлов дедлока на написанных примитивах.
5. Добавить проверку других моделей: например, последовательную согласованность, отсутствие препятствий, отсутствия ожиданий [31].
