该体系结构以一个确定性的事务排序器为中心，它使用混合逻辑时钟来排序操作，而不是物理时间，从而消除TrueTime系统固有的时钟偏移依赖。协调者实现了Calvin协议的变体，其中在执行之前，事务意图被复制到大多数分片领导者，以通过确定性调度而非分布式锁定来确保可串行性。TLA+ 规范对协调者的状态转换进行建模，正式验证系统在部分网络分区期间仍然保持安全性（严格可串行性）和活跃性（所有已提交的事务最终完成）。
协调者使用Paxos共识将事务日志持久化到WAL（预写日志），以确保跨可用区的耐久性。分片代理抽象化底层存储引擎——无论是PostgreSQL、MongoDB 还是 Cassandra——为执行引擎提供统一接口。冲突检测使用在排序阶段构建的依赖图，允许同时执行非冲突事务，同时保持与串行顺序的等价性。
一家全球投资银行需要将其交易结算系统从单体Oracle数据库迁移到跨AWS和Azure区域的分片架构。关键挑战在于确保涉及存储在不同数据库技术中的多个资产类别的交易的原子结算——股权存储在PostgreSQL中，衍生品存储在ScyllaDB中——而无需部署原子时钟或GPS时间源进行同步。
一个提出的解决方案是使用标准XA事务与由Narayana事务管理器管理的两阶段提交（2PC）协议。该方法提供了强一致性和成熟的生态系统支持，但引入了阻塞行为，在准备阶段协调者失败时，分片将无限期地持有锁，从而违反跨云网络不稳定期间的活跃性要求。
另一个备选方案考虑了通过 Axon Framework 实现的Saga模式，利用补偿事务进行回滚场景。虽然这提供了高可用性并避免了分布式锁定，但牺牲了严格可串行性——对于财务结算来说，这是不可接受的，因为中间状态绝不能被观察到，而不可逆的外部市场操作的补偿逻辑证明复杂性过高。
选择的架构实施了一个受Calvin启发的确定性协调者，进行了TLA+形式验证。系统通过使用Raft进行协调日志的复制状态机对所有结算事务进行排序，然后在所有分片上以相同顺序执行它们，使用幂等存储过程。这消除了执行期间对分布式锁定的需要，并允许**TLA+**模型检查数学证明系统在任意网络分区期间不会死锁或丢失结算。
部署结果与遗留的Oracle系统相比，结算延迟减少了40%，同时在多个云中保持全ACID保证。在随后的区域范围AWS停电期间，系统继续处理交易，无需手动干预，验证了形式证明的活跃性特性。
严格可串行性和线性可串行性之间的根本区别是什么，为什么分布式事务协调器通常目标前者而非后者？
严格可串行性结合了可串行性（事务似乎按某种顺序执行）与线性可串行性的实时约束（事务在后续事务开始之前完成）。线性可串行性适用于单对象操作，严格可串行性将其扩展到多对象事务。候选人常常混淆这两者，设计确保单键线性可串行性但未能防止跨多个键的写偏差的系统。协调者通过建立事务的全局顺序来实现严格可串行性——通常通过排序层或时间戳神谕来实现——而单靠线性可串行性可以在每个分片上满足，而无跨分片排序保证。
为什么两阶段提交（2PC）协议在协调器失败期间无限期阻塞，三阶段提交（3PC）如何在网络分区下无法解决此问题？
在2PC中，一旦参与者在准备阶段投票“是”，它持有锁，直到接收到协调者的全球提交/中止决定。如果协调者在收到所有投票后但在广播决定之前失败，参与者将保持不确定和被锁定，违反可用性。3PC试图通过添加预提交阶段和基于超时的进展来解决此问题，但在网络分区下，参与者无法区分失败的协调者和被分区的协调者。这导致了分脑场景，其中不同分区做出相互冲突的决定，违反了一致性。根本问题是FLP不可能性证明在异步系统中，即使是一个故障流程，确定性共识也是不可能的，这意味着任何提交协议必须在某些故障模式中选择阻塞（安全性）和潜在不一致（活跃性）之间进行权衡。
TLA+如何验证事务协调者的活跃性特性，以及具体的时间逻辑运算符如何表达“最终提交”与“从不丢失数据”？
TLA+使用时间逻辑来指定好的事情最终会发生（活跃性），而坏的事情永远不会发生（安全性）。所有发起的事务最终完成的活跃性属性使用最终运算符（◇）表示，通常写成Initiated(t) ~> Committed(t)（导致），意味着如果事务t被发起，它最终将提交或中止。类似“从不丢失数据”的安全属性使用始终运算符（□），写作□(Committed(t) ⇒ ◇(Query(t) = Value))，意味着一旦提交，该值始终可在某个时候被读取。候选人常常忽视活跃性检查需要公平性假设——弱公平性（WF_vars(Action)）确保如果一个行动保持启用，它最终必须发生，防止协调者无限制地停止采取步骤。没有这些公平性约束，**TLA+**模型将通过不采取任何行动轻松满足活跃性属性。