TY - GEN
T1 - On Validity of Program Transformations in the Java Memory Model
AU - Sevcik, Jaroslav
AU - Aspinall, David
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=49049109657&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-70592-5_3
DO - 10.1007/978-3-540-70592-5_3
M3 - Conference contribution
SN - 978-3-540-70591-8
T3 - Lecture Notes in Computer Science
SP - 27
EP - 51
BT - ECOOP 2008 — Object-Oriented Programming
A2 - Vitek, Jan
PB - Springer
ER -