Tang Liu translation

Recently I saw a article www.anishathalye.com/2017/06/04/… “Was written so well that it was decided to translate it into Chinese with the consent of the author Anish. However, some parts will not be translated verbatim and will be adjusted slightly for better understanding.

Implementing a distributed system correctly is very challenging because of the concurrency and failure issues that need to be handled well. Network packets can be delayed, repeated, out of order, or discarded, and machines can go down at any time. Even if some designs are proved correct by the paper, it is still difficult to avoid bugs in the implementation.

Unless we use the formal method [^1], we need to test the system even if we assume that the implementation is correct. Testing distributed systems can also be very challenging. Concurrency and uncertainty make it very difficult to catch bugs during testing, especially in extreme cases such as simultaneous machine downtime or extreme network latency.

correctness

Before discussing the correctness of testing distributed systems, let’s first define what “correctness” means. Even for simple systems, it can be quite complicated to be completely sure that the system meets expectations [^2].

Consider a simple key-value system, such as ETCD, that supports two operations: Put(key, value) and Get(key). First, we need to consider its behavior in the sequential case.

Order specifications

For a key-value store, we can have an intuitive understanding of its behavior below the sequential operation: if the Get operation is after the Put operation, it must Get the result of the Put. For example, if Put(“x”, “y”), then Get(“x”) will Get “y”. If you Get “z”, then this is not true.

We use Python to define a simple key-value store:

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, "")Copy the code

The code above is relatively simple, but contains enough information about what the initial state is, how the internal state is changed by the result of the operation, and what the result is from the operation in the key-value store. Note here that Get() returns an empty string for non-existent keys.

Linear consistency

Next, let’s consider how our key-value store behaves under concurrency. Note that the ordering specification does not specify what happens under concurrent operations. For example, the ordering specification does not say what key-value stores will allow in the following scenario.

It is not immediately clear what the Get(“x”) operation will allow to return. Intuitively, we can say that Get(“x”) is executed with Put(“x”, “y”) and Put(“x”, “z”), so it can possibly return a value, or even “”. If another Get(“x”) operation is executed later, we can say that this must return “z” because it was last written and there are no other concurrent writes at that time.

For concurrent operations based on sequential specifications, we use a consistency model, that is, linear consistency, to illustrate its correctness. In a linear consistent system, any operation can be performed atomically and instantaneously between calls or returns. In addition to linear consistency, there are other consistent models, but most distributed systems provide linear consistency operations: Linear consistency is a strong consistent model, and it is easy to build other systems based on linear consistency systems. Consider the following historical example of a key-value store operation:

The history is linear. In the blue area of the image below, we have realistically indicated the point of linear consistency. Put the order history (” x “, “0”), Get (” x “) – > “0”, the Put (” x “, “1”), Get (” x “) – > “1”, for the order specification is a history of right.

Correspondingly, the history below is not linearly consistent.

For the sequential specification, this history is not linearly consistent: we cannot specify linearly consistent points in the historical operation. We can draw clients 1,2 and 3, but we can’t draw client 4, because it’s obviously an expired value. Similarly, we could draw clients 1,2 and 4, so the operation on client 2 would definitely come after the operation on 4, but then we wouldn’t be able to handle client 3, which would only legally return “” or “0”.

test

With a correct definition, we can consider how to test distributed systems. The usual practice is to do random error injection over and over again for the correct operation, such as machine downtime, network isolation, etc. We can even simulate the entire network, so we can do long network delays and so on. Because testing is random, we need to run it many times to make sure that a system implementation is correct.

Specialized test

How do we actually test for correct operations? In the simplest software, we can use an input and output test, such as assert(Expected_output == F (input)). We can also use a similar method on distributed systems, such as the Key-value store, When multiple clients start performing operations, we can have the following tests:

forclient_id = 0.. 10 { spawn thread {fori = 0.. 1000 { value = rand() kvstore.put(client_id, value) assert(kvstore.get(client_id) == value) } } }wait for threadsCopy the code

If the test fails, then the system must not be linearly consistent, and of course, the test is not very complete, because it is possible that systems that are not linearly consistent may pass the test.

Linear consistency

A better approach is for concurrent clients to run entirely random operations. For example, repeating calls to kvstore.put(rand(), rand()), and kvstore.get(rand()) can increase the probability of conflicts with very few keys. But how do we define what is the right thing to do in this case? In the simple test above, because each client operates on a separate key, we can be very clear about the output.

But when clients concurrently operate on the same heap of keys, things get complicated. We can’t predict the return value of every operation because there is no single answer. But we can do it another way: we can record the history of the entire operation and then verify that the operation history is linearly consistent.

Linear consistency verification

A linear conformance validator takes a sequential specification and a history of concurrent operations, and then executes a decider to check whether the history is linearly consistent under the specification.

NP complete

Unfortunately, linear consistency verification is NP-complete. The proof is very simple: we can show that linear consistency verification is an NP problem, and we can also show that an NP hard problem can be reduced to linear consistency verification. Obviously, linear consistency verification is NP problem. For example, the linear consistency points of all operations can be verified in polynomial time according to the relevant order specification.

To show that linear consistency verification is NP hard, we can reduce the subset problem to linear consistency verification. For the subset problem, we give the non-negative set S={s1,s2… Sn} and the target result t. Then we must determine whether there exists a subset S whose sum is equal to t. We can simplify this problem to the following linear consistency verification. Consider the order specification:

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

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

    def get(self):
        return self._totalCopy the code

And history:

History is linear only if the answer to the subset problem is “yes”. If the history is linear, then we assume that for any Add(s_i) operation, there is a point of linear consistency before Get(), and this corresponds to Si in the subset, whose union is t. If the sum of a subset of the set is t, we can construct a linearization of the subset Si with Add(s_i) before Get and the rest after Get().

PS: I probably know what this chapter means, but I can’t find a better expression to translate, so IT’s ok. Please read the paper later for further understanding.

implementation

Even if linear consistency verification is NP-complete, in practice it still works well on small histories. The implementation of a linear consistency validator takes an executable specification, adds a history, performs a search procedure to construct a linearization, and uses tricks to limit the search space.

In Jepsen, there is a consistency validation tool called Knossos, but unfortunately, Knossos does not work very well when testing distributed key-value stores, and may only work with a small number of concurrent clients with a history of a few hundred events. But in some tests, there are more clients, and more history events are generated. To solve the Knossos problem, the authors developed Procupine, a faster linear conformance verification tool written in Go. Porcupine uses an implementation specification developed with Go to verify that history is linear. According to actual tests, Porcupine is many times faster than Knossos.

The effect

Error injection is an effective method to test the linear consistency of distributed systems.

In contrast, the authors used both approaches when testing the key-value store with Porcupine, a dedicated test. The authors introduced different design errors when implementing their own key-value store, such as expired reads after modifications, to see if these tests would fail. Specialized tests catch a lot of bugs, but they don’t have the ability to catch more sneaky bugs. Relatively speaking, the authors have yet to find a correct bug that linear consistency testing cannot catch.

[^1]: Formal methods can guarantee the correctness of a distributed system. For example, the UM PLSE research team recently used Coq Proof Assistnt to verify the Raft consistency protocol. Unfortunately, validation requires specific knowledge, plus a lot of work to validate the actual system. Verification may one day be used in real systems, but for now, it’s more about testing than verification.

[^2]: Theoretically, all production systems will have a formal specification, and some already have one, for example Raft has a formal specification written in TLA+. Unfortunately, most systems don’t.