Proving Linearizability Using Linearizations of Delete Operations

Abstract Linearizability is a commonly accepted correctness criterion for concurrent data structures. Concurrent queues and stacks are among themost fundamental concurrent data structures. In this paper, we presentnecessary and sufficient conditions for proving linearizability of concurrent queues and stacks, which make use of linearizations of dequeueand pop operations. The verification conditions intuitively express the FIFO/LIFO semantics of concurrent queues/stacks and can be verified just by reasoning about the happened-before order of operations. Wehave successfully applied the proof technique to prove 9 challenging concurrent queues and stacks and optimize the TS queue. We believe thatour proof technique can be extended to the concurrent data structureswhich have the ordering requirements when their elements are removed.