Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang
Modern programming languages, such as C++ and Java, provide a sequentially
consistent (SC) memory model for well-behaved programs that follow
a certain synchronization discipline, e.g., for those that are data-race free (DRF).
However, performance-critical libraries often violate the discipline by using low-level
hardware primitives, which have a weaker semantics. In such scenarios, it is
important for these libraries to protect their otherwise well-behaved clients from
the weaker memory model.
In this paper, we demonstrate that a variant of linearizability can be used to reason
formally about the interoperability between a high-level DRF client and a
low-level library written for the Total Store Order (TSO) memory model, which
is implemented by x86 processors. Namely, we present a notion of linearizability
that relates a concrete library implementation running on TSO to an abstract specification
running on an SC machine. A client of this library is said to be DRF if its
SC executions calling the abstract library specification do not contain data races.
We then show how to compile a DRF client to TSO such that it only exhibits SC
behaviors, despite calling into a racy library.
In International Symposium on Distributed Computing (DISC '12)
Publisher European Association for Theoretical Computer Science