Abstract
Data races do not cover all kinds of concurrency errors. This paper presents a data-flow-based technique to find stale-value errors, which are not found by low-level and high-level data race algorithms. Stale values denote copies of shared data where the copy is no longer synchronized. The algorithm to detect such values works as a consistency check that does not require any assumptions or annotations of the program. It has been implemented as a static analysis in JNuke. The analysis is sound and requires only a single execution trace if implemented as a run-time checking algorithm. Being based on an analysis of Java bytecode, it encompasses the full program semantics, including arbitrarily complex expressions. Related techniques are more complex and more prone to over-reporting.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arnold, K., Gosling, J.: The Java Programming Language. Addison-Wesley, Reading (1996)
Artho, C., Biere, A.: Applying static analysis to large-scale, multithreaded Java programs. In: Grant, D. (ed.) Proc. 13th ASWEC, Canberra, Australia, IEEE Computer Society, Los Alamitos (2001)
Artho, C., Havelund, K., Biere, A.: High-level data races. Journal on Software Testing. Verification & Reliability (STVR) 13(4) (2003)
Artho, C., Schuppan, V., Biere, A., Eugster, P., Baur, M., Zweimüller, B.: JNuke: efficient dynamic analysis for Java. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 462–465. Springer, Heidelberg (2004)
Blanchet, B.: Escape analysis for object-oriented languages: application to Java. In: Proc. OOPSLA 1999, Denver, USA, pp. 20–34. ACM Press, New York (1999)
Blanchet, B.: Escape analysis for java, theory and practice. ACM Transactions on Programming Languages and Systems 25(6), 713–775 (2003)
Bogda, J., Hölzle, U.: Removing unnecessary synchronization in Java. In: Proc. OOPSLA 1999, Denver, USA, pp. 35–46. ACM Press, New York (1999)
Burrows, M., Leino, R.: Finding stale-value errors in concurrent programs. Technical Report SRC-TN-2002-004, Compaq SRC, Palo Alto, USA (2002)
Choi, J., Gupta, M., Serrano, M., Sreedhar, V., Midkiff, S.: Escape analysis for Java. In: Proc. OOPSLA 1999, Denver, USA, pp. 1–19. ACM Press, New York (1999)
Flanagan, C.: Verifying commit-atomicity using model-checking. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 252–266. Springer, Heidelberg (2004)
Flanagan, C., Freund, S.: Atomizer: a dynamic atomicity checker for multithreaded programs. SIGPLAN Not 39(1), 256–267 (2004)
Flanagan, C., Leino, R., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for Java. In: Proc. PLDI 2002, Berlin, Germany, pp. 234–245. ACM Press, New York (2002)
Flanagan, C., Qadeer, S.: Types for atomicity. In: Proc. Workshop on Types in Language Design and Implementation (TLDI 2003), New Orleans, USA, ACM Press, New York (2003)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (2000)
Harrow, J.: Runtime checking of multithreaded applications with Visual Threads. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, Springer, Heidelberg (2000)
Lea, D.: Concurrent Programming in Java, Second Edition, 2nd edn. Addison-Wesley, Reading (1999)
Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)
Praun, C.v., Gross, T.: Static detection of atomicity violations in object-oriented programs. In: Proc. Formal Techniques for Java-like Programs, vol. 408 of Technical Reports from ETH Zürich. ETH Zürich (2003)
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. on Computer Systems 15(4) (1997)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal 10(2) ( April 2003)
von Praun, C., Gross, T.: Object-race detection. In: OOPSLA 2001, Tampa Bay, USA, ACM Press, New York (2001)
Wang, L., Stoller, S.: Run-time analysis for atomicity. In: Proc. Run-Time Verification Workshop (RV 2003), Boulder, USA. ENTCS, vol. 89(2), Elsevier, Amsterdam (2003)
Whaley, J., Rinard, M.: Compositional pointer and escape analysis for Java programs. In: Proc. OOPSLA 1999, Denver, USA, pp. 187–206. ACM Press, New York (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Artho, C., Havelund, K., Biere, A. (2004). Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive