什么是分布式一致性领域的CALM定理? -ACM


逻辑单调性的一致性(Consistency As Logical Monotonicity:CALM):当且仅当问题是单调的时,问题才具有一致的、无需协调的分布式实现。
CALM定理是为了避免分布式事务机制中的协调机制,试图实现如同没有红绿灯的交通路口,需要程序员对业务问题进行设计,保证问题是单调性的,也就是说,输出结果与输入数据的之间顺序没有关联关系,输入数据的前后顺序不会影响输出结果,典型案例如CRDT(无冲突的复制数据类型)。
 
分布式系统很棘手。多个不可靠的机器并行运行,它们在网络链路上以任意延迟相互发送消息。尽管存在这种混乱局面,我们如何才能确信这些系统能够实现我们想要的功能?
这个问题应该引起我们的关注,因为我们今天使用的几乎所有软件都是分布式系统的一部分。手机上的应用程序与云中的托管服务一起参与;它们一起形成一个分布式系统。托管服务本身是大规模分布的系统,通常在遍布全球的计算机上运行。大数据系统和大规模数据库分布在许多机器上。大多数科学计算和机器学习系统可跨多个处理器并行工作。甚至传统的桌面操作系统和应用程序(例如电子表格和文字处理器)也与分布式后端服务紧密集成。
建立正确的分布式系统的挑战越来越紧迫,但这并不是新问题。一种传统的答案是通过内存一致性保证来降低这种复杂性-对内存(堆变量,数据库密钥等)的访问以受控方式进行的保证。但是,用于执行这些保证的机制(协调协议)经常被批评为分布式系统的高性能,规模和可用性的障碍。
 
协调成本高
协调协议使自治的,松散耦合的机器可以共同决定如何控制基本行为,包括访问共享内存的顺序。这些协议是分布式计算中最聪明和被广泛引用的思想之一。一些公知的技术包括的Paxos和两阶段提交(2PC)协议和基础计算模型等散装同步并行计算全局障碍。
不幸的是,协调协议的开销会使它们成为程序员的“禁果”。来自亚马逊网络服务公司的詹姆斯·汉密尔顿(James Hamilton)用“一致性机制”一词强力地说明了这一点,在其中使用了协调:
成功的可伸缩性的首要原则是将一致性机制降低到最低程度,将它们移出关键路径,将它们隐藏在系统很少访问的角落,然后使应用程序开发人员尽可能地难以获得许可。使用它们。” 
问题不在于协调很难实现,尽管确实如此。主要问题是协调会大大降低计算速度或完全停止计算。一些现代的全球规模的系统利用协调协议。Google Spanner交易数据库是同时使用Paxos和2PC的著名示例但是,这些协议的时延较高,大约为10ms-100ms。依赖于这些协议的全球级系统并不意味着应用程序能够快速运行。协调等待时间问题也转化为微观规模。最近的工作表明,最新的多处理器键值存储能将90%的时间用于协调。
一个名为Anna的无协调实现通过消除这种协调实现了两个数量级以上的加速。我们可以像汉密尔顿建议的那样更广泛地避免协调吗?什么时候?
 
更大的前景:程序一致性

直到最近才解决了何时需要协调才能实现一致性的一般问题。
关于一致性的传统工作集中在诸如线性化性和冲突可串行化性之类类的属性上,这些属性通过限制冲突的存储器访问的顺序来确保存储器的一致性。这种传统掩盖了一个基本问题,即是否需要协调才能确保特定计划结果的一致性?要从整体上解决问题,我们需要向上移动堆栈,预留低层的细节以支持程序语义。
交通交叉口提供了一个与现实世界类似的有用类比。为避免在繁忙的十字路口发生事故,我们经常安装停车灯,以协调两条相交道路的交通。但是,在这种情况下,协调并不是必不可少的事情:我们还可以通过为其中一条道路建造立交桥或隧道来预防事故。“交通路口问题”是具有免协调解决方案的示例。重要的是,无法通过巧妙地控制进入道路在地图上重叠的关键区域的顺序来找到解决方案。解决方案包括对道路进行工程设计,以完全避免协调。
对于交通交叉路口问题,事实证明,有一种解决方案可以完全避免协调。并非所有问题都使用这样的解决方案。对于任何给定的计算问题,我们如何知道它是否具有免协调解决方案,或者是否需要协调以实现一致性?为了增强我们的直觉,我们考虑了分布式系统规范中的两个几乎相同的问题:两者都涉及图形的可到达性,但是一个没有协调性,另一个则没有,见下面
 
分布式死锁检测
分布式数据库在分布式图形中标识周期,以便检测和修复死锁。在传统的数据库系统中,事务T i可能正在等待另一个事务T j持有的锁,而另一个事务T j可能正在等待另一个T i持有的锁。死锁检测器通过分析有向图来识别这种“等待”周期,在有向图中,节点表示事务,而边缘表示一个事务在锁定队列上等待另一个事务。死锁是一个稳定的属性:等待周期中的事务无法取得进展,因此周期中的所有边缘都将无限期地保持。
在分布式数据库中,等待图的“本地”(单机)视图仅包含全局等待图中边的子集。在这种情况下,本地死锁检测器如何协同工作以识别全局死锁?
图1显示了跨越多台计算机的等待周期。为了识别这种分布式死锁,每台机器都与其他机器交换其边缘的副本以累积有关全局图的更多信息。机器只要观察到到目前为止已接收到的信息中的周期,就可以在该周期的事务之间声明死锁。

我们可能会担心由于此分布式计算中的消息延迟或重新排序而导致的瞬时错误。本地探测器是否必须与其他机器配合以确保观察到死锁?在这种情况下,不需要协调。要看到这一点,请注意,一旦我们知道图中存在循环,就知道新的边永远不可能使循环消失。例如,一旦机器1和机器2共同识别出T 1和T 3之间的死锁,来自Machine 3的新信息将不会改变这一事实。其他事实只能导致检测到其他周期:每台机器的输出随输入单调增长。最后,如果最终在所有机器之间共享所有边缘,则机器将基于完整图形对结果达成共识。
  
分布式垃圾回收
分布式系统中的垃圾收集器必须在内存引用的分布式图中标识无法访问的对象。垃圾收集通过识别与系统运行时的“根”断开连接的图形组件来工作。“垃圾”属性也是稳定的:一旦图形组件与根的连接被删除,该组件中的对象将不会被重新引用。
在分布式系统中,对对象的引用可以跨越机器。参考图的局部视图仅包含全局图中边的子集。多个本地垃圾收集器如何协同工作以标识真正无法访问的对象?
请注意,一台机器可能有一个本地对象,却不知道该对象是否已连接到根目录。机3和对象ø 4在图2中形成的例子。但是,从根到对象的路径仍然可能存在,该路径由分布在其他计算机上的边组成。因此,每台机器与其他机器交换边的副本,以累积有关图形的更多信息。

和以前一样,我们可能会担心由于消息延迟或重新排序而导致的错误。本地收集者可以自主声明和取消分配垃圾吗?在这里,答案是不同的:确实需要协调!要看到这一点,请注意,基于不完整信息的决策(例如,机器3判定图2中的对象O 4不可达),可以通过随后到达新的证明可达性的信息(例如,边缘Root→ O 1,O 1 → O 3,O 3 → O 4)。输出不会随输入单调增长:可能需要撤消临时“答案”。为了避免这种情况,机器必须确保在宣布对象无法到达之前已经听完了所有听到的声音。知道它听到的一切的唯一方法是与所有其他机器(甚至没有参考边缘的机器)进行协调以建立事实。正如我们将要讨论的,即使在没有数据依赖的情况下,通信的要求也是协调的标志。
 
一致性的关键:单调性
这些示例使我们回到了适用于任何并行计算框架的基本问题。
问题:我们说,如果存在一个分布式实现(即解决问题的程序),而无需使用协调来计算一致的输出,那么计算问题就不会产生协调。什么是无协调问题情况,情况之外有什么问题?
偶然使用的协调与固有的协调需求之间是有区别的:前者是实施选择的结果;后者是计算选择的结果。后者是计算问题的性质。因此,我们的问题是可计算性之类问题之一,例如P对NP或可判定性。它询问一个聪明的程序员不可能实现的是什么。
 
定理1.作为逻辑单调性的一致性(Consistency As Logical Monotonicity:CALM)。当且仅当问题是单调的时,问题才具有一致的、无需协调的分布式实现。

非单调系统接收信息的顺序决定了它们如何来回切换状态,这反过来又可以确定其最终状态(我们将在后面的内容中看到)。购物车示例)。相比之下,单调的输出仅取决于输入的内容,而不取决于输入的顺序。
到目前为止,我们的讨论仍停留在直觉上。下一部分提供了CALM定理的证明的草图,包括对一致性和协调性定义的进一步讨论。该证明使用了数据库理论中的逻辑形式主义,并证明了将数据库理论(ACM PODS)和分布式系统(ACM PODC)紧密结合在一起的好处。
 
证明过程点击标题见原文
 
CAP和CALM
Brewer的CAP定理14非正式地指出,系统只能显示以下三个属性中的两个:一致性,可用性和分区容限。CAP是一个负面结果:它捕获了通常无法实现的属性。
CAP的表达达到了其目的,这是使设计者可以在更广泛的系统和折衷方案中开放思想。现代CAP的目标应该是最大化对特定情况有意义的一致性和可用性的组合。
在这个领域,CALM是一个积极的成果:它界定了可以同时实现所有三个CAP属性的问题类别。要看到这一点,请注意以下几点:

  • 观察1.无协调性等同于分区下的可用性。

根据定义,可以在分区下找到无协调程序:所有机器都可以独立进行。当分区恢复正常时,状态合并是单调且一致的。相反,如果参与协调的机器跨越了分区,则采用协调的程序将在协调协议期间停顿(变得不可用)。
CALM会询问并回答CAP的基本问题:“哪些问题可以一致地计算,而在分区下仍然可用?” CALM与CAP不矛盾。取而代之的是,CALM从更广泛的参考框架中实现了分布式一致性:
  • 首先,在所有问题的范围内,CAP都是负面结果:CALM确认了这一粗略结果,但在更细粒度上描绘了正面和负面的情况。使用融合作为一致性的定义,CALM显示单调问题实际上可以同时满足所有三个CAP属性;非单调问题是不能解决的。
  • CALM的关键见解是从程序结果的角度关注一致性,而不是冲突行动的传统有序历史(通常是存储突变)。对要计算的问题的强调将重点从命令式实现转移到声明式输出规范;这使我们可以提出关于可以进行哪些计算的问题。

 
分布式设计模式
无冲突的复制数据类型(CRDT)为单调编程模式(例如逻辑删除)提供了面向对象的框架,通常用于复制状态的上下文中。
CRDT是一种抽象的数据类型,可以使用关联内部格中的交换,关联,幂等联接函数合并CRDT的两个实例。最终,两个CRDT副本的状态可能会看到不同的输入和顺序,始终可以确定性地合并到一个新的最终状态中,该状态将合并两个双方看到的所有输入。
 
Bloom编程语言
鼓励良好的分布式设计模式的一种方法是使用专门围绕这些模式的语言。Bloom是我们本着这种精神设计的一种编程语言。实际上,CALM猜想和Bloom语言是一起开发的。
Bloom的主要目标是使分布式系统更易于推理和编程。我们认为,一种适用于某个领域的好语言会掩盖无关紧要的细节,并将那些重要的内容集中在一起。鉴于数据一致性是分布式计算中的核心挑战,我们将Bloom设计为以数据为中心:系统状态和事件均表示为命名数据,而计算则表示为对该数据的查询。

详细点击标题见原文