KIT | KIT-Bibliothek | Impressum | Datenschutz

Animating the Formalised Semantics of a Java-like Language

Lochbihler, Andreas; Bulwahn, Luka

Abstract:

We present a machine-checked formalisation of the Java memory model and connect it to an operational semantics for Java source code and bytecode. This provides the link between sequential semantics and the memory model that has been missing in the literature. Our model extends previous formalisations by dynamic memory allocation, thread spawns and joins, infinite executions, the wait-notify mechanism and thread interruption. We prove the Java data race freedom guarantee for the complete formalisation in a modular way. This work makes the assumptions about the sequential semantics explicit and shows how to discharge them.


Originalveröffentlichung
DOI: 10.1007/978-3-642-22863-6_17
Dimensions
Zitationen: 17
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2011
Sprache Englisch
Identifikator ISBN: 978-3-642-22862-9
KITopen-ID: 1000027293
Erschienen in Interactive theorem proving : Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22 - 25, 2011, proceedings. Ed.: M. Van Eekelen
Verlag Springer-Verlag
Seiten 216-232
Serie Lecture notes in computer science ; 6898
Nachgewiesen in Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page