Paper Info
Title
Show no weakness: sequentially consistent specifications of TSO libraries
Abstract
Modern programming languages, such as C++ and Java, provide a sequentially consistent (SC) memory model for well-behaved programs that follow a certain synchronisation 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 behaviours, despite calling into a racy library.
Year
DOI
Venue
2012
10.1007/978-3-642-33651-5_3
DISC
Keywords
Field
DocType
low-level library,concrete library implementation,sequentially consistent specification,memory model,abstract library specification,sc execution,sc machine,drf client,performance-critical library,tso library,racy library,sc behaviour
x86,Programming language,Computer science,Interoperability,Real-time computing,Memory model,Distributed computing,Linearizability,Synchronization,Compiler,Java,Semantics,Operating system
Conference
Volume
ISSN
Citations 
7611
0302-9743
24
PageRank 
References 
Authors
0.94
13
3
Name
Order
Citations
PageRank
Alexey Gotsman143928.62
Madanlal Musuvathi2168781.73
Hongseok Yang32313115.85