CALM猜想（以及后来的定理）在2010年的一次主题演讲中首次被介绍给世界。在其简单的公式背后，有一个深刻的教训，可以学习到在我们的行业中产生类似于CAP定理影响的涟漪的力量。它奖励花在深思熟虑的时间。因此，我很高兴看到Hellerstein&Alvaro的这篇文章提供了一个全新的、非常平易近人的CALM视角，为我们提供了一个这样做的理由。我们现在需要的只是一个引人注目的运动名称！一个CALM的系统就是一个“不协调”NoCo系统
对于高性能可伸缩的分布式系统，协调是一个杀手。它是通用可伸缩性定律中的主要术语。当我们能够避免或减少对协调的需求时，事情往往会变得更简单和更快。例如，可以参见数据库系统中的协调避免，以及最近Anna的惊人性能，它通过协调消除提供了两个数量级的速度。所以我们应该尽量避免协调。
到目前为止还不错，但我们到底什么时候才能避免协调呢？在回答这个问题时变得精确是CALM定理的全部内容。你可能熟悉布鲁克斯在他的“无银弹”文章中对本质复杂性和偶然复杂性的区分。在这里，我们将梳理出基本协调和意外协调之间的区别，前者是不协调就无法提供的保证，后者是通过更仔细的设计可以避免的协调。
在许多情况下，协调并不是必要的坏事，而是设计决策的附带要求。
意外协调的原因之一是，我们专注于使用存储语义来解决堆栈较低级别的一致性问题。这里有一个端到端的争论，我们需要考虑的是应用程序级语义。低层有一部分要发挥作用，但如果我们只专注于那里，就无法释放全部潜力。正如帕特·海兰在流沙上的建筑-谈系统稳定性一文中所阐述的那样，写作并不通勤，但应用程序级的操作可以通勤。也只有在应用程序级别，我们才能用协调来换取道歉。
不管怎样，关键问题是：
- 在没有协调的情况下，可以以分布式方式一致地计算问题的范围是什么？该领域之外还有哪些问题？
当上述设置中的机器交换它们所感知的边缘的信息时，在某个时刻涉及T_1和T_3的循环将被曝光。不管后来发现了什么其他的边，我们都知道我们陷入了僵局。该系统中的死锁检测是单调的。
这是另一个看起来非常相似的分布式图，但这次我们对垃圾收集的可达性很感兴趣。
更准确地说，我们对无法到达感兴趣。根据目前的信息，我们可能认为某个对象是不可到达的。不过，这个性质不是单调的——我们发现的下一个边缘可能会使它再次达到。
首先，我们问的是“是否存在？”？“（\存在）问题。一个正面例子的出现给了我们一个肯定的答案，而其他正面例子并不能改变这个事实。在第二个例子中，我们问的是“不存在？” ( !\存在）问题。我们只有看了每个例子才能回答这样的问题。“为所有人…”问题（为所有人）也是一样的。
如果我们对可达性而不是不可达性的性质感兴趣，那么对于完全相同的图和完全相同的边缘发现算法，那将是单调的。一旦我们知道一个对象是可到达的，通过第二条路径发现它也是可到达的并不会改变这个事实。除非…我们的系统允许删除对象和边。然后，一个可到达的对象可能再次变得不可到达，并且可到达性不再是单调的。
我们从这些例子中学到的是否定和普遍的量化会破坏单调性。我们需要这样的性质，即一旦我们掌握了全部信息，对部分信息作出的结论将继续有效。
这种单调性的观点被证明是至关重要的。是时候满足CALM定理了（一致性作为逻辑单调性）：
逻辑单调性的一致性（CALM）。当且仅当程序是单调的时，程序才具有一致的、无协调的分布式实现。
CALM定理描述了可能（即“如果”部分）和不可能（即“仅如果”部分）之间的边界。如果你保持CALM，那么你总是可以“继续”而不需要停下来协调。
再多说些“C”（coordination）字
我们正在取得进展。我们现在可以把原来的问题提炼成这样：“什么是可以以单调方式计算的问题家族，这个家族之外还有什么问题？”？“到目前为止，我们一直在谈论冷静、一致和协调。现在我们需要再介绍几个“C”字：交换的和合流的。
回想一下，如果一个二进制操作数的顺序对结果没有影响，那么它是可交换的。加法是可交换的，减法不是。应用于程序操作的合流是同一思想的推广。如果一个操作为一组输入的任何非确定性排序和批处理产生相同的输出集，则该操作是合流的。
合流操作组合：如果一个合流操作的输出被另一个合流操作消耗，则生成的复合操作是合流的。因此，合流可以应用于单个操作、数据流中的组件，甚至整个分布式程序。如果我们限制自己通过组合合流操作来构建程序，那么尽管组件内部和组件之间存在消息顺序或执行竞争，我们的程序还是通过构造而合流的。
合流运算是单调系统的基石。我们仍然需要注意避免否定（删除！\已存在，其替代公式为：。处理否定/删除的一个创造性的解决方案，如CRDT集合所使用的，是在添加的同时保留一个单独的增长的删除集合。在关系代数术语中，我们可以有选择、投影、交集、连接和传递闭包，但不能有集合差分。在可变状态方面，我们可以允许插入，但不允许更新和删除。
CALM的关键观点是从程序结果的角度来关注一致性，而不是传统的存储突变历史。对正在计算的程序的强调将重点从实现转移到规范：它允许我们询问关于哪些计算是可能的。
CALM在现实系统中的实践
CRDTs为单调编程模式提供了一个面向对象的框架。不过，我们确实希望在函数式编程上下文中使用它们，或者至少在避免对可变变量进行裸赋值的上下文中使用它们。不变性是一个平凡的单调模式，可变性是非单调的。更进一步，Bloom语言被明确设计为支持CALM应用程序开发：
Bloom使面向集合、单调（因此合并）的编程成为程序员在语言中使用的最简单的结构。
Bloom可以利用基于CALM的静态分析来证明程序何时提供CRDTs提供的基于状态的收敛特性，以及这些特性何时跨模块组合保留。
如果不能为应用程序的每个特性找到单调的实现，一个好的策略是保持关键路径上的协调。例如，在前面介绍的垃圾收集示例中，垃圾收集可以在后台运行。另一种选择是在没有协调的情况下继续，但建立一种机制来检测何时会导致不一致，以便应用程序能够“道歉”。
CALM定理给出了一个正的结果，它描绘了可能性的边界。CALM表明，单调性是程序的一个属性，它意味着一致性，即程序任何执行的输出的一个属性。反之亦然：非单调程序需要运行时强制（协调）以确保一致的执行。作为程序属性，CALM通过静态程序分析实现推理，并限制或消除运行时检查的使用。
论文上还有很多好的题材，我没有足够的篇幅来讨论，所以如果这些想法引起了你的兴趣，我鼓励你去看看。
若有收获，就点个赞吧
0 人点赞
