Show No Weakness: Sequentially Consistent Specification of TSO Libraries

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.


Publication typeProceedings
Published inInternational Symposium on Distributed Computing (DISC '12)
PublisherEuropean Association for Theoretical Computer Science
> Publications > Show No Weakness: Sequentially Consistent Specification of TSO Libraries