\[ \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\reads{\mathsf{reads}} \def\writes{\mathsf{writes}} \def\Writes{\mathsf{Writes}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \def\RA{\mathsf{RA}} \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{green}{wr}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\VIS{\mathsf{\textcolor{green}{VIS}}} \def\antiVIS{\mathsf{\overline{\VIS^{-1}}}} \def\AR{\mathsf{\textcolor{green}{AR}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{blue}{WW}}} \def\RW{\mathsf{\textcolor{cyan}{RW}}} \def\H{\mathcal{H}} \def\T{\mathcal{T}} \def\X{\mathcal{X}} \def\G{\mathcal{G}} \def\P{\mathcal{P}} \def\Int{\mathtt{Int}} \def\Ext{\mathtt{Ext}} \def\Session{\mathtt{Session}} \def\Prefix{\mathtt{Prefix}} \def\NoConflict{\mathtt{NoConflict}} \def\TotalVis{\mathtt{TotalVis}} \def\PreExecSI{\mathsf{PreExecSI}} \def\Executions{\mathsf{Executions}} \def\modelOf{\mathsf{modelOf}} \def\ExecSI{\mathsf{ExecSI}} \def\ExecSER{\mathsf{ExecSER}} \def\HistSI{\mathsf{HistSI}} \def\HistSER{\mathsf{HistSER}} \def\GraphSER{\mathsf{GraphSER}} \def\GraphSI{\mathsf{GraphSI}} \def\graph{\mathsf{graph}} \def\splice{\mathsf{splice}} \def\DCG{\mathsf{DCG}} \]
摘要
为了实现可扩展性，现代互联网服务通常依赖于分布式数据库，其事务一致性模型比可序列化性要弱。目前，应用程序员通常缺乏确保这些一致性模型的弱点不会违反应用程序正确性的技术。我们提出了一些标准来检查依赖于仅提供弱一致性的数据库的应用程序是否具有鲁棒性，即其行为是否像使用提供可序列化的数据库一样。在这种情况下，应用程序员可以获得弱一致性的可扩展性优势，同时能够轻松检查所需的正确性属性。我们的结果系统而统一地处理了最近提出的几种弱一致性模型，以及一种增强应用程序各部分一致性的机制。
Introduction
为了实现可扩展性和可用性，现代互联网服务通常依赖于大型数据库，这些数据库在大量节点和/或广阔的地理跨度上复制和分区数据（例如，[14、20、26、3、6、4、5、11、22、27、10]）。数据库客户端在任何节点上调用数据事务，节点之间使用消息传递相互传达更改。理想情况下，我们希望这个分布式系统能够提供关于事务处理的强保证，例如可序列化性 [8]：如果这些事务按某种顺序串行执行，则可以获得并发执行一组事务的结果。可序列化性很有用，因为它允许应用程序程序员轻松建立所需的正确性属性。例如，要检查应用程序的事务是否保留给定的数据完整性约束，程序员只需检查每个事务在单独执行时是否都保留了约束，而不必担心并发性。不幸的是，实现可串行化需要数据库节点之间进行过多的同步，这会减慢数据库的速度，甚至在副本之间的网络连接失败时导致数据库不可用 [17, 1]。因此，如今的大型数据库通常提供弱一致性保证，这允许非串行化行为，称为异常。
作为一个激励性的例子，考虑一个玩具在线拍卖应用程序，其交易由图 1 中的交易程序定义。程序 RegUser 创建一个新用户帐户。它操作表 USERS，该表的行包含主键 (uId) 和昵称。只有昵称 uname 未出现在 USERS 中时，RegUser(uname) 的调用才会在 USERS 中插入新行，以确保昵称是唯一的。程序 ViewUsers 可用于查看所有用户。某些数据库 [22, 26, 3] 可能允许执行 RegUser 和 ViewUsers，例如图 2(c) 中所示的那个。RegUser 的两次调用生成事务 T1 和 T2；它们写入两行 USERS，用 x 和 y 表示，以注册用户 Alice 和 Bob。然后程序 ViewUsers() 被调用两次；T3 中的调用看到 Alice 但没有 Bob，而 T4 中的调用看到 Bob 但没有 Alice。这个结果称为长分叉异常，无法通过以任何顺序执行这四个事务来获得，因此是不可序列化的。
过去几年，针对现代大型数据库提出了许多新的事务一致性模型 [22、11、26、3、5]，这些模型的不同之处在于它们通过暴露此类异常来削弱一致性，以换取更好的性能。不幸的是，应用程序程序员通常缺乏确保这些一致性模型的弱点不会违反应用程序正确性的技术。这种情况阻碍了主流数据库开发人员和应用程序程序员采用新的一致性模型。
解决此问题的一种方法是使用应用程序稳健性的概念 [16, 15, 9]。如果应用程序在使用该模型或序列化能力的数据库时表现相同，则该应用程序对特定弱一致性模型具有稳健性。如果应用程序对给定的弱一致性模型具有稳健性，那么程序员就可以获得使用弱一致性的性能优势，同时能够轻松检查所需的正确性属性。
在本文中，我们制定了针对三种最近提出的一致性模型检查应用程序稳健性的标准——因果（又名因果+）一致性（CC）[22]、前缀一致性[11]（PC）和并行快照隔离[26]（PSI，又名非单调快照隔离[3]）。作为我们研究结果的推论，我们还推导出了经典快照隔离模型[6]（SI）的现有稳健性标准[16]。我们的标准还处理一致性模型的变体，这些变体允许应用程序员要求在可序列化性下执行某些事务，从而确保原本不稳健的应用程序的稳健性。
我们利用最近提出的框架 [12] 以声明方式指定其语义（第 2 节），以统一和系统的方式处理上述四种一致性模型。特别是，我们考虑的所有一致性模型都保证事务的原子可见性：事务执行的所有写入操作要么可以被其他事务观察到，要么都不能被观察到。这使我们能够通过从应用程序执行中的事务内部抽象出来，来简化建立稳健性标准所需的推理。我们首先提出一个动态稳健性标准，用于检查给定执行是否可序列化（第 3 节）。我们根据执行的依赖关系图 [2] 制定此标准，描述其事务之间的几种关系：如果执行的依赖关系图不包含某种形式的循环，则执行是可序列化的，我们称之为关键。针对不同一致性模型的稳健性标准在哪些循环被视为关键方面有所不同。然后，我们说明如何将单个执行上的动态稳健性标准提升为静态标准，以检查给定应用程序的所有执行是否可序列化（第 4 节）。
Consistency Model Specifications
我们首先回顾一下 [12] 中数据库计算的正式模型和我们处理的一致性模型的规范。这些规范是声明性的，这大大简化了我们的形式化开发。尽管如此，如 [12] 所示，这些规范相当于某些操作规范，接近于实现。
Dynamic Robustness Criteria
Static Robustness Criteria
Related Work
在数据库环境中，应用程序鲁棒性最早是由 Fekete 等人 [16] 研究的，他们提出了针对快照隔离 (SI) 的鲁棒性标准 [6]。然后，Fekete 将该标准扩展到 SI 数据库，允许程序员为某些事务请求可序列化性 [15]，我们也考虑了这种机制。我们的标准的制定方式与 Fekete 等人的类似，使用依赖图 [2]。然而，与他们的工作相比，我们考虑了更微妙的并行快照隔离、前缀一致性和因果一致性模型，这些模型允许比 SI 更多的异常。我们使用的方法也不同于 Fekete 等人的方法。他们考虑了 SI 的操作规范 [6]，这使得鲁棒性标准的证明高度复杂。相比之下，我们可以从使用声明性规范中受益，通过利用事务的原子可见性 [12] 实现简洁性。这使我们能够更系统地提出鲁棒性标准。
还研究了在常见多处理器和编程语言的弱共享内存模型上运行的应用程序的鲁棒性（例如 [9]）。然而，这方面的工作尚未考虑使用事务的应用程序。事务使一致性模型语义复杂化，这使得建立鲁棒性标准更具挑战性。
应用程序中事务的可序列化性简化了其正确性属性的建立，但对此并非必要。因此，建立应用程序正确性的另一种方法是直接证明其所需属性，而不要求事务仅产生可序列化的行为。Lu 等人 [23] 为 ANSI SQL 隔离级别和 SI 提出了相应的方法，Gotsman 等人 [18] 为 PSI 和其他一些最新模型提出了相应的方法。这些方法是我们的补充：它们所需的条件可以被更多应用程序满足，但比健壮性更难检查。
Conclusion
在本文中，我们迈出了理解最近提出的大型数据库事务一致性模型对使用它们的应用程序的正确性属性的影响的第一步。为此，我们提出了检查使用弱一致性模型的应用程序何时仅表现出强一致性行为的标准。这使程序员能够检查应用程序的正确性是否会因选择特定的一致性模型或要在可序列化下执行的事务而得到保留。
Fekete 等人对 SI 的稳健性结果此前已催生出用于静态检测应用程序中异常的自动工具 [19]。我们的工作可以为提供较弱一致性模型的数据库的类似进展奠定基础。我们的动态稳健性标准也具有独立意义：除了作为静态分析的基础外，此类标准还可用于优化运行时监控算法 [24, 28]。
在建立稳健性标准时，我们采用了一种利用公理规范的系统方法 [12]：使用一致性模型的公理，我们表征了模型执行依赖图中允许的循环，并利用这些表征提供了可靠的静态分析技术。我们希望这种方法可以适用于针对大型数据库提出的其他一致性模型。
