|
|
|
| | |
|
gefördert von der DFG im Rahmen des Emmy Noether-Programms Verifikation und Optimierung bei der Übersetzung höherer Programmiersprachen
Das Gesamtziel des 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
diesem Projekt konzentrieren wir uns auf Prozessoren mit folgenden
Merkmalen: Prozessoren mit sehr langen Instruktionswörtern (very long
instruction words, VLIW), mit bedingten (predicated) Instruktionen und
mit spekulativer Ausführung. Dabei soll insbesondere untersucht
werden, wie optimierende, maschinenabhängige Transformationen mittels
Graphersetzungsmethoden ausgedrückt werden können. Des weiteren soll
geklärt werden, wie solche Transformationen mit Isabelle/HOL formal
verifiziert werden können und wie ihre korrekte Implementierung mit
Programmprüfung sichergestellt werden kann.Projektbeteiligte
| | | |
