Thu, 13 May 2010 19:00:54 +0100

Related articles |
---|

How to verify that optimizations preserve semantics linuxkaffee_@_gmx.net (Stephan Ceram) (2010-05-11) |

Re: How to verify that optimizations preserve semantics bfranke@inf.ed.ac.uk (=?ISO-8859-1?Q?Bj=F6rn_Franke?=) (2010-05-12) |

Re: How to verify that optimizations preserve semantics monnier@iro.umontreal.ca (Stefan Monnier) (2010-05-12) |

Re: How to verify that optimizations preserve semantics jeremy.wright@microfocus.com (Jeremy Wright) (2010-05-13) |

Re: How to verify that optimizations preserve semantics tc@cs.bath.ac.uk (Tom Crick) (2010-05-13) |

Re: How to verify that optimizations preserve semantics walter@bytecraft.com (Walter Banks) (2010-05-14) |

Re: How to verify that optimizations preserve semantics cr88192@hotmail.com (BGB / cr88192) (2010-05-14) |

From: | Tom Crick <tc@cs.bath.ac.uk> |

Newsgroups: | comp.compilers |

Date: | Thu, 13 May 2010 19:00:54 +0100 |

Organization: | University of Bath |

References: | 10-05-062 |

Keywords: | optimize, bibliography |

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

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

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.