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)