如何验证线性一致性

  

线性一致性(Linearizability)是分布式系统中常见的一致性保证。那么如何验证系统是否正确地提供了线性一致性服务呢?本文希望从‘什么是线性一致性’,‘如何验证线性一致性’,问题复杂度,常见的通用算法,以及工程实现五个部分,直观、易懂地回答这个问题。

MAURICE P. HERLIHY 和 JEANNETTE M. WING曾在“ Linearizability: A Correctness Condition for Concurrent Objects ” 中对线性一致性给出了形式化的定义和证明,对分布式系统来说,简单的讲就是即使发生网络分区或机器节点异常,整个集群依然能够像单点一样提供一致的服务,即依次原子地执行每一条操作。假如我们可以站在最终操作执行的视角,将整个系统看做一个整体,一个保证线性一致性的服务应该如下图所示进行服务:
如何验证线性一致性

由于每条操作是依次、原子的执行,相互之间没有重叠,为了方便理解,可以把一个操作在图上简化为一个点。如下图所示:

如何验证线性一致性

然而,实际情况中,分布式系统通常是很多节点作为一个整体对外提供服务,并在内部处理网络或节点异常,我们无法站在上帝视角看到其执行序列。同时,我们真正关心的也是其作为一个整体对外的表现,而不是其中的每个单独节点。我们所能做的是站在客户端的角度,通过读写事件的发起和结束来感知整个系统。正如站在地球上仰望星空,通过光来感知天体,看到的每一次闪烁,可能真正发生在上万年之前。因此,下图才是真正可以看到的情况:
如何验证线性一致性

上图,展示了在每个客户端看来,其请求从发起到结束的时间点。因此,我们希望通过一系列客户端的执行和返回序列来判断系统是否正确提供了线性一致性服务。

为了判断系统是否正确提供了线性一致性,首先在运行过程中获得一系列不同的执行历史,接着验证每组历史是否满足线性一致性,只要有一个不满足,便可以说系统不满足线性一致性。但如果没有发现不满足的历史,也不证明系统一定正确。然而,在工程中通过对大量的执行历史的验证,使得我们对自己的系统更充满信心,这就足够了。那么现在的问题转变为:如何验证一组执行历史是否满足线性一致性

通过客户端可以看到一个读写请求的发起和结束时间,而其真正在服务端的执行可能发生在开始和结束中间的任意一点。因此,验证线性一致性的关键就是找到一组依次执行的序列,如果这组执行序列存在,则可以说这组执行历史是满足线性一致的,如下图所示:
如何验证线性一致性
明显的,存在这么一组序列,因此我们说这组执行历史是符合线性一致性的。再来看一个不符合线性一致性的例子,如下图,可以看出,由于Client 3已经读到1,说明在Client 3请求结束前Client 2已经写成功,而又没有其他请求再次修改x的值,因此Client 4不应该在之后读到0。
如何验证线性一致性
实践中,通常会通过在频繁注入异常的情况下,随机生成请求序列,收集执行的发起和结束历史,并寻找合理的线性执行序列,如Jespen。

直观来看,这个问题是一个排序问题,极端情况下的时间复杂度为O(N!)。事实上,Phillip B. Gibbons和Ephraim Korach在Testing Shared Memories中已经证明其是一个NP-Complete问题。虽然Gavin Lowe在Testing for Linearizability中给出了一些特殊限制下的多项式甚至是线性复杂度的算法,但在通用场景下,判定线性一致性并不是一个容易解决的问题,其搜索空间会随着执行历史的规模急速膨胀。

虽然判定线性一致性的复杂度极高,但我们还是能够通过一些技巧,在大多数场景下,在工程可接受的时间内给出结果,这里介绍三个常见的,且一脉相承的通用算法。在此之前,先对算法面临的问题进行抽象,以下图执行历史为例,给出算法的输入和期待的输出:

如何验证线性一致性

如何验证线性一致性