Weakness Can Be Quarantined!

Опубликовано 12 августа 2016, 2:10

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.