Parosh Abdulla
Stavros Aronis
ABSTRACT
Stateless model checking is a powerful technique for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR). We present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, which replace the role of persistent sets in previous algorithms. First, we show how to modify an existing DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm. Second, we extend this algorithm with a novel mechanism, called wakeup trees, that allows to achieve optimality. We have implemented both algorithms in a stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance and that wakeup trees incur only a small overhead in both time and space.
Supplemental Material
- J. Armstrong. Erlang. phComm. of the ACM, 53 (9): 68--75, 2010. Google Scholar
Digital Library
- M. Christakis, A. Gotovos, and K. Sagonas. Systematic testing for detecting concurrency errors in Erlang programs. In ICST, 2013. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, M. Minea, and D. Peled. State space reduction using partial order techniques. phSTTT, 2: 279--287, 1999.Google Scholar
- C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In POPL, pages 110--121. ACM, 2005. Google ScholarDigital Library
- C. Flanagan and P. Godefroid. Addendum to Dynamic partial-order reduction for model checking software, 2005. Available at http://research.microsoft.com/en us/um/people/pg/.Google Scholar
- P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. PhD thesis, University of Liège, 1996. Also, volume 1032 of LNCS, Springer. Google ScholarDigital Library
- P. Godefroid. Model checking for programming languages using VeriSoft. In POPL, pages 174--186. ACM Press, 1997. Google ScholarDigital Library
- P. Godefroid. Software model checking: The VeriSoft approach. Formal Methods in System Design, 26 (2): 77--101, 2005. Google ScholarDigital Library
- P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In CAV, volume 697 of LNCS, 1993. Google ScholarDigital Library
- P. Godefroid, G. J. Holzmann, and D. Pirottin. State-space caching revisited. Formal Methods in System Design, 7 (3): 227--241, 1995. Google ScholarDigital Library
- K. Kähkönen, O.Saarikivi, and Heljanko. Using unfoldings in automated testing of multithreaded programs. In ASE, pages 150--159. ACM, 2012. Google ScholarDigital Library
- V. Kahlon, C. Wang, and A. Gupta. Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In CAV, volume 5643 of LNCS, pages 398--413. Springer, 2009. Google ScholarDigital Library
- S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101: 337--359, 1992. Google ScholarDigital Library
- S. Lauterburg, R. Karmani, D. Marinov, and G. Agha. Evaluating ordering heuristics for dynamic partial-order reduction techniques. In FASE, volume 6013 of LNCS, pages 308--322. Springer, 2010. Google ScholarDigital Library
- Y. Lei and R. Carver. Reachability testing of concurrent programs. IEEE Trans. Softw. Eng., 32 (6): 382--403, 2006. Google ScholarDigital Library
- F. Mattern. Virtual time and global states of distributed systems. In M. Cosnard, editor, Proc. Workshop on Parallel and Distributed Algorithms, pages 215--226, Ch. de Bonas, France, 1989. Elsevier.Google Scholar
- A. Mazurkiewicz. Trace theory. In Advances in Petri Nets, 1986. Google Scholar
- K. McMillan. A technique of a state space search based on unfolding. Formal Methods in System Design, 6 (1): 45--65, 1995. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446--455, 2007. Google ScholarDigital Library
- M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In OSDI, pages 267--280. USENIX Association, 2008. Google ScholarDigital Library
- D. Peled. All from one, one for all, on model-checking using representatives. In CAV, volume 697 of LNCS, pages 409--423, 1993. Google ScholarDigital Library
- O. Saarikivi, K. Kähkönen, and K. Heljanko. Improving dynamic partial order reductions for concolic testing. In ACSD. IEEE, 2012. Google ScholarDigital Library
- K. Sen and G. Agha. Automated systematic testing of open distributed programs. In FASE, volume 3922 of LNCS, pages 339--356, 2006. Google ScholarDigital Library
- K. Sen and G. Agha. A race-detection and flipping algorithm for automated testing of multi-threaded programs. In Haifa Verification Conference, volume 4383 of LNCS, pages 166--182. Springer, 2007. Google ScholarDigital Library
- S. Tasharofi et al. TransDPOR: A novel dynamic partial-order reduction technique for testing actor programs. In FMOODS/FORTE, volume 7273 of LNCS, pages 219--234. Springer, 2012. Google ScholarDigital Library
- A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets, volume 483 of LNCS, pages 491--515, 1990. Google ScholarDigital Library
Index Terms
- Optimal dynamic partial order reduction
Recommendations
Dynamic partial-order reduction for model checking software
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to ...
Optimal dynamic partial order reduction
POPL '14Stateless model checking is a powerful technique for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, ...
Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
Stateless model checking is a powerful method for program verification that, however, suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is ...
Comments