Abstract

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! Recently, we have been trying to show that linearizability is more important than that by generalising it to realistic settings and establishing theorems that allow exploiting it to verify concurrent programs compositionally.

In this talk, I will present our definition of linearizability on the TSO weak memory model (used by Intel processors) and a theorem showing 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 Sebastian Burckhardt, Madan Musuvathi (Microsoft Research) and Hongseok Yang (University of Oxford, UK).