Abstract
In applying stateless model checking methods to realistic multithreaded programs, we find that stateless search methods are ineffective in practice, even with dynamic partial order reduction (DPOR) enabled. To solve the inefficiency of stateless runtime model checking, this paper makes two related contributions. The first contribution is a novel and conservative light-weight method for storing abstract states at runtime to help avoid redundant searches. The second contribution is a stateful dynamic partial order reduction algorithm (SDPOR) that avoids a potential unsoundness when DPOR is naively applied in the context of stateful search. Our stateful runtime model checking approach combines light-weight state recording with SDPOR, and strikes a good balance between state recording overheads, on one hand, and the elimination of redundant searches, on the other hand. Our experiments confirm the effectiveness of our approach on several multithreaded benchmarks in C, including some practical programs.
Supported in part by NSF award CNS00509379, Microsoft HPC Institute Program, and SRC Contract 2005-TJ-1318.
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
Lee, E.A.: The problem with threads, vol. 39, pp. 33–42. IEEE Computer Society Press, Los Alamitos (2006)
Godefroid, P.: Model Checking for Programming Languages using Verisoft. In: POPL, pp. 174–186 (1997)
Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 446–455. ACM, New York (2007)
Flanagan, C., Godefroid, P.: Dynamic Partial-order Reduction for Model Checking Software. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 110–121. ACM, New York (2005)
Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A Pragmatic Approach to Model Checking Real Code. In: OSDI (2002)
Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In: ASE, pp. 3–12 (2000)
Pratikakis, P., Foster, J.S., Hicks, M.: Locksmith: context-sensitive correlation analysis for race detection. In: PLDI, pp. 320–331. ACM Press, New York (2006)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Heidelberg (1996)
Palmer, R.L.: Formal Analysis for MPI-based High Performance Computing Software, Ph.D. Dissertation, University of Utah (2007)
Yang, Y., Chen, X., Gopalakrishnan, G.: UUCS-08-004:Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical report (2008)
Salcianu, A., Rinard, M.: Pointer and escape analysis for multithreaded programs. In: PPoPP, pp. 12–23. ACM Press, New York (2001)
Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bosnacki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 95–112. Springer, Heidelberg (2007)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)
Robby, Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: ESEC / SIGSOFT FSE, pp. 267–276 (2003)
Yi, X., Wang, J., Yang, X.: Stateful Dynamic Partial-Order Reduction. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 149–167. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.M. (2008). Efficient Stateful Dynamic Partial Order Reduction. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)