Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 8

Proceedings of the 2016 Federated Conference on Computer Science and Information Systems

Efficient Data-Race Detection with Dynamic Symbolic Execution

DOI: http://dx.doi.org/10.15439/2016F117

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 ()

Full text

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.

References

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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.
  11. 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
  12. 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
  13. 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.
  14. 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
  15. 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
  16. 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
  17. A. Ibing, “Dynamic symbolic execution with interpolation based path merging,” in Int. Conf. Advances and Trends in Software Engineering, 2016.
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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
  23. M. Naik, “Effective static race detection for java,” Ph.D. dissertation, Stanford University, 2008.
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. C. Flanagan and S. Freund, “FastTrack: Efficient and precise dynamic race detection,” in PLDI, 2009. http://dx.doi.org/10.1145/1542476.1542490
  32. 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
  33. 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.
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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