Textdokument
Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler
Lade...
Volltext URI
Dokumententyp
Dateien
Zusatzinformation
Datum
2013
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik
Zusammenfassung
Charakteristisch für die Programmiersprache Java sind sowohl ihre Sicherheitsgarantien wie beispielsweise Typsicherheit und die Sicherheitsarchitektur als auch die direkte Unterstützung von Threads. In der hier vorgestellten Dissertation [Loc12b] wird ein maschinengeprüftes Modell von nebenläufigem Java einschließlich des Java-Speichermodells entwickelt und die Auswirkungen der Nebenläufigkeit auf diese Garantien untersucht. Aus dem formalen Modell wurde automatisch ein ausführbarer Interpreter, Übersetzer und eine virtuelle Maschine einschließlich eines Bytecode-Verifizierers generiert, mit dem das Modell empirisch gegen Java-Benchmarks validiert wurde.