Abstract

When constructing complex concurrent systems, abstraction is vital: programmers should be able to reason about concurrent libraries in terms of abstract specifications that hide the implementation details. Relaxed memory models present substantial challenges in this respect, as libraries need not provide sequentially consistent abstractions: to avoid unnecessary synchronisation, they may allow clients to observe relaxed memory effects, and library specifications must capture these.

This talk describes a criterion for sound library abstraction in the new C11 memory model, generalising the standard sequentially consistent notion of linearizability. We have proved that our criterion soundly captures all client-library interactions, both through call and return values, and through the subtle synchronisation effects arising from the memory model. To illustrate the approach, a specification and verified implementation of the lock-free Treiber stack will be described. Ours is the first approach to compositional reasoning for concurrent C11 programs.

This is joint work with Mike Dodds and Alexey Gotsman.

This is a POPL practice talk, so should fit into a 30 minute slot. Comments are welcome!