Sandeep Bindal
ABSTRACT
Previous approaches to systematic state-space exploration for testing multi-threaded programs have proposed context-bounding and depth-bounding to be effective ranking algorithms for testing multithreaded programs. This paper proposes two new metrics to rank thread schedules for systematic state-space exploration. Our metrics are based on characterization of a concurrency bug using v (the minimum number of distinct variables that need to be involved for the bug to manifest) and t (the minimum number of distinct threads among which scheduling constraints are required to manifest the bug). Our algorithm is based on the hypothesis that in practice, most concurrency bugs have low v (typically 1-2) and low t (typically 2-4) characteristics. We iteratively explore the search space of schedules in increasing orders of v and t. We show qualitatively and empirically that our algorithm finds common bugs in fewer number of execution runs, compared with previous approaches. We also show that using v and t improves the lower bounds on the probability of finding bugs through randomized algorithms. Systematic exploration of schedules requires instrumenting each variable access made by a program, which can be very expensive and severely limits the applicability of this approach. Previous work has avoided this problem by interposing only on synchronization operations (and ignoring other variable accesses). We demonstrate that by using variable bounding (v) and a static imprecise alias analysis, we can interpose on all variable accesses (and not just synchronization operations) at 10-100x less overhead than previous approaches.
- L. O. Andersen. Program analysis and specialization for the C programming language. Technical report, 1994.Google Scholar
- K. R. Apt, N. Francez, and S. Katz. Appraising fairness in distributed languages. In POPL ’87. Google ScholarDigital Library
- A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM, 53:66–75, February 2010. Google ScholarDigital Library
- S. Bindal, S. Bansal, and A. Lal. Variable and thread bounding for systematic testing of multithreaded programs. Technical report, IIT Delhi, 2012. http://arxiv.org/abs/1207.2544.Google Scholar
- D. Bruening and J. Chapin. Systematic testing of multithreaded programs. Technical report, LCS-TM-607, MIT/LCS, 2000.Google Scholar
- S. Burckhardt, P. Kothari, M. Musuvathi, and S. Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In ASPLOS ’10. Google ScholarDigital Library
- S. Chiba. Javassist — a reflection-based programming wizard for java. In OOPSLA ’98.Google Scholar
- T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: a race and transactionaware java runtime. In PLDI ’07. Google ScholarDigital Library
- M. Emmi, S. Qadeer, and Z. Rakamaric. Delay-bounded scheduling. In POPL, pages 411–422, 2011. Google ScholarDigital Library
- Y. Eytani, K. Havelund, S. D. Stoller, and S. Ur. Toward a framework and benchmark for testing tools for multi-threaded programs. Concurrency and Computation: Practice & Experience, 19(3):267––279, 2007. Google ScholarDigital Library
- P. Godefroid. Model checking for programming languages using VeriSoft. In POPL ’97. Google ScholarDigital Library
- P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1996. Google ScholarDigital Library
- P. Godefroid, R. S. Hanmer, and L. J. Jagadeesan. Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft. In ISSTA ’98. Google ScholarDigital Library
- P. Joshi, C.-S. Park, K. Sen, and M. Naik. A randomized dynamic program analysis technique for detecting real deadlocks. In PLDI ’09. Google ScholarDigital Library
- S. Khurshid, C. S. Păsăreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS’03. Google ScholarDigital Library
- O. Lhoták and L. Hendren. Evaluating the benefits of contextsensitive points-to analysis using a bdd-based implementation. ACM Trans. Softw. Eng. Methodol., 18:3:1–3:53, October 2008. Google ScholarDigital Library
- S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ASPLOS ’08. Google ScholarDigital Library
- S. Lu, J. Tucek, F. Qin, and Y. Zhou. Avio: detecting atomicity violations via access interleaving invariants. In ASPLOS ’06. Google ScholarDigital Library
- D. Marino, M. Musuvathi, and S. Narayanasamy. Literace: effective sampling for lightweight data-race detection. In PLDI ’09. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI ’07. Google ScholarDigital Library
- M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. In OSDI ’08.Google Scholar
- M. Naik, A. Aiken, and J. Whaley. Effective static race detection for java. In PLDI ’06. Google ScholarDigital Library
- S. Park, S. Lu, and Y. Zhou. CTrigger: Exposing atomicity violation bugs from their hiding places. In ASPLOS ’09. 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. Comput. Syst., 15:391–411, November 1997. Google ScholarDigital Library
- K. Sen. Race directed random testing of concurrent programs. In PLDI ’08. Google ScholarDigital Library
- S. D. Stoller. Model-checking multi-threaded distributed java programs. In SPIN Workshop on Model Checking and Software Verification, 2000. Google ScholarDigital Library
- J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI ’04. Google ScholarDigital Library
- W. Xiong, S. Park, J. Zhang, Y. Zhou, and Z. Ma. Ad hoc synchronization considered harmful. In OSDI ’10. Google ScholarDigital Library
- Y. Yu, T. Rodeheffer, and W. Chen. Racetrack: efficient detection of data race conditions via adaptive tracking. In SOSP ’05. Google ScholarDigital Library
Index Terms
- Variable and thread bounding for systematic testing of multithreaded programs
Recommendations
Iterative context bounding for systematic testing of multithreaded programs
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationMultithreaded programs are difficult to get right because of unexpected interaction between concurrently executing threads. Traditional testing methods are inadequate for catching subtle concurrency errors which manifest themselves late in the ...
Iterative context bounding for systematic testing of multithreaded programs
Proceedings of the 2007 PLDI conferenceMultithreaded programs are difficult to get right because of unexpected interaction between concurrently executing threads. Traditional testing methods are inadequate for catching subtle concurrency errors which manifest themselves late in the ...
Testing multithreaded programs via thread speed control
ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software EngineeringA multithreaded program's interleaving space is discrete and astronomically large, making effectively sampling thread schedules for manifesting concurrency bugs a challenging task. Observing that concurrency bugs can be manifested by adjusting thread ...
Comments