It's well known in distributed system community that linearizability testing is NP-complete. Luckily, in a common use-case it's possible to check linearizability in polynomial time.
Linearizability is a correctness condition for a concurrent system, in which all execution histories are equivalent to a correct sequential history, with a constraint on a wall-clock time (absolute time).
It requires that all the data operations appear to have executed atomically in some sequential order that is consistent with a global order (wall-clock time) of non-overlapping operations. Hagit Attiya and Jennifer L Welch: “Sequential Consistency versus Linearizability,” ACM Transactions on Computer Systems (TOCS), volume 12, number 2, pages 91–122, May 1994. doi:10.1145/176575.176576
Fun fact! Linearizability is expensive in distributed systems and in multithreaded programming, so both fields have relaxed models :) eventual consistency and out-of-order execution.
E.g. the JVM's out-of-order execution makes it necessary to explicitly control the visibility of the changes by using such primitives as "volatile" variables. Please read the astonishing post by Aleksey Shipilёv on Safe Publication and Safe Initialization in Java for more information, examples of linearizability violations and the ways to prevent it.
Violations of linearizability in the distributed systems are similar, for example, it's a violation when Alice successfully writes a value to a key/value storage, calls Bob via an off-system channel, asks him to read a value and he reads some other value.
It's a process of searching linearizability violations in a black box system claiming to provide it.
Usually, the process consists of two parts. The first part executes a real world scenario against a system using failure injections and keeps per-client logs of operations (operation, start time, end time, result). The second part digests the logs and checks if an execution is an equivalent to a sequential execution.
Of course linearizability testing is an overloaded term, so it also means a class of algorithms describing how the second part of the process works. I use the latter definition.
Alex Horn and Daniel Kroenin write in the Faster linearizability checking via P-compositionality paper:
The problem of checking linearizability is NP-complete. This high computational complexity means that writing an efficient linearizability checker is inherently difficult. The problem is to find ways of pruning a huge search space: in the worst case, its size is O(N!)
Where N is the number of operations in the log.
Anish Athalye wrote an excellent post Testing Distributed Systems for Linearizability where he proved its NP-completeness with a very elegant example.
Not really 😏 In a common use-case a linearizable system can be replaced with a sequentially consistent system with compare-and-set without loss of generality. And the latter can be checked with polynomial time.
It's an environment when concurrent clients need to work with strongly consistent distributed key/value storage. The concurrent nature of the clients implies the need for concurrency control mechanisms like compare and set.
The examples of well-known systems which fit this use case are DocumentDB, ZooKeeper, Etcd, DynamoDB, MongoDB, HBase, CockroachDB, and others.
Let's assume that we use CAS for every write. (We don't lose generality here because otherwise even linearizable storage wouldn't prevent certain anomalies like lost updates caused by the concurrent clients)
Then use wiki to revise what the sequential consistency guarantees:
the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program
And combine things together: sequential consistency linearizes writes, CAS makes sure that they capture causality and the in-process order gives read-you-writes consistency, so the only possible anomaly is the stale reads. Let's fix it by using linearizability of writes to linearize reads:
As a result, we found a way to use a sequentially consistent system as a strongly consistent system 🙌
Of course, it looks expensive to write after each read but:
Now let's return to the question how to test that a system is sequentially consistent.
Phillip B. Gibbons and Ephraim Korach explored complexity of the linearizability testing in the Testing shared memories paper. They noticed that when read-mapping and write-order are provided the problem jumps into O(n ln n) complexity class.
What is read-mapping? It is a situation when for each read operation, it is known precisely which write wrote that value.
What is write-order? There is a total order on the write operations which resolves ambiguity when writes overlap. So for any two writes, it's known which happened before another.
Hopefully, those restrictions aren't exotic, if we use CAS for every write then the above conditions are satisfied.
Indeed, we can say which write is responsible for a given read — we just need to take a look on the etag field of the read record and pick a write with the same value of its etag record. Also, the prevEtag field defines a total order on the writes so we have the write-order too.
Not really, the problem hides behind DateTime.now() — we need it to return absolute time but it's physically impossible. A distributed system is a physical system and follows the laws of nature. Since there is no absolute time in real word then we can't guarantee that DateTime.now() would yield it.
It looks like a failure but Testing shared memories has another result: when we know read-mapping and write-order the problem of sequential consistency testing also jumps into O(n ln n).
In the next post, we'll do impossible and check linearizability in linear time, stay tuned :)