Efficient Data-Race Detection with Dynamic Symbolic Execution

被引：1
|
作者：
Ibing, Andreas [1 ]
机构：
[1] Tech Univ Munich, Chair IT Secur, Bollzmannstr 3, D-85748 Garching, Germany
来源：
PROCEEDINGS OF THE 2016 FEDERATED CONFERENCE ON COMPUTER SCIENCE AND INFORMATION SYSTEMS (FEDCSIS) | 2016年 / 8卷
关键词：
race detection; symbolic execution; interpolation; branch coverage;
D O I：
10.15439/2016F117
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
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.
引用
收藏
页码：1719 / 1726
页数：8
相关论文
共 50 条
  • [1] IFRit: Interference-Free Regions for Dynamic Data-Race Detection
    Effinger-Dean, Laura
    Lucia, Brandon
    Ceze, Luis
    Grossman, Dan
    Boehm, Hans-J
    [J]. ACM SIGPLAN NOTICES, 2012, 47 (10) : 467 - 483
  • [2] Online data-race detection via coherency guarantees
    Perkovic, D
    Keleher, PJ
    [J]. PROCEEDINGS OF THE SECOND SYMPOSIUM ON OPERATING SYSTEMS DESIGN AND IMPLEMENTATION (OSDI '96), 1996, : 47 - 57
  • [3] LiteRace: Effective Sampling for Lightweight Data-Race Detection
    Marino, Daniel
    Musuvathi, Madanlal
    Narayanasamy, Satish
    [J]. ACM SIGPLAN NOTICES, 2009, 44 (06) : 134 - 143
  • [4] LiteRace: Effective Sampling for Lightweight Data-Race Detection
    Marino, Daniel
    Musuvathi, Madanlal
    Narayanasamy, Satish
    [J]. PLDI'09 PROCEEDINGS OF THE 2009 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2009, : 134 - 143
  • [5] Ready, set, Go! Data-race detection and the Go language
    Fava, Daniel Schnetzer
    Steffen, Martin
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2020, 195
  • [6] Fast and accurate static data-race detection for concurrent programs
    Kahlon, Vineet
    Yang, Yu
    Sankaranarayanan, Sriram
    Gupta, Aarti
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2007, 4590 : 226 - +
  • [7] Leveraging Abstract Interpretation for Efficient Dynamic Symbolic Execution
    Alatawi, Eman
    Sondergaard, Harald
    Miller, Tim
    [J]. PROCEEDINGS OF THE 2017 32ND IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE'17), 2017, : 619 - 624
  • [8] Employing Dynamic Symbolic Execution for Equivalent Mutant Detection
    Ghiduk, Ahmed S.
    Girgis, Moheb R.
    Shehata, Marwa H.
    [J]. IEEE ACCESS, 2019, 7 : 163767 - 163777
  • [9] OpenMP aware MHP Analysis for Improved Static Data-Race Detection
    Bora, Utpal
    Vaishay, Shraiysh
    Joshi, Saurabh
    Upadrasta, Ramakrishna
    [J]. PROCEEDINGS OF THE SEVENTH ANNUAL WORKSHOP ON THE LLVM COMPILER INFRASTRUCTURE IN HPC (LLVM-HPC2021), 2021, : 1 - 11
  • [10] An Efficient and Accurate Mixed Dynamic Data Race Detection Method
    Sun, Jiaze
    Yang, Yanman
    Shu, Xinfeng
    [J]. ACM International Conference Proceeding Series, 2021, : 531 - 535
12345