Как мы написали конкурентные структуры данных на C++ и научились их верифицировать
Привет! В команде ВКонтакте мы переписываем рантайм движков баз данных — они становятся быстрее, надёжнее, а ещё с новым рантаймом проще писать код. Однако есть нюанс: в новом рантайме много конкурентных структур данных, в том числе нужных для работы с корутинами из С++20. Появляется интересная задача — проверять корректность этих конкурентных структур данных до выхода кода в продакшен.
Для решения этой задачи команда ВКонтакте вместе со студентами из университетов ИТМО и СПбГУ работала над научно-исследовательским проектом — верификацией конкурентных структур данных на языке C++. В этой статье подробно расскажем, как мы в рамках проекта проверяли корректность наших конкурентных структур данных и заодно исправили найденную в нашем новом рантайме ошибку.
Зачем нужны корутины в C++
Дать всеобъемлющее и понятное объяснение корутины сложно. Можно рассматривать её как легковесную (занимающую гораздо меньше памяти, чем тред ОС) прерываемую задачу. Если корутина захочет сделать действие, требующее ожидания, — например, подождать, пока в сокет придёт сообщение, и прочитать его, — то текущую корутину можно прервать и заставить тред ОС исполнять какую-то другую корутину. К исходной корутине можно будет вернуться, как только в сокете будут готовы данные. Прерывать корутину тоже проще, чем прерывать тред ОС. Для этого не нужны аппаратные прерывания и переключение из контекста пользователя (user space) в контекст ядра (kernel space) и обратно, а только сохранение пачки регистров и longjump. Это один из примеров реализации, а их существует достаточно много — описание одного из простых способов приведено тут.
Корутины существуют давно, со времён Scheme как минимум, но для широкой аудитории их продвинул Golang. Проблема в том, что корутины Golang нас разбаловали: в них есть почти всё, что нужно для счастья, — не блокирующая треды ОС работа с сетью, не блокирующие треды ОС примитивы синхронизации, work-stealing планировщик корутин и т. д.
Основным примитивом синхронизации корутин выступает канал. Канал — это очередь ограниченного размера, хранящая не более N элементов. При этом, если корутина хочет прочитать из канала, а в нём нет элементов, она будет ждать, пока там не появится хотя бы один элемент, который вставит другая корутина. Только после этого корутина вернёт этот элемент. Причём она будет ждать, не блокируя тред ОС, — он начнёт исполнять другую корутину, пока в канале не появятся данные, и тогда можно будет вернуться к исполнению текущей корутины.
Если корутина хочет в канал что-то положить, а в нём нет места (то есть в канале уже N элементов), она будет ждать, пока место освободится. То есть пока какая-то другая корутина не заберёт хотя бы один элемент. Только потом корутина вставит свой элемент, причём опять же будет ждать, не блокируя тред ОС, — он начнёт исполнять другую корутину, пока в канале не появится место, и тогда можно будет вернуться к исполнению текущей корутины.
Структуры данных, которые умеют приостанавливать исполнение корутин до наступления некоторого условия и только потом возвращать им управление, называются дуальными. Их сложно писать, а у нас в библиотеке их много.
А ещё рантайм Golang предоставляет нам планировщик корутин — это компонент, запускающий несколько тредов ОС и решающий для каждого момента времени, какую корутину будет исполнять каждый из доступных ему тредов ОС. Так как корутина — прерываемая задача, тред ОС исполняет назначенную ему корутину до ближайшей точки прерывания, а затем начинает исполнять другую доступную для исполнения корутину. Он откладывает исполнение текущей корутины до наступления некоторого условия — например, до появления данных в сокете или элемента в канале. После наступления этого условия корутина «разблокируется» и может снова быть исполнена одним из тредов ОС.
А что в «плюсах»? Там корутины появились в C++20, но только как языковой механизм — прерываемая функция, которую можно продолжить исполнять с того места, на котором прервались. Больше ничего нет — ни неблокирующей работы с сетью, ни примитивов синхронизации для корутин (например, каналов), ни даже планировщика корутин.
Если чего-то нет, значит, надо это написать. Вот мы и написали библиотеку, содержащую:
примитивы синхронизации для корутин;
обычные lock-free структуры данных вроде FAA-очереди;
корутинный сетевой движок;
планировщик корутин;
другие необходимые для работы наших баз данных компоненты.
Раз код есть, значит, надо его тестировать. Проблема в том, что код наш многопоточный, то есть запускаемый на множестве тредов ОС. Значит, корректность его работы зависит от того, как именно эти треды будут исполнены операционной системой.
Есть простой пример. Пусть у нас будет код, увеличивающий значение переменной Variable на единицу.
Ещё есть два треда, увеличивающие одну и ту же переменную, изначально равную 0. В примере ниже исполнение будет корректным: два инкремента произошло, значение переменной увеличилось с 0 до 2.
При этом исполнение на примере ниже будет некорректным: два инкремента произошли, а значение переменной увеличилось с 0 до 1, то есть один из инкрементов мы «потеряли».
Мы провели один запуск теста — он показал, что проблемы нет. Можем ли мы быть уверены, что проверено в том числе проблемное второе исполнение, а не только корректное первое? На проде проблема может всплыть под нагрузкой, когда планировщик тредов ОС будет активнее переключать треды. Но в тесте под малой нагрузкой, когда планировщик тредов ОС активно треды не переключает, она может не проявиться. Из этого следует важный вывод: нужно уметь гарантировать, что мы перебрали вообще все возможные варианты исполнения.
Существует и другая возможная проблема. Допустим, мы провели тест и нашли баг (второе исполнение), а потом он перестал воспроизводиться — в последующих запусках теста операционная система не переключает треды ОС так, чтобы получилось второе исполнение. Пофиксить баг, не умея воспроизводить его, сложно. Из этого следует вывод: нужно управлять исполнением самим, не позволяя недетерминированному планировщику тредов ОС мешать нам. Таким образом, необходимо разработать способ тестирования, который, с одной стороны, будет проверять все интересующие нас варианты исполнения, а с другой — детерминировано воспроизводить найденные баги.
Была вероятность, что найти такой способ вообще не получится. Но мы рискнули и решили инвестировать вдолгую: не просто запустить процесс верификации собственного кода, а привлечь к нему студентов инженерных направлений. У них появилась бы площадка для получения опыта, а у нас — возможность исследования конкретной прикладной задачи.
Как мы организовали проект команды инфраструктуры ВКонтакте
При поддержке VK Education мы запустили научно-исследовательскую лабораторию для студентов, как делали годом ранее вместе с университетом ИТМО. В рамках такого проекта студенты пишут дипломную работу, одновременно решая задачи компании. В прошлом году они доказывали корректность распределённых систем. В этом году задача чуть изменилась — мы поручили участникам лаборатории верификацию конкурентных структур данных на языке C++.
В «прошлом сезоне» мы сотрудничали с руководителем научно-исследовательской лаборатории ИТМО Виталием Аксеновым. К нему же обратились для запуска новой лаборатории. По опыту работы с ним были уверены, что проект будет вестись грамотно и с чётким результатом. В этот раз мы расширили сотрудничество с университетами. Кроме ИТМО, с которым мы давно работаем, нашим партнёром стал СПбГУ. Там преподаёт старший разработчик баз данных ВКонтакте Илья Кокорин, который пригласил поучаствовать своих студентов и стал куратором лаборатории.
В работе лаборатории приняли участие пять бакалавров и магистров ИТМО и СПбГУ, которые прошли предварительное тестирование и собеседование. На проекте двое студентов работали с верификацией конкурентных структур данных, а остальных заинтересовали другие направления — оптимизация объектного кеша, оптимизация десериализатора языка межсервисного взаимодействия RPC/TL и разработка прототипа гибридного транзакционно-аналитического движка баз данных. Желающих попасть в лабораторию было больше. Для студентов это возможность поработать над востребованным проектом: многие пишут свои конкурентные структуры данных, но немногие умеют их проверять. А мы анонсировали, что будем работать над способом выполнять такие проверки.
Вторую лабораторию мы запустили в октябре 2023-го. Для начала провели несколько установочных встреч с участниками, где рассказали, какие компоненты есть в новом рантайме наших баз данных и почему нам важно доказательство корректности. Верификацию можно поручить человеку не из компании — это не user-facing элемент, если будет допущена ошибка, то весь продакшен не рухнет. Мы можем дать код студенту и попросить выполнить проверку — нам остаётся лишь наблюдать за процессом.
Еженедельно участники лаборатории созванивались с Ильёй Кокориным и Виталием Аксеновым, ежемесячно проходили сборы команды — каждый показывал презентацию с примерами кода и делился результатами исследования. По итогам работы лаборатории каждый студент получил R&D-проект в портфолио — причём трудился он над ним не в абстрактной ситуации, а с опытной командой работающего бизнеса. Выпускная работа может в перспективе перерасти в серьёзную научную статью, которая будет опубликована в ведущих журналах мира. К тому же ВКонтакте не забирает разработку себе — в будущем студент может свободно использовать решение в других своих проектах.
Самые талантливые из участников лаборатории могут получить офер в компанию. По итогам прошлого года мы трудоустроили двух из трёх выпускников, причём один из них сейчас занимается той же темой, с которой работал на проекте, — адаптирует модель для большего числа случаев и тестов.
Описание разработанного алгоритма проверки
Архитектура решения будет следующей: мы заведём несколько виртуальных потоков, выполняющих операции над тестируемой структурой данных. Каждый виртуальный поток — это последовательность ассемблерных инструкций, это не физический тред ОС. Будем исполнять их на одном физическом треде ОС, чередуя и переключая виртуальные потоки. К примеру, исполнить пять ассемблерных инструкций из первого виртуального потока, потом две ассемблерные инструкции из второго виртуального потока, одну ассемблерную инструкцию из третьего виртуального потока, снова переключимся на первый и так далее — такой способ чередования операций повсеместно используется при анализе конкурентных и распределённых алгоритмов.
Предположим, есть два виртуальных потока. Первый будет исполнять следующие инструкции:
А второй — вот такие:
Тогда следующее исполнение будет одним из примеров допустимого чередования инструкций этих двух потоков, но не единственным:
Исполнение ниже — тоже пример допустимого чередования:
Плюс последовательного исполнения операций в одном треде ОС в том, что оно строго детерминировано. Если однажды запуск пяти инструкций из второго виртуального потока и четырёх инструкций из первого привели к ошибке, то они будут приводить к той же самой ошибке и при дальнейших запусках (вынесем за скобки вопрос недетерминизма в коде тестируемой структуры).
Проблема в том, что язык C++ не предоставляет возможности исполнить несколько (одну, две, три) ассемблерных инструкций — он может исполнить только целую функцию. Значит, необходимо разработать такой механизм. Базово он будет работать следующим образом: тестируемая функция превращается в корутину — ведь корутины могут прерывать своё исполнение, а потом продолжать его с того же места, на котором прервались. Затем мы после каждой интересующей нас ассемблерной инструкции вставляем оператор прерывания корутины co_yield. Этот оператор прерывает исполнение тестируемой функции, возвращая управление вызывающему коду таким образом, что потом можно продолжить исполнение с инструкции, следующей за co_yield.
Теперь покажем, что будет с кодом ниже после этой операции:
Он превратится в следующий код:
Это позволит нам исполнять столько ассемблерных инструкций, сколько мы захотим. Например, исполнить только x := ATOMIC_READ(Variable), не исполняя ATOMIC_WRITE(Variable, y), и исполнить код другого виртуального потока между операциями чтения и записи — как на примере ниже.
Код нашей тестирующей системы будет всё это вызывать. Он будет работать следующим образом:
Придумываем несколько функций с аргументами:
Push(3),Pop(),Pop(),Push(5), и так далее, виртуальными потоками будут ассемблерные инструкции кода этих функций.Нужно выбрать один виртуальный поток и исполнить его либо до следующего
co_yield, либо до завершения (кончились инструкции, исполнение функции завершено).Если произошёл
co_yield, просто выберем другой (или тот же самый) виртуальный поток и продолжим его исполнение.Если функция завершилась, дадим этому виртуальному потоку исполнять другую функцию (придумаем функцию и аргументы для неё).
Когда надоест, перестаём давать виртуальным потокам новые функции и дожидаемся их завершения.
После завершения этой процедуры нам известна последовательность, в которой каждый поток вызывал функции тестируемой структуры данных, аргументы этих функций, а также их возвращаемые значения. Такая последовательность может быть проверена на корректность в конкурентной среде: мы проверяем истории обычных структур данных на линеаризуемость, а дуальных структур данных — на дуальную линеаризуемость.
Важно отметить, что код тестирующей системы должен быть особым образом адаптирован для тестирования дуальных структур данных. Например, у нас есть изначально пустой канал ch и два виртуальных потока, первый из которых выполняет операцию взятия элемента из канала x := ch.Take(), а второй — операцию добавления элемента в канал ch.Put(42). Пусть первой начинает исполняться операция взятия элемента из канала x := ch.Take(). В ходе исполнения этой операции первый виртуальный поток понимает, что в канале нет элементов, и возвращает управление коду тестирующей системы. Теперь тестирующая система не должна передавать управление коду первого виртуального потока до тех пор, пока в канал не будет вставлен элемент 42, так как операция x := ch.Take() блокирует исполняющую её корутину до появления в канале хотя бы одного элемента. Передача управления коду первого виртуального потока до появления в канале хотя бы одного элемента может нарушить инварианты реализации функции Take. Представить подробное описание алгоритма запуска и проверки мы планируем в отдельной статье.
Заметим, что теперь мы можем перебрать вообще все варианты чередования виртуальных потоков. Для двух инструкций из двух потоков это варианты:
Благодаря этому мы можем гарантировать, что никакое исполнение не будет некорректным. Чтобы ограничить пространство перебора, мы можем ограничить суммарное число исполняемых системой функций: например, запустим три виртуальных потока, каждый из которых исполнит по десять функций. Похожий алгоритм реализует TLA+. Такая методология проверки всех возможных исполнений в заданных ограничениях называется Bounded Model Checking.
К сожалению, наша верификация всё равно не может гарантировать отсутствие бага. Может быть, баг проявится на пяти виртуальных потоках, каждый из которых исполнит по сто операций. Но, будучи исполненной в разумных ограничениях (для достаточно большого числа виртуальных потоков и операций), верификация значительно повышает нашу уверенность в собственном коде. Мы круглосуточно перебираем исполнения в поисках ранее не обнаруженных проблем, резко уменьшая возможность выхода багов в прод.
На практике мы работаем не медленнее Lincheck — практической state-of-the-art системы верификации для конкурентных структур данных на языке Java. Мы выложим решение в open source, когда окончательно доведём его до ума.
Результаты и практическое применение
Мы подвели итоги проекта в конце июня, и от него уже есть практическая польза: мы верифицировали некоторые структуры из нашей библиотеки и в большинстве проверенных структур ошибок не нашли. Значит, скорее всего, их там нет. В одной из проверенных структур — очереди, относящейся к планировщику корутин, — нашли баг и исправили его. Баг в конкурентных структурах данных исправлять не так сложно, когда он стабильно воспроизводится нашим верификатором, а не выступает гейзенбагом, который воспроизвёлся однократно, а потом перестал. Теперь мы сильно повысили свою уверенность, что при выкладке кода сбоя не будет. Другие решения лаборатории ещё проходят апробацию. Пока планируем публикацию материалов в научных сборниках и участие в конференциях.
24 июня мы организовали выпускной для участников второй лаборатории, который прошёл в офисе ВКонтакте у Красного моста. Студенты делились техническими деталями своих проектов, а разработчики ВКонтакте задавали им уточняющие вопросы. Некоторые из выпускников станут нашими коллегами — один уже получил офер.
А мы обдумываем планы на продолжение исследований:
ускорять верификацию с помощью параллелизации проверки исполнения на линеаризуемость;
научиться работать со слабыми моделями памяти;
искать баги в open-source библиотеках с примитивами конкурентного программирования на C++;
минимизировать проблемное исполнение, например, как в github.com/flyingmutant/rapid;
научиться тестировать более сложные алгоритмы, управляющие жизненным циклом собственных корутин — например, RPC-сервер, запускающий собственные корутины для работы с каждым из клиентских сокетов.
