Software mechanics for Java multi-threading

Abstract

For a subset JavaTck (Java Thread Composition Kernel) of Java an empirical semantics has been developed. Special emphasis is put on the role of synchronization features. The validity of empirical semantics is discussed in the light of a number of compiler postulates. A translation of process algebra with conditions and free merge to Java is used as an example.