Verifying Michael and Scott's Lock-Free Queue Algorithm using Trace Reduction

Groves, L.

Lock-free algorithms have been developed to avoid various problems associated with using locks to control access to shared data structures. These algorithms are typically more intricate than lock-based algorithms, as they allow more complex interactions between processes, and many published algorithms have turned out to contain errors. There is thus a pressing need for practical techniques for verifying lock-free algorithms and programs that use them. In this paper we show how Michael and Scott's well known lock-free queue algorithm can be verified using a trace reduction method, based on Lipton's reduction method. Michael and Scott's queue is an interesting case study because, although the basic idea is easy to understand, the actual algorithm is quite subtle, and it demonstrates several way in which the basic reduction method needs to be extended.

Cite as: Groves, L. (2008). Verifying Michael and Scott's Lock-Free Queue Algorithm using Trace Reduction. In Proc. Fourteenth Computing: The Australasian Theory Symposium (CATS 2008), Wollongong, NSW, Australia. CRPIT, 77. Harland, J. and Manyem, P., Eds. ACS. 133-142.

(from crpit.com) (local if available)