|[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.