MIT-6.824-lecture4: Consistency, Linearizability

Preparation

Testing Distributed Systems for Linearizability

分布式系统的正确实现颇具挑战性，因为它们必须应对并发和故障。网络可能会延迟、重复、重新排序甚至丢弃数据包，而机器也可能随时发生故障。即便设计在理论上被证明是正确的，在实际实现中仍然难以避免那些微妙的错误。

除非我们选择使用形式化方法¹，否则如果我们希望确保实现是正确的，就必须对系统进行测试。然而，测试分布式系统同样充满挑战。并发性和不确定性使得在测试中捕捉错误变得困难，尤其是当那些最微妙的错误仅在某些不常见的情况下才会显现，例如同时发生机器故障或极端的网络延迟。

¹ 形式化方法：指使用数学模型和方法来验证系统正确性的一种技术。

Correctness

在我们讨论如何测试分布式系统的正确性之前，首先需要明确“正确”的含义。即便是看似简单的系统，精确地描述系统应该如何运行也是一个复杂的过程²。

以一个简单的键值存储系统为例，类似于etcd，它将字符串映射到字符串，并支持两种操作：Put(key, value) 和 Get(key)。首先，我们考虑它在顺序执行情况下的行为。

² 复杂的过程：指定义系统行为时需要考虑多种因素和细节，以确保描述的准确性和全面性。

Sequential Specifications

我们可能对键值存储在顺序操作下的行为有一个直观的理解：Get操作必须反映所有先前Put操作的结果。例如，我们可以执行一个Put(“x”, “y”)，然后随后的Get(“x”)应该返回”y”。如果操作返回了例如”z”，那就是不正确的。

比起用英语描述，我们可以将键值存储的规范写成可执行的代码，这样更加正式：

class KVStore:
    def __init__(self):
        self._data = {}

    def put(self, key, value):
        self._data[key] = value

    def get(self, key):
        return self._data.get(key, "")

这段代码虽然简短，但它涵盖了所有重要的细节：初始状态、操作如何修改内部状态，以及键值存储调用返回的值。规范还明确了当Get()被调用在一个不存在的键上时会发生什么，但总的来说，它与我们直观的键值存储定义是一致的。

Linearizability

接下来，我们考虑键值存储在并发操作下的行为。需要注意的是，顺序执行的规范并没有告诉我们并发操作下会发生什么。例如，顺序规范并没有说明在以下场景中键值存储的行为：

在这种情况下，Get(“x”)操作应该返回什么值并不明显。直观上，我们可能会说，由于Get(“x”)与Put(“x”, “y”)和Put(“x”, “z”)是并发的，它可以返回任意一个值，甚至是””。如果我们有一个场景，另一个客户端在很久之后执行了Get(“x”)，我们可能会说该操作必须返回”z”，因为这是最后一次写入的值，而最后一次写操作并没有与其他写操作并发。

我们基于顺序规范，使用一种称为线性一致性的一致性模型来正式指定并发操作的正确性。在线性一致性系统中，每个操作看起来都是原子性地且瞬时地在调用和响应之间的某个时间点执行。除了线性一致性之外，还有其他一致性模型，但许多分布式系统提供了线性一致性的行为：线性一致性是一种强一致性模型，因此在其基础上构建其他系统相对容易。

考虑一个包含键值存储操作的调用和返回值的历史示例：

这个历史是线性一致的。我们可以通过显式地为所有操作找到线性化点（在下图中用橙色标出）来证明这一点。由此产生的顺序历史是：Put(“x”, “0”)，Get(“x”) -> “0”，Put(“x”, “1”)，Get(“x”) -> “1”，这是相对于顺序规范的正确历史。

相比之下，这个历史不是线性一致的：

这个历史没有相对于顺序规范的线性化：我们无法为这个历史中的操作分配线性化点。我们可以从客户端1、2和3的操作开始分配线性化点，但随后将无法为客户端4分配线性化点：它将观察到一个陈旧的值。同样，我们可以从客户端1、2和4的操作开始分配线性化点，但客户端2的操作的线性化点将在客户端4的操作开始之后，然后我们将无法为客户端3分配线性化点：它合法地只能读取””或”0”。

Testing

有了对正确性的明确定义，我们就可以思考如何测试分布式系统。通常的方法是在随机注入故障（如机器故障和网络分区）的情况下测试系统的正确操作。我们甚至可以模拟整个网络，从而实现诸如造成极长网络延迟等操作。由于测试是随机的，我们希望多次运行这些测试，以确保系统实现的正确性。

Ad-hoc testing

我们如何实际测试系统的正确操作呢？对于最简单的软件，我们通过输入输出用例进行测试，例如assert(expected_output == f(input))。我们也可以对分布式系统采用类似的方法。例如，对于我们的键值存储，我们可以编写以下测试，其中多个客户端并行地对键值存储执行操作

for client_id = 0..10 {
    spawn thread {
        for i = 0..1000 {
            value = rand()
            kvstore.put(client_id, value)
            assert(kvstore.get(client_id) == value)
        }
    }
}
wait for threads

如果上述测试失败，那么键值存储显然不是线性一致的。然而，这个测试并不够全面：存在一些非线性一致的键值存储系统会始终通过这个测试。

Linearizability

更好的测试方法是让并行客户端执行完全随机的操作，例如反复调用kvstore.put(rand(), rand())和kvstore.get(rand())，可能限制在一个小的键集合上以增加竞争。但在这种情况下，我们如何确定什么是“正确”的操作呢？在更简单的测试中，每个客户端操作的是不同的键，因此我们可以准确预测输出。

当客户端并发地操作同一组键时，事情变得更加复杂：我们无法预测每个操作的输出，因为答案并不唯一。因此，我们必须采用另一种方法：通过记录系统上所有操作的历史，然后检查该历史是否相对于顺序规范是线性一致的，来测试系统的正确性。

Linearizability Checking

线性一致性检查器将顺序规范和并发历史作为输入，并运行决策程序来检查历史是否相对于规范是线性一致的。

NP-Completeness

不幸的是，线性一致性检查是NP完全的。证明其实相当简单：我们可以证明线性一致性检查属于NP，并且可以证明一个NP难问题可以归约为线性一致性检查。显然，线性一致性检查属于NP：给定一个线性化点（即所有操作的线性化点），我们可以在多项式时间内检查它是否是相对于顺序规范的有效线性化。

为了证明线性一致性检查是NP难的，我们可以将子集和问题归约为线性一致性检查。回顾一下，在子集和问题中，我们给定一个非负整数集合 $S = { s_1, s_2, … , s_n }$ 和一个目标值$t$,我们需要确定是否存在一个子集 $S$ 的和等于
$t$。我们可以将这个问题归约为线性一致性检查，如下所示。考虑以下顺序规范：

class Adder:
    def __init__(self):
        self._total = 0

    def add(self, value):
        self._total += value

    def get(self):
        return self._total

并考虑以下历史：

这个历史是线性一致的，当且仅当子集和问题的答案是“是”。如果历史是线性一致的，那么我们可以取所有在Get()操作的线性化点之前的Add(s_i)操作，这些操作对应于一个子集中的元素 $s_i$，其和为 $t$。如果集合确实有一个子集的和为 $t$，那么我们可以通过让对应于该子集中元素 $s_i$的Add(s_i)操作在Get()操作之前发生，而其余操作在Get()操作之后发生，来构造一个线性化操作。

Implementation

尽管线性一致性检查是NP完全的，但在实践中，它在小规模历史记录上可以很好地工作。线性一致性检查器的实现会接收一个可执行的规范和一个历史记录，并运行搜索程序来尝试构建一个线性化，使用一些技巧来限制搜索空间的大小。

现有的线性一致性检查器如Knossos，它被用于Jepsen测试系统中。不幸的是，当我尝试测试自己编写的分布式键值存储实现时，我发现Knossos无法检查我的历史记录。它似乎在小规模历史记录上工作得还可以，比如在只有几个并发客户端的情况下，总共大约有100个历史事件，但在我的测试中，我有数十个客户端生成了数千个事件的历史记录。

为了能够测试我的键值存储，我编写了Porcupine，一个用Go实现的快速线性一致性检查器。Porcupine检查历史记录是否相对于用Go编写的可执行规范是线性一致的。根据经验，Porcupine比Knossos快数千倍。我能够使用它来测试我的键值存储，因为它能够在几秒钟内检查包含数千个事件的历史记录。

Effectiveness

使用故障注入和线性一致性检查来测试线性一致的分布式系统是一种有效的方法。

为了比较临时测试和使用Porcupine进行线性一致性检查的效果，我尝试使用这两种方法测试我的分布式键值存储。我尝试在实现中引入不同类型的设计错误，例如会导致陈旧读取的修改，并检查哪些测试会失败。临时测试捕捉到了一些最明显的错误，但无法捕捉到更微妙的错误。相比之下，我无法引入任何一个线性一致性测试无法捕捉的正确性错误。