Weakness Can Be Quarantined!

The Data Race Freeness (DRF) property has been advocated as the de-facto technique for reasoning about concurrent programs with a relaxed memory semantics. However, DRF has a “whole program” nature, which hinders modularity. The problem is then, how to shield a client from data races in the implementation of a library; and symmetrically, how to shield the implementor of a library from subtle issues of relaxed memory exposed by clients?

We describe two compositional reasoning techniques to mitigate this situation.

1. We identify a notion of linearizability that is appropriate to relaxed memory models. We prove an abstraction theorem: a component can safely be replaced by its interface in a non-interfering program context, and a composition theorem: the composition of non-interfering components satisfies the composition of their interfaces.
2. We identify a notion of local sequential consistency (LSC) that permits a component to be viewed solely in terms of its SC traces. LSC can be viewed as a modular (or local) version of DRF. We prove that the composition of non-interfering LSC components is LSC.

Our results can be adapted to different memory models: we demonstrate them for SC and variants of TSO and JMM.

Joint work with G. Petri and J. Riely.