Архитектура сосредоточена на детерминированном последовательном устройстве транзакций, которое упорядочивает операции с использованием Гибридных Логических Часов, а не физического времени, устраняя зависимости от несоответствий часов, присущие системам на основе TrueTime. Координатор реализует вариант протокола Calvin, где намерения транзакций реплицируются у большинства лидеров шардов перед выполнением, обеспечивая сериализуемость благодаря детерминированному планированию, а не распределенной блокировке. Спецификации TLA+ моделируют переходы состояний координатора, формально проверяя, что система поддерживает безопасность (строгую сериализуемость) и жизнеспособность (все завершенные транзакции в конечном итоге завершаются), даже во время частичных сетевых разделений.
Координатор сохраняет журналы транзакций в WAL (Журнал предзаписи) с использованием консенсуса Paxos для долговечности через зоны доступности. Прокси шардов абстрагируют основные движки хранения — будь то PostgreSQL, MongoDB или Cassandra — предоставляя единый интерфейс для исполнительного движка. Обнаружение конфликтов использует граф зависимости, построенный в фазе последовательности, позволяя параллельное выполнение неконфликтующих транзакций, сохраняя эквивалентность к сериализированному порядку.
Глобальный инвестиционный банк требовал миграции своей системы расчетов по сделкам с монолитной базы данных Oracle на шардированную архитектуру, охватывающую регионы AWS и Azure. Критическая задача заключалась в обеспечении атомарных расчетов сделок, которые затрагивали несколько классов активов, хранящихся в различных технологиях баз данных — акции в PostgreSQL и деривативы в ScyllaDB — без развертывания атомных часов или источников времени GPS для синхронизации.
Одно из предложенных решений использовало стандартные транзакции XA с управляемым протоколом двухфазного подтверждения (2PC) с помощью менеджера транзакций Narayana. Этот подход предлагал сильную согласованность и зрелую поддержку экосистемы, но приводил к блокирующему поведению, когда сбой координатора в фазе подготовки оставлял шард с захваченными блокировками на неопределенное время, нарушая требования к жизнеспособности во время нестабильности сети между облаками.
Альтернатива рассматривала паттерн Saga, реализованный через Axon Framework, использующий компенсирующие транзакции для сценариев отката. Хотя это обеспечивало высокую доступность и избегало распределенной блокировки, это жертвовало строгой сериализуемостью — неприемлемой для финансовых расчетов, где промежуточные состояния никогда не должны быть видны, а логика компенсации для необратимых операций на внешних рынках оказалась чрезмерно сложной.
Выбранная архитектура реализовала детерминированный координатор, вдохновленный Calvin, с формальной верификацией TLA+. Система последовательного записи всех расчетных транзакций через реплицируемую конечную машину с использованием Raft для журнала координации, а затем выполняла их в том же порядке на всех шардов, используя идемпотентные хранимые процедуры. Это исключило необходимость в распределенной блокировке во время выполнения и позволило проверку модели TLA+ математически доказать, что система не может застрять или потерять расчеты во время произвольных сетевых разделений.
Внедрение привело к снижению латентности расчетов на 40% по сравнению с устаревшей системой Oracle, одновременно сохраняя полные гарантии ACID по облакам. Во время последующего отключения AWS по всему региону система продолжала обрабатывать сделки без ручного вмешательства, подтверждая формально доказанные свойства жизнеспособности.
В чем основное отличие строгой сериализуемости от линейизуемости и почему координатор распределенных транзакций обычно нацеливается на первое, а не на второе?
Строгая сериализуемость объединяет сериализуемость (транзакции выглядят так, будто выполняются в некотором последовательном порядке) с реальным ограничением линейизуемости (транзакции завершаются до начала последующих). В то время как линейизуемость применяется к операциям с одним объектом, строгая сериализуемость расширяет это на многослойные транзакции. Кандидаты часто путают это, проектируя системы, которые обеспечивают линейизуемость для одного ключа, но не предотвращают аномалии, такие как сдвиг записи между несколькими ключами. Координатор достигает строгой сериализуемости, устанавливая глобальный порядок транзакций — часто через слой последовательности или временной орекл — в то время как линейизуемость может быть выполнена на уровне каждого шарда без гарантий упорядочивания между шардом.
Почему протокол двухфазного подтверждения (2PC) блокируется на неопределенное время во время сбоя координатора и как трехфазное подтверждение (3PC) не решает эту проблему во время сетевых разделений?
В 2PC, как только участник голосует "да" во время фазы подготовки, он удерживает блокировки, пока не получит глобальное решение о подтверждении/отмене от координатора. Если координатор терпит неудачу после получения всех голосов, но до передачи решения, участники остаются в неведении и заблокированными, нарушая доступность. 3PC пытается решить эту проблему, добавляя фазу предварительного подтверждения и основанное на таймаутах продвижение, но в условиях сетевых разделений участник не может различить сбой координатора и его изолированность. Это приводит к сценариям разделения мозга, когда разные разделы принимают противоречивые решения, нарушая согласованность. Основная проблема заключается в том, что невозможность FLP доказывает, что детерминированный консенсус невозможен в асинхронных системах с хотя бы одним неисправным процессом, что означает, что любой протокол подтверждения должен выбирать между блокировкой (безопасностью) и потенциальной несогласованностью (жизнеспособностью) во время определенных режимов сбоя.
Как TLA+ проверяет свойства жизнеспособности в координаторе транзакций и какие конкретные операторы временной логики выражают "в конечном итоге подтверждаются" против "никогда не теряют данные"?
TLA+ использует временную логику для указания того, что хорошие вещи в конечном итоге происходят (жизнеспособность), в то время как плохие вещи никогда не происходят (безопасность). Свойство жизнеспособности, что все инициированные транзакции в конечном итоге завершаются, выражается с использованием оператора в конечном итоге (◇), обычно записываемого как Initiated(t) ~> Committed(t) (ведет к), что означает, что если транзакция t инициируется, она в конечном итоге либо завершится, либо будет отменена. Свойства безопасности, такие как "никогда не теряет данные", используют оператор всегда (□), записываемый как □(Committed(t) ⇒ ◇(Query(t) = Value)), что означает, что однажды подтвержденное значение всегда в конечном итоге будет доступно для чтения. Кандидаты часто упускают, что проверка жизнеспособности требует предположений о справедливости — слабая справедливость (WF_vars(Action)) гарантирует, что если действие остается включенным, оно должно в конечном итоге произойти, предотвращая бесконечное замирание, когда координатор просто перестает выполнять шаги. Без этих ограничений справедливости модели TLA+ теоретически удовлетворяли бы свойствам жизнеспособности, ничем не действуя.