|How to verify that optimizations preserve semantics linuxkaffee_@_gmx.net (Stephan Ceram) (2010-05-11)|
|Re: How to verify that optimizations preserve semantics email@example.com (=?ISO-8859-1?Q?Bj=F6rn_Franke?=) (2010-05-12)|
|Re: How to verify that optimizations preserve semantics firstname.lastname@example.org (Stefan Monnier) (2010-05-12)|
|Re: How to verify that optimizations preserve semantics email@example.com (Jeremy Wright) (2010-05-13)|
|Re: How to verify that optimizations preserve semantics firstname.lastname@example.org (Tom Crick) (2010-05-13)|
|Re: How to verify that optimizations preserve semantics email@example.com (Walter Banks) (2010-05-14)|
|Re: How to verify that optimizations preserve semantics firstname.lastname@example.org (BGB / cr88192) (2010-05-14)|
|From:||Tom Crick <email@example.com>|
|Date:||Thu, 13 May 2010 19:00:54 +0100|
|Organization:||University of Bath|
|Posted-Date:||14 May 2010 10:24:53 EDT|
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
"Denali: A Practical Algorithm for Generating Optimal Code"
Joshi et al.
ACM Transactions on Programming Languages and Systems
Volume 28 Issue 6, 2006
"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
Return to the
Search the comp.compilers archives again.