Reporting Races in Dynamic Partial Order Reduction
Data races are a common type of bug found in multithreaded programs. The dynamic partial order reduction algorithm (DPOR) is an efficient algorithm for exploring a reduced set of interleavings that guarantees all assertion errors and deadlocks to be found. However, while DPOR does in effect explore different outcomes of data races, it was not originally designed to report them. In this paper a method for reporting data races during DPOR is presented. This allows data races to be found even when they do not trigger assertion errors or deadlocks. Additionally, for programs written in C++11 and a large subset of Java, the presented method allows DPOR to warn the user when it can not guarantee completeness due to the program having data races that trigger weak memory model semantics for it.
KeywordsRace detection Partial order reduction C++ Java DPOR
Unable to display preview. Download preview PDF.
- 2.Elmas, T., Qadeer, S., Tasiran, S.: Precise race detection and efficient model checking using locksets. Tech. Rep. MSR-TR-2005-118, Microsoft Research (2005)Google Scholar
- 10.Saarikivi, O., Kähkönen, K., Heljanko, K.: Improving dynamic partial order reductions for concolic testing. In: 12th International Conference on Application of Concurrency to System Design, ACSD 2012, Hamburg, Germany, June 27–29, 2012, pp. 132–141 (2012)Google Scholar