Abstract
The Java memory model guarantees sequentially consistent behavior only for programs that are data race free. Legal executions of programs with data races may be sequentially inconsistent but are subject to constraints that ensure weak safety properties. Occasionally, one allows programs to contain data races for performance reasons and these constraints make it possible, in principle, to reason about their correctness. Because most model checking tools, including Java Pathfinder, only generate sequentially consistent executions, they are not sound for programs with data races. We give an alternative semantics for the JMM that characterizes the legal executions as a least fixed point and show that this is an overapproximation of the JMM. We have extended Java Pathfinder to generate these executions, yielding a tool that can be soundly used to reason about programs with data races.
Chapter PDF
References
Aspinall, D., Ševčík, J.: Formalising Java’s Data Race Free Guarantee. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 22–37. Springer, Heidelberg (2007)
Bacon, D., Bloch, J., Bogda, J., Click, C., Haahr, P., Lea, D., May, T., Maessen, J., Manson, J., Mitchell, J.D., Nilsen, K., Pugh, B., Sirer, E.G.: The “double-checked locking is broken” declaration, http://www.cs.umd.edu/~pugh/java/memoryModel/DoubleCheckedLocking.html
Botinčan, M., Glavan, P., Runje, D.: Verification of Causality Requirements in Java Memory Model Is Undecidable. In: Wyrzykowski, R., Dongarra, J., Karczewski, K., Wasniewski, J. (eds.) PPAM 2009. LNCS, vol. 6068, pp. 62–67. Springer, Heidelberg (2010)
Burckhardt, S., Alur, R., Martin, M.M.K.: Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 489–502. Springer, Heidelberg (2006)
Burckhardt, S., Musuvathi, M.: Effective Program Verification for Relaxed Memory Models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107–120. Springer, Heidelberg (2008)
Burnim, J., Sen, K., Stergiou, C.: Testing concurrent programs on relaxed memory models. In: ISSTA (2011)
Cenciarelli, P., Knapp, A., Sibilio, E.: The Java Memory Model: Operationally, Denotationally, Axiomatically. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 331–346. Springer, Heidelberg (2007)
De, A., Roychoudhury, A., D’Souza, D.: Java Memory Model aware software validation. In: PASTE (2008)
Ferrara, P.: Static analysis via abstract interpretation of the happens-before memory model. In: Proceedings of the 2nd International Conference on Tests and Proofs (2008)
Flanagan, C., Freund, S.N.: Adversarial memory for detecting destructive races. In: PLDI, pp. 244–254 (2010)
Gosling, J., Joy, B., Steele, G., Bracha, G.: Java Language Specification, 3rd edn. Addison Wesley (2005)
Jin, H., Yavuz-Kahveci, T., Sanders, B.A.: Java memory model-aware model checking. Tech. Rep. REP-2011-516, Department of Computer and Information Science, University of Florida (2011), http://www.cise.ufl.edu/tr/REP-2011-516/
Jin, H., Yavuz-Kahveci, T., Sanders, B.A.: Java Path Relaxer: Extending JPF for JMM-aware model checking. In: JPF Workshop 2011 (2011)
JMM causality test cases, http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/testcases.html
Java Pathfinder, http://babelfish.arc.nasa.gov/trac/jpf
Java Racefinder, http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-racefinder
Kim, K., Yavuz-Kahveci, T., Sanders, B.A.: JRF-E: Using model checking to give advice on eliminating memory model-related bugs. In: ASE (2010)
Manson, J., Pugh, W.: The Java Memory Model simulator. In: Workshop on Formal Techniques for Java-like Programs (2002)
Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL 2005 (2005)
Oracle thread analyzer’s user guide, http://download.oracle.com/docs/cd/E18659_01/html/821-2124/gecqt.html
Torlak, E., Vaziri, M., Dolby, J.: MemSAT: checking axiomatic specifications of memory models. In: PLDI (2010)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal 10(2) (April 2003)
Ševčík, J., Aspinall, D.: On Validity of Program Transformations in the Java Memory Model. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 27–51. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jin, H., Yavuz-Kahveci, T., Sanders, B.A. (2012). Java Memory Model-Aware Model Checking. In: Flanagan, C., König, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2012. Lecture Notes in Computer Science, vol 7214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28756-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-28756-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28755-8
Online ISBN: 978-3-642-28756-5
eBook Packages: Computer ScienceComputer Science (R0)