本文是作者在 FLOPS 2022 会议上的演讲，重点分享了使用Liquid Haskell语言集成验证系统来构建可靠的分布式系统的有趣的探索经历。
早上好，FLOPS！我是 Lindsey Kuper。我是加州大学圣克鲁兹分校的助理教授。
非常感谢 Atsushi 和 Michael 以及整个 FLOPS 组织团队邀请我在 FLOPS 上发言，以及他们组织这次活动的工作。就个人而言，FLOPS 是我第一次有论文被拒绝的会议，那是在 2010 年我刚开始读研究生的时候。所以今天被邀请做这个演讲，我感到特别荣幸。
这个演讲是关于我最近在做的非常兴奋的事情，即使用现代语言集成验证工具来帮助我们构建保证按预期工作的分布式系统的潜力，这些保证不仅适用于模型，还适用于真实运行的代码。
在本次演讲的开始部分，我将解释我所说的“分布式系统”的含义以及它们所面临的具体挑战。然后简单介绍一下 Liquid Haskell 语言集成的验证系统。最后，探险记：我将分享我和我的学生和合作者一直在这个领域开展的两个项目的一些亮点。
那么，让我们从讨论分布式系统开始吧！
其中许多问题与故障有关，并且需要在系统出现部分故障的情况下继续运行。亚马逊在其关于 Dynamo 数据存储系统的 SOSP 2007 论文中对此进行了非常生动的描述：“客户必须能够将商品添加到他们的购物车中，即使磁盘出现故障、网络路由抖动或数据中心被龙卷风摧毁。” （我恰好来自美国中西部的爱荷华州，所以龙卷风对我来说是非常真实的成长过程，但可以随意替换你选择的任何自然灾害。）
因此，由于龙卷风或任何其他原因，不仅网络连接会失败，而且该网络中的节点也会失败。即使在出现故障的情况下，系统也必须继续运行并响应请求，这一点很重要，因为用 Werner Vogels 的话来说，“一切都在失败”。
因此，部分故障的问题，以及需要在部分故障存在的情况下继续运行，在许多方面是分布式系统的定义特征。
这是一束电线，每根大约 30 厘米长。格蕾丝·霍珀（Grace Hopper）在她的有名的讲座中分发了这些，以展示电信号在一纳秒内可以传播的距离。这些是她分发的一些实际的电线；他们现在在史密森尼博物馆。
所以，光速很慢！它在一纳秒内仅移动约 30 厘米。或者，正如我的朋友 Mae Milano 所说，每个时钟周期只有大约 4 英寸。
因此，如果我们谈论的机器可能彼此位于世界的另一端，那么即使在理想条件下，在消息发送和消息到达之间也可能会经历很多时钟周期。
所以，无论我们是在谈论故障——磁盘故障、宇宙射线、网络连接被反铲挖掘机截断、数据中心被龙卷风摧毁——或者只是更普通但不可避免的问题，即相距很远的机器之间的长时间延迟，缓解这些挑战的一种方法是在多个物理位置复制数据。这有助于确保数据的可用性——换句话说，有助于确保每个请求都得到有意义的响应。
如果我有我不想丢失并且我想确保仍然可用的数据，无论是我女儿的婴儿照片还是我可能关心的任何其他数据，我将存储该数据的多个副本在数据中心内，以及在不同数据中心之间。
这样做是出于容错的原因——你拥有的副本越多，你丢失它的可能性就越小——以及数据局部性，以最大限度地减少延迟——我们希望数据的副本接近任何人的尝试访问它 - 以及吞吐量的原因：如果你有多个数据副本，那么原则上你可以为更多尝试同时访问它的客户提供服务。但是，尽管出于所有这些原因拥有多个副本是必不可少的，但它引入了必须保持副本彼此一致的新问题，特别是在我们拥有的网络中，由于网络分区，副本之间的延迟可能任意长。
因此，正如我告诉参加我的分布式系统课程的本科生，复制既是大多数分布式系统问题的原因，也是解决方案。我们必须复制数据，但我们必须保持这些副本彼此一致。
现在，我们知道试图始终保持地理分布的副本完全一致是徒劳的。一个经典的不可能结果告诉我们，在存在网络分区的情况下实现完美一致性的唯一方法是牺牲数据的可用性。由于在处理地理分布式数据时网络分区是不可避免的，我们通常选择以允许客户观察副本之间某些类型的分歧的方式设计系统，以优先考虑可用性。
如果我们要允许副本之间存在某些类型的分歧，那么我们需要一种指定策略的方法，该策略告诉我们允许副本以何种方式不同意，在什么情况下允许他们不同意，以及在什么情况下他们必须同意。让我们看一下这些一致性策略的几个示例，以及可能违反它们的一些方式。
在这个例子中，情况很明显，因为我们复制的数据结构是一个集合，并且这两个添加到集合中的元素相互交换。
例如，这里有一个不同的执行，它不是强收敛的。假设我们从具有包含一张照片的相同相册的两个副本开始。和以前一样，我添加了一张照片。假设我的照片首先进入 R1。同时，假设我们的照片应用程序提供了一个 share_with_mom 以照片为参数的操作。我的伙伴想与他的妈妈分享照片，因此他尝试将 share_with_mom 操作映射到相册中的所有内容。
该 map 操作首先进入 R2，然后应用于相册中的所有内容，此时相册只是一张照片。但后来当我添加的照片到达时，它在 map 操作运行时不是集合的一部分，所以根据副本 R2，它没有与我的婆婆共享。同时，副本 R1接收第二个 map 操作并映射两张照片，因此两张照片都被共享。不幸的是，这些操作不会相互通信，因此，如果此地图操作是我们相册提供的接口的一部分，那么每次执行都不会保持强收敛。
解决此问题的一种方法是仔细设计数据结构的接口，以确保其上的所有操作都可以通信。具有这种行为的数据结构被称为无冲突复制数据类型或 CRDT，它们通常通过巧妙的技巧使操作可以在原本不会进行的情况下进行交换，或者利用关于应用操作顺序的假设来工作。新的 CRDT 设计是一个活跃的研究领域。随着这些数据结构的设计变得越来越复杂，它们激发了对机械验证实现的需求，这些实现可以保证在所有可能的执行中收敛。
我们稍后会回到这个问题，但在此之前，让我们先看看另一种一致性问题。
再说一次，我向相册添加了一张照片。我碰巧与副本 R1 通信，R1 将更新异步发送到 R2。后来，我的搭档过来看照片。他看到了我的更新，因为他碰巧与进行更新的副本相同。但是假设他在那之后试图发表评论，不幸的是，那篇文章发给了 R2，它还没有拿到照片。因为照片还没有，所以复制品不能附加评论。
这可能会表现为某种难以理解的错误消息，例如“抱歉，出了点问题。再试一次。” 你可能以前见过这种东西。
要了解这里出了什么问题，我们必须考虑事件的因果关系。我的搭档试图对这张照片发表评论，因为他在服务器的回复中看到了这张照片。这是由于之前的添加操作而发生的。所以，这个添加操作是尝试评论的因果历史的一部分，我们可以通过随着时间的推移跟踪这些消息并看到评论操作可以从添加操作中看到。但在尝试评论发生时，此副本尚未发现其因果历史中的此添加事件。所以这违反了所谓的因果一致性。
解决此问题的一种方法是使用确保消息按因果顺序传递到副本的机制，其中“已传递”一词意味着在收到后实际应用于副本的状态。一种广泛使用的方法是将元数据附加到每条消息中，以总结该消息的因果历史——例如，矢量时钟。我们可以使用此元数据来确定两条消息之间的因果关系（如果有的话），并延迟将消息传递到给定副本，直到每条因果先前的消息都已传递。在这种情况下，comment发送到副本 R2 的消息将排队，直到add消息到达，然后可以应用评论。
在这里，我再次认为需要机械验证的实现，因为因果消息排序抽象是分布式系统非常有用的构建块，但是很多系统并没有做到这一点。我们稍后再讨论这个问题。
事实证明，知道我们应该执行哪个策略也很重要，因为这些一致性策略以及它们指定的有关执行的属性不一定很好地映射到我们关心的给定应用程序的不变量上。
例如，假设我和我的伙伴正在使用照片共享服务的免费层级，它说我们最多可以拥有 1000 张照片，否则我们必须开始付费，不然我们将面临删除旧照片的风险。如果相册中有 999 张照片，添加一张照片应该没问题；没有违反不变量。
另一方面，如果我的伴侣也同时添加了照片怎么办？那么，当两个副本同步时，就会违反不变量。
我们应该怎么做呢？如果需要维护不变量，则需要拒绝我的更新或我的伙伴的更新，这将要求我们每次添加照片时同步副本。在实践中，我们可能希望避免这种同步，直到我们接近 1000 张照片的限制。此外，其他操作，如删除照片，不需要同步来保持这个特定的不变量。一般来说，同步副本的需求取决于操作和我们需要维护的特定于应用程序的不变量。
我们之前谈到的与应用程序无关的属性，如强收敛和因果消息传递，并不能让我们一路走好，但它们可能会让我们走上一段路。事实上，验证这些特定于应用程序的属性的工作通常依赖于已经存在强收敛或因果消息传递等属性的假设。如果我们可以依赖底层数据结构的某些属性是真实的，或者在其之下，消息传递层，我们可以简化应用程序级别的验证任务（或者，就此而言，只是关于应用程序代码行为的非正式推理）。
我们刚刚看到了一些我们可能希望针对复制数据的一致性实施的策略示例。要知道这样的策略适用于所有执行，需要对通常非常大的执行状态空间进行推理，其中有很多消息丢失和消息排序的可能性。
这些策略的规范称为一致性模型，其中有很多。不久前我向我的研究生展示了这个数字，现在它困扰着他们的梦想。它来自 Viotti 和 Vukolić 于 2016 年发表的一篇调查论文，其中对分布式系统文献中的 50 多个一致性概念进行了分类，并按照所谓的“语义强度”对它们进行了排序。
换句话说，一致性模型的顺序越高，允许的执行次数越少，副本之间的分歧就越少。你走的越低，允许的执行越多，副本之间的分歧越大。而且，正如你所看到的，这是一个偏序——有许多对一致性模型，其中一个都不比另一个强。
刚才，我们看了这个空间的两点。我们刚才谈到的因果一致性在左边结束了。我们之前谈到的强收敛性并没有出现在 Viotti 和 Vukolić 的身上，尽管他们确实在他们的论文中谈到了这一点。如果确实出现了，它必须是右侧“强最终一致性”和左侧“因果+一致性”的下限。
虽然图中没有出现强收敛，但我认为独立考虑它是一个很好的属性，因为它是强最终一致性的安全部分。这个数字有点令人困惑，不仅因为这个偏序集合有这么多元素，还因为这个集合的一些元素将安全性和活性属性混为一谈。但如果它令人困惑，那只能说明即使弄清楚如何从分布式系统中指定我们想要的行为也很困难（更不用说实际验证这些规范是否得到满足）。
所以我们有两个问题。一个问题是为给定的应用程序确定我们想要什么策略、策略组合或策略的一部分。另一个问题是确保没有执行违反该策略。这些都是难题，程序员不应该在没有帮助的情况下独自驯服这个动物园。程序员应该拥有强大的、语言集成的工具来指定他们想要从分布式系统实现中获得的行为，然后确保他们的实现符合这些规范。
所以，这就是蓝天愿景：我们希望程序员能够机械地指定和验证正确性属性——不仅仅是模型，而是分布式系统的真实、可执行实现。此外，他们应该能够使用集成到他们用于实现的相同通用、工业强度编程语言中的验证功能来做到这一点。
我们中的许多人已经被通过表达类型系统的语言集成验证所吸引，这就是我今天要讨论的验证方法。
这将我带到了谈话的下一部分。我们刚刚讨论了分布式系统和一些我们可能想要指定和验证的属性示例；现在我们将介绍 Liquid Haskell 并转向我们如何以及是否可以使用 Liquid Haskell 来完成我们想要的。
Liquid Haskell 采用的语言集成验证方法以细化类型为中心。出于本次演讲的目的，我将细化类型定义为允许程序员指定逻辑谓词的数据类型，这些谓词限制或细化可以包含该类型的值集。根据谓词语言的表达能力，程序员可以使用细化类型指定丰富的属性，有时会以类型检查的可判定性为代价。Liquid Haskell 所基于的 Liquid 类型通过将细化谓词限制为 SMT 可判定逻辑来避免该问题。
这里有几个简单的例子，我使用 Liquid Haskell 语法编写的。
例如，我们可以定义一个称为精化EvenInt的Haskell 内置Int类型的类型，它带有一个细化谓词，我在这里强调过，它表示我们的 Int 必须能被 2 整除。
type EvenInt = { n:Int | n mod 2 == 0 }
同样，我们可以OddInt使用细化谓词定义一个类型，该谓词表示除以 2 时得到余数 1。
type OddInt = { n:Int | n mod 2 == 1 }
让我们看看如何使用这些类型。在 Liquid Haskell 中，我可以编写一个名为的函数 oddAdd，它需要两个OddInts 并返回它们的总和。参数的类型表示x和y将为奇数的前置条件，返回类型 EvenInt 表示 x + y 将评估为偶数的后置条件。
oddAdd :: OddInt -> OddInt -> EvenInt oddAdd x y = x + y
Liquid Haskell 通过生成在编译时由底层 SMT 求解器检查的验证条件来自动证明此类后置条件成立。如果求解器发现验证条件无效，则类型检查失败。例如，如果返回类型为 oddAdd，OddInt 则 oddAdd 函数将无法进行类型检查，Liquid Haskell 将产生类型错误消息。
虽然这对于熟悉细化类型的人来说都不是什么新鲜事，但值得指出的是，就我们目前所见，我们已经可以做一些相当有用的事情了。例如，这里有一个 tail 从 Haskell Prelude（Haskell 的标准库）调用的函数，给定一个列表，它给出了该列表头部之后的所有内容，该列表必须是非空的。如果你要调用 tail 一个空列表，你会在运行时得到一个异常。
tail :: [a] -> [a]
tail (_:xs) = xs
tail [] = error "oh no!"
使用细化类型，我们可以给出 tail 一个表示其输入不能是空列表的类型。
tail :: { l:[a] | l /= [] } -> [a]
tail (_:xs) = xs
如果我们这样做，那么我们实际上可以摆脱空列表的情况，使我们的代码更简单一些。
此外，我们还可以在返回类型中添加一个细化谓词，tail 这将说明它返回的列表的长度；特别是，它比参数列表的长度短一个。所以现在 tail 有一个后置条件，可能对 tail。
tail :: { l:[a] | xs /= [] } -> { l':[a] | len l - 1 == len l' }
到目前为止，这几乎是你对细化类型系统的期望。然而，我认为 Liquid Haskell 真正闪耀的地方在于，它允许你超越指定单个函数的前置条件和后置条件，并允许你使用一种称为细化反射的机制来验证不特定于任何特定函数定义的外部属性。让我们回到偶数和奇数的例子，看看它会是什么样子。
这是一个名为 sumEven 的类型 sumEven 表示 oddAdd 返回偶数的外在属性。实际上，sumEven 是一个 Haskell 函数，它返回一个返回偶数的证明 oddAdd。
我们看到返回类型 sumEven 是 Proof。在 Liquid Haskell 中，这种 Proof 类型只是 Haskell 的 ()（单位）类型的类型别名。精炼谓词 Proof 指定我们要证明的属性oddAdd——即，当我们调用 时，结果将是偶数。得益于 Liquid Haskell 的细化反射机制，我们能够在 oddAdd 细化类型中指向 sumEven。
我们现在可以编写 sumEven 函数的主体：它忽略它的参数并返回 ()（单位）。sumEven 的函数体看起来并不多 - 但它是一个诚实的证明术语！它看起来不太像的原因是这个特殊的证明——如果 x 和 y 是奇数，那么调用 oddAdd x y 将评估为偶数的证明——是底层 SMT 求解器很容易自动执行的证明。如果不是这样，那么我们需要在这里编写一个更高级的证明术语，使用Liquid Haskell 提供的证明组合器。
现在，sumEven 不是太令人兴奋的财产；毕竟，它并没有告诉我们任何我们从 oddAdd。但是现在我们有了 oddAdd 在细化谓词中引用的能力，我们也可以做更多有趣的事情。例如，我可以使用 Liquid Haskell 来证明它 oddAdd 是可交换的。
这次我们返回类型的细化谓词有两次调用 oddAdd，所以我们需要一个与多次调用的结果相关的证明。再一次，Liquid Haskell 可以自动提出这个证明。它部分是通过利用底层 SMT 求解器的知识来实现的，即整数上的加法是可交换的。
虽然这两种证明都是自动的，但总的来说，情况可能并非如此。Liquid Haskell 程序员可以在细化类型中指定任意外部属性，然后程序员可以通过使用提供的证明组合器编写包含这些细化类型的程序来证明这些外部属性。
因此，Liquid Haskell 可以做的比传统的细化类型更多。它不只是让你为你正在编写的程序提供更精确的类型。它还允许你使用细化类型注释作为指定你可能想要证明的代码的任何可判定属性的地方。然后，你可以通过编写 Haskell 程序来容纳这些类型来帮助 SMT 求解器证明该属性。
我认为 Liquid Haskell 位于基于 SMT 的程序验证器（如 Dafny）和利用 Curry-Howard 对应关系的证明助手（如 Coq 和 Agda）的交叉点。Liquid Haskell 程序可以包含应用程序代码，如 oddAdd（像往常一样在执行时运行）和验证代码，如 sumEvenand 和 oddAddComm，它们只经过类型检查，但令人高兴的是，它们都只是 Haskell 程序，只是具有细化类型。
基于 Haskell 可以让程序员逐渐将代码从普通的 Haskell 移植到 Liquid Haskell，在代码中添加更丰富的规范。例如，程序员可能从 的实现开始 oddAdd，Int -> Int -> Int 然后将其细化为 OddInt -> OddInt -> EvenInt，然后证明外部属性 sumEven 和 oddAddComm，然后再使用 sumEven 和 oddAddComm 作为前提来证明另一个更有趣的外在属性。
最后要注意的是，与传统的证明助手不同，传统的证明助手需要你从用证明助手的白话语言编写的代码中提取可执行实现，在 Liquid Haskell 中，你直接证明了有关你将要执行的代码的事情运行，所以最后，你可以立即执行经过验证的代码，无需提取步骤，因此无需信任提取过程。
现在我们已经体验了 Liquid Haskell，让我们开始有趣的部分：探险记！在我的小组中，我们一直在研究如何使用 Liquid Haskell，特别是我们如何使用这种精巧的反射能力来表达和证明分布式系统实现的有趣属性。
特别是，我们有兴趣解决我在演讲开始部分讨论的两个问题：首先，确保复制的数据结构是强收敛的，其次，保证消息以因果顺序在副本中传递。我在演讲开始部分讨论的第三个问题是保证特定于应用程序的不变量成立的问题，虽然我不会专门讨论这个问题，但我会指出我们的目标之一是前两个验证任务的结果可用作验证这些应用程序级属性的模块化构建块。所以如果我们成功了，第三个任务会更容易。
首先，验证复制数据结构的强收敛性。这是与合作者 Yiyun Liu、James Parker、Michael Hicks 和 Niki Vazou 以及我的博士生 Patrick Redmond 共同完成的。回想一下，强收敛意味着如果副本以任何顺序应用了相同的更新操作集，那么它们具有相同的状态。提供此属性的数据结构称为无冲突复制数据类型或 CRDT。
就像我们之前看到的，复制数据结构的强收敛取决于对该数据结构的操作的交换性。这取决于数据结构提供了哪些操作。然而，一旦你有了交换性证明，获得强收敛的其余推理就与特定复制数据结构的细节无关。
我们能够通过在 Liquid Haskell 中的通用 CRDT 接口级别声明和证明强收敛性来利用这种独立性，然后为我们想要验证的每个单独的 CRDT 插入一个特定于数据结构的交换性证明。
在 Haskell 中，这些通用接口被称为类型类，并且能够以这种模块化方式进行这种证明需要扩展 Liquid Haskell 以添加在类型类级别声明和证明属性的能力。这实际上是一个巨大的挑战，因为在类型类被编译掉之后，Liquid Haskell 在 Haskell 代码的中间级别上运行。我的合作者扩展了 Liquid Haskell 以支持类型类，这需要对 Liquid Haskell 进行大修并带来了自己有趣的挑战，你可以在我们的 OOPSLA '20 论文中阅读所有相关内容。
一旦可以在 Liquid Haskell 中声明和证明类型类的属性，这意味着 CRDT 类型类级别的与操作无关的证明可以与单个 CRDT 级别的特定于操作的交换性证明相结合，以获得完整的强证明该 CRDT 的收敛性。
让我们仔细看看我们需要在类型类级别证明的属性，以及我们如何在 Liquid Haskell 中表达它。
所以，这里有一个用于 CRDT 的 Liquid Haskell 类型类。类型类的每个实例都有一个关联Op类型，该类型指定可以更新 CRDT 状态的操作。该 apply 方法接受一个状态，对其运行给定的操作，并返回更新后的状态。类型 lawCommut 指定了操作必须可交换的属性，单个 CRDT 实例的实现者需要提供这样的可交换性证明。
我在这里展示的是 CRDT 类型类的简化版本，它在我们的实际实现中省略了一些微妙之处。特别是，实际上并非所有操作都必须通信；相反，有一个特定于 CRDT 的“兼容”操作的概念，实际上只有兼容的操作必须是可交换的，因为 CRDT 的设计排除了不兼容的操作不能同时应用。
此外，某些操作只能在 CRDT 处于给定状态时应用。对于最简单的 CRDT，例如只增长计数器，所有操作都将相互兼容并且始终适用，而对于更复杂的 CRDT，情况并非如此。你可以在我们的论文中找到有关此兼容性概念的更多详细信息。
一旦我们能够以这种方式定义 CRDT 类型类，我们就能够在类型类级别表达强大的收敛性。这是 strongConvergence Liquid Haskell 中的财产声明。这再次从真实事物中简化，但抓住了关键思想，即如果两个操作列表是彼此的排列，那么将任一操作应用于相同的输入 CRDT 状态将产生相同的输出状态。这个属性的证明是大约 300 行 Liquid Haskell 代码。它是通过对操作列表进行归纳，并利用 CRDT 实例提供的操作交换性证明。然而，strongConvergence 证明独立于任何特定的 CRDT 实例，因此适用于所有这些实例。
我之前对应用程序代码和验证码进行了区分，我们也可以在这里看到。该 apply 函数实际上在运行时用于 CRDT 的实现。lawCommut 函数和函数永远不会在 strongConvergence 运行时运行，所以它们是验证码。
但是我们可以从 的细化类型中看出，它是对的行为 lawCommut 的一个证明，也正是由于 Liquid Haskell 的细化反射，才有可能引用in的类型。最后，作为函数调用，或者换句话说，用作引理，在 strongConvergence 的主体中，因为它太长，所以这里没有显示。
现在，CRDT 实例提供这种操作交换性证明有多容易 lawCommut？这取决于 CRDT 的复杂性。这里有几个例子。
最简单的 CRDT 之一是只能增长的计数器。此计数器上的操作只是数字，CRDT 的状态是它们的总和。对于这个 CRDT，Liquid Haskell 可以自动执行交换性证明，就像我之前展示的加法交换性证明一样。
另一方面，这里有一个更高级的 CRDT：一个支持键值对上的插入、更新和删除操作的字典，其中值本身是 CRDT 类型的。对于这个 CRDT，交换性证明占用了超过一千行代码。
交换性证明的复杂性是 CRDT 实现复杂性的结果。例如，对于这个字典 CRDT，我省略了apply函数的实现，但它有点毛茸茸。例如，如果它接收到尚未插入的键的更新操作，它将这些更新操作存储在待处理操作的缓冲区中，然后在相关插入发生时立即应用它们。
值得指出的是，这种实现复杂性是必要的，因为这些 CRDT 的设计方式几乎不需要来自底层消息传递层的排序保证。这就是为什么一个副本可以接收尚未到达该副本的密钥的更新操作的原因。虽然这确实意味着我们可以在更多设置中使用我们的 CRDT，但它为非平凡的 CRDT 提供了更加艰苦的验证工作。
尽管我们在将与 CRDT 无关的强收敛性证明与特定于 CRDT 的交换性证明分开的方式上已经有了一些模块化，但这种艰苦的验证工作表明，一种更加模块化的方法可以将较低级别的消息传递问题与较高级别的数据分开需要结构语义。这个想法将引导我们进入我将在本次演讲中讨论的第二个也是最后一个项目。
让我们回顾一下我们之前看到的示例，以激发对因果消息传递的需求。在此示例中，我用新照片更新了共享相册，我的伙伴看到了它，但是当他试图对新照片发表评论时，他与尚未获得更新的副本通信。正如我们所讨论的，这违反了消息的因果顺序：他的评论因果取决于我之前的照片添加操作。
解决此类问题的一种方法是让副本跟踪表示它们彼此传递了多少消息的元数据，并让消息携带表示它们的因果依赖关系的元数据，并且直到它的依赖关系才在副本上传递消息已经很满意了。例如，从副本 1 到我的伙伴的响应可以携带一个向量时钟，指示副本 1 知道一个消息传递，并且该向量时钟元数据可以在来自客户端的下一个请求中线程化。当请求到达副本 2 时，副本 2 可以检查向量时钟，将其与自己的时钟进行比较，确定消息是否可传递，如果需要，将消息排队，直到收到并传递了因果前面的消息。
在广播消息的情况下确保因果消息传递的经典协议称为 CBCAST 协议，是“因果广播”的缩写。该协议由 Ken Birman 等人介绍。在 90 年代初期，他们在 Isis 系统的背景下进行了容错分布式计算。
该协议确保当一个进程接收到一条消息时，该消息在必要时被延迟然后传递，这意味着仅在任何因果先前的消息已经传递之后才应用于该进程的状态。特别是，如果消息 m 的发送发生在消息 m' 的发送之前，在 Lamport 的发生之前关系的意义上，那么我们知道在所有进程中，m 的传递必须先于 m' 的传递。
在 CBCAST 中，这是通过使用矢量时钟来表示因果依赖关系，并在接收方的队列中延迟消息直到可以传递它们来完成的。通过将接收进程的向量时钟与消息的向量时钟进行比较来完成可传递性检查。
在我们最近的工作中，我和我的学生在 Liquid Haskell 中实现了 Birman 等人的 CBCAST 协议，并且我们使用 Liquid Haskell 来验证我们的实现是否具有因果传递属性。
下面是我们如何使用 Liquid Haskell 中的改进来表达观察因果传递的过程类型的简化视图。因此，一个进程会跟踪迄今为止在其上发生的事件，包括它所传递的任何消息——而该事件序列构成了它的进程历史。这种类型 ，CausalDelivery表示如果任何两条消息 m 和 m' 都出现在进程历史中作为已传递，并且 m 因果上在 m' 之前，那么这些传递必须以与其因果一致的顺序出现在进程历史中命令。因此，这实质上是从论文中获取因果传递的定义，并将其转化为我们可以对流程强制执行的属性。
现在我们已经定义了这种类型，验证任务是确保对于任何可以通过运行 CBCAST 协议实际产生的过程历史，这种因果传递属性都成立。
然后我们可以证明我在 causalDeliveryPreservation 这里调用的一个属性，它表示如果一个进程一开始就观察到因果传递，那么任何可能由协议产生的状态转换序列产生的进程也将观察到因果传递。
这需要几百行 Liquid Haskell 代码来证明，其中最有趣的部分当然是处理 deliver 操作的部分。
我认为关于这个结果有一些有趣的事情需要指出。首先，我们发现真正的关键是在状态转换系统方面实现协议。这不是原始论文中描述的方式，尽管当然所有的想法都在那里。但我们发现这是我们需要做的才能表达和证明这样的属性，我们花了一段时间才得出这个设计，尽管回想起来似乎很明显。
其次，我想指出，这个协议对消息的内容是完全不可知的。它只查看附加到消息的因果元数据，而不是消息本身。现在，这种选择也有不利之处。如果你正在实现一个端到端系统，那么如果你对正在处理的消息的语义有所了解，那么你可能能够对消息传递做出更明智的选择。
例如，一条可能被因果广播协议认为无法传递的消息在你的自定义语义下可能会更快地传递。另一方面，选择与消息内容无关意味着我们现在拥有一个通用的、经过验证的因果消息广播库，它可以作为许多应用程序的基础。
我们现在即将结束我的演讲，但如果我要谈论因果广播作为基础，那么我不禁要展示这个令人愉快的形象，我不能把它归功于 - 这个形象由目前在 CMU 攻读博士学位的 Matt Weidner 创建。这里的想法是，一旦满足基本需求——食物、水、住所、互联网——然后因果广播就位于其之上，作为 CRDT 的基础，因此也是协作软件的基础。
我之前提到过，我们的一些 CRDT 进行了艰苦的证明工作来验证，部分原因是因为这些 CRDT 没有假设来自底层网络的因果消息传递。然而，既然我们确实有这项关于验证因果广播的新工作，我的主张是执行这些 CRDT 交换性证明会更容易，我想回去重新审视这项工作并在因果广播的基础上进行构建。
相反，一些 CRDT 实际上并不需要因果广播来强收敛，例如，我之前展示的计数器 CRDT，事实上，我的主张是那些不需要因果广播的正是那些Liquid Haskell 可以自动验证 的交换性。对于那些做需要因果广播，验证任务，更不用说 CRDT 本身的实现，现在应该会变得更简单，因为我们已经建立了因果广播。
我还想补充一点，CRDT 并不是唯一可以位于这个层次结构级别的东西。一旦你有了因果广播，实现一个因果一致的数据库也变得相对简单。PL 社区已经在验证因果一致性方面做了很多出色的工作，但据我所知，这项工作并没有将因果广播协议分解到它自己单独验证的层中，这就是我们已经完成了。所以我们认为应该可以在因果广播之上以模块化方式验证因果一致性，这是我们接下来要研究的事情之一。
由于细化反射，Liquid Haskell可以习惯了把 Haskell 变成了一个证明助手，没错，我觉得这一切都是可能的，这很好。但是在 Liquid Haskell 中开发长证明是相当痛苦的。
部分问题在于，Agda 和 Coq 等更成熟的证明助手为交互式证明开发和对证明状态的洞察提供了更好的支持（例如，仍然需要证明哪些子目标才能完成部分完整的证明）。相比之下，Liquid Haskell 只提供非常粗粒度的反馈——它要么报告类型错误，这意味着你的证明没有完成，要么没有，这意味着它已经完成。
我和我的学生和合作者一直在思考如何改善这种情况，我们的建议之一是扩展 Liquid Haskell，支持 Agda 风格的类型孔，以及利用它们的交互式编辑命令。类型化的漏洞将允许程序员指出证明的未完成部分，并在与编译器的对话中逐步完成证明。虽然 GHC Haskell 已经拥有自己的受 Agda 启发的类型孔支持，但我们认为如果结合 Liquid Haskell 的细化类型和 SMT 自动化，类型孔将特别强大和有用。
我们去年在 HATRA 研讨会上发表了一篇关于这个想法的简短论文，但是还有很多工作要做，所以我会邀请任何有兴趣在这里提供帮助的人合作。
总而言之，我们看到我们可以使用 Liquid Haskell 的细化类型来表达有关复制数据结构的收敛性的属性，并使用 Liquid Haskell 的细化反射和证明组合从外部证明这些属性。同样，我们可以表达和证明广播消息在流程中传递的顺序的属性，这应该能够更容易地在消息传递层之上实现和验证应用程序，无论是 CRDT 还是其他任何东西。虽然 Liquid Haskell 可以胜任这项任务，但我们仍然认为它可以更容易使用，我们期待继续改进它。
推荐阅读：
分布式实验室策划的《Kubernetes线上实战训练营》正式上线了。这门课程通过4天线上培训，3个课后大作业，30天课后辅导，把Kubernetes的60多个重要知识点讲给你，并通过实战让你掌握Kubernetes。培训重实战、重项目、更贴近工作，边学边练，10月29日正式开课。
👇 点击下图加入学习👇
原文始发于微信公众号（分布式实验室）：回答有关分布式系统的几个核心问题
- 左青龙
- 微信扫一扫
-
- 右白虎
- 微信扫一扫
-
评论