Universität Karlsruhe
On the Construction of Correct Compiler Back-Ends: An ASM Approach


[Zimmer-Gaul:97]Thilo Gaul, Wolf Zimmermann, On the Construction of Correct Compiler Back-Ends: An ASM Approach, Journal of Universal Computer Science (JUCS) 3(5), p. 504-567, Aug 1997.


Existing works on the construction of correct compilers have at least one of the following drawbacks: (i) correct compilers do not compile into machine code of existing processors. Instead they compile into programs of an abstract machine which ignores limitations and properties of real-life processors. (ii) the code generated by correct compilers is orders of magnitudes slower than the code generated by unverified compilers. (iii) the considered source language is much less complex than real-life programming languages. This paper focuses on the construction of correct compiler back-ends which generate machine-code for real-life processors from realistic intermediate languages. Our main results are the following: (i) We present a proof approach based on abstract state machines for bottom-up rewriting system specifications (BURS) for back-end generators. A significant part of this proof can be parametrized with the intermediate and machine language. (ii) The performance of the code constructed by our approach is in the same order of magnitude as the code generated by non-optimizing unverified C-compilers.

[Erzeuge bibTeX Eintrag]


Prof. Wolf Zimmermann
Dr. Thilo Gaul