Azadeh Farzan
ABSTRACT
In this paper, we consider the problem of verifying thread-state properties of multithreaded programs in which the number of active threads cannot be statically bounded. Our approach is based on decomposing the task into two modules, where one reasons about data and the other reasons about control. The data module computes thread-state invariants (e.g., linear constraints over global variables and local variables of one thread) using the thread interference information computed by the control module. The control module computes a representation of thread interference, as an incrementally constructed data flow graph, using the data invariants provided by the data module. These invariants are used to rule out patterns of thread interference that can not occur in a real program execution. The two modules are incorporated into a feedback loop, so that the abstractions of data and interference are iteratively coarsened as the algorithm progresses (that is, they become weaker) until a fixed point is reached. Our approach is sound and terminating, and applicable to programs with infinite state (e.g., unbounded integers) and unboundedly many threads. The verification method presented in this paper has been implemented into a tool, called Duet. We demonstrate the effectiveness of our technique by verifying properties of a selection of Linux device drivers using Duet, and also compare Duet with previous work on verification of parameterized Boolean program using the Boolean abstractions of these drivers.
Supplemental Material
- J. Alglave, D. Kroening, N. He, A. Ranjan, N. Seghir, and M. Tautschnig. CPROVER project, Nov. 2011. URL http://www.cprover.org/.Google Scholar
- T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, pages 221--234, 2001. Google ScholarDigital Library
- G. Basler, M. Mazzucchi, T. Wahl, and D. Kroening. Symbolic counter abstraction for concurrent software. In CAV, pages 64--78, 2009. Google ScholarDigital Library
- J. Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam, and M. Sagiv. Thread quantification for concurrent shape analysis. In CAV, volume 5123 of LNCS, pages 399--413. 2008. Google ScholarDigital Library
- J. Bertrand and A. Miné. Apron: A library of numerical abstract domains for static analysis. In CAV, pages 661--667, 2009. Google ScholarDigital Library
- A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In CAV, pages 403--418, 2000. Google ScholarDigital Library
- J. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. SIGPLAN Not., 37: 258--269, 2002. Google ScholarDigital Library
- E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In K. Jensen and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), volume 2988 of Lecture Notes in Computer Science, pages 168--176. Springer, 2004. ISBN 3--540--21299-X.Google Scholar
- E. M. Clarke, D. Kroening, N. Sharygina, and K. Yorav. Satabs: Sat-based predicate abstraction for ansi-c. In TACAS, pages 570--574, 2005. Google ScholarDigital Library
- A. Cohen and K. S. Namjoshi. Local proofs for linear-time properties of concurrent programs. In CAV, pages 149--161, 2008. Google ScholarDigital Library
- A. F. Donaldson, A. Kaiser, D. Kroening, and T. Wahl. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In CAV, pages 356--371, 2011. Google ScholarDigital Library
- E. A. Emerson and V. Kahlon. Model checking large-scale and parameterized resource allocation systems. In TACAS, pages 251--265, 2002. Google ScholarDigital Library
- E. A. Emerson and A. P. Sistla. Symmetry and model checking. Form. Methods Syst. Des., 9: 105--131, 1996. Google ScholarDigital Library
- D. Engler and K. Ashcraft. Racerx: effective, static detection of race conditions and deadlocks. SIGOPS Oper. Syst. Rev., 37: 237--252, 2003. Google ScholarDigital Library
- A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, pages 331--344, 2011. Google ScholarDigital Library
- C. N. Ip and D. L. Dill. Verifying systems with replicated components in murφ;, 1997.Google Scholar
- R. Johnson and K. Pingali. Dependence-based program analysis. In PLDI, pages 78--89, 1993. Google ScholarDigital Library
- V. Kahlon, S. Sankaranarayanan, and A. Gupta. Semantic reduction of thread interleavings in concurrent programs. In TACAS, pages 124--138, 2009. Google ScholarDigital Library
- A. Kaiser, D. Kroening, and T. Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV, pages 645--659. 2010. Google ScholarDigital Library
- Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In CAV, pages 424--435, 1997. Google ScholarDigital Library
- Y. Kesten, A. Pnueli, E. Shahar, and L. D. Zuck. Network invariants in action. In CONCUR, pages 101--115, 2002. Google ScholarDigital Library
- S. La Torre, P. Madhusudan, and G. Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV, pages 629--644. 2010. Google ScholarDigital Library
- S. K. Lahiri and R. E. Bryant. Predicate abstraction with indexed predicates. ACM Trans. Comput. Logic, 9, 2007. Google ScholarDigital Library
- L. Lamport. A new solution of dijkstra's concurrent programming problem. Commun. ACM, 17 (8): 453--455, 1974. Google ScholarDigital Library
- 011)}mineA. Miné. Static analysis of run-time errors in embedded critical parallel c programs. In ESOP, pages 398--418, Berlin, Heidelberg, 2011. Springer-Verlag. ISBN 978--3--642--19717--8. Google ScholarDigital Library
- M. Naik and A. Aiken. Conditional must not aliasing for static race detection. SIGPLAN Not., 42: 327--338, 2007. Google ScholarDigital Library
- M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. SIGPLAN Not., 41: 308--319, 2006. Google ScholarDigital Library
- G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. Cil: Intermediate language and tools for analysis and transformation of c programs. In CC, pages 213--228, 2002. Google ScholarDigital Library
- A. Pnueli, S. Ruah, and L. D. Zuck. Automatic deductive verification with invisible invariants. In TACAS, pages 82--97, 2001. Google ScholarDigital Library
- A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1, ı)-counter abstraction. In CAV, pages 107--122, 2002. ISBN 3--540--43997--8. Google ScholarDigital Library
- P. Pratikakis, J. S. Foster, and M. Hicks. Locksmith: context-sensitive correlation analysis for race detection. SIGPLAN Not., 41: 320--331, 2006. Google ScholarDigital Library
- N. Sterling. Warlock - a static data race analysis tool. In USENIX Winter, pages 97--106, 1993.Google Scholar
- J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. SIGPLAN Not., 39: 131--144, June 2004. ISSN 0362--1340. Google ScholarDigital Library
Index Terms
- Verification of parameterized concurrent programs by modular reasoning about data and control
Recommendations
Verification of parameterized concurrent programs by modular reasoning about data and control
POPL '12In this paper, we consider the problem of verifying thread-state properties of multithreaded programs in which the number of active threads cannot be statically bounded. Our approach is based on decomposing the task into two modules, where one reasons ...
Efficient Verification of Sequential and Concurrent C Programs
There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Verifying safety properties of concurrent heap-manipulating programs
We provide a parametric framework for verifying safety properties of concurrent heap-manipulating programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to verification algorithms that are ...
Comments