A simple and correct shared-queue algorithm using compare-and-swap

Abstract

A compare-and-swap shared-queue algorithm is presented that permits concurrent access. This algorithm is nondelaying in that no processor need wait for an action by another processor. A verification method that analyzes the states of the shared data structure is given. By drawing a graph that incorporates in a simple way the effects of multiprocessor interleaving, one can quickly find errors in an algorithm or produce a proof of correctness. Since enqueue and dequeue operations may begin at any time, concurrent queue operations are represented by providing, in each state of the shared data structure, one transition that initiates an enqueue operation and another transition for a dequeue operation. The method is a practical one that is applicable to a variety of algorithms that use shared data structures.