Subscribe

Issue No.07 - July (2013 vol.39)

pp: 1018-1039

Yang Liu , Nanyang Technological University, Singapore

Wei Chen , Microsoft Research Asia, Beijing

Yanhong A. Liu , State University of New York at Stony Brook, Stony Brook

Jun Sun , Singapore University of Technology and Design, Singapore

Shao Jie Zhang , National University of Singapore, Singapore

Jin Song Dong , National University of Singapore, Singapore

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.82

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 are serializable, and 2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on refinement checking of finite-state systems specified as concurrent processes with shared variables. To tackle state space explosion, we develop and apply symmetry reduction, dynamic partial order reduction, and a combination of both for refinement checking. We have built the method into the PAT model checker, and used PAT to automatically check a variety of implementations of concurrent objects, including the first algorithm for scalable nonzero indicators. Our system is able to find all known and injected bugs in these implementations.

INDEX TERMS

History, Sun, Educational institutions, Optimization, Electronic mail, Semantics, PAT, Linearizability, refinement, model checking

CITATION

Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun, Shao Jie Zhang, Jin Song Dong, "Verifying Linearizability via Optimized Refinement Checking",

*IEEE Transactions on Software Engineering*, vol.39, no. 7, pp. 1018-1039, July 2013, doi:10.1109/TSE.2012.82REFERENCES

- [1] http://www.comp.nus.edu.sg/~patlinear/, 2013.
- [2] R. Alur, K. Mcmillan, and D. Peled, "Model-Checking of Correctness Conditions for Concurrent Objects,"
Proc. 12th IEEE Symp. Logic in Computer Science, pp. 219-228, 1996.- [3] D. Amit, N. Rinetzky, T. Reps, M. Sagiv, and E. Yahav, "Comparison under Abstraction for Verifying Linearizability,"
Proc. 19th Int'l Conf. Computer Aided Verification, pp. 477-490, 2007.- [4] M.K. Arguilera, E. Gafni, and L. Lamport, "The Mailbox Problem,"
Proc. 22nd Int'l Symp. Distributed Computing, pp. 1-15, 2008.- [5] H. Attiya and J. Welch,
Distributed Computing: Fundamentals, Simulations, and Advanced Topics, second ed. John Wiley & Sons, Inc., 2004.- [6] J. Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam, and S. Sagiv, "Thread Quantification for Concurrent Shape Analysis,"
Proc. 20th Int'l Conf. Computer Aided Verification, pp. 399-413, 2008.- [7] S. Burckhardt, C. Dern, M. Musuvathi, and R. Tan, "Line-Up: A Complete and Automatic Linearizability Checker,"
Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 330-340, 2010.- [8] P. Cerný, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, "Model Checking of Linearizability of Concurrent List Implementations,"
Proc. 22nd Int'l Conf. Computer Aided Verification, pp. 465-479, 2010.- [9] E.M. Clarke, O. Grumberg, and D.A. Peled,
Model Checking. MIT Press, 2000.- [10] R. Colvin, S. Doherty, and L. Groves, "Verifying Concurrent Data Structures by Simulation,"
Electronic Notes in Theoretical Computer Science, vol. 137, no. 2, pp. 93-110, 2005.- [11] R. Colvin and L. Groves, "Formal Verification of an Array-Based Nonblocking Queue,"
Proc. 10th IEEE Int'l Conf. Eng. of Complex Computer Systems, pp. 507-516, 2005.- [12] R. Colvin and L. Groves, "A Scalable Lock-Free Stack Algorithm and Its Verification,"
Proc. Fifth IEEE Int'l Conf. Software Eng. and Formal Methods, pp. 339-348, 2007.- [13] R. Colvin, L. Groves, V. Luchangco, and M. Moir, "Formal Verification of a Lazy Concurrent List-Based Set Algorithm,"
Proc. 18th Int'l Conf. Computer Aided Verification, pp. 475-488, 2006.- [14] J. Derrick, G. Schellhorn, and H. Wehrheim, "Proving Linearizability via Non-Atomic Refinement,"
Proc. Sixth Int'l Conf. Integrated Formal Methods, pp. 195-214, 2007.- [15] J. Derrick, G. Schellhorn, and H. Wehrheim, "Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack,"
Proc. 10th IFIP WG 6.1 Int'l Conf. Formal Methods for Open Object-Based Distributed Systems, pp. 78-95, 2008.- [16] J. Derrick, G. Schellhorn, and H. Wehrheim, "Mechanically Verified Proof Obligations for Linearizability,"
ACM Trans. Programming Languages and Systems, vol. 33, no. 1, pp. 4:1-4:43, Jan. 2011.- [17] J. Derrick, G. Schellhorn, and H. Wehrheim, "Verifying Linearisability with Potential Linearisation Points,"
Proc. 17th Int'l Conf. Formal Methods, pp. 323-337, 2011.- [18] D.L. Dill, A.J. Hu, and H. Wong-Toi, "Checking for Language Inclusion Using Simulation Preorders,"
Proc. Third Int'l Conf. Computer Aided Verification, pp. 255-265, 1991.- [19] S. Doherty, L. Groves, V. Luchangco, and M. Moir, "Formal Verification of a Practical Lock-Free Queue Algorithm,"
Proc. 24th Int'l Conf. Formal Techniques for Networked and Distributed Systems, pp. 97-114, 2004.- [20] F. Ellen, Y. Lev, V. Luchangco, and M. Moir, "SNZI: Scalable NonZero Indicators,"
Proc. 26th Ann. ACM Symp. Principles of Distributed Computing, pp. 13-22, 2007.- [21] F. Ellen, Y. Lev, V. Luchangco, and M. Moir, "SNZI: Scalable NonZero Indicators,"
Proc. 26th Ann. ACM Symp. Principles of Distributed Computing, pp. 13-22, 2007.- [22] E. Emerson, S. Jha, and D. Peled, "Combining Partial Order and Symmetry Reductions,"
Proc. Third Int'l Workshop Tools and Algorithms for the Construction and Analysis of Systems, vol. 1217, pp. 19-34, 1997.- [23] E.A. Emerson and A.P. Sistla, "Symmetry and Model Checking,"
Formal Methods in System Design, vol. 9, no. 1/2, pp. 105-131, Aug. 1996.- [24] E.A. Emerson and R.J. Trefler, "From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking,"
Proc. 10th IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods, pp. 142-156, 1999.- [25] C. Flanagan and P. Godefroid, "Dynamic Partial-Order Reduction for Model Checking Software,"
Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp. 110-121, 2005.- [26] P. Godefroid,
Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Secaucus, 1996.- [27] G. Gueta, C. Flanagan, E. Yahav, and M. Sagiv, "Cartesian Partial-Order Reduction,"
Proc. 14th Int'l SPIN Workshop Model Checking Software, pp. 95-112, 2007.- [28] T.L. Harris, K. Fraser, and I.A. Pratt, "A Practical Multi-Word Compare-and-Swap Operation,"
Proc. 16th Int'l Conf. Distributed Computing, pp. 265-279, 2002.- [29] D. Hendler, N. Shavit, and L. Yerushalmi, "A Scalable Lock-Free Stack Algorithm,"
Proc. 16th Ann. ACM Symp. Parallelism in Algorithms and Architectures, pp. 206-215, 2004.- [30] M. Herlihy and N. Shavit,
The Art of Multiprocessor Programming. Morgan Kaufmann, 2008.- [31] M. Herlihy and J.M. Wing, "Linearizability: A Correctness Condition for Concurrent Objects,"
ACM Trans. Programming Language and Systems, vol. 12, no. 3, pp. 463-492, 1990.- [32] J.E. Hopcroft,
Introduction to Automata Theory, Languages, and Computation. Addison Wesley, 2001.- [33] R. Iosif, "Symmetry Reduction Criteria for Software Model Checking,"
Proc. Ninth Int'l SPIN Workshop Model Checking Software, vol. 2318, pp. 31-33, 2002.- [34] C.N. Ip and D.L. Dill, "Better Verification through Symmetry,"
Formal Methods in System Design, vol. 9, no. 1/2, pp. 41-75, Aug. 1996.- [35] R.P. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün, "Static Partial Order Reduction,"
Proc. Fourth Int'l Conf. Tools and Algorithms for Construction and Analysis of Systems, pp. 345-357, 1998.- [36] M. Leuschel, T. Massart, and A. Currie, "How to Make FDR Spin LTL Model Checking of CSP by Refinement,"
Proc. Int'l Symp. Formal Methods Europe on Formal Methods for Increasing Software Productivity, pp. 99-118, 2001.- [37] Y. Liu, W. Chen, Y.A. Liu, and J. Sun, "Model Checking Linearizability via Refinement,"
Proc. Second World Congress Formal Methods, pp. 321-337, 2009.- [38] Y. Liu, J. Sun, and J.S. Dong, "PAT 3: An Extensible Architecture for Building Multi-Domain Model Checkers,"
Proc. 22nd Ann. Int'l Symp. Software Reliability Eng., pp. 190-199, 2011.- [39] G. Lowe, "Specification of Communicating Processes: Temporal Logic versus Refusals-Based Refinement,"
Formal Aspects of Computing, vol. 20, no. 3, pp. 277-294, May 2008.- [40] N. Lynch,
Distributed Algorithms. Morgan Kaufmann, 1997.- [41] R. Manevich, T. Lev-Ami, M. Sagiv, G. Ramalingam, and J. Berdine, "Heap Decomposition for Concurrent Shape Analysis,"
Proc. 15th Int'l Symp. Static Analysis, pp. 363-377, 2008.- [42] M.M. Michael and M.L. Scott, "Nonblocking Algorithms and Preemption-Safe Locking on Multiprogrammed Shared Memory Multiprocessors,"
J. Parallel and Distributed Computing, vol. 51, pp. 1-26, 1998.- [43] N. Moffat, M. Goldsmith, and B. Roscoe, "A Representative Function Approach to Symmetry Exploitation for CSP Refinement Checking,"
Proc. 10th Int'l Conf. Formal Methods and Software Eng., pp. 258-277, 2008.- [44] D. Plagge and M. Leuschel, "Seven at One Stroke: LTL Model Checking for High-Level Specifications in b, z, Csp, and More,"
Int'l J. Software Tools for Technology Transfer, vol. 12, no. 1, pp. 9-21, Jan. 2010.- [45] A.W. Roscoe, "Model-Checking CSP,"
A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 353-378, Prentice Hall,, 1994.- [46] A.W. Roscoe,
The Theory and Practice of Concurrency. Prentice-Hall, 1997.- [47] C.H. Shann, T.L. Huang, and C. Chen, "A Practical Nonblocking Queue Algorithm Using Compare-and-Swap,"
Proc. Seventh Int'l Conf. Parallel and Distributed Systems, pp. 470-475, 2000.- [48] A.P. Sistla and P. Godefroid, "Symmetry and Reduced Symmetry in Model Checking,"
ACM Trans. Programming Languages and Systems, vol. 26, no. 4, pp. 702-734, July 2004.- [49] J. Sun, Y. Liu, and J.S. Dong, "Model Checking CSP Revisited: Introducing a Process Analysis Toolkit,"
Proc. Third Int'l Symp. Leveraging Applications of Formal Methods, Verification and Validation, vol. 17, pp. 307-322, 2008.- [50] J. Sun, Y. Liu, J.S. Dong, and C.Q. Chen, "Integrating Specification and Programs for System Modeling and Verification,"
Proc. Third Int'l Symp. Theoretical Aspects of Software Eng., pp. 127-135, 2009.- [51] J. Sun, Y. Liu, J.S. Dong, and J. Pang, "PAT: Towards Flexible Verification under Fairness,"
Proc. 21th Int'l Conf. Computer Aided Verification, pp. 709-714, 2009.- [52] J. Sun, Y. Liu, J.S. Dong, and H.H. Wang, "Specifying and Verifying Event-Based Fairness Enhanced Systems,"
Proc. 10th Int'l Conf. Formal Methods and Software Eng., pp. 318-337, 2008.- [53] R.K. Treiber, "Systems Programming: Coping with Parallelism," Technical Report RJ 5118, IBM Almaden Research Center, 1986.
- [54] V. Vafeiadis, "Shape-Value Abstraction for Verifying Linearizability,"
Proc. 10th Int'l Conf. Verification, Model Checking, and Abstract Interpretation, pp. 335-348, 2009.- [55] V. Vafeiadis, "Automatically Proving Linearizability,"
Proc. 22nd Int'l Conf. Computer Aided Verification, pp. 450-464, 2010.- [56] V. Vafeiadis, M. Herlihy, T. Hoare, and M. Shapiro, "Proving Correctness of Highly-Concurrent Linearisable Objects,"
Proc. 11th ACM SIGPLAN Symp. Principles and Practice of Parallel Programming, pp. 129-136, 2006.- [57] A. Valmari, "Stubborn Sets for Reduced State Space Generation,"
Proc. 10th Int'l Conf. Applications and Theory of Petri Nets: Advances in Petri Nets 1990, pp. 491-515, 1991.- [58] M. Vechev and E. Yahav, "Deriving Linearizable Fine-Grained Concurrent Objects,"
Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 125-135, 2008.- [59] M. Vechev, E. Yahav, and G. Yorsh, "Experience with Model Checking Linearizability,"
Proc. 16th Int'l SPIN Workshop Model Checking Software, pp. 261-278, 2009.- [60] L. Wang and S. Stoller, "Static Analysis of Atomicity for Programs with Non-Blocking Synchronization,"
Proc. 10th ACM SIGPLAN Symp. Principles and Practice of Parallel Programming, pp. 61-71, 2005.- [61] T. Wang, S. Song, J. Sun, Y. Liu, J.S. Dong, X. Wang, and S. Li, "More Anti-Chain Based Refinement Checking,"
Proc. 14th Int'l Conf. Formal Eng. Methods, pp. 364-380, 2012.- [62] P. Wolper, "Temporal Logic Can Be More Expressive,"
Proc. 22nd Ann. Symp. Foundations of Computer Science, pp. 340-348, 1981. |