Shulou(Shulou.com)06/01 Report--

Linear consistency (Linearizability) is a common consistency guarantee in distributed systems. So how to verify that the system provides linear consistency services correctly? This paper hopes to answer this question intuitively and easily from five parts: "what is linear consistency", "how to verify linear consistency", problem complexity, common general algorithms, and engineering implementation.

What is linear consistency?

MAURICE P. HERLIHY and JEANNETTE M. WING have given a formal definition and proof of linear consistency in "Linearizability: A Correctness Condition for Concurrent Objects". For distributed systems, simply speaking, even if a network partition or machine node exception occurs, the whole cluster can still provide consistent services like a single point, that is, performing each operation in turn. If we can look at the whole system as a whole from the perspective of the execution of the final operation, a service that ensures linear consistency should be served as shown in the following figure:

Since each operation is performed sequentially and atomically, and there is no overlap with each other, in order to facilitate understanding, an operation can be simplified to a point on the graph. As shown in the following figure:

However, in the actual situation, many nodes usually provide services as a whole and handle network or node exceptions internally, so we can not see its execution sequence from the perspective of God. At the same time, what we really care about is its external performance as a whole, not each individual node. What we can do is to perceive the whole system from the point of view of the client, through the initiation and termination of read and write events. Just like standing on the earth looking up at the starry sky and perceiving celestial bodies through light, every flicker you see may have really happened tens of thousands of years ago. Therefore, the following figure is what you can really see:

The figure above shows the point in time from the initiation to the end of the request for each client. Therefore, we hope to judge whether the system provides linear consistency service correctly through a series of client execution and return sequences.

How to verify linear consistency

In order to judge whether the system provides linear consistency correctly, we first obtain a series of different execution histories in the process of operation, and then verify whether each group of history satisfies the linear consistency, as long as one of them is not satisfied. it can be said that the system does not satisfy linear consistency. However, if there is no history of dissatisfaction, it does not prove that the system must be correct. However, through the verification of a large number of implementation history in the project, it is enough to make us more confident in our own system. So the question now turns to: how to verify whether a set of execution history satisfies linear consistency.

Through the client, you can see the initiation and end time of a read and write request, and its real execution on the server may occur at any point in the middle between the start and the end. Therefore, the key to verifying linear consistency is to find a set of sequentially executed sequences. if this set of execution sequences exists, it can be said that this set of execution history is linearly consistent, as shown in the following figure:

Obviously, there is such a set of sequences, so we say that this set of execution history is linearly consistent. Looking at another example that does not conform to linear consistency, as shown in the following figure, you can see that Client 3 has read 1, indicating that Client 2 has successfully written before the end of the Client 3 request, and there are no other requests to change the value of x again, so Client 4 should not read 0 later.

In practice, we usually randomly generate request sequences in the case of frequent injection exceptions, collect the initiation and end history of execution, and find reasonable linear execution sequences, such as Jespen.

Problem complexity

Intuitively, this problem is a scheduling problem, and in extreme cases, the time complexity is O (N!). In fact, Phillip B. Gibbons and Ephraim Korach have proved to be a NP-Complete problem in Testing Shared Memories. Although Gavin Lowe gives some algorithms of polynomial or even linear complexity under special restrictions in Testing for Linearizability, in general scenarios, determining linear consistency is not an easy problem to solve, and its search space will expand rapidly with the scale of execution history.

General algorithm

Although the complexity of determining linear consistency is extremely high, we can still use some techniques to give results within an acceptable time for engineering in most scenarios. Here are three common general algorithms that come down in one continuous line. Before that, the problems faced by the algorithm are abstracted. The following figure shows the input and expected output of the algorithm as an example:

Input: call history

1MagneClient1: Invoke Put Xen02: Invoke Put Xeno13: Return Put Xen04: Invoke Get x5: Invoke Get x6Client3: Return Get 17: Return Put X6Client4: Return Get 08Client2: Return Put Xen1

Output: execution sequence

Client1 Put x=0Client4 Get 0Client2 Put x=1Client3 Get 11PowerWG algorithm

In the call history of a request, there is a partial order relationship: Prev. If the Return of one request occurs earlier than the Invoke of another request, we call it Prev another request. Obviously, this kind of partial order relation must be preserved in the consistency verification algorithm. Misfortune and good fortune depend on, and it is this reservation of partial order relation that gives the algorithm the possibility of acceleration. The idea of the WG algorithm is very simple: find out the items without Prev from the call history, execute and take out the corresponding request, and then repeat the algorithm for the rest of the call history until there is no more call history or the execution result is not satisfied.

As in the example above, "Client1 Put xpendo" and "Client2 Put xpend1" can be taken out first because they do not have any request Return before their Invoke. If you select "Client1 Put xero0", take their corresponding Invoke and Return from the call history and get a new history:

2 Invoke Put client 2: Invoke Get x6: Invoke Get X6 client 3: Return Get 17 peer 4: Return Get 08 parade client 2: Return Put x5

And a serialized request:

Client1 Put Xero0

At this point, you can see that for the rest of the history, there is no other requested Return before the Invoke of each request, so it can be used as the next choice to fetch. Suppose Client3 Get 1 is selected this time, however, it is obvious that the result of executing Get at this time should be 0, which is different from the return of 1 from the actual execution result of the request. In this case, you need to fallback and try other fetch strategies. You can see that the WG algorithm is actually a depth-first search of the tree. The search tree is shown in the figure below, where each node identifies the Invoke sequence number in the call history corresponding to the request that you try to serialize:

Because you can stop when you find a linear sequence, the dotted part of it will not be actually executed.

2dwgl algorithm

The WGL algorithm is improved by Gavin Lowe on the basis of the WG algorithm. The main way of improvement is to prune the search tree: to reduce repeated searches by caching configurations that have been seen before. The cache configuration consists of two parts:

Requests that are currently serialized

Current x value

As you can see from the search process above, if the current serialized request is exactly the same as the current x value, the subsequent search process must be the same, so it can be skipped.

3This algorithm is based on Prelectionality algorithm.

The P-compositionality algorithm uses the Locality principle of linear consistency, that is, if all sub-histories of a call history satisfy linear consistency, then the history itself also satisfies linear consistency. Therefore, some unrelated histories can be separated to form multiple smaller sub-histories, which in turn verify the linear consistency of these sub-histories, such as operations on different key in kv data structures. It is mentioned above that the computing time of the algorithm expands rapidly with the increase of the historical scale, and P-compositionality is equivalent to using the divide-and-conquer method to reduce the historical scale, which will be very useful in scenarios where molecular problems can be delimited.

Why would Solitaire

In engineering practice, not only distributed systems, but also systems that need parallel access may need to verify the linear consistency function exposed by the system. Of course, there are many tools to verify linear consistency, such as Knossos used by the famous Jespen, which is a Clojure version of the WGL algorithm implementation; Porcupine is a Go version of the P-compositionality implementation; linearizability-checker is an example of the P-compositionality algorithm author's own implementation. However, there are still several problems in use that remain unsolved:

Slow computing: due to the complexity mentioned above, the verification time of consistency algorithms is usually the bottleneck in related tests. Speed up its calculation as much as possible, and verify more history at the same time, which is very important to find potential problems in the system.

Single data model: most verification tools are oriented to KV interfaces, which requires users to convert different actual system interfaces into KV interfaces, which will mask many complexities in the system, such as losing the verification of mutual coverage operations after converting Device interfaces into KV.

Specific analysis of specific problems: for some data models, there may be algorithms with polynomial or even linear complexity, so using the general WGL algorithm for these data models is too far away.

Solitaire (https://github.com/CatKang/Solitaire) is a C++ implementation, faster, supports multiple data models of linear consistency detection tool, dedicated to solve the above problems. Its name comes from the famous Windows desktop card game of the last century, which requires players to organize the messed-up playing cards into order under the restriction of the size first order. It can be said that it fits well with our linear consistency verification work.

Referenc

Linearizability: A Correctness Condition for Concurrent Objects

Testing for Linearizability

Faster linearizability checking via P-compositionality

Testing Distributed Systems for Linearizability

Testing Shared Memories

Linear consistency theory

Solitaire: a faster consistency verification tool that adapts to more data models

Knossos: the consistency verification tool used by Jespen and the implementation of WGL algorithm

Porcupine: implementation of P-compositionality algorithm in go version

Linearizability-checker: implementation of P-compositionality algorithm

Jespen

Original link: https://mp.weixin.qq.com/s/calyZj0-ZfiYuDlJWQoHaA

Welcome to subscribe "Shulou Technology Information " to get latest news, interesting things and hot topics in the IT industry, and controls the hottest and latest Internet news, technology news and IT industry trends.