Advertisement

Reporting Races in Dynamic Partial Order Reduction

  • Olli SaarikiviEmail author
  • Keijo Heljanko
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)

Abstract

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.

Keywords

Race detection Partial order reduction C++ Java DPOR 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. SIGPLAN Not. 43(6), 68–78 (2008)CrossRefGoogle Scholar
  2. 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
  3. 3.
    Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: A race and transaction-aware Java runtime. SIGPLAN Not. 42(6), 245–255 (2007)CrossRefGoogle Scholar
  4. 4.
    Flanagan, C., Freund, S.N.: FastTrack: Efficient and precise dynamic race detection. SIGPLAN Not. 44(6), 121–133 (2009)CrossRefGoogle Scholar
  5. 5.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. SIGPLAN Not. 40(1), 110–121 (2005)CrossRefGoogle Scholar
  6. 6.
    Itzkovitz, A., Schuster, A., Zeev-Ben-Mordehai, O.: Toward integration of data race detection in DSM systems. J. Parallel Distrib. Comput. 59(2), 180–203 (1999)CrossRefGoogle Scholar
  7. 7.
    Kähkönen, K., Heljanko, K.: Lightweight state capturing for automated testing of multithreaded programs. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 187–203. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  8. 8.
    Lochbihler, A.: Java and the java memory model — a unified, machine-checked formalisation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 497–517. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  9. 9.
    Norris, B., Demsky, B.: CDSchecker: Checking concurrent data structures written with C/C++ atomics. SIGPLAN Not. 48(10), 131–150 (2013)CrossRefGoogle Scholar
  10. 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
  11. 11.
    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Department of Computer Science and EngineeringAalto University School of ScienceEspooFinland

Personalised recommendations