Date: Wed 12 Nov
Time: 15.00
Place: room 214

Speaker: Dr. Pietro Cenciarelli (Institut fuer Informatik, Ludwig-Maximilians-Universitaet, Muenchen)
Title: From Sequential to Multi-Threaded Java: an Event-Based Operational Semantics
Reference: Eugenio Moggi

Abstract. A structural operational semantics of a non trivial sublanguage of Java is presented. This language includes dynamic creation of objects, blocks, and synchronization of threads. First we introduce a simple operational description of the sequential part of the language, where the memory is treated as an algebra with suitably axiomatized operations. Then, the interaction between threads via a shared memory is described in terms of structures called ``event spaces,'' whose well-formedness conditions formalize directly the rules given in the Java language specification. Event spaces are included in the operational judgements to develop the semantics of the full multi-threaded sublanguage, which is shown to extend the one for sequential Java conservatively. The result allows sequential programs to be reasoned about in a simplified computational framework without loss of generality.

(joint work with: Alexander Knapp, Bernhard Reus and Martin Wirsing)