Sebastian Burckhardt
ABSTRACT
Modular development of concurrent applications requires thread-safe components that behave correctly when called concurrently by multiple client threads. This paper focuses on linearizability, a specific formalization of thread safety, where all operations of a concurrent component appear to take effect instantaneously at some point between their call and return. The key insight of this paper is that if a component is intended to be deterministic, then it is possible to build an automatic linearizability checker by systematically enumerating the sequential behaviors of the component and then checking if each its concurrent behavior is equivalent to some sequential behavior.
We develop this insight into a tool called Line-Up, the first complete and automatic checker for deterministic linearizability. It is complete, because any reported violation proves that the implementation is not linearizable with respect to any sequential deterministic specification. It is automatic, requiring no manual abstraction, no manual specification of semantics or commit points, no manually written test suites, no access to source code.
We evaluate Line-Up by analyzing 13 classes with a total of 90 methods in two versions of the .NET Framework 4.0. The violations of deterministic linearizability reported by Line-Up exposed seven errors in the implementation that were fixed by the development team.
- M. Abadi and L. Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2), 1991. Google Scholar
Digital Library
- S. Burckhardt, R. Alur, and M. Martin. CheckFence: Checking consistency of concurrent data types on relaxed memory models. In Programming Language Design and Impl. (PLDI), pages 12--21, 2007. Google ScholarDigital Library
- S. Burckhardt and M. Musuvathi. Effective program verification for relaxed memory models. In Computer-Aided Verification (CAV), pages 107--120, 2008. Google ScholarDigital Library
- R. Colvin, L. Groves, V. Luchangco, and M. Moir. Formal verification of a lazy concurrent list-based set algorithm. In Computer-Aided Verification (CAV), LNCS 4144, pages 475--488. Springer, 2006. Google ScholarDigital Library
- K. Coons, M. Musuvathi, and S. Burckhardt. Gambit: Effective unit testing of concurrency libraries. In Principles and Practice of Parallel Programming (PPoPP), 2010. Google ScholarDigital Library
- S. Doherty, D. Detlefs, L. Grove, C. Flood, V. Luchangco, P. Martin, M. Moir, N. Shavit, and G. Steele. DCAS is not a silver bullet for nonblocking algorithm design. In Symposium on Parallel Algorithms and Architectures (SPAA), pages 216--224, 2004. Google ScholarDigital Library
- T. Elmas, S. Qadeer, and S. Tasiran. A calculus of atomic actions. In Principles of Programming Languages (POPL), 2009. Google ScholarDigital Library
- T. Elmas and S. Tasiran. VyrdMC: Driving runtime refinement checking with model checkers. Electr. Notes Theor. Comput. Sci., 144:41--56, 2006. Google ScholarDigital Library
- T. Elmas, S. Tasiran, and S. Qadeer. VYRD: verifying concurrent programs by runtime refinement-violation detection. In Programming Language Design and Impl. (PLDI), pages 27--37, 2005. Google ScholarDigital Library
- A. Farzan and P. Madhusudan. Monitoring atomicity in concurrent programs. In Computer-Aided Verification (CAV), 2008. Google ScholarDigital Library
- C. Flanagan and S. Freund. Efficient and precise dynamic race detection. In Programming Language Design and Impl. (PLDI), 2009. Google ScholarDigital Library
- C. Flanagan, S. Freund, and J.Yi. Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs. In Programming Language Design and Impl. (PLDI), 2008. Google ScholarDigital Library
- K. Fraser. Practical Lock-Freedom. PhD thesis, University of Cambridge, 2004.Google Scholar
- K. Fraser and T. Harris. Concurrent programming without locks. ACM Trans. Comput. Syst., 25(2), 2007. Google ScholarDigital Library
- M. Herlihy and J. Wing. Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463--492, 1990. Google ScholarDigital Library
- L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comp., C-28(9):690--691, 1979. Google ScholarDigital Library
- D. Marino, M. Musuvathi, and S. Narayanasamy. LiteRace: Effective sampling for lightweight data-race detection. In Programming Language Design and Impl. (PLDI), 2009. Google ScholarDigital Library
- M. Michael and M. Scott. Correction of a memory management method for lock-free data structures. Technical Report TR599, University of Rochester, 1995. Google ScholarDigital Library
- MSDN, http://blogs.msdn.com/somasegar/archive/2007/11/29/parallel-extensions-to-the-net-fx-ctp.aspx. Parallel Extensions to the .NET FX CTP, November 2007.Google Scholar
- MSDN, http://msdn.microsoft.com/en-us/library/dd460718(VS.100).aspx. .NET Framework 4 Data Structures for Parallel Programming, November 2009.Google Scholar
- M. Musuvathi and S. Qadeer. Fair stateless model checking. In Programming Language Design and Impl. (PLDI), 2008. Google ScholarDigital Library
- M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In Operating Systems Design and Impl. (OSDI), pages 267--280, 2008. Google ScholarDigital Library
- C. H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 4(26), October 1979. Google ScholarDigital Library
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comp. Sys., 15(4):391--411, 1997. Google ScholarDigital Library
- V. Vafeiadis. Shape-value abstraction for verifying linearizability. In Verification, Model Checking and Abstract Interpretation (VMCAI). Springer-Verlag, 2009. Google ScholarDigital Library
- V. Vafeiadis, M. Herlihy, T. Hoare, and M. Shapiro. Proving correctness of highly-concurrent linearisable objects. In Principles and Practice of Parallel Programming (PPoPP), pages 129--136, 2006. Google ScholarDigital Library
- M. Vechev, E. Yahav, and G. Yorsh. Experience with model checking linearizability. In SPIN, 2009. Google ScholarDigital Library
Index Terms
- Line-up: a complete and automatic linearizability checker
Recommendations
Line-up: a complete and automatic linearizability checker
PLDI '10Modular development of concurrent applications requires thread-safe components that behave correctly when called concurrently by multiple client threads. This paper focuses on linearizability, a specific formalization of thread safety, where all ...
Help when needed, but no more: Efficient read/write partial snapshot
An atomic snapshot object is an object that can be concurrently accessed by asynchronous processes prone to crash. It is made of m components (base atomic registers) and is defined by two operations: an update operation that allows a process to ...
Static analysis of atomicity for programs with non-blocking synchronization
PPoPP '05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programmingIn concurrent programming, non-blocking synchronization is very efficient but difficult to design correctly. This paper presents a static analysis to show that code blocks are atomic, i.e., that every execution of the program is equivalent to one in ...
Comments