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)
|