Efficient Data-Race Detection with Dynamic Symbolic Execution
This paper presents data race detection using dy-namic symbolic execution and hybrid lockset / happens-beforeanalysis. Symbolic execution is used to explore the execution treeof multi-threaded software for FIFO scheduling on a single CPUcore. Compared to exploring the joint scheduling and executiontree, the combinatorial explosion is drastically reduced.An SMTsolver is used to control a debugger’s machine interface foradap-tive dynamic instrumentation to drive program execution intodesired paths. Data races are detected in concrete execution withavailable static binary instrumentation using hybrid analysis.State interpolation using unsatisfiable cores is employed for pathpruning, to avoid exploration of paths that do not contribute toincreasing branch coverage. An implementation in Eclipse CDTis described and evaluated with data race test cases from theJuliet C/C++ test suite for program analyzers.Index Terms—race detection; symbolic execution; interpola-tion; branch coverage.
Efficient Data-Race Detection with Dynamic Symbolic Execution
IEEE Software Engineering Workshop
| Authors: | Andreas Ibing |
| Year/month: | 2016/9 |
| Booktitle: | IEEE Software Engineering Workshop |
| Fulltext: | ibing16races.pdf |
Abstract |
|
| This paper presents data race detection using dy-namic symbolic execution and hybrid lockset / happens-beforeanalysis. Symbolic execution is used to explore the execution treeof multi-threaded software for FIFO scheduling on a single CPUcore. Compared to exploring the joint scheduling and executiontree, the combinatorial explosion is drastically reduced.An SMTsolver is used to control a debugger’s machine interface foradap-tive dynamic instrumentation to drive program execution intodesired paths. Data races are detected in concrete execution withavailable static binary instrumentation using hybrid analysis.State interpolation using unsatisfiable cores is employed for pathpruning, to avoid exploration of paths that do not contribute toincreasing branch coverage. An implementation in Eclipse CDTis described and evaluated with data race test cases from theJuliet C/C++ test suite for program analyzers.Index Terms—race detection; symbolic execution; interpola-tion; branch coverage. | |
Bibtex:
@inproceedings { 435,author = { Andreas Ibing},
title = { Efficient Data-Race Detection with Dynamic Symbolic Execution },
year = { 2016 },
month = { September },
booktitle = { IEEE Software Engineering Workshop },
url = {https://www.sec.in.tum.de/i20/publications/efficient-data-race-detection-with-dynamic-symbolic-execution/@@download/file/ibing16races.pdf}
}