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