Re: How to verify that optimizations preserve semantics

Stephan Ceram wrote:
> I was wondering how compiler optimisations can be verified,
> i.e. whether they perform always valid code modifications? How is it
> done in practice?
>
> I assume that the only safe way would be to formulate the applied code
> modifications as formal transformations that model every possible
> situation that can ever occur. But on the other hand this seems to be
> infeasible for most optimisations since they are too complex for
> analytical models.


There has been some work[1,2] in using declarative techniques (logic
programming) and automatic theorem proving for generating optimal code
sequences -- these approaches require demonstrating functional
equivalence of code sequences, so could potentially be extended to
verify compiler optimisation algorithms.


However, as you mention, doing so can be computationally expensive but
some of the modern solving/theorem proving techniques make this problem
tractable.


Regards,


Tom




[1]
"Denali: A Practical Algorithm for Generating Optimal Code"
Joshi et al.
ACM Transactions on Programming Languages and Systems
Volume 28 Issue 6, 2006
http://doi.acm.org/10.1145/1186632.1186633




[2]
"Generating Optimal Code Using Answer Set Programming"
Crick et al.
Proceedings of the 10th International Conference on Logic Programming
and Nonmonotonic Reasoning (LPNMR 2009)
LNCS 5735, 2009
http://dx.doi.org/10.1007/978-3-642-04238-6_57

Return to the comp.compilers page.
Search the comp.compilers archives again.