Cenciarelli, Pietro, Knapp, Alexander, Reus, Bernhard and Wirsing, Martin (1999) An event-based structural operational semantics of multi-threaded Java. In: Alves-Foss, Jim (ed.) Formal Syntax and Semantics of Java. Lecture Notes in Computer Science, 1523 . Springer-Verlag, Berlin, Germany, pp. 157-200. ISBN 9783540661580

Postscript Restricted to SRO admin only Download (698kB)

Abstract

A structural operational semantics of a significant sublanguage of Java is presented, including the running and stopping of threads, thread interaction via shared memory, synchronization by monitoring and notification, and sequential control mechanisms such as exception handling and return statements. The operational semantics is parametric in the notion of "event space" [6], which formalizes the rules that threads and memory must obey in their interaction. Different computational models are obtained by modifying the well-formedness conditions on event spaces while leaving the operational rules untouched. In particular, we implement the prescient stores described in [10, §17.8] which allow certain intermediate code optimizations, and prove that such stores do not affect the semantics of properly synchronized program

Item Type:	Book Section
Schools and Departments:	School of Engineering and Informatics > Informatics
Subjects:	Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User:	Chris Keene
Date Deposited:	03 Mar 2008
Last Modified:	24 Sep 2019 13:08
URI:	http://sro.sussex.ac.uk/id/eprint/1437
Google Scholar:	85 Citations

View download statistics for this item

📧 Request an update