  Linearizability of concurrent data structures is usually proved by monolithic
simulation arguments relying on the identification of the so-called
linearization points. Regrettably, such proofs, whether manual or automatic,
are often complicated and scale poorly to advanced non-blocking concurrency
patterns, such as helping and optimistic updates. In response, we propose a
more modular way of checking linearizability of concurrent queue algorithms
that does not involve identifying linearization points. We reduce the task of
proving linearizability with respect to the queue specification to establishing
four basic properties, each of which can be proved independently by simpler
arguments. As a demonstration of our approach, we verify the Herlihy and Wing
queue, an algorithm that is challenging to verify by a simulation proof.
