Abstraction for concurrent objects

Concurrent data structures are usually designed to satisfy correctness conditions such as sequential consistency or 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.

Authors

• Ivana Filipović
• Peter O’Hearn
• Noam Rinetzky
• Hongseok Yang

Keywords

• Linearizability
• Sequential consistency
• Observational equivalence
• Observational refinement