Abstract
Multithreaded programs are prone to errors caused by unintended interference between concurrent threads. This paper focuses on verifying that deterministically-parallel code is free of such thread interference errors. Deterministically-parallel code may create and use new threads, via fork and join, and coordinate their behavior with synchronization primitives, such as barriers and semaphores. Such code does not satisfy the traditional non-interference property of atomicity (or serializability), however, and so existing atomicity tools are inadequate for checking deterministically-parallel code. We introduce a new non-interference specification for deterministically-parallel code, and we present a dynamic analysis to enforce it. We also describe SingleTrack, a prototype implementation of this analysis. SingleTrack’s performance is competitive with prior atomicity checkers, but it produces many fewer spurious warnings because it enforces a more general non-interference property that is applicable to more software.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Java Grande benchmark suite (2008), http://www.javagrande.org
Cheng, G.-I., Feng, M., Leiserson, C.E., Randall, K.H., Stark, A.F.: Detecting data races in Cilk programs that use locks. In: SPAA, pp. 298–309 (1998)
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, pp. 258–269 (2002)
Christiaens, M., Bosschere, K.D.: TRaDe: Data Race Detection for Java. In: Alexandrov, V.N., Dongarra, J., Juliano, B.A., Renner, R.S., Tan, C.J.K. (eds.) ICCS-ComputSci 2001. LNCS, vol. 2074, pp. 761–770. Springer, Heidelberg (2001)
Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: a race and transaction-aware Java runtime. In: PLDI, pp. 245–255 (2007)
Farzan, A., Madhusudan, P.: Causal atomicity. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 315–328. Springer, Heidelberg (2006)
Feng, M., Leiserson, C.E.: Efficient detection of determinacy races in Cilk programs. In: SPAA, pp. 1–11 (1997)
Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: POPL, pp. 256–267 (2004)
Flanagan, C., Freund, S.N., Lifshin, M., Qadeer, S.: Types for atomicity: Static checking and inference for Java. TOPLAS 30(4), 1–53 (2008)
Flanagan, C., Freund, S.N., Yi, J.: Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs. In: PLDI (2008)
Harris, T., Fraser, K.: Language support for lightweight transactions. In: OOPSLA, pp. 388–402 (2003)
Harris, T., Marlow, S., Peyton-Jones, S., Herlihy, M.: Composable memory transactions. In: PPOPP, pp. 48–60 (2005)
Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Communications of the ACM 18(12), 717–721 (1975)
Mattern, F.: Virtual time and global states of distributed systems. In: International Workshop on Parallel and Distributed Algorithms (1988)
Mellor-Crummey, J.: On-the-fly detection of data races for programs with nested fork-join parallelism. In: Supercomputing, pp. 24–33 (1991)
Netzer, R.H.B., Miller, B.P.: What are race conditions? some issues and formalizations. LOPLAS 1, 74–88 (1992)
Pozniansky, E., Schuster, A.: Efficient on-the-fly data race detection in multihreaded C++ programs. In: PPOPP, pp. 179–190 (2003)
Sasturkar, A., Agarwal, R., Wang, L., Stoller, S.D.: Automated type-based analysis of data races and atomicity. In: PPOPP, pp. 83–94 (2005)
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)
Schonberg, E.: On-the-fly detection of access anomalies. In: PLDI, pp. 285–297 (1989)
Shavit, N., Touitou, D.: Software transactional memory. In: PODC, pp. 204–213 (1995)
Vitek, J., Jagannathan, S., Welc, A., Hosking, A.L.: A semantic framework for designer transactions. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 249–263. Springer, Heidelberg (2004)
von Praun, C., Gross, T.: Object race detection. In: OOPSLA, pp. 70–82 (2001)
Wang, L., Stoller, S.D.: Accurate and efficient runtime detection of atomicity errors in concurrent programs. In: PPOPP, pp. 137–146 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sadowski, C., Freund, S.N., Flanagan, C. (2009). SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs. In: Castagna, G. (eds) Programming Languages and Systems. ESOP 2009. Lecture Notes in Computer Science, vol 5502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00590-9_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-00590-9_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00589-3
Online ISBN: 978-3-642-00590-9
eBook Packages: Computer ScienceComputer Science (R0)