Notes

Graph View

Linearizability

3 min read

What is Linearizability?

Linearizability is the strongest consistency model, referred as **Strong Consistency**

This consistency model works as if all the operations are running in a single system and not distributed, because the sequential history operations is stored.

So the responses/results are always consistent and won’t be stale.

The operations are maintained in Total Ordering (Linear Order) with comparator being time. No partial ordering or convergence is observed. [ref]

  • If operation A completes before operation B starts, the system orders A before B in real-time.
  • If neither A nor B completes before the
    other starts, then there is no guarantee that these events will be
    ordered in real-time. However, there would still be some total order.

Linearizability is similar to using threads in a program without using locks — any concurrent accesses to the same data are races. It’s possible to program correctly this way but it requires care.

The next strongest consistency notions involve transactions, as found in many databases, which effectively lock any data used. For programs that read and write multiple data items, transactions make programming easier than linearizability. Serializability is one consistency model that provides transactions.

Linearization Points

image 31.png

https://excalidraw.com/#json=m6wkXjdiX_SQ6lNBtRmOk,EYpwytltQIEYaF8wXUxT0Q

This history is linearizable. We can show this by explicitly finding linearization points for all operations (drawn in orange above). The induced sequential history, Put("x", 0), Get("x") -> 0, Put("x", 1),Get("x") -> 1, is a correct history with respect to the sequential specification. Now, a non linearizable example.

image 1 20.png

https://excalidraw.com/#json=yFGCxOgmFB0nUrrDzF6De,5FQoQQddLSueH-uMnJAKrA

There is no linearization of this history with respect to the sequential specification: there is no way to assign linearization points to operations in this history.

We could start assigning linearization points to the operations from clients 1, 2, and 3, but then there would be no way to assign a linearization point for client 4: it would be observing a stale value.

Similarly, we could start assigning linearization points to the operations from clients 1, 2, and 4, but then the linearization point of client 2’s operation would be after the start of client 4’s operation, and then we wouldn’t be able to assign a linearization point for client 3: it could legally only read a value of 0 or -1 (xis not present).

Linearizability checkers will try to find if there are any points that satisfy by literally brute forcing combinations. They’re also optimized to eliminate some combinations, to fasten the linearizability test.

wrt Serializability

Backlinks

Graph View