Proving Linearizability Using Reduction

Lipton's reduction theory provides an intuitive and simple way for deducing the non-interference properties of concurrent programs, but it is difficult to directly apply the technique to verify linearizability of sophisticated fine-grained concurrent data structures. In this paper, we propose three reduction-based proof methods that can handle such data structures. The key idea behind our reduction methods is that an irreducible operation can be viewed as an atomic operation at a higher level of abstraction. This allows us to focus on the reduction properties of an operation related to its abstract semantics. We have successfully applied the methods to verify 11 concurrent data structures including the most challenging ones: the Herlihy and Wing queue, the HSY elimination-based stack, and the time-stamped queue, and the lazy list. Our methods inherit intuition and simplicity of Lipton's reduction, and concurrent data structures designers can easily and quickly learn to use the methods.