EVA STAR Trefferanzeige

Volltext 2011,34_pdfa.pdf1.pdf (755 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-254682
Titel A Unified, Machine-Checked Formalisation of Java and the Java Memory Model
Autor Lochbihler, Andreas
Institution Fakultät für Informatik (INFORMATIK)
Institut für Programmstrukturen und Datenorganisation (IPD)
Dokumenttyp Buch
Verlag Karlsruhe
Jahr 2011
Serie Karlsruhe Reports in Informatics (früher: Interner Bericht. Fakultät für Informatik, Karlsruher Institut für Technologie) ; 2011,34
ISSN: 2190-4782
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.