Abstract
We analyse the validity of several common program transformations in multi-threaded Java, as defined by the Memory Model section of the Java Language Specification. The main design goal of the Java Memory Model (JMM) was to allow as many optimisations as possible. However, we find that commonly used optimisations, such as common subexpression elimination, can introduce new behaviours and so are invalid for Java. In this paper, we describe several kinds of transformations and explain the problems with a number of counterexamples. More positively, we also examine some valid transformations, and prove their validity. Our study contributes to the understanding of the JMM, and has the practical impact of revealing some cases where the Sun Hotspot JVM does not comply with the Java Memory Model.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Adve, S.: The SC- memory model for Java (2004), http://www.cs.uiuc.edu/~sadve/jmm
Adve, S.V., Aggarwal, J.K.: A unified formalization of four shared-memory models. IEEE Trans. Parallel Distrib. Syst. 4(6), 613–624 (1993)
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer 29(12), 66–76 (1996)
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: principles, techniques, and tools. Addison-Wesley Longman Publishing Co., Inc, Boston (1986)
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)
Aspinall, D., Ševčík, J.: Java memory model examples: Good, bad and ugly. Technical Report EDI-INF-RR-1121, School of Informatics, University of Edinburgh (2007)
Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1-3), 227–270 (2007)
Brookes, S.D.: Full abstraction for a shared variable parallel language. In: LICS, pp. 98–109. IEEE Computer Society, Los Alamitos (1993)
Cenciarelli, P., Knapp, A., Sibilio, E.: The Java memory model: Operationally, denotationally, axiomatically. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421. Springer, Heidelberg (2007)
Click, C.: Global code motion/global value numbering. SIGPLAN Not. 30(6), 246–257 (1995)
Gosling, J., Joy, B., Steele, G., Bracha, G.: Java(TM) Language Specification. In: Threads and Locks, 3rd edn. Java Series, pp. 557–573. Addison-Wesley Professional, Reading (2005)
Intel. A formal specification of Intel Itanium processor family memory ordering (2002), http://www.intel.com/design/itanium/downloads/251429.htm
Intel. Intel 64 architecture memory ordering white paper (2007), http://www.intel.com/products/processor/manuals/318147.pdf
Jeffrey, A., Rathke, J.: A fully abstract may testing semantics for concurrent objects. Theor. Comput. Sci. 338(1-3), 17–63 (2005)
Kennedy, K., Allen, J.R.: Optimizing compilers for modern architectures: a dependence-based approach. Morgan Kaufmann Publishers Inc., San Francisco (2002)
Maessen, J.-W., Shen, X.: Improving the Java memory model using CRF. In: OOPSLA, pp. 1–12. ACM Press, New York (2000)
Manson, J.: The Java memory model. PhD thesis, University of Maryland, College Park (2004)
Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 378–391. ACM Press, New York (2005)
Paleczny, M., Vick, C., Click, C.: The Java Hotspot(TM) server compiler. In: USENIX Java(TM) Virtual Machine Research and Technology Symposium (April 2001)
Pugh, W.: The Java memory model is fatally flawed. Concurrency - Practice and Experience 12(6), 445–455 (2000)
Pugh, W., Manson, J.: Java memory model causality test cases (2004), http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html
Reynolds, J.C.: Toward a grainless semantics for shared-variable concurrency. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 35–48. Springer, Heidelberg (2004)
Saraswat, V., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: ACM 2007 SIGPLAN Conference on Principles and Practice of Parallel Computing. ACM Press, New York (2007)
Sparc International. Sparc architecture manual, version 9 (2000), http://developers.sun.com/solaris/articles/sparcv9.html
Ševčík, J.: The Sun Hotspot JVM does not conform with the Java memory model. Technical Report EDI-INF-RR-1252, School of Informatics, University of Edinburgh (2008)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ševčík, J., Aspinall, D. (2008). On Validity of Program Transformations in the Java Memory Model. In: Vitek, J. (eds) ECOOP 2008 – Object-Oriented Programming. ECOOP 2008. Lecture Notes in Computer Science, vol 5142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70592-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-70592-5_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70591-8
Online ISBN: 978-3-540-70592-5
eBook Packages: Computer ScienceComputer Science (R0)