Abstract
Distributed algorithms are inherently complex to verify. In this paper we show how to verify that a concurrent lock-free implementation of a stack is correct by mechanizing the proof that it is linearizable, linearizability being a correctness notion for concurrent objects. Our approach consists of two parts: the first part is independent of the example and derives proof obligations local for one process which imply linearizabilty. The conditions establish a (special sort of non-atomic) refinement relationship between the specification and the concurrent implementation. These are used in the second part to verify the lock-free stack implementation. We use the specification language Z to describe the algorithms and the KIV theorem prover to mechanize the proof.
Chapter PDF
Similar content being viewed by others
References
Abrial, J.-R., Cansell, D.: Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity). Journal of Universal Computer Science 11(5), 744–770 (2005)
Barden, R., Stepney, S., Cooper, D.: Z in Practice. BCS Practitioner Series. Prentice-Hall, Englewood Cliffs (1994)
Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. ENTCS 137, 93–110 (2005)
de Roever, W., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Press, Cambridge (1998)
Derrick, J., Boiten, E.: Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer, Heidelberg (2001)
Derrick, J., Schellhorn, G., Wehrheim, H.: Proving linearizability via non-atomic refinement. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 195–214. Springer, Heidelberg (2007)
Derrick, J., Wehrheim, H.: Using coupled simulations in non-atomic refinement. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 127–147. Springer, Heidelberg (2003)
Derrick, J., Wehrheim, H.: Non-atomic refinement in Z and CSP. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, Springer, Heidelberg (2005)
Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97–114. Springer, Heidelberg (2004)
Groves, L., Colvin, R.: Derivation of a scalable lock-free stack algorithm. ENTCS (to appear, 2007)
Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: SPAA 2004: ACM symposium on Parallelism in algorithms and architectures, pp. 206–215. ACM Press, New York (2004)
Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems 12(3), 463–492 (1990)
Hesselink, W.H.: Refinement verification of the lazy caching algorithm. Acta Inf. 43(3), 195–222 (2006)
Hesselink, W.H.: A criterion for atomicity revisited. Acta Inf. 44(2), 123–151 (2007)
Web presentation of the linearization case study in KIV. URL: http://www.informatik.uni-augsburg.de/swt/projects/linearizability.html
Lamport, L., Schneider, F.B.: Pretending atomicity. Technical Report TR89-1005, SRC Digital (1989)
Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)
Michael, M.M., Scott, M.L.: Nonblocking algorithms and preemption-safe locking on multiprogrammed shared — memory multiprocessors. Journal of Parallel and Distributed Computing 51(1), 1–26 (1998)
Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV (ch. 1: Interactive Theorem Proving). In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications. Systems and Implementation Techniques, vol. II, pp. 13–39. Kluwer Academic Publishers, Dordrecht (1998)
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (1992)
Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Derrick, J., Schellhorn, G., Wehrheim, H. (2008). Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack. In: Barthe, G., de Boer, F.S. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2008. Lecture Notes in Computer Science, vol 5051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68863-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-68863-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68862-4
Online ISBN: 978-3-540-68863-1
eBook Packages: Computer ScienceComputer Science (R0)