Привет, Хабр! В команде ВКонтакте существует система управления репликацией и консенсусом в кластере, которая называется BARSiC (Binary Asynchronous Replication with Simple Consensus). Прежде всего она контролирует состав кластера, определяя, кто реплика, а кто — мастер. А при выходе мастера из строя реплики выбирают нового с непротиворечивой линейной историей.
Для решения этой задачи команда ВКонтакте совместно с университетом ИТМО работали над научно-исследовательским проектом «Разработка моделей для верификации распределенных алгоритмов в системе BARSiC». В этой статье подробно расскажем о том, как мы в рамках проекта верифицировали выбранный для BARSiC алгоритм, и попутно исправили найденную в нём ошибку.
Как появился BARSiC?
ВКонтакте повсеместно используются движки — специализированные базы данных, где хранится вся информация, загруженная пользователями на сайт. Это фотографии, комментарии, лайки, посты, а также много разной служебной информации. Так вот — для хранения всего этого у нас есть около 50 видов движков, которые занимают почти 800 кластеров.
С ростом объёмов данных у нашей команды появилась задача повышения отказоустойчивости кластеров. Для этого мы начали разрабатывать координатор распределённой системы — внешнюю систему, которая будет контролировать репликацию и выборы мастера. У нас используется репликация master-slave, и переключение на новый мастер происходило в ручном режиме. В то время как алгоритм консенсуса позволяет избежать простоя при переключении.
Мы рассматривали разные алгоритмы консенсуса. Сразу отказались от популярных решений Paxos и Raft. Остановились на алгоритме ViewStamped Replication, описанном в работах Барбары Лисков (1, 2 — обе статьи в соавторстве), и модифицировали его. Например, адаптировали для работы в реальных условиях: поддержали корректность неатомарной работы с персистентным состоянием, переработали выбор мастера, добавили некоторые свойства для обеспечения необходимой нам задержки и прочие оптимизации.
У алгоритма не было формальной верификации — ни авторской, ни сторонней. А мы хотели убедиться, что этот протокол консенсуса является непротиворечивым и формально верным, и что наши изменения не ухудшили его. Проверка была важнейшим бизнес-требованием, потому что выбор консенсуса — один из главных инструментов для обеспечения отказоустойчивости движков и репликации данных. Ведь мы не можем себе позволить потерять пользовательские данные. Поэтому мы подошли к делу основательно: использовали прикладные проверки на корректность — различные фазинг-тестирования и интеграционные тесты, — а также верифицировали модель на TLA+. К слову, не так много протоколов, баз данных и алгоритмов проходят подобную проверку.
Сотрудничество с ИТМО
С одной стороны, задача верификации — академическая. С другой, у нас не было ресурсов, чтобы этим заняться. Поэтому мы обратились за помощью к нашему давнему партнёру, университету ИТМО. У нас уже были налажены контакты с руководителем научно-исследовательской лаборатории Виталием Аксёновым, и исторически сложилось так, что в программе работает много выходцев, студентов или преподавателей из ИТМО. Поэтому мы знали, что проект будет вестись грамотно и с отличным результатом.
Исследования
Работу над проектом начали в ноябре 2022 года. Для начала провели несколько установочных встреч с командой ИТМО, где рассказали друг другу, что у нас есть и почему нам важно доказательство корректности.
Мы ещё не знали, сколько у нас будет проектов и участников. Сначала планировали поставить на эту тему одного человека, потом ей заинтересовались ещё двое. Число задач и направлений постоянно увеличивалось, и мы выбирали такой объём, который мог быть представлен в виде независимых научных работ, чтобы участники могли получить от проекта максимальную пользу.
Определившись с темами, мы распределили их по участникам и стали прорабатывать. Начали с базового анализа: на этом этапе наши ребята знакомились с инструментами, в первую очередь с TLA+. Кто-то занялся формальным описанием модели на этом языке, кто-то углубился во внутреннее устройство. Спустя какое-то время мы стали лучше понимать задачи и подходы к их решению, и вырисовались три направления работы:
Взять ViewStamped Replication как модель и доказать её корректность. Есть известная научная статья, и хотелось проверить упрощённую и полную модели, о которых там говорится.
Составить спецификацию как общей модели, так и доработанной нами, с оптимизацией неатомарной передачи логов. Нужно было изучить нашу реализацию в коде и проверить её.
Самое интересное с прикладной точки зрения направление: получив на втором этапе модель, нужно было научиться преобразовывать сгенерированное TLA-доказательство в набор тестов на Go, покрывающих все интересные нам исполнения. Это очень важно для тестирования реального кода, потому что описанная на TLA+ модель может отличаться от нашей реализации.
Сначала мы доказали общий алгоритм, а после — перешли к доказательству нашей оптимизированной версии и генерации тестов на реализацию по доказательству. Наконец, круг замкнулся — теперь мы могли утверждать, что корректны и модель, и наша реализация.
Затем мы регулярно встречались с командой и обменивались информацией о том, что каждому из нас удалось сделать на разных этапах проекта. Интересность и сложность была в том, что модель периодически менялась, и меняется до сих пор. Ребята должны были подхватывать изменения и адаптировать их в своей работе. То есть мы построили конвейер между теоретиками и практиками, итеративно проверяя наши гипотезы.
Самым трудным был первый этап, когда никто не понимал, что делать. Какие-то TLA+, формальные верификации и прочее, а дальше и наши знания уже практически заканчивались. Мы примерно понимали, как можно к этому подойти, но практического опыта у нас не было. То есть сложнее всего далось выделение трёх направлений дальнейшей работы.
Вторым по сложности и интересности оказалось третье направление, когда мы из модели делали отображение в код на Go, который прогоняет тесты. Идея была понятна, но как реализовать? Обсудили постановку задачи, разбили её на этапы, поняли, чего хотим достичь. У нас есть модель, которая умеет проверять определённые свойства, и нам нужно составить тесты, которые будут проходить по нашей реализации на Go. То есть нужно было построить граф состояний с помощью TLA+ и покрыть его путями — будущими «тестами». Эффективный алгоритм их построения оказался нетривиальным — мы использовали алгоритм Диница для построения максимального потока и доказали почти-линейную асимптотику времени работы в нашем случае.
Результаты
Мы не стали доверяться воле случая и тщательно проверили «вроде бы надёжный» алгоритм перед использованием в критически важной системе. Сотрудничество нашей компании с исследовательской командой университета дало не только практические результаты, но и помогло усилить научную базу ViewStamped Replication. В итоге мы получили непротиворечивую и корректную модель консенсуса. Попутно нашли ошибку в исходном алгоритме: неконсистентно изменялись данные при изменении состава кластера. Из-за вариативности и сложности исходных условий найти её привычными инструментами в виде фаззера и конвенционного тестирования вряд ли удалось бы. Нам удалось исправить протокол и доказать отсутствие этой проблемы в новой версии.
Другим важным результатом стал выработанный конвейер проверки алгоритма. Теперь, добавляя новые оптимизации в алгоритм консенсуса, мы просто прогоняем его через модель, достраивая её, и проверяем логическую корректность.
Двое из трёх исследователей, трудившихся над проектом, сейчас работают в нашей команде в VK. Один из них продолжит дорабатывать модель на TLA+. В будущем с помощью нашего конвейера проверим ещё ряд сложных алгоритмов, чтобы убедиться, что у нас нет нарушенных инвариантов. И продолжим работать над корректностью, убеждаться в отсутствии ошибок в реализации.
Практическое применение
Проверенный алгоритм ViewStamped Replication сейчас внедрён на тестовых и некоторых production-кластерах. Этот проект обеспечит отказоустойчивость ВКонтакте на уровне ЦОДов: к концу лета внедрим и в критически важных компонентах, в том числе в движке, хранящем сообщения пользователей. Но это далеко не всё: под новый алгоритм мы полностью переработали выбор мастера. Пока что у нас принципиально возможно расхождение данных между мастером репликой. С новой системой появилось понятие коммит-блока: если блок закоммичен, то его уже нельзя откатить. Также там заложена идея блокчейна: у нас идёт цепочка подписей для защиты от изменения случайных данных в середине в случае повреждения диска. Подпись последнего блока является дайджестом от предыдущего блока плюс дайджест его хеш-суммы. То есть в цепочку зашиты хеш-суммы.
Сейчас мы находимся на завершающей стадии, оформляем научные статьи и продолжаем работать над этой темой — переносим формальную модель, описанную на языке TLA+, в инструмент для проверки конкретной реализации на Go.
Наши исследователи расскажут о BARSiC на конференциях SmartData и HighLoad++, приглашаем послушать.