\[ \def\ABORT{\mathsf{ABORT}} \def\ACCEPT{\mathsf{ACCEPT}} \def\ACCEPTACK{\mathsf{ACCEPT\_ACK}} \def\act{\mathsf{act}} \def\ballot{\mathsf{ballot}} \def\certify{\mathsf{certify}} \def\client{\mathsf{client}} \def\COMMIT{\mathsf{COMMIT}} \def\committed{\mathsf{committed}} \def\coord{\mathsf{coord}} \def\dec{\mathsf{dec}} \def\DECIDED{\mathsf{DECIDED}} \def\decide{\mathsf{decide}} \def\DECISION{\mathsf{DECISION}} \def\decision{\mathsf{decision}} \def\FOLLOWER{\mathsf{FOLLOWER}} \def\follower{\mathsf{follower}} \def\l{\mathcal{l}} \def\LEADER{\mathsf{LEADER}} \def\leader{\mathsf{leader}} \def\D{\mathcal{D}} \def\next{\mathsf{next}} \def\Obj{\mathsf{Obj}} \def\P{\mathcal{P}} \def\phase{\mathsf{phase}} \def\PREPARE{\mathsf{PREPARE}} \def\PREPARED{\mathsf{PREPARED}} \def\PREPAREACK{\mathsf{PREPARE\_ACK}} \def\proc{\mathsf{proc}} \def\RECOVERING{\mathsf{RECOVERING}} \def\S{\mathcal{S}} \def\shards{\mathsf{shards}} \def\START{\mathsf{START}} \def\status{\mathsf{status}} \def\T{\mathcal{T}} \def\txn{\mathsf{txn}} \def\Val{\mathsf{Val}} \def\Ver{\mathsf{Ver}} \def\vote{\mathsf{vote}} \]
摘要
原子事务提交（ACP）是一个和一致性相似的单次协议问题，旨在模拟易出错的分布式系统的事务提交协议属性。我们认为，ACP 限制太多以至于不能捕获现代事务数据存储的复杂性，其中提交协议和并发控制集成，并且他们对不同事务的执行是相互依赖的。作为替代方案，我们引入了传输认证服务（TCS），一个新的正式问题，它通过集成的并发控制来捕获多发事务提交协议的安全保证。TCS 由可实例化的认证函数参数化，以支持常见的隔离级别，如可串行化和快照隔离。然后，我们推导出一个可证明正确性的弹性崩溃协议，用于通过连续改进来实现 TCS。我们的协议比主流方法实现了更好的时间复杂度，主流方法在 Paxos 风格的复制之上分两阶段提交。
概论
现代数据存储通常被需要管理大量数据，同时为用户提供严格的事务保证。它们通过将数据划分为独立管理的分片和容错性来实现可伸缩性，方法是在一组服务器上复制每个分片。实现这样的系统需要复杂的协议来确保分布式事务满足通常称为 ACID 的所需属性的组合：原子性，一致性，隔离性和持久性。
传统上，分布式计算文献将实现这些属性的方法抽象为单独的问题：特别是保证原子性的原子提交问题（ACP）和保证隔离性的并发控制（CC）。ACP 正式化作为一个一次性协议问题，其中涉及事务的多个分片需要就其最终结果作出决策：如果所有分片都投票提交，则决策提交，否则放弃。并发控制负责确保全局历史符合所需的隔离级别。在典型的实现中，每个分片跟踪事务访问的本地对象，并根据本地观察到的与其他活动事务的冲突确定其对事务结果的投票（提交或放弃）。虽然 ACP 和 CC 都必须在任何现实的事务处理系统中解决，但它们在现有文献中被视为不相交的。特别是，ACP 的解决方案将投票视为问题的输入，并把与负责产生投票的 CC 进行交互这件事遗留在问题范围之外。
然而，这种分离过于简单，无法捕捉到许多实际实现的复杂性，其中提交协议和并发控制紧密集成，因此可能会以微妙的方式相互影响。例如，考虑经典的两阶段提交（2PC）协议，用于解决可靠进程之间的 ACP。事务处理系统通常为每个事务执行一个 2PC 实例。当管理分片 \(s\) 的进程 \(p_i\) 收到一个事务 \(t\) 时，它会执行一个本地并发控制检查并相应地投票提交或中止 \(t\)。不同进程的投票 \(t\) 被聚合，然后最终决定分发给所有进程。如果 \(p_i\) 投票支持 \(t\)，只要它不知道对 \(t\) 的最终决定，它就必须保守地假定 \(t\) 已提交。这可能会导致 \(p_i\) 在另一个 2PC 实例中为与 \(t\) 冲突的事务 \(t'\) 投票中止，即使最终 \(t\) 被中止。在这种情况下，一个 2PC 实例（对于 \(t'\)）的结果取决于另一个实例（对于 \(t\)）执行的内部结构和使用的并发控制策略。
目前，缺乏一个正式的框架来捕捉实际实现的这些复杂方面使得它们难以理解和证明。在本文中，我们迈出了弥合这一差距的第一步。我们介绍了事务认证服务（TCS，第 2 节），这是一个新的正式问题，用于捕获具有集成并发控制的多次事务提交协议的安全保证。TCS 暴露了一个简单的接口，允许客户端通过一个返回提交或放弃的 \(\certify\) 请求提交事务以进行认证。TCS 旨在用于具有乐观并发控制的事务处理系统的上下文中，其中首先乐观地执行事务，然后将结果（例如，读取和写入集）提交给 TCS 以进行认证。与 ACP 相比，TCS 对重复调用 \(\certify\) 的数量或其并发性没有任何限制。因此，它自然有助于将事务提交和并发控制之间的交互形式化。为此，TCS 由一个认证函数参数化，该函数封装了所需隔离级别的并发控制策略，例如可串行化和快照隔离。然后通过要求其认证决策与认证功能一致来制定 TCS 的正确性。
我们利用 TCS 开发一个正式的框架，用于构建具有可定制隔离级别的可证明正确的多次事务提交协议。我们框架的核心是一个新的多次两阶段提交协议（第 3 节）。它形式化了经典 2PC 如何与许多实际事务处理系统中的并发控制交互，其方式在提供的隔离级别中是参数化的。该协议还用作派生更复杂的 TCS 实现的模板。我们证明了多次两阶段提交协议正确地实现了具有给定认证功能的 TCS，前提是每个分片使用的并发控制策略与此函数匹配。
接下来，我们提出了一个崩溃容错 TCS 实现，并通过证明它模拟多次 2PC（第 4 节）来确定其正确性。使 2PC 容错的一种常见方法是让每个分片使用复制协议（例如 Paxos）来模拟可靠的 2PC 进程。与最近的工作类似，我们的实现通过将 2PC 和 Paxos 编织在一起来优化该方案的时间复杂度。特别是，我们的协议避免持续复制 2PC 协调者，以换取协调者单方面中止事务的能力。反过来，这允许消除普通容错 2PC 中所需的 Paxos 一致性，以在分片上保留对事务的最终决策：如果发生故障，可以从分片的当前状态重建决策。与以前遵循相同设计的协议相比，我们的协议在隔离级别上是通用的，并且经过严格证明是正确的。因此，它可以作为未来分布式事务提交实现的参考解决方案。此外，我们协议的一个变体具有与一致性和非阻塞原子提交的下限相匹配的时间复杂度。
我们协议的一个特性使得证明其正确性变得特别微妙，即避免就事务的最终决策达成共识，而是将决策异步传播到相关的分片副本。这意味着不同的分片副本可能在不同的时间收到决策，因此它们的状态可能不一致。为了解决这个问题，在我们的协议中，投票由单个分片领导者根据可用的信息在本地计算； 其他进程仅存储投票。这种被动复制方法在设计从领导者故障中恢复的方式并证明其正确性时要小心。
事务确认服务（TCS）
接口
事务认证服务 （TCS）接受来自 \(\T\) 的事务并从 \(\D = \{ \ABORT, \COMMIT\}\) 产生决策。客户端使用两种类型的操作与 TCS 交互：形式为 \(\certify(t)\) 的认证请求，其中 \(t \in \T\)，以及形式为 \(\decision(t, d)\) 的响应，其中 \(d \in \D\)。
在本文中，我们关注使用（向后）乐观并发控制的事务处理系统。因此，我们假设提交给 TCS 的事务包括其乐观执行产生的所有信息。例如，考虑一个事务系统管理集合 \(\Obj\) 中具有集合 \(\Val\) 中的值的对象，其中事务可以对对象执行读取和写入。这些对象与一个完全有序的版本集合 \(\Ver\) 相关联，该集合具有一个可区分的最低版本 \(v_0\)。那么提交给 TCS 的每个事务 \(t\) 可能与以下数据相关联：
- 读集 \(R(t) \subseteq \Obj \times \Ver\)：\(t\) 读取的对象及其版本的集合，每个对象包含一个版本。
- 写集 \(W(t) \subseteq \Obj \times \Val\)：\(t\) 写入的具有其值的对象集合，其中每个对象包含一个值。我们要求任何写入的对象也已被读取：\(\forall (x, \_) \in W(t).(x, \_) \in R(t)\)。
- 提交版本 \(V_c(t) \in \Ver\)：分配给 \(t\) 写入的版本。我们要求此版本高于读取的任何版本：\(\forall(\_,v) \in R(t).V_c(t)>v\)。
认证函数
TCS 由认证函数 \(f:2^{\mathcal{T}} \times \mathcal{T} \to \mathcal{D}\) 参数化，该函数封装了所需隔离级别的并发控制策略。结果 \(f(T, t)\) 是给定先前提交的事务 \(T\) 的集合对事务 \(t\) 的决策。我们要求 \(f\) 在以下意义上是分布式的：
\[ \forall T_1, T_2, t. f(T_1 \cup T_2, t) = f(T_1, t) \sqcap f(T_2, t) \tag 1 \]
其中操作符 \(\sqcap\) 定义如下：\(\COMMIT \sqcap \COMMIT= \COMMIT\) 并且对任何 \(d\)，\(d \sqcap \ABORT = \ABORT\) 这个要求是合理的，因为 \(f(T, t)\) 的通用定义分别检查 \(t\) 是否与 \(T\) 中的每个事务发生冲突。
例如，给定上述事务域，以下认证函数封装了可串行化的经典并发控制策略： \(f(T, t) = \COMMIT\) 当且仅当 \(t\) 读取的版本都没有被 \(T\) 中的事务覆盖，即，
\[ \forall x,v.(x,v) \in R(t) \Rightarrow (\forall t'. \in T.(x, \_) \in W(t') \Rightarrow Vc(t') \le v). \tag 2 \]
快照隔离 (SI) 的认证函数类似，但将认证检查限制在事务 \(t\) 写入的对象：\(f(T, t) = \COMMIT\) 当且仅当
\[ \forall x,v.(x,v) \in R(t) \wedge (x, \_) \in W(t) \Rightarrow (\forall t' \in T.(x, \_) \in W(t') \Rightarrow V_c(t') \le v). \tag 3 \]
很容易检查认证函数 (2) 和 (3) 是分布式的。
历史
我们使用历史来表示 TCS 执行——验证和决定动作的有限序列，使得每个事务最多出现一次作为 \(\certify\) 的参数，并且每个决定动作都是对前一个验证动作的响应。对于历史 \(h\)，我们让 \(\act(h)\) 是 \(h\) 中的动作集合。对于动作 \(a\)，\(a' \in \act(h)\)，当 \(a\) 出现在 \(h\) 中的 \(a'\) 之前，我们写 \(a \prec_h a'\)。如果其中的每个 \(\certify\) 动作都具有匹配的 \(\decide\) 动作，则历史 \(h\) 是完整的。如果一个完整的历史由连续的 \(\certify\) 和匹配 \(\decide\) 动作对组成，则该历史是连续的。如果 \(h\) 包含 \(\decision(t, \COMMIT)\)，则事务 \(t\) 在历史 \(h\) 中提交。我们用 \(\committed(h)\) 表示 \(h\) 到对应在 \(h\) 中提交的事务的动作的投影。对于完整的历史 \(h\)，\(h\) 的线性化 \(\mathcal{l}\) 是一个顺序历史，使得：
- \(h\) 和 \(l\) 包含相同的动作
- \(\forall t, t'. \decide(t,\_) \prec_ h \certify(t') \Rightarrow \decide(t, \_) \prec_l \certify(t').\)
TCS 正确性
一个完整的序列历史 \(h\) 对于一个认证函数 \(f\) 是合法的，如果它的证明决定是根据 \(f\) 计算的： \(\forall a = \decide(t, d) \in \act(h). d = f(\{t' \mid \decide(t', \COMMIT) \prec_h a \}, t).\)
如果 \(h \mid \committed(h)\) 具有合法的线性化，则历史 h 关于 f 是正确的。如果所有历史记录都是正确的，则 TCS 实现对于 \(f\) 是正确的。
使用 TCS 规范
可以在事务处理系统 (TPS) 中轻松使用正确的 TCS。例如，考虑前面定义的事务域。基于乐观并发控制的典型 TPS 将确保提交的认证事务读取数据库中已经存在的版本。形式上，这意味着对于由 TCS 接口的动作引起的每个历史 \(h\)，该命题成立：如果 \(t\) 是一个事务，使得 \(\certify(t)\) 发生在 \(h\) 中，并且 \((x,v) \in R(t)\)，那么存在一个事务 \(t'\) 使得 \((x, \_) \in W(t') \wedge V_c(t') = v\)，并且 \(h\) 在 \(\certify(t)\) 之前包含了 \(\decision(t , \COMMIT)\)。很容易看出，这意味着如果 \(h\) 对于可序列化性 (2) 的认证函数是正确的，那么按照 \(h\) 的合法线性化的规定，对提交的事务进行排序会产生正确的序列历史：由事务 \(t\) 读取的每个对象的值是由最近的先前事务写入该对象的值。因此，关于认证功能（2）正确的 TCS 确实可以用于实现 可序列化的 TPS。
多次 2PC 和本地分片认证函数
我们现在展示经典两阶段提交 (2PC) 协议的多次版本，它是每个分片使用的并发控制策略中的参数。然后，我们证明该协议实现了由给定认证函数参数化的正确事务认证服务，前提是每个分片的并发控制与该函数匹配。与 2PC 一样，我们的协议假设过程可靠。在下一节中，我们通过证明它模拟多次 2PC 的行为来确定允许崩溃的协议的正确性。
系统模型
我们考虑一个由一组进程 \(\P\) 组成的异步消息传递系统。在本节中，我们假设进程是可靠的，并且通过可靠的 FIFO 通道连接。我们假设一个函数 \(\client: \T \to \P\) 确定发出给定事务的客户端进程。系统管理的数据从集合 \(\S\) 中被划分为分片。一个函数 \(\shards: \T→ 2^\S\) 确定需要证明给定事务的分片集合，通常是存储事务访问的数据的分片。每个分片 \(s \in \S\) 由进程 \(\proc(s) \in \P\) 管理。为简单起见，我们假设分片和进程之间存在一对一的映射。我们有时将 \(\proc\) 应用于一组分片，以获得管理它们的一组进程。
一般情况协议
我们在图 1 中给出了协议的伪代码，并在图 2a 中说明了它的消息流。图 1 中的每个处理程序都是原子执行的。
1 | |
为了验证事务 \(t\)，客户端在 \(\PREPARE\) 消息中将其发送到相关分片（第 6 行）。管理分片的进程将收到的所有事务安排到一个总的认证订单中，存储在一个数组 \(\txn\) 中；\(\next\) 变量指向数组中最后一个填充的插槽。收到事务 \(t\)（第 8 行）后，进程将 \(t\) 存储在 \(\txn\) 的下一个空闲槽中。该进程还计算其投票，说明是 \(\COMMIT\) 还是 \(\ABORT\) 事务，并将其存储在数组 \(\vote\) 中。我们按照以下方式解释投票计算；直观地说，投票是由事务 \(t\) 是否与之前收到的事务冲突来决定的。在管理分片 \(s\) 的进程收到 \(t\) 后，我们说 \(t\) 在 \(s\) 处准备好。该进程在数组 \(\phase\) 跟踪事务状态，其条目最初存储 \(\START\)，一旦事务准备好，就会更改为 \(\PREPARED\)。准备好事务 \(t\) 后，该过程发送一个 \(\PREPAREACK\) 消息，其中包含其在认证顺序中的位置和给 \(t\) 的协调者的投票。该过程由该函数确定： \(\coord: \T \to \P\) 使得 \(\forall t.\coord(t) \in \proc(\shards(t))\)。
事务 \(t\) 的协调者一旦从其每个分片 \(s\) 接收到针对 \(t\) 的 \(\PREPAREACK\) 消息就会采取行动，该消息携带 \(s\) 的投票 \(d_s\)（第 14 行）。协调者使用 \(\sqcap\) 算子（第 2 节）计算关于 \(t\) 的最终决定，并将其以 \(\DECISION\) 消息的形式发送给客户端和所有相关分片。当进程接收到事务的决定时（第 18 行），它将决定存储在 \(\dec\) 数组中，并将事务的阶段推进到 \(\DECIDED\)。请注意，我们不允许协调者单方面中止事务：这可以最大限度地减少我们在第 4 节中介绍的协议的容错版本中的延迟。
投票计算
管理分片 \(s\) 的进程将投票计算为两个分片本地认证函数 \(f_s:s^{\T} \times \T \to \D\) 和 \(g_s:s^{\T} \times \T \to \D\) 的结合。与第 2 节的认证函数不同，分片本地认证函数仅用于检查由 \(s\) 管理的对象上的冲突。他们将已经决定在分片上提交的事务集以及仅准备提交的事务集作为第一个参数（第 11 行）。我们要求上述函数是分布式的，类似于（1）。
例如，考虑第 2 节中给出的事务模型。并假设对象集 \(\Obj\) 在分片之间进行分区：\(\Obj = \uplus _{s \in \S} \Obj_s\)。那么为可串行化定义分片本地认证函数的一种可能方法如下：\(f_s(T, t) = \COMMIT\) 当且仅当：
\[ \forall x \in \Obj_s . \forall v.(x, v) \in R(t) \Rightarrow (\forall t' \in T.(x,\_)\in W(t') \Rightarrow V_c(t') \le v), \tag 4 \]
并且 \(g_s(T, t) = \COMMIT\) 当且仅当：
\[ \forall x \in \Obj_s. \forall v. \\ ((x, \_)\in R(t) \Rightarrow (\forall t' \in T.(x,\_)\notin W(t'))) \wedge \\ ((x, \_)\in W(t) \Rightarrow (\forall t' \in T.(x,\_)\notin R(t'))) \tag 5 \]
遗忘和回忆决策
图 1 中的协议在 21 行和 24 行有两个额外的函数，它们并不确定性地执行。在第 4 部分我们将展示，这些是为了抽象协议能够捕捉乐观容错 TCS 实现的行为。因为进程被破坏，这些执行可能临时丢失和最终决策有关的信息，并且之后从相关的分片的投票重构它。同时，正如我们之前解释过的，决策的丢失可能影响到一些投票计算。21 行的函数遗忘某一事务的决策（而不是投票）。24 行的函数允许进程向协调者重新发送他们知道的投票，这些协调者之后会重新发送最终决策（14 行）。这让遗忘决策的进程从相关分片存储的投票重构它。
正确性
如果 \(f_s\) 和 \(g_s\) 给出的本地分片确认并发控制与（6）-（8）描述的全局认证函数 \(f\) 给出的分片不可知并发控制相关，下面的定理确定了多次 2PC 的正确性。
定理略。
容错提交协议
系统模型
我们现在通过允许进程因崩溃而失败（即永久停止执行）来削弱上一节的假设。 我们仍然假设进程是通过可靠的 FIFO 通道连接的，在以下意义上：消息按 FIFO 顺序传递，并且非故障进程之间的消息保证最终传递。 每个分片 \(s\) 现在由一组 \(2k+1\) 个进程管理，其中最多 \(k\) 个可能失败。我们称这组中的一组 \(k+1\) 个进程为 \(s\) 的法定人数。对于一个分片 \(s\)，我们将 \(\proc(s)\) 重新定义为管理此分片的一组进程。为简单起见，我们假设管理不同分片的进程组是不相交的。
一般协议
在上述模型中实现 TCS 的一种直接方法是使用状态机复制使分片模拟多次 2PC 中的可靠过程； 这通常基于共识协议，例如 Paxos。在这种情况下，永远不会忘记事务的最终决定，因此不会模拟第 21 行和第 24 行的处理程序。尽管这种方法被多个系统使用，但多名研究人员观察到，由此产生的协议需要大量不必要的消息延迟。即，图 2a 中的多次 2PC 的每个动作都需要额外往返同一分片中的一组进程以保持其效果，从而产生图 2b 中的消息流图。 请注意，协调者的操作也必须被复制，因为如果协调者宕机，多次 2PC 将阻塞。生成的协议需要 7 次消息延迟，客户端才能了解事务决策。
优化的协议概述
在图 5 中，我们给出了一个提交协议，该协议通过将跨分片的多次 2PC 和每个分片内的类 Paxos 协议编织在一起来减少消息延迟的数量。 我们从代码中省略了与消息重传相关的细节。我们在图 2c 中说明了协议的消息流，并在图 6 中总结了其正确性证明中使用的关键不变量。
一个进程维护与多次 2PC 协议中相同的变量（图 1）和一些额外的变量。 分片中的每个进程要么是分片的领导者，要么是追随者。 如果领导者失败，则其中一个追随者接管。\(\status\) 变量记录进程是 \(\LEADER\) 状态、\(\FOLLOWER\) 状态，还是处于领导者更改期间使用的特殊 \(\RECOVERING\) 状态。 使用整数 \(\ballot\) 表示特定进程充当领导者的一段时间。 对于 \(b \ge 1\) 的选票，进程 \(\leader(b) = ((b - 1) \mod (2 f + 1))\) 是选票的领导者。我们使用整组整数作为选票，因为给定的进程可能多次扮演领导者的角色。 在任何给定时间，一个进程都参与一个单一的投票，该投票存储在一个变量 \(cballot\) 中并且永远不会减少。在领导者更换期间，我们还使用额外的选票变量 \(\ballot\)。
与图 2b 中所示的一般协议不同，我们的协议不执行共识以将 \(\DECISION\) 消息的内容持久保存在分片中。相反，事务的最终决定被异步发送给每个相关分片的成员。这意味着不同的分片成员可能会在不同的时间收到关于事务的决定。由于对事务的最终决定会影响在认证顺序中跟随它的事务的投票计算（第 3 节），因此在不同的分片成员上计算对后续事务的投票可能会产生不同的结果。为了解决这个问题，在我们的协议中，只有领导者构建认证顺序并计算投票。追随者是被动的：他们只是复制领导者的决定。一旦分片的领导者收到最终决定，就会在分片的投票计算中考虑它。
无故障案例
为了验证事务 \(t\)，客户端在 \(\PREPARE\) 消息中将其发送到相关分片（第 10 行）。 进程 \(p_i\) 仅在它是其分片 \(s_0\) 的领导者时才处理消息（第 12 行）。 我们推迟描述当另一个进程 \(p_j\) 正在向 \(p_i\) 重新发送 \(\PREPARE\) 消息（第 13 行）以及 \(p_i\) 过去已经收到 \(t\) 时（第 15 行）的情况。
在接收到 \(\PREPARE(t)\) 后，领导者 \(p_i\) 首先确定一个进程 \(p\)，它将作为 \(t\) 的协调者。如果领导者第一次收到 \(t\)（第 17 行），那么与多镜头 2PC 类似，它附加 \(t\)到认证订单并根据本地可用信息计算投票。领导者接下来执行 Paxos 的“阶段 2”的类似操作，试图说服其分片 \(s_0\) 接受它的提议。为此，它向 \(s_0\) 发送 \(\ACCEPT\) 消息（包括它自己，为了统一），这类似于 Paxos 的“2a”消息（第 23 行）。该消息携带领导者的选票、事务 \(t\)、它在认证顺序中的位置、投票和 \(t\) 的协调者的身份。领导者代码确保图 6 中的不变量 1：在给定的选票 b 中，可以将唯一的事务-投票对分配给认证顺序中的插槽 \(k\)。
只有当一个进程参与相应的投票（第 25 行）时，它才会处理 \(\ACCEPT\) 消息。如果进程之前没有听说过 \(t\)，它会存储事务和投票，并将事务的阶段推进到准备就绪。然后它向 \(t\) 的协调器发送 \(\ACCEPTACK\) 消息，类似于 Paxos 的“2b”消息。这确认该过程已接受事务和投票。追随者的认证顺序始终是追随者所在选票的领导者的认证顺序的前缀，如不变量 2 所示。当追随者接收到 \(\ACCEPT\) 消息时，由于通道的 FIFO 排序，该不变量被保留。
事务 \(t\) 的协调者一旦从它的每个分片 \(s \in \shards(t)\) 接收到 \(t\) 的 \(\ACCEPTACK\) 消息的法定人数就会采取行动，这些分片携带 \(s\) 的投票 \(d_s\)（第 31 行）。协调器计算关于 \(t\) 的最终决策，并将其在 \(\DECISION\) 消息中发送给客户端和每个相关分片。当一个进程收到一个事务的决定时（第 35 行），该进程将它存储起来并将事务的阶段推进到决定。请注意，与第 3 节中的多镜头 2PC 协议一样。协调者不能单方面中止事务。一旦事务的最终决定被传递给分片的领导者，它就会在该分片的未来投票计算中被考虑在内。以可序列化（4）和（5）的分片本地函数为例，如果写入对象 \(x\) 的事务最终决定中止，那么将此决定传递给领导者可能会允许另一个写入 \(x\) 的事务提交。
领导者恢复
协调者恢复
优化
协议正确性
相关工作
结论
在本文中，我们迈出了在现代事务处理系统中构建分布式事务提交理论的第一步，该理论捕获了原子提交和并发控制之间的交互。我们提出了一个事务认证服务的新问题，以及一个在可靠进程之间解决它的抽象协议。由此，我们系统地推导出了一个可证明正确的优化容错协议。
