摘要
为了实现可扩展性,现代互联网服务通常依赖于分布式数据库,其事务一致性模型比可序列化性要弱。目前,应用程序员通常缺乏确保这些一致性模型的弱点不会违反应用程序正确性的技术。我们提出了一些标准来检查依赖于仅提供弱一致性的数据库的应用程序是否具有鲁棒性,即其行为是否像使用提供可序列化的数据库一样。在这种情况下,应用程序员可以获得弱一致性的可扩展性优势,同时能够轻松检查所需的正确性属性。我们的结果系统而统一地处理了最近提出的几种弱一致性模型,以及一种增强应用程序各部分一致性的机制。
本文的研究对象的是分布式数据库及其一致性。
作者:
- Giovanni Bernardi, IMDEA Software Institute
- Alexey Gotsman, IMDEA Software Institute
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] 制定此标准,描述其事务之间的几种关系:如果执行的依赖关系图不包含某种形式的循环,则执行是可序列化的,我们称之为关键(critical)。针对不同一致性模型的鲁棒性标准在哪些循环被视为关键方面有所不同。然后,我们说明如何将单个执行上的动态鲁棒性标准提升为静态标准,以检查给定应用程序的所有执行是否可序列化(第 4 节)。
Consistency Model Specifications
我们首先回顾一下 [12] 中数据库计算的正式模型和我们处理的一致性模型的规范。这些规范是声明性的,这大大简化了我们的形式化开发。尽管如此,如 [12] 所示,这些规范相当于某些操作规范,接近于实现。
定义 1
事务
是一对 ,其中 是具有不同标识符的有限非空事件集,程序顺序 是 上的全序。历史 是具有不相交事件标识符集的事务的有限集。带注释的历史 是一对,其中 是历史, 。执行是三元组 ,其中 是带注释的历史, 是 上的严格偏序, 是 上的全序,且满足 。我们称 为 先行发生关系(happens-before),称 为 仲裁(arbitration)。
我们将执行的组件表示为
事务记录了一组操作以及客户端程序调用它们的顺序。历史记录了在有限的数据库计算中提交的事务。为了简化,我们省略了对已中止和进行中的事务以及无限数据库计算的处理。带注释的历史通过一个函数
我们使用集合
给定一个全序
内部一致性公理(
当且仅当 $\max\set{e \in E | e \vdash\write(x,_) }, <_{\po}) \vdash\write(x, n) $; - $T \vdash\read(x, n) $ 当且仅当 $\min{e \in E | e \vdash_(x,_) }, <_{\po}) \vdash\read(x, n) $。
根据
公理
因果一致性允许丢失更新异常(lost update anomaly),如图 2(b) 所示。该异常可能由程序
我们通过使用公理
Dynamic Robustness Criteria
我们的第一个目标是定义标准来检查我们考虑的一致性模型之一中的单个执行
我们的动态标准是基于依赖图来制定的,这在数据库文献中被广泛使用 [2]。设标签集
给定一个图
- 如果
,则 ; - 如果
,并且存在某个 使得 ,则 。
我们用
定义 2 依赖图
执行
的动态依赖图是 ,其中对于每个 , 包含了下列三元组:
- 读依赖:
,若 并且 ; - 写依赖:
,若 并且 ; - 反向依赖:
若 并且满足以下的一个条件:
并且 ; 。
引理 3
对于每个
,若 满足 和 公理(这意味着 符合 ),且 无环,则 。
定义 4 执行的关键环
给定一个执行
,某个边 是不被保护的,若 或 。 (其中 )包含某个简单无弦且 rw-最小的环 是:
- CC-critical:若
包含两个未被保护的边 和 ,其中 且 ; - PC-critical:若
包含一个未被保护的边 和至少两个相邻的未被保护的标记属于 边; - PSI-critical:若
包含至少两个未被保护的 边,并且; - 对每个
,若 ,则 ; - SI-critical:若
包含至少两个相邻的未被保护的 边,并且; - 对每个
,若 ,则 。
图 2 中的执行图(级别为
定理 5
对于每个
和 ,如果 ,则 包含一个环,当且仅当它包含一个 关键环。
根据定理 5 和引理 3,我们得到我们的动态鲁棒性标准。
推论 6 动态鲁棒性充分条件(其实也是充要条件)
对于每个
和每个 ,如果 且 不包含任何 关键环,则 。
我们注意到,上述 SI 鲁棒性标准是现有标准的一个变体 [16, 15]。在我们的设置中,它只是我们新标准的一个结果。
为了证明定理 5,我们展示图 3 中的公理如何影响依赖图中的边和路径的性质。首先,观察到
这些蕴含关系使我们得以证明,在某些条件下,如果两个事务在依赖图中通过路径连接,它们也通过发生前关系或仲裁相互关联。
引理 7
对于任意
, ,且 ,如果 ,则:
- 如果所有
和 边在 中受到保护,则 ; - 如果所有
边在 中受到保护,则 ; - 如果
并且所有 边在 中受到保护,则 。
接下来的引理表明,如果
引理 8
定理 5 证明
该命题的“如果”蕴含关系是显而易见的,因此让我们证明“当且仅当”的含义。假设图
包含一个循环 。从 我们可以很容易地构建一个循环:
在
从依赖图推导执行
在 CONCUR'16 原文中:
边意味着 关系; 公理下的 边意味着 关系; 边意味着 关系;
对于
定理
在
公理约束下,被保护的 边意味着 和 ;
定理 7 实际上是这一命题利用
如果对
RA | Update Atomic | SI | SER | protected edge ( |
(by SER-(2)) |
||
---|---|---|---|---|---|---|---|
none | none | none | none | none |
Static Robustness Criteria
我们现在说明如何将动态鲁棒性标准(推论 6)提升为静态标准,这使得程序员能够分析其应用程序的行为,并可作为静态分析工具的基础。
我们通过一组事务程序 fi 来定义应用程序 A,并给出其事务代码:A = {f1, ..., fn}(例如,参见图 1)。按照数据库文献 [16] 中的标准,这从应用程序逻辑的其余部分中抽象出来,以专注于直接与数据库交互的部分。我们将程序对 I = (f, v) 和其实际参数向量称为程序实例。应用程序实例 I 是一组程序实例,带注释的应用程序实例是一对 (I, levelS),其中 levelS : I → {SER, ⊥} 定义程序员请求在可序列化下执行哪些程序。我们首先制定检查特定带注释的应用程序实例的稳健性的标准,该标准是通过使用给定参数运行一组事务程序得出的。然后,我们概述了如何将这些标准推广到整个应用程序。
我们旨在以最简单的形式说明将动态稳健性标准提升为静态稳健性标准的想法。为此,我们从编程语言的语法中抽象出来,并假设我们只给出了每个事务程序读取或写入的对象集的近似信息。也就是说,我们假设一个函数 rwsets 将每个程序实例 I 映射到三元组 rwsets(I) = (R3, W3, W2)。非正式地说,R3 和 W3 是可能在 I 的某些执行中读取或写入的所有对象的集合,而 W2 是必须在 I 的任何执行中写入的对象的集合,但前提是 W2 ⊆ W3。例如,对于 I = (StoreBid,hiId1, 7i)(图 1),我们有
其中
为了形式化读/写集的含义,我们定义了一个关系,该关系确定是否可以由给定的 I 生成历史记录。我们让 T I 对于 rwsets(I) = (R3, W3, W2),如果:
我们将 与带注释的历史和带注释的应用实例的关系提升:
定义 9 静态依赖图
图 6 显示了 (3) 中 I 的静态依赖图。非正式地,静态依赖图 SDG(I) 的边描述了由 I 产生的执行中事务之间可能存在的依赖关系:边 I λ > J 表示可能存在的依赖关系,边 I λ ←→ J 表示必须存在的依赖关系。正式地,给定一个带注释的应用程序实例 (I, levelS),我们说对 (DDG(X), X.level) 被对 (SDG(I), levelS) 过度近似,写为 (DDG(X), X.level) (SDG(I), levelS)(即,前者是后者的子图),如果对于某个总函数 f : X.H → I 我们有:
引理 10
我们现在通过使用与动态依赖图相同的路径和循环概念来制定静态鲁棒性标准(第 3 节)。给定一对 (I, levelS) 和程序实例 I0, I1, . . . , In(其中 I0 = In)中 π ∈ SDG(I) 中的一个循环。
定义 11 程序实例的关键环
对于一对
,若 或 ,则称 是未被保护的。一个环 包括 (其中 )是:
- CC-critical:若
包含两条未被保护的边 ,其中 并且 ; - PC-critical:若
包含一个未被保护的边 和至少两个相邻的未被保护的标记属于 边; - PSI-critical:若
包含至少两个未被保护的 边,并且; - 对每个
,若 ,则 ; - SI-critical:若
包含至少两个相邻的未被保护的 边,并且; - 对每个
,若 ,则 。
请注意,与动态依赖图中的关键循环(定义 4)不同,静态图中的关键循环不必是简单的。以下引理指出
定理 12
对每个
和 ,使得 ,若 包含 wm-critical 环,则 包含 wm-critical 环。 换言之,若
不包含 wm-critical 环,则 不包含 wm-critical 环。该关系是单向的。
定理 13 静态鲁棒性充分条件
对每个
和 ,若 不包含 wm-critical 环并且 ,则若 ,我们有 。
- 静态鲁棒性充分条件:若程序
满足某条件,则 产生的所有历史 ;反之,若 不满足这些条件,则不能保证所有 ; - 程序鲁棒性充要条件:若程序
满足某条件,则 产生的所有历史 ;反之,若 不满足这些条件,则保证并非所有 。
如果在定理 13 的基础上,能构造出某个反例
Analysing Whole Applications
定理 13 中的静态标准允许程序员分析给定应用程序实例的鲁棒性。使用定理完整分析应用程序需要考虑其无限数量的实例,这项任务最好由自动静态分析工具完成。我们现在概述如何使用抽象解释 [13, 25] 中的想法来有限地表示和分析应用程序的所有实例集。在未来,这可以为在静态分析工具中自动化我们的鲁棒性标准铺平道路。由于篇幅限制,我们仅通过示例介绍这些概念。
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]:使用一致性模型的公理,我们表征了模型执行依赖图中允许的循环,并利用这些表征提供了可靠的静态分析技术。我们希望这种方法可以适用于针对大型数据库提出的其他一致性模型。