The Importance of Being Linearizable

Specifications of concurrent libraries are commonly given by the well-known notion of linearizability. However, to date linearizability has been no more than a box to be ticked in a paper with a new concurrent algorithm, lest it should get rejected. The notion has not even been defined for realistic settings in which concurrent algorithms usually get used! We show that linearizability is more important than that:

• We generalise it to a realistic setting, including multiple libraries sharing an address space with their clients, and interacting by transferring the ownership of memory cells. Our definition is appropriate for both safety and liveness properties.
• We present the first theorem that allows exploiting linearizability to verify concurrent programs compositionally. We show that, while verifying a client using a concurrent library, we can soundly replace the library by another one related to the original library by our generalisation of linearizability.

This is joint work with Hongseok Yang (University of Oxford, UK).