アーキテクチャは、物理時間ではなくハイブリッド論理クロックを使用して操作を順序付ける決定論的トランザクションシーケンサーに基づいており、TrueTimeベースのシステムに固有のクロックスキュー依存を排除します。コーディネーターは、トランザクションのインテントを実行前に過半数のシャードリーダーにレプリケートするカルビンプロトコルのバリアントを実装しており、分散ロックではなく決定論的スケジューリングによって直列性を保証しています。**TLA+**の仕様はコーディネーターの状態遷移をモデル化し、システムが安全性（厳格な直列性）と生存性（すべてのコミットされたトランザクションが最終的に完了する）を維持することを形式的に検証します。
コーディネーターは、WAL（書き込み前ログ）にトランザクションログを保持し、耐久性のあるPaxosコンセンサスを使用して可用性ゾーン全体で耐久性を確保します。シャードプロキシは、基盤となるストレージエンジン（PostgreSQL、MongoDB、またはCassandra）を抽象化し、実行エンジン用に統一されたインターフェースを提供します。競合検出は、シーケンスフェーズ中に構築される依存グラフを使用して、競合のないトランザクションの同時実行を可能にし、直列順序に対して同等性を維持します。
あるグローバル投資銀行は、トレード決済システムをモノリシックなOracleデータベースからAWSおよびAzure地域にまたがるシャーディングアーキテクチャに移行する必要がありました。重要な課題は、異なるデータベース技術に保存されている複数の資産クラスにわたるトレードの原子的な決済を保証することでした。これは、PostgreSQLに株式、ScyllaDBにデリバティブが格納されており、同期のために原子時計やGPSのタイムソースを導入しないことを前提としていました。
提案された解決策の一つは、Narayanaトランザクションマネージャーによって管理される二相コミット（2PC）プロトコルを利用した標準XAトランザクションでした。このアプローチは強い整合性と成熟したエコシステムサポートを提供しましたが、準備段階でコーディネーターの障害が発生すると、シャードが無期限にロックを保持するブロック動作を引き起こし、クロスクラウドのネットワーク不安定性の間に生存性の要件を違反しました。
別の代替案は、ロールバックシナリオのために補償トランザクションを利用したAxon Frameworkを介して実装されたSagaパターンを検討しました。これにより高い可用性が提供され、分散ロックを回避しましたが、厳格な直列性が犠牲となり、これは金融決済にとって受け入れがたいものであり、中間状態は決して観察されるべきではなく、不可逆的な外部市場操作のための補償ロジックは非常に複雑であることが判明しました。
選択されたアーキテクチャは、TLA+の形式検証を伴うカルビン風の決定論的コーディネーターを実装しました。システムは、Raftを使用して調整ログを持つレプリケート状態マシンを介してすべての決済トランザクションをシーケンシングし、次にすべてのシャードで同じ順序で実行されました。冪等ストアドプロシージャを使用することで、実行中の分散ロックの必要が排除され、**TLA+**モデルチェックにより、システムがデッドロックや任意のネットワークパーティション中に決済を失うことができないことが数学的に証明されました。
デプロイメントの結果、従来のOracleシステムに比べて決済のレイテンシが40％削減され、クラウド間での完全なACID保証が維持されました。その後の地域全体のAWS outageの間、システムは手動介入なしにトレードを処理し続け、形式的に証明された生存性の特性を検証しました。
厳格な直列性と線形性の根本的な違いは何であり、なぜ分散トランザクションコーディネーターは通常前者をターゲットにするのか？
厳格な直列性は、直列性（トランザクションはある順序で実行されるように見える）を線形性のリアルタイム制約（トランザクションは次のものが始まる前に完了する）と組み合わせます。線形性が単一オブジェクト操作に適用されるのに対し、厳格な直列性はこれを複数オブジェクトのトランザクションにまで拡張します。候補者はこれらを混同し、単一キーの線形性を確保するシステムを設計しますが、複数のキーにまたがる書き込みスキューのような異常を防ぐことには失敗します。コーディネーターは、グローバルなトランザクションの順序を確立することで厳格な直列性を達成します—これは通常シーケンシングレイヤーやタイムスタンプオラクルを介して行われます—それに対して線形性だけではシャードごとに満たすことができ、シャード間の順序保証はありません。
なぜ二相コミット（2PC）プロトコルはコーディネーターの障害中に無期限にブロックされ、三相コミット（3PC）がネットワークパーティションの下でこれを解決しないのか？
2PCでは、参加者が準備段階で"はい"と投票すると、その参加者はコーディネーターからのグローバルなコミット/アボートの決定を受け取るまでロックを保持します。コーディネーターがすべての投票を受け取った後、決定をブロードキャストする前に障害が発生すると、参加者は不確実なままロックされたままで、可用性が違反されます。3PCは、事前コミット段階とタイムアウトに基づく進行を追加することでこれを解決しようとしますが、ネットワークパーティション中、参加者は失敗したコーディネーターとパーティションされたコーディネーターを区別できず、異なるパーティションが矛盾する決定を下す分裂脳シナリオを引き起こします。根本的な問題は、FLP不可能性が非同期システムにおける決定論的コンセンサスが1つの故障プロセスがあっても不可能であることを証明し、任意のコミットプロトコルは、安全性のためにブロッキング（安全）と、特定の障害モードにおける潜在的不整合（生存性）の間で選択しなければならないことです。
TLA+はトランザクションコーディネーターの生存性特性をどのように検証し、「最終的にコミットする」と「決してデータを失わない」を表す特定の時間論理演算子は何ですか？
**TLA+**は時間論理を使用して、良いことが最終的に起こること（生存性）と悪いことが決して起こらないこと（安全性）を指定します。開始されたトランザクションが最終的に完了するという生存性の特性は、最終的に演算子（◇）を使用して表され、通常はInitiated(t) ~> Committed(t)（リード・トゥ）として書かれ、トランザクションtが開始されると、それは最終的にコミットまたはアボートされることを意味します。データを「決して失わない」といった安全性の特性は、常に演算子（□）を使用し、□(Committed(t) ⇒ ◇(Query(t) = Value))のように書かれ、コミットされると、その値は常に最終的に読み取れることを意味します。候補者はしばしば、生存性チェックには公正性の前提条件が必要であることを見落とします—弱い公正性（WF_vars(Action)）は、アクションが有効であり続ける場合、それは最終的に発生しなければならないことを保証し、コーディネーターが単にステップを停止する無限のスタタリングを防ぎます。これらの公正性制約がない場合、**TLA+**モデルは何もせずに生存性の特性を自明に満たすことができます。