Abstraction for Concurrent Objects

ion for Concurrent Objects Ivana Filipovi´c, Peter O’Hearn, Noam Rinetzky, and Hongseok Yang Queen Mary University of London, UK 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 refinement. Our study also provides a new understanding of sequential consistency and linearizability in terms of abstraction of dependency between computation steps of client programs.

• Type: Conference
• Year: 2009
• Where: ESOP
• Authors: Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang
• Keywords: Client Programs, ESOP 2009, Programming Languages, Queen Mary University Of London, Sequential Consistency