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 programs.
Research partially supported by the HCM project CHRX-CT94-0591 “De Stijl.”
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Martín Abadi and Luca Cardelli. A Theory of Objects. Springer, NewYork, 1996.
Martín Abadi and K. Rustan M. Leino. A Logic of Object-Oriented Programs. In Michel Bidoit and Max Dauchet, editors, Proc. 7 th Int. Conf. Theory and Practice of Software, volume 1214 of Lect. Notes Comp. Sci., pages 682–696, Berlin, 1997. Springer.
Jim Alves-Foss, editor. Formal Syntax and Semantics of Java. Lect. Notes Comp. Sci. Springer, Berlin, 1998. This volume
Ken Arnold and James Gosling. The Java Programming Language. Addison-Wesley, Reading,Mass., 1996.
Egon Börger and Wolfram Schulte. A Programmer Friendly Modular Definition for the Semantics of Java. In Alves-Foss [3]. This volume.
Pietro Cenciarelli, Alexander Knapp, Bernhard Reus, and Martin Wirsing. From Sequential to Multi-threaded Java: An Event-Based Operational Semantics. In Michael Johnson, editor, Proc. 6 th Int. Conf. Algebraic Methodology and Software Technology, volume 1349 of Lect. Notes Comp. Sci., pages 75–90, Berlin, 1997. Springer.
Richard Cohen. The Defensive Java Virtual Machine Specification. Technical report, Computational Logic Inc., 1997. Draft at http://www.cli.com.
Sophia Drossopoulou and Susan Eisenbach. Java is Type Safe — Probably. In Alves-Foss [3]. This volume.
Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. A Programmer’s Reduction Semantics for Classes and Mixins. In Alves-Foss [3]. This volume.
James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, Reading,Mass., 1996.
Yuri Gurevich. Evolving Algebras 1993: Lipari Guide. In Egon Börger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.
Doug Lea. Concurrent Programming in Java. Addison-Wesley, Reading,Mass., 1997.
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, Cambridge, Mass., 1997.
Tobias Nipkow and David von Oheimb. Machine-checking the Java Specification: Proving Type-Saftey. In Alves-Foss [3]. This volume.
Gordon D. Plotkin. A Structural Approach to Operational Semantics (Lecture notes). Technical Report DAIMI FN-19, Aarhus University, 1981 (repr. 1991).
Zhenyu Qian. A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subroutines. In Alves-Foss [3]. This volume.
Bernhard Reus, Alexander Knapp, Pietro Cenciarelli, and Martin Wirsing. Verifying a Compiler Optimization for Multi-threaded Java. In Francesco Parisi Presicce, editor, Sel. Papers 12 th Int. Wsh. Recent Trends in Algebraic Development Techniques, volume 1376 of Lect. Notes Comp. Sci., pages 402–417, Berlin, 1998. Springer.
Raymie Stata and Martín Abadi. A Type System for Java Bytecode Subroutines. In Proc. 25 th ACM Symp. Principles of Programming Languages, 1998. To appear.
David Syme. Proving Java Type Soundness. In Alves-Foss [3]. This volume.
Charles Wallace. The Semantics of the Java Programming Language: Preliminary Version. Technical Report CSE-TR-355-97, University of Michigan, 1997.
Glynn Winskel. An Introduction to Event Structures. In JacobusW. de Bakker, Willem P. de Roever, and Grzegorg Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lect. Notes Comp. Sci., pages 364–397. Springer, Berlin, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M. (1999). An Event-Based Structural Operational Semantics of Multi-threaded Java. In: Alves-Foss, J. (eds) Formal Syntax and Semantics of Java. Lecture Notes in Computer Science, vol 1523. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48737-9_5
Download citation
DOI: https://doi.org/10.1007/3-540-48737-9_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66158-0
Online ISBN: 978-3-540-48737-1
eBook Packages: Springer Book Archive