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%.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: Static race detection for Java. TOPLAS 28(2), 207–255 (2006)
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)
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)
Barik, R., Sarkar, V.: Interprocedural load elimination for dynamic optimization of parallel programs. In: PACT, pp. 41–52 (2009)
Boyapati, C., Rinard, M.: A parameterized type system for race-free Java programs. In: OOPSLA, pp. 56–69 (2001)
CERN. Colt 1.2.0., http://dsd.lbl.gov/~hoschek/colt/
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)
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)
Choi, J.-D., Miller, B.P., Netzer, R.H.B.: Techniques for debugging parallel programs with flowback analysis. TOPLAS 13(4), 491–530 (1991)
Christiaens, M., Bosschere, K.D.: TRaDe: Data Race Detection for Java. In: International Conference on Computational Science, pp. 761–770 (2001)
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)
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)
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)
Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: A race and transaction-aware Java runtime. In: PLDI, pp. 245–255 (2007)
Engler, D.R., Ashcraft, K.: RacerX: Effective, static detection of race conditions and deadlocks. In: SOSP, pp. 237–252 (2003)
Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. TOSEM 17(2) (2008)
Flanagan, C., Freund, S.N.: Type-based race detection for Java. In: PLDI, pp. 219–232 (2000)
Flanagan, C., Freund, S.N.: FastTrack: Efficient and precise dynamic race detection. Commun. ACM 53(11), 93–101 (2010)
Flanagan, C., Freund, S.N.: Redcard: Redundant check elimination for dynamic race detectors. Technical Report UCSC-SOE-13-05, UC Santa Cruz (2013)
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002)
Fleury, E., Sutre, G.: Raja, version 0.4.0-pre4 (2007), http://raja.sourceforge.net/
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)
Grossman, D.: Type-safe multithreading in Cyclone. In: TLDI (2003)
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)
Java Grande Forum. Java Grande benchmark suite (2008), http://www.javagrande.org
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
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)
Mattern, F.: Virtual time and global states of distributed systems. In: Workshop on Parallel and Distributed Algorithms (1989)
Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI (2008)
Naik, M., Aiken, A., Whaley, J.: Effective static race detection for Java. In: PLDI (2006)
Nishiyama, H.: Detecting data races using dynamic escape analysis based on read barrier. In: Virtual Machine Research and Technology Symposium, pp. 127–138 (2004)
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)
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)
Ronsse, M., Bosschere, K.D.: RecPlay: A fully integrated practical record/replay system. TCS 17(2), 133–152 (1999)
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)
Standard Performance Evaluation Corporation. SPEC benchmarks (2003), http://www.spec.org/
von Praun, C., Gross, T.: Object race detection. In: OOPSLA, pp. 70–82 (2001)
von Praun, C., Gross, T.: Static conflict analysis for multi-threaded object-oriented programs. In: PLDI, pp. 115–128 (2003)
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)
Voung, J.W., Jhala, R., Lerner, S.: Relay: static race detection on millions of lines of code. In: FSE, pp. 205–214 (2007)
T.J. Watson Libraries for Analysis (WALA) (2012), http://wala.sourceforge.net/
Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. In: POPL, pp. 27–40 (2001)
Yu, Y., Rodeheffer, T., Chen, W.: RaceTrack: Efficient detection of data race conditions via adaptive tracking. In: SOSP, pp. 221–234 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)