Тема: Исследование и реализация методов верификации и тестирования конкурентных алгоритмов на С++
Закажите новую по вашим требованиям
Представленный материал является образцом учебного исследования, примером структуры и содержания учебного исследования по заявленной теме. Размещён исключительно в информационных и ознакомительных целях.
Workspay.ru оказывает информационные услуги по сбору, обработке и структурированию материалов в соответствии с требованиями заказчика.
Размещение материала не означает публикацию произведения впервые и не предполагает передачу исключительных авторских прав третьим лицам.
Материал не предназначен для дословной сдачи в образовательные организации и требует самостоятельной переработки с соблюдением законодательства Российской Федерации об авторском праве и принципов академической добросовестности.
Авторские права на исходные материалы принадлежат их законным правообладателям. В случае возникновения вопросов, связанных с размещённым материалом, просим направить обращение через форму обратной связи.
📋 Содержание
Цели и задачи работы 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].



