University of Cambridge > > Computer Laboratory Automated Reasoning Group Lunches > Plan B: A Buffered Memory Model for Java

Plan B: A Buffered Memory Model for Java

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact William Denman.

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

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity