Speeding Up Maximal Causality Reduction with Static Dependency Analysis

Authors Shiyou Huang, Jeff Huang



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.16.pdf
  • Filesize: 0.76 MB
  • 22 pages

Document Identifiers

Author Details

Shiyou Huang
Jeff Huang

Cite AsGet BibTex

Shiyou Huang and Jeff Huang. Speeding Up Maximal Causality Reduction with Static Dependency Analysis. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.16

Abstract

Stateless Model Checking (SMC) offers a powerful approach to verifying multithreaded programs but suffers from the state-space explosion problem caused by the huge thread interleaving space. The pioneering reduction technique Partial Order Reduction (POR) mitigates this problem by pruning equivalent interleavings from the state space. However, limited by the happens-before relation, POR still explores redundant executions. The recent advance, Maximal Causality Reduction (MCR), shows a promising performance improvement over the existing reduction techniques, but it has to construct complicated constraints to ensure the feasibility of the derived execution due to the lack of dependency information. In this work, we present a new technique, which extends MCR with static analysis to reduce the size of the constraints, thus speeding up the exploration of the state space. We also address the redundancy problem caused by the use of static analysis. We capture the dependency between a read and a later event e in the trace from the system dependency graph and identify those reads that e is not control dependent on. Our approach then ignores the constraints over such reads to reduce the complexity of the constraints. The experimental results show that compared to MCR, the number of the constraints and the solving time by our approach are averagely reduced by 31.6% and 27.8%, respectively.
Keywords
  • Model Checking
  • Dynamic Analysis
  • Program Dependency Analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Joana: Information flow control framework for java. URL: http://pp.ipd.kit.edu/projects/joana/.
  2. Wala. URL: https://github.com/wala/WALA.
  3. Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Optimal dynamic partial order reduction. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, 2014. Google Scholar
  4. Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Optimal dynamic partial order reduction. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014. Google Scholar
  5. Sarita V Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. computer, 29(12):66-76, 1996. Google Scholar
  6. Hiralal Agrawal and Joseph R. Horgan. Dynamic program slicing. In Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, PLDI, 1990. Google Scholar
  7. Edmund M Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT press, 1999. Google Scholar
  8. Katherine E. Coons, Madanlal Musuvathi, and Kathryn S. Mckinley. Bounded partial-order reduction. In In Proceedings of the 2013 Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 833-848, 2013. Google Scholar
  9. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  10. Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005. Google Scholar
  11. Patrice Godefroid. Model checking for programming languages using verisoft. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1997. Google Scholar
  12. Patrice Godefroid. Software model checking: The verisoft approach. Formal Methods in System Design, 2005. Google Scholar
  13. Patrice Godefroid, J van Leeuwen, J Hartmanis, G Goos, and Pierre Wolper. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, volume 1032. Springer Heidelberg, 1996. Google Scholar
  14. Jurgen Graf. Speeding up context-, object- and field-sensitive sdg generation. In Proceedings of the 2010 10th IEEE Working Conference on Source Code Analysis and Manipulation, SCAM, 2010. Google Scholar
  15. S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. In Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI, 1988. Google Scholar
  16. Jeff Huang. Stateless model checking concurrent programs with maximal causality reduction. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, 2015. Google Scholar
  17. Jeff Huang, Patrick O'Neil Meredith, and Grigore Rosu. Maximal sound predictive race detection with control flow abstraction. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014. Google Scholar
  18. Jeff Huang and Lawrence Rauchwerger. Finding schedule-sensitive branches. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE, 2015. Google Scholar
  19. Jeff Huang, Charles Zhang, and Julian Dolby. Clap: Recording local executions to reproduce concurrency failures. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, 2013. Google Scholar
  20. Shiyou Huang and Jeff Huang. Maximal causality reduction for tso and pso. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA, 2016. Google Scholar
  21. Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. Computers, IEEE Transactions on, 100(9):690-691, 1979. Google Scholar
  22. Nuno Machado, Brandon Lucia, and Luís Rodrigues. Production-guided concurrency debugging. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '16, 2016. Google Scholar
  23. Madanlal Musuvathi and Shaz Qadeer. Partial-order reduction for context-bounded state exploration. Technical report, Tech. Rep. MSR-TR-2007-12, Microsoft Research, 2007. Google Scholar
  24. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In OSDI, volume 8, pages 267-280, 2008. Google Scholar
  25. Karl J. Ottenstein and Linda M. Ottenstein. The program dependence graph in a software development environment. In Proceedings of the First ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, SDE 1, 1984. Google Scholar
  26. Scott Owens, Susmit Sarkar, Peter Sewell, and A Better. x86 memory model: x86-tso. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, 2009. Google Scholar
  27. Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. Soot - a java bytecode optimization framework. In Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, CASCON, 1999. Google Scholar
  28. Mark Weiser. Program slicing. In Proceedings of the 5th International Conference on Software Engineering, ICSE, 1981. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail