Efficient Data-Race Detection with Dynamic Symbolic Execution
Citation: Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 8, pages 1719–1726 (2016)
Abstract. This paper presents data race detection using dynamic symbolic execution and hybrid lockset / happens-before analysis. Symbolic execution is used to explore the execution tree of multi-threaded software for FIFO scheduling on a single CPU core. Compared to exploring the joint scheduling and execution tree, the combinatorial explosion is drastically reduced. An SMT solver is used to control a debugger's machine interface for adaptive dynamic instrumentation to drive program execution into desired paths. Data races are detected in concrete execution with available static binary instrumentation using hybrid analysis. State interpolation using unsatisfiable cores is employed for path pruning, to avoid exploration of paths that do not contribute to increasing branch coverage. An implementation in Eclipse CDT is described and evaluated with data race test cases from the Juliet C/C++ test suite for program analyzers.
- R. Netzer and B. Miller, “What are race conditions?: Some issues and formalizations,” ACM Letters on Programming Languages and Systems, pp. 74–88, 1992. http://dx.doi.org/10.1145/130616. 130623
- L. Lamport, “Time, clocks, and the ordering of events in a distributed system,” Communications of the ACM, vol. 21, no. 7, pp. 558–565, 1978. http://dx.doi.org/10.1145/359545.359563
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson, “Eraser: A dynamic data race detector for multi-threaded programs,” ACM Trans. Computer Systems, vol. 15, no. 4, pp. 391–411, 1997. http://dx.doi.org/10.1145/268998.266641
- R. O’Callahan and J. Choi, “Hybrid dynamic data race detection,” in ACM Symposium on Principles and Practice of Parallel Programming, 2003. http://dx.doi.org/10.1145/966049.781528
- K. Serebryany and T. Iskhodzhanov, “ThreadSanitizer: data race detection in practice,” in Workshop on Binary Instrumentation and Applications, 2009, pp. 62–71. http://dx.doi.org/10.1145/1791194.1791203
- J. King, “Symbolic execution and program testing,” Communications of the ACM, vol. 19, no. 7, pp. 385–394, 1976. http://dx.doi.org/10.1145/360248.360252
- L. de Moura and N. Bjorner, “Satisfiability modulo theories: Introduction and applications,” Communications of the ACM, vol. 54, no. 9, 2011. http://dx.doi.org/10.1145/1995376.1995394
- P. Godefroid, N. Klarlund, and K. Sen, “DART: Directed automated random testing,” in Conference on Programming Language Design and Implementation, 2005, pp. 213–223. http://dx.doi.org/10.1145/1064978.1065036
- K. Sen, D. Marinov, and G. Agha, “CUTE: A concolic unit testing engine for C,” in European Software Engineering Conference and International Symposium on Foundations of Software Engineering, 2005, pp. 263–272. http://dx.doi.org/10.1145/1095430.1081750
- C. Cadar, D. Dunbar, and D. Engler, “KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs,” in USENIX Symp. Operating Systems Design and Implementation, 2008.
- K. Sen and G. Agha, “CUTE and jCUTE: concolic unit testing and explicit path model-checking tools,” in Int. Conf. Computer Aided Verification, 2006, pp. 419–423. http://dx.doi.org/10.1007/11817963_38
- A. Farzan, A. Holzer, N. Razavi, and H. Veith, “Con2colic testing,” in ESEC/FSE Joint Meeting on Foundations of Software Engineering, 2013, pp. 37–47. http://dx.doi.org/10.1145/2491411.2491453
- K. Kähkönen, O. Saarikivi, and K. Heljanko, “LCT: A parallel distributed testing tool for multithreaded Java programs,” Electronic Notes in Theoretical Computer Science, pp. 253—259, 2013.
- C. Flanagan and P. Godefroid, “Dynamic partial-order reduction for model checking software,” in ACM Symposium on Principles of Programming Languages, 2005, pp. 110–121. http://dx.doi.org/10.1145/1047659.1040315
- T. Boland and P. Black, “Juliet 1.1 C/C++ and Java test suite,” IEEE Computer, vol. 45, no. 10, 2012. http://dx.doi.org/10.1109/MC.2012.345
- J. Jaffar, A. Santosa, and R. Voicu, “An interpolation method for CLP traversal,” in Int. Conf. Principles and Practice of Constraint Programming (CP), 2009, pp. 454–469. http://dx.doi.org/10.1007/978-3-642-04244-7_37
- A. Ibing, “Dynamic symbolic execution with interpolation based path merging,” in Int. Conf. Advances and Trends in Software Engineering, 2016.
- L. deMoura and N. Bjorner, “Z3: An efficient SMT solver,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008, pp. 337–340. http://dx.doi.org/10.1007/978-3-540-78800-3_24
- M. Abadi, C. Flanagan, and S. Freund, “Types for safe locking: Static race detection for Java,” ACM Trans. Programming Languages and Systems, vol. 28, no. 2, pp. 207–255, 2006. http://dx.doi.org/10.1145/1119479.1119480
- J. Voung, R. Jhala, and S. Lerner, “RELAY: static race detection on millions of lines of code,” in ACM Symp. Foundations of Software Engineering (ESEC-FSE), 2007. http: //dx.doi.org/10.1145/1287624.1287654
- P. Pratikakis, J. Foster, and M. Hicks, “LOCKSMITH: Practical static race detection for C,” ACM Trans. Programming Languages and Systems, vol. 33, 2011. http://dx.doi.org/10.1145/1889997.1890000
- M. Eslamimehr and J. Palsberg, “Race directed scheduling of concurrent programs,” in ACM Symposium on Principles and Practice of Parallel Programming, 2014, pp. 301–314. http://dx.doi.org/10.1145/2692916.2555263
- M. Naik, “Effective static race detection for java,” Ph.D. dissertation, Stanford University, 2008.
- S. Qadeer and J. Rehof, “Context-bounded model checking of concurrent software,” in TACAS, 2005. http://dx.doi.org/10.1007/978-3-540-31980-1_7
- I. Rabinovitz and O. Grumberg, “Bounded model checking of concurrent programs,” in Int. Conf. Computer Aided Verification (CAV), 2005. http://dx.doi.org/10.1007/11513988_9
- L. Cordeiro and B. Fischer, “Verifying multi-threaded software using SMT-based context-bounded model checking,” in ACM Int. Conf. Software Eng., 2011, pp. 331–340. http://dx.doi.org/10.1145/1985793.1985839
- P. Godefroid, “Partial-order methods for the verification of concurrent systems - an approach to the state-explosion problem,” Lecture Notes in Computer Science, vol. 1032, 1996. http://dx.doi.org/10.1007/3-540-60761-7
- V. Kahlon, C. Wang, and A. Gupta, “Monotonic partial order reduction: An optimal symbolic partial order reduction technique,” in CAV, 2009. http://dx.doi.org/10.1007/978-3-642-02658-4_31
- P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas, “Optimal dynamic partial order reduction,” in ACM Symposium on Principles of Programming Languages, 2014. http://dx.doi.org/10.1145/2535838.2535845
- D. Marino, M. Musuvathi, and S. Narayanasamy, “LiteRace: Effective sampling for lightweight data-race detection,” in ACM Conf. Programming Language Design and Implementation, 2009. http://dx.doi.org/10.1145/1542476.1542491
- C. Flanagan and S. Freund, “FastTrack: Efficient and precise dynamic race detection,” in PLDI, 2009. http://dx.doi.org/10.1145/1542476.1542490
- M. Bond, K. Coons, and K. McKinley, “PACER: proportional detection of data races,” in ACM Conf. Programming Language Design and Implementation, 2010. http://dx.doi.org/10.1145/1806596.1806626
- J. Erickson, M. Musuvathi, S. Burchhardt, and K. Olynyik, “Effective data-race detection for the kernel,” in USENIX Symposium on Operating Systems Design and Implementation, 2010.
- A. Itzkovitz, A. Schuster, and O. Mordehai, “Towards integration of data race detection in DSM systems,” J. Parallel and Distributed Computing, vol. 59, pp. 180–203, 1999. http://dx.doi.org/10.1006/jpdc.1999.1574
- E. Pozniansky and A. Schuster, “MultiRace: Efficient on-the-fly data race detection in multithreaded C++ programs,” J. Concurrency and Computation: Practice and Experience, vol. 19, no. 3, pp. 327–340, 2007. http://dx.doi.org/10.1002/cpe.v19:3
- Y. Yu, T. Rodeheffer, and W. Chen, “RaceTrack: Efficient detection of data race conditions via adaptive tracking,” in ACM Operating Systems Review, 2005. http://dx.doi.org/10.1145/1095809. 1095832
- T. Elmas, S. Qadeer, and S. Tasiran, “Goldilocks: a race-aware Jave runtime,” Communications of the ACM, vol. 53, no. 11, pp. 85–92, 2010. http://dx.doi.org/10.1145/1839676.1839698
- P. Zhou, R. Teodorescu, and Y. Zhou, “HARD: Hardware-assisted lockset-based race detection,” in Int. Symp. High-Performance Computer Architecture, 2007. http://dx.doi.org/10.1109/ HPCA.2007.346191
- J. Devietti, B. Wood, K. Strauss, L. Ceze, D. Grossman, and S. Qadeer, “RADISH: always-on sound and complete race detection in software and hardware,” in Int. Symp. Computer Architecture, 2012, pp. 202–212. http://dx.doi.org/10.1145/2366231.2337182
- P. Deligiannis, A. Donaldson, and Z. Rakamaric, “Fast and precise symbolic analysis of concurrency bugs in device drivers,” in Int. Conf. Automated Software Eng., 2015. http://dx.doi.org/10.1109/ASE.2015.30
- K. McMillan, “Lazy annotation for program testing and verification,” in Int. Conf. Computer Aided Verification (CAV), 2010, pp. 104–118. http://dx.doi.org/10.1007/978-3-642-14295-6_10
- D. Chu and J. Jaffar, “A framework to synergize partial order reduction with state interpolation,” in Hardware and Software: Verification and Testing, 2014, pp. 171–187. http://dx.doi.org/10.1007/978-3-319-13338-6_14