Abstract
This paper describes the methods used in Empire, a tool to detect concurrency-related bugs, namely atomic-set serializability violations in Java programs. The correctness criterion is based on atomic sets of memory locations, which share a consistency property, and units of work, which preserve consistency when executed sequentially. Empire checks that, for each atomic set, its units of work are serializable. This notion subsumes data races (single-location atomic sets), and serializability (all locations in one atomic set).
To obtain a sound, finite model of locking behavior for use in Empire, we devised a new abstraction principle, random isolation, which allows strong updates to be performed on the abstract counterpart of each randomly-isolated object. This permits Empire to track the status of a Java lock, even for programs that use an unbounded number of locks. The advantage of random isolation is that properties proved about a randomly-isolated object can be generalized to all objects allocated at the same site. We ran Empire on eight programs from the ConTest benchmark suite, for which Empire detected numerous violations.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Vaziri, M., Tip, F., Dolby, J.: Associating synchronization constraints with data in an object-oriented language. In: POPL (2006)
Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL (2003)
Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 334–349. Springer, Heidelberg (2006)
Hammer, C., Dolby, J., Vaziri, M., Tip, F.: Dynamic detection of atomic-set-serializability violations. In: ICSE (2008)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. In: TSE (1986)
Eytani, Y., Havelund, K., Stoller, S.D., Ur, S.: Towards a framework and a benchmark for testing tools for multi-threaded programs. Conc. and Comp.: Prac. and Exp. 19(3), 267–279 (2007)
Jones, N., Muchnick, S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: POPL (1982)
Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for Java. TOSEM 14(1) (2005)
Kidd, N., Lal, A., Reps, T.: Language strength reduction. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 283–298. Springer, Heidelberg (2008)
Watson Libraries for Analysis (WALA), T.J.: http://wala.sourceforge.net/wiki/index.php
Horwitz, S., Pfeiffer, P., Reps, T.: Dependence analysis for pointer variables. In: PLDI (1989)
Jones, N., Muchnick, S.: Flow analysis and optimization of Lisp-like structures. In: Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs (1981)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3) (2002)
Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221–239. Springer, Heidelberg (2006)
McMillan, K.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219–237. Springer, Heidelberg (1999)
Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1, ∞ )-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 107. Springer, Heidelberg (2002)
Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 69–84. Springer, Heidelberg (2002)
Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA (2002)
Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. In: PLDI (2004)
Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: POPL (2007)
von Praun, C., Gross, T.R.: Object race detection. In: OOPSLA (2001)
Min, S.L., Choi, J.D.: An efficient cache-based access anomaly detection scheme. In: ASPLOS (1991)
O’Callahan, R., Choi, J.D.: Hybrid dynamic data race detection. In: PPoPP (2003)
Artho, C., Havelund, K., Biere, A.: High-level data races. In: Proc. NDDL/VVEIS 2003 (2003)
Burrows, M., Leino, K.R.M.: Finding stale-value errors in concurrent programs. Conc. and Comp.: Prac. and Exp. 16(12) (2004)
Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. In: POPL, pp. 256–267 (2004)
Sasturkar, A., Agarwal, R., Wang, L., Stoller, S.D.: Automated type-based analysis of data races and atomicity. In: PPoPP (2005)
Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: Detecting atomicity violations via access interleaving invariants. In: ASPLOS (2006)
Wang, L., Stoller, S.D.: Accurate and efficient runtime detection of atomicity errors in concurrent programs. In: PPoPP (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kidd, N., Reps, T., Dolby, J., Vaziri, M. (2008). Finding Concurrency-Related Bugs Using Random Isolation. In: Jones, N.D., Müller-Olm, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2009. Lecture Notes in Computer Science, vol 5403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-93900-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-93900-9_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-93899-6
Online ISBN: 978-3-540-93900-9
eBook Packages: Computer ScienceComputer Science (R0)