Proving Linearizability of Concurrent Queues

Proving Linearizability of Concurrent Queues

Linearizability is a commonly accepted correctness criterion for concurrent data structures. Concurrent queues are among the most fundamental concurrent data structures. In this paper, we present necessary and sufficient conditions for proving linearizability of concurrent queues, which make use of linearization of dequeue operations. The verification conditions intuitively express the “FIFO” semantics of concurrent queues and can be verified just by reasoning about the happened-before order of operations. We have successfully applied the proof technique to prove several challenging concurrent queues. We believe that our proof technique can be extended to the concurrent data structures which have the ordering requirements when their elements are removed.