KIT | KIT-Bibliothek | Impressum
DOI: 10.1007/978-3-642-19861-8_4

SSA-Based Register Allocation with PBQP

Buchwald, Sebastian; Zwinkau, Andreas; Bersch, Thomas

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.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Jahr 2011
Sprache Englisch
Identifikator ISBN: 978-3-642-19861-8
KITopen ID: 1000027295
Erschienen in Compiler construction : 20th International Conference, CC 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April 3, 2011; Proceedings. Ed.: J. Knoop
Verlag Springer, Berlin
Seiten 42-61
Serie Lecture notes in computer science ; 6601
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page