4. Week 04: Linearisability and Atomicity

This week, we’re starting to look at various ways to specify and verify distributed systems. Many of those approaches work equally well for more familiar concurrent (i.e., multi-threaded) programs and were introduced to reason about them in the first place. This is because back in the days the difference between concurrent and distributed systems has not been perceived as a big one, since there was not that much focus on fault-tolerance.

This week, we’ll be looking at specifying the correct behaviour of concurrent/distributed systems from the perspective of interaction with the user.

4.1. Specifying Concurrent Objects

In concurrent programming, an operation (or set of operations) is linearisable if it consists of an ordered sequence of invocation (calls) and response events (returns), that may be extended by adding response events such that:

  • The extended sequence can be re-expressed as a sequential history (is serialisable).
  • That sequential history is a subset of the original unextended sequence.

Informally, this means that the unmodified list of events is linearisable if and only if its invocations were serialisable, but some of the responses of the serial schedule have yet to return. In application to distributed systems implementing state-machine replication, this precisely means that an external client can see interaction with the replicated system as interaction with a single machine, and multiple clients, when put their respected “observations” together, can reconstruct a valid sequential history. In other words, linearisability allows to see a series of potentially overlapping concurrent operations as a fully ordered sequence of sequential operations. Because of this, sometimes “linearisablity” is being used as a synonym for “atomicity” (i.e., the property of a system that does not allow to observe it “in the middle” of operations).

Mandatory Reading

The original paper Linearizability: A Correctness Condition for Concurrent Objects by Herlihy and Wing introduces the notion. You may also want to check Week 4 slides for additional examples.

Highlights:

  • Linearisability is compositional: one can construct a linearisable system from linearisable components.
  • Linearisation points is a sound by incomplete method for proving linearisability of concurrent/distributed objects.
  • The example in the paper doesn’t admit simple linearisation points.