  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.
