LFCS Theory Seminar,
Room 2511, JCMB, King's Buildings
1.30pm, Monday 10th November 1997

(* NOTE NONSTANDARD DAY AND TIME *)

Title: From sequential to multi-threaded Java: An event-based operational semantics

Speaker: Martin Wirsing (University of Munich)

Java is a new object-oriented programming language. Among other things Java offers simple and tightly integrated support for concurrent programming by threads. A concurrent program consists of multiple tasks that are or behave as if they are executed all at one time. In Java tasks are implemented using threads (short for "threads of control"), sequences of instructions that run independently within the encompassing program. In this talk a structural operational semantics of the concurrency aspects of Java is presented. First we introduce a simple operational description of the sequential part of the language, where the memory is treated as an algebra with suitably axiomatised operations. Then, the interaction between threads via a shared memory is described in terms of structures, called ``event spaces,'' whose well-formedness conditions formalise directly the rules given in the Java language specification. Event spaces are included in the operational judgements to develop the semantics of the full language, which is shown to extend the one for sequential Java conservatively. By changing the well-formedness conditions, while leaving the operational rules untouched, one can enforce different language implementations.

In cooperation with Pietro Cenciarelli, Alexander Knapp, Bernhard Reus:

Institut f"ur Informatik, Ludwig-Maximilians-Universit"at M"unchen, Oettingenstr. 67, D-80538 M"unchen, Germany Email: {wirsing, cenciare, knapp, reus}@informatik.uni-muenchen.de