Verifying a compiler optimization for multi-threaded java

Abstract

The specification for the object-oriented concurrent language Java [3] is rather loose with respect to the interaction of shared memory and the local working memories of different threads. This allows maximal freedom in the language implementation. Such freedom is reflected in the semantics provided in [2], where threads-memory interaction is formalized in terms of structures called event spaces. Two kinds of memories are described in the Java specification: a “normal” memory and a more liberal one, where values can sometimes be stored even before they are produced as results of computation. Here we compare two structural operational semantics of a sublanguage of Java modelling the two types of memory. The two semantics share the same set of operational rules but put different requirements (expressed as first order theories) on the notion of event space. We prove a result which is informally stated in [3]: the two semantics coincide for properly synchronized programs. This shows the applicability of a new technique for combining structural operational semantics and first order specification of process behaviour.