Skip to main content
SpringerLink
Log in

RedCard: Redundant Check Elimination for Dynamic Race Detectors

  • Conference paper
ECOOP 2013 – Object-Oriented Programming (ECOOP 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7920))

Included in the following conference series:

Abstract

Precise dynamic race detectors report an error if and only if an observed program trace exhibits a data race. They must typically check for races on all memory accesses to ensure that they catch all races and generate no spurious warnings. However, a race check for a particular memory access is guaranteed to be redundant if the accessing thread has already accessed that location within the same release-free span. A release-free span is any sequence of instructions containing no lock releases or other “release-like” synchronization operations, such as wait or fork.

We present a static analysis to identify redundant race checks by reasoning about memory accesses within release-free spans. In contrast to prior whole program analyses for identifying accesses that are always race-free, our redundant check analysis is span-local and can also be made method-local without any major loss in effectiveness. RedCard, our prototype implementation for the Java language, enables dynamic race detectors to reduce the number of run-time checks by close to 40% with no loss in precision.

We also present a complementary shadow proxy analysis for identifying when multiple memory locations can be treated as a single location by a dynamic race detector, again with no loss in precision. Combined, our analyses reduce the number of memory accesses requiring checks by roughly 50%.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: Static race detection for Java. TOPLAS 28(2), 207–255 (2006)

    Article  Google Scholar 

  2. Adve, S.V., Hill, M.D., Miller, B.P., Netzer, R.H.B.: Detecting data races on weak memory systems. In: ISCA, pp. 234–243 (1991)

    Google Scholar 

  3. Agarwal, R., Stoller, S.D.: Type inference for parameterized race-free java. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 149–160. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Barik, R., Sarkar, V.: Interprocedural load elimination for dynamic optimization of parallel programs. In: PACT, pp. 41–52 (2009)

    Google Scholar 

  5. Boyapati, C., Rinard, M.: A parameterized type system for race-free Java programs. In: OOPSLA, pp. 56–69 (2001)

    Google Scholar 

  6. CERN. Colt 1.2.0., http://dsd.lbl.gov/~hoschek/colt/

  7. Chamillard, A., Clarke, L.A., Avrunin, G.S.: An empirical comparison of static concurrency analysis techniques. Technical Report 96-084, Department of Computer Science, University of Massachusetts at Amherst (1996)

    Google Scholar 

  8. Choi, J.-D., Lee, K., Loginov, A., O’Callahan, R., Sarkar, V., Sridhara, M.: Efficient and precise datarace detection for multithreaded object-oriented programs. In: PLDI (2002)

    Google Scholar 

  9. Choi, J.-D., Miller, B.P., Netzer, R.H.B.: Techniques for debugging parallel programs with flowback analysis. TOPLAS 13(4), 491–530 (1991)

    Article  Google Scholar 

  10. Christiaens, M., Bosschere, K.D.: TRaDe: Data Race Detection for Java. In: International Conference on Computational Science, pp. 761–770 (2001)

    Google Scholar 

  11. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Effinger-Dean, L., Boehm, H.-J., Chakrabarti, D.R., Joisha, P.G.: Extended sequential reasoning for data-race-free programs. In: MSPC, pp. 22–29 (2011)

    Google Scholar 

  13. Effinger-Dean, L., Lucia, B., Ceze, L., Grossman, D., Boehm, H.-J.: IFRit: interference-free regions for dynamic data-race detection. In: OOPSLA, pp. 467–484 (2012)

    Google Scholar 

  14. Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: A race and transaction-aware Java runtime. In: PLDI, pp. 245–255 (2007)

    Google Scholar 

  15. Engler, D.R., Ashcraft, K.: RacerX: Effective, static detection of race conditions and deadlocks. In: SOSP, pp. 237–252 (2003)

    Google Scholar 

  16. Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. TOSEM 17(2) (2008)

    Google Scholar 

  17. Flanagan, C., Freund, S.N.: Type-based race detection for Java. In: PLDI, pp. 219–232 (2000)

    Google Scholar 

  18. Flanagan, C., Freund, S.N.: FastTrack: Efficient and precise dynamic race detection. Commun. ACM 53(11), 93–101 (2010)

    Article  Google Scholar 

  19. Flanagan, C., Freund, S.N.: Redcard: Redundant check elimination for dynamic race detectors. Technical Report UCSC-SOE-13-05, UC Santa Cruz (2013)

    Google Scholar 

  20. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002)

    Google Scholar 

  21. Fleury, E., Sutre, G.: Raja, version 0.4.0-pre4 (2007), http://raja.sourceforge.net/

  22. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  23. Grossman, D.: Type-safe multithreading in Cyclone. In: TLDI (2003)

    Google Scholar 

  24. Hosking, A.L., Nystrom, N., Whitlock, D., Cutts, Q.I., Diwan, A.: Partial redundancy elimination for access path expressions. Softw., Pract. Exper. 31(6), 577–600 (2001)

    Article  MATH  Google Scholar 

  25. Java Grande Forum. Java Grande benchmark suite (2008), http://www.javagrande.org

  26. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  27. Martin, J.-P., Hicks, M., Costa, M., Akritidis, P., Castro, M.: Dynamically checking ownership policies in concurrent C/C++ programs. In: POPL, pp. 457–470 (2010)

    Google Scholar 

  28. Mattern, F.: Virtual time and global states of distributed systems. In: Workshop on Parallel and Distributed Algorithms (1989)

    Google Scholar 

  29. Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI (2008)

    Google Scholar 

  30. Naik, M., Aiken, A., Whaley, J.: Effective static race detection for Java. In: PLDI (2006)

    Google Scholar 

  31. Nishiyama, H.: Detecting data races using dynamic escape analysis based on read barrier. In: Virtual Machine Research and Technology Symposium, pp. 127–138 (2004)

    Google Scholar 

  32. Pozniansky, E., Schuster, A.: MultiRace: Efficient on-the-fly data race detection in multithreaded C++ programs. Concurrency and Computation: Practice and Experience 19(3), 327–340 (2007)

    Article  Google Scholar 

  33. Raman, R., Zhao, J., Sarkar, V., Vechev, M., Yahav, E.: Efficient data race detection for async-finish parallelism. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 368–383. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  34. Ronsse, M., Bosschere, K.D.: RecPlay: A fully integrated practical record/replay system. TCS 17(2), 133–152 (1999)

    Google Scholar 

  35. Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: A dynamic data race detector for multi-threaded programs. TOCS 15(4), 391–411 (1997)

    Article  Google Scholar 

  36. Standard Performance Evaluation Corporation. SPEC benchmarks (2003), http://www.spec.org/

  37. von Praun, C., Gross, T.: Object race detection. In: OOPSLA, pp. 70–82 (2001)

    Google Scholar 

  38. von Praun, C., Gross, T.: Static conflict analysis for multi-threaded object-oriented programs. In: PLDI, pp. 115–128 (2003)

    Google Scholar 

  39. von Praun, C., Schneider, F.T., Gross, T.R.: Load elimination in the presence of side effects, concurrency and precise exceptions. In: Rauchwerger, L. (ed.) LCPC 2003. LNCS, vol. 2958, pp. 390–405. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  40. Voung, J.W., Jhala, R., Lerner, S.: Relay: static race detection on millions of lines of code. In: FSE, pp. 205–214 (2007)

    Google Scholar 

  41. T.J. Watson Libraries for Analysis (WALA) (2012), http://wala.sourceforge.net/

  42. Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. In: POPL, pp. 27–40 (2001)

    Google Scholar 

  43. Yu, Y., Rodeheffer, T., Chen, W.: RaceTrack: Efficient detection of data race conditions via adaptive tracking. In: SOSP, pp. 221–234 (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of California at Santa Cruz, USA

    Cormac Flanagan

  2. Williams College, USA

    Stephen N. Freund

Authors
  1. Cormac Flanagan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stephen N. Freund
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS, PPS - Université Paris Diderot, Case 7014, 75205, Paris Cedex 13, France

    Giuseppe Castagna

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Flanagan, C., Freund, S.N. (2013). RedCard: Redundant Check Elimination for Dynamic Race Detectors. In: Castagna, G. (eds) ECOOP 2013 – Object-Oriented Programming. ECOOP 2013. Lecture Notes in Computer Science, vol 7920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39038-8_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39038-8_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39037-1

  • Online ISBN: 978-3-642-39038-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation