Abstract
The typical proof of linearizability establishes an abstraction map from the concurrent program to a sequential specification, and identifies the commit points of operations. If the concurrent program uses fine-grained concurrency and complex synchronization, constructing such a proof is difficult. We propose a sound proof system that significantly simplifies the reasoning about linearizability. Linearizability is proved by transforming an implementation into its specification within this proof system. The proof system combines reduction and abstraction, which increase the granularity of atomic actions, with variable introduction and hiding, which syntactically relate the representation of the implementation to that of the specification. We construct the abstraction map incrementally, and eliminate the need to reason about the location of commit points in the implementation. We have implemented our method in the QED verifier and demonstrated its effectiveness and practicality on several highly-concurrent examples from the literature.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 463–492 (1990)
Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82, 253–284 (1991)
Park, S., Dill, D.L.: Protocol verification by aggregation of distributed transactions. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 300–310. Springer, Heidelberg (1996)
Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL 2009: ACM Symposium on Principles of Programming Languages. ACM, New York (2009)
Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 335–348. Springer, Heidelberg (2009)
Hesselink, W.H.: Eternity variables to prove simulation of specifications. ACM Trans. Comput. Logic 6, 175–201 (2005)
Jonsson, B., Pnueli, A., Rump, C.: Proving refinement using transduction. Distrib. Comput. 12, 129–149 (1999)
Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002)
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, New York (2004)
Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free dynamic hash tables with open addressing. Distrib. Comput. 18, 21–42 (2005)
Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 475–488. Springer, Heidelberg (2006)
Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19, 279–285 (1976)
Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP 2006 ACM Symposium on Principles and practice of parallel programming, pp. 129–136. ACM, New York (2006)
Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 477–490. Springer, Heidelberg (2007)
Wang, L., Stoller, S.D.: Static analysis for programs with non-blocking synchronization. In: ACM SIGPLAN 2005 Symposium on Principles and Practice of Parallel Programming (PPoPP). ACM Press, New York (2005)
Groves, L.: Verifying michael and scott’s lock-free queue algorithm using trace reduction. In: CATS 2008: Symposium on Computing: the Australasian theory, Darlinghurst, Australia, pp. 133–142. Australian Computer Society, Inc. (2008)
Elmas, T., Sezgin, A., Tasiran, S., Qadeer, S.: An annotation assistant for interactive debugging of programs with common synchronization idioms. In: Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (2009)
Elmas, T., Qadeer, S., Sezgin, A., Subasi, O., Tasiran, S.: Simplifying the proof of linearizability with reduction and abstraction. Technical Report, Koc University (2009), http://theorem.ku.edu.tr/tacas10tr.pdf
Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18, 717–721 (1975)
Treiber, R.K.: Systems programming: Coping with parallelism. rj5118 (1986)
Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC 1996: ACM symposium on Principles of distributed computing, pp. 267–275. ACM, New York (1996)
Krieger, O., Stumm, M., Unrau, R., Hanna, J.: A fair fast scalable reader-writer lock. In: ICPP 1993: The International Conference on Parallel Processing, Washington, DC, USA, pp. 201–204. IEEE Computer Society, Los Alamitos (1993)
Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL 2008: ACM symposium on Principles of programming languages, pp. 171–182. ACM, New York (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Elmas, T., Qadeer, S., Sezgin, A., Subasi, O., Tasiran, S. (2010). Simplifying Linearizability Proofs with Reduction and Abstraction. In: Esparza, J., Majumdar, R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12002-2_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-12002-2_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12001-5
Online ISBN: 978-3-642-12002-2
eBook Packages: Computer ScienceComputer Science (R0)