Aktionsplan-Informatik: Verifikation und Optimierung bei der Übersetzung höherer Programmiersprachen

点击翻译按钮获取中文摘要

Das Ziel des hier vorgestellten Forschungsprojekts ist die Entwicklung einer Methodik zur korrekten und optimierenden Codeerzeugung für neueste Formen von Prozessorarchitekturen. Übersetzer (Compiler) sind das Herzstück bei der Erstellung von Software, erlauben sie es doch, Programme in höheren Programmiersprachen zu schreiben, die dann mit Hilfe von Übersetzern in Maschinencode transformiert werden. Um zuverlässige Software zu erstellen, ist es daher unbedingt erforderlich, dass Übersetzer nachweislich korrekt arbeiten. Außerdem müssen Übersetzer die Architekturen moderner Hardwarestrukturen ausnutzen und darauf optimierten Maschinencode erzeugen, damit auch die Effizienz des erzeugten Maschinencodes gewährleistet ist. In unserer Arbeit wollen wir uns auf Prozessoren mit folgenden Merkmalen konzentrieren: Prozessoren mit sehr langen Instruktionswörtern (very long instruction words, VLIW), mit bedingten (predicated) Instruktionen und mit spekulativer Ausführung. Dabei wollen wir insbesondere untersuchen, wie wir optimierende, maschinenabhängige Transformationen mittels Graphersetzungsmethoden ausdrücken können. Des weiteren wollen wir klären, wie solche Transformationen mit Isabelle/HOL formal verifiziert werden können und wie wir mit Programmprüfung ihre korrekte Implementierung sicherstellen können.