Abstract
We describe a semi-automated verification of a slightly optimised version of Michael and Scott’s lock-free FIFO queue implementation. We verify the algorithm with a simulation proof consisting of two stages: a forward simulation from an automaton modelling the algorithm to an intermediate automaton, and a backward simulation from the intermediate automaton to an automaton that models the behaviour of a FIFO queue. These automata are encoded in the input language of the PVS proof system, and the properties needed to show that the algorithm implements the specification are proved using PVS’s theorem prover.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-3-540-30232-2_24
Download to read the full chapter text
Chapter PDF
References
Michael, M., Scott, M.: Nonblocking algorithms and preemption safe locking on multiprogrammed shared memory multiprocessors. Journal of Parallel and Distributed Computing 51, 1–26 (1998)
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. TOPLAS 12, 463–492 (1990)
Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida (1995)
Moir, M.: Practical implementations of non-blocking synchronization primitives. In: Proceedings of the 15th Annual ACM Symposium on the Principles of Distributed Computing, Santa Barbara, CA (1997)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations – Part I: Untimed systems. Information and Computation 121, 214–233 (1995)
Ramírez-Robredo, J.A.: Paired simulation of I/O automata. Master’s thesis, Massachusetts Institute of Technology (2000)
Devillers, M.: Translating IOA automata to PVS. Technical Report CSI-R9903, Computing Science Institute, University of Nijmegen, the Netherlands (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 IFIP International Federation for Information Processing
About this paper
Cite this paper
Doherty, S., Groves, L., Luchangco, V., Moir, M. (2004). Formal Verification of a Practical Lock-Free Queue Algorithm. In: de Frutos-Escrig, D., Núñez, M. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2004. FORTE 2004. Lecture Notes in Computer Science, vol 3235. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30232-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-30232-2_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23252-0
Online ISBN: 978-3-540-30232-2
eBook Packages: Springer Book Archive