Abstract

The Java Memory Model (JMM) is an ambitious attempt to provide a semantics for concurrent and, possibly, racy Java programs. It aims to provide a precise semantics that is portable across architectures and enables a variety of compiler optimizations. Unfortunately, the JMM has proven to be challenging for users to understand and for compiler writers to use. In fact, the formal statement of the model is flawed and existing Java compilers do not comply with it. We propose to investigate an alternative proposal that has a tractable definition and intuitive semantics, relates easily to existing architectures, and while still enabling useful optimizations. To this end, we introduce a Buffered Memory Model for Java. Beyond its simplicity advantages for the programmer, the model is also amenable for formal reasoning and verification.

Joint work with D. Demange, V. Laporte, L. Zhao, S. Jagannathan and J. Vitek