Sciweavers

Share
ESOP
2012
Springer

Concurrent Library Correctness on the TSO Memory Model

8 years 2 months ago
Concurrent Library Correctness on the TSO Memory Model
Abstract. Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms. Unfortunately, it is only appropriate for sequentially consistent memory models, while the hardware and software platforms that algorithms run on provide weaker consistency guarantees. In this paper, we present the first definition of linearizability on a weak memory model, Total Store Order (TSO), implemented by x86 processors. We establish that our definition is a correct one in the following sense: while proving a property of a client of a conlibrary, we can soundly replace the library by its abstract implementation related to the original one by our generalisation of linearizability. This allows abstracting from the details of the library implementation while reasoning about the client. We have developed a tool for systematically testing concurrent libraries against our definition and applied it to several challenging algorithms.
Sebastian Burckhardt, Alexey Gotsman, Madanlal Mus
Added 21 Apr 2012
Updated 21 Apr 2012
Type Journal
Year 2012
Where ESOP
Authors Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang
Comments (0)
books