Improving the Java memory model using CRF

We describe an alternative memory semantics for Java programs using an enriched version of the Commit/Reconcile/Fence (CRF) memory model [SAR99]. We need to enrich CRF with semantics for Java's monitor-style locking, and with an instruction to mark cached data which will never change so that we can give semantics for nal slots. With these enrichments, we give an instruction-by-instruction translation of Java memory operations into CRF operations. The resulting Java memory semantics allow anumber of optimizations such as load reordering that are currently prohibited. Using the translation, we develop a simple thread-local algebraic semantics for Java so that optimizations can be expressed at the source or bytecode level. Finally, we show how the given semantics can be applied to give a simple dependency analysis algorithm for Java.