Title: Abstraction for Concurrent Objects


 Noam Rinetzky (Queen Mary University of London)

Abstract:
Concurrent data structures are usually designed to satisfy correctness 
conditions such as sequential consistency and linearizability. In this paper, we 
consider the following fundamental question: what guarantees are provided by 
these conditions for client programs? We formally show that these conditions can 
be characterized in terms of observational re?nement. Our study also provides a 
new understanding of sequential consistency and linearizability in terms of ab- 
straction of dependency between computation steps of client programs. 


Authors Ivana Mijajlovic (Queen Mary University of London), Peter O'Hearn (Queen Mary University of London),
 Noam Rinetzky (Queen Mary University of London), Hongseok Yang (Queen Mary University of London)