Abstract
Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that 1) all executions of concurrent operations be serializable, and 2) the serialized executions be correct with respect to the sequential semantics. This paper describes a new method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. Our method avoids the often difficult task of determining linearization points in implementations, but can also take advantage of linearization points if they are given. The method exploits model checking of finite state systems specified as concurrent processes with shared variables. Partial order reduction is used to effectively reduce the search space. The approach is built into a toolset that supports a rich set of concurrent operators. The tool has been used to automatically check a variety of implementations of concurrent objects, including the first algorithms for the mailbox problem and scalable NonZero indicators. Our system was able to find all known and injected bugs in these implementations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Mcmillan, K., Peled, D.: Model-checking of Correctness Conditions for Concurrent Objects. In: LICS 1996, pp. 219–228. IEEE, Los Alamitos (1996)
Amit, D., Rinetzky, N., Reps, T., 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)
Arguilera, M.K., Gafni, E., Lamport, L.: The Mailbox Problem. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 1–15. Springer, Heidelberg (2008)
Attiya, H., Welch, J.: Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd edn. John Wiley & Sons, Inc., Publication, Chichester (2004)
Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, S.: Thread Quantification for Concurrent Shape Analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 399–413. Springer, Heidelberg (2008)
Colvin, R., Doherty, S., Groves, L.: Verifying Concurrent Data Structures by Simulation. Electronic Notes in Theoretical Computer Science 137(2), 93–110 (2005)
Colvin, R., Groves, L.: Formal Verification of an Array-Based Nonblocking Queue. In: ICECCS 2005, pp. 507–516. IEEE, Los Alamitos (2005)
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)
Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for Language Inclusion Using Simulation Preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 255–265. Springer, Heidelberg (1992)
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)
Ellen, F., Lev, Y., Luchangco, V., Moir, M.: SNZI: Scalable NonZero Indicators. In: PODC 2007, pp. 13–22. ACM, New York (2007)
Emerson, E.A., Trefler, R.J.: From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999)
Herlihy, M., Wing, J.M.: Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Language and Systems 12(3), 463–492 (1990)
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1985), www.usingcsp.com/cspbook.pdf
Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model Checking Linearizability via Refinement. Technical Report TR08c, National Univ. of Singapore (May 2009), http://www.comp.nus.edu.sg/~pat/report.pdf
Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1997)
Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., Berdine, J.: Heap Decomposition for Concurrent Shape Analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 363–377. Springer, Heidelberg (2008)
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–26 (1998)
Roscoe, A.W.: Model-checking CSP. In: A classical mind: essays in honour of C. A. R. Hoare, pp. 353–378 (1994)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)
Shann, C.H., Huang, T.L., Chen, C.: A Practical Nonblocking Queue Algorithm Using Compare-and-Swap. In: ICPADS 2000, pp. 470–475. IEEE, Los Alamitos (2000)
Sun, J., Liu, Y., Dong, J.S.: Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. In: ISoLA 2008, pp. 307–322. Springer, Heidelberg (2008)
Sun, J., Liu, Y., Dong, J.S., Chen, C.Q.: Integrating Specification and Programs for System Modeling and Verification. In: TASE 2009, pp. 127–135. IEEE, Los Alamitos (2009)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 702–708. Springer, Heidelberg (2009)
Treiber, R.K.: Systems Programming: Coping with Parallelism. Technical Report RJ 5118, IBM Almaden Research Center (1986)
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)
Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving Correctness of Highly-concurrent Linearisable Objects. In: PPoPP 2006, pp. 129–136. ACM, New York (2006)
Valmari, A.: Stubborn Set Methods for Process Algebras. In: PMIV 1996. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 213–231 (1996)
Vechev, M., Yahav, E.: Deriving Linearizable Fine-grained Concurrent Objects. In: PLDI 2008, pp. 125–135. ACM, New York (2008)
Wang, L., Stoller, S.: Static Analysis of Atomicity for Programs with Non-blocking Synchronization. In: PPoPP 2005, pp. 61–71. ACM, New York (2005)
Wehrheim, H.: Partial Order Reductions for Failures Refinement. Electronic Notes in Theoretical Computer Science 27 (1999)
Zhang, S.J., Liu, Y., Sun, J., Dong, J.S., Chen, W., Liu, Y.A.: Formal Verification of Scalable NonZero Indicators. In: SEKE 2009, pp. 406–411. Knowledge Systems Institute Graduate School (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, Y., Chen, W., Liu, Y.A., Sun, J. (2009). Model Checking Linearizability via Refinement. In: Cavalcanti, A., Dams, D.R. (eds) FM 2009: Formal Methods. FM 2009. Lecture Notes in Computer Science, vol 5850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05089-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-05089-3_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05088-6
Online ISBN: 978-3-642-05089-3
eBook Packages: Computer ScienceComputer Science (R0)