Deriving Linearizable Fine-Grained Concurrent Objects

Practical and efficient algorithms for concurrent data structures are difficult to construct and modify. Algorithms in the literature are often optimized for a specific setting, making it hard to separate the algorithmic insights from implementation details. The goal of this work is to systematically construct algorithms for a concurrent data structure starting from its sequential implementation. Towards that goal, one follows a construction process that combines manual steps corresponding to high-level insights with automatic exploration of implementation details. To assist in this process, the paper built a new tool called PARAGLIDER. The tool quickly explores large spaces of algorithms and uses bounded model checking to check linearizability of algorithms.