Re: How to verify that optimizations preserve semantics

"Jeremy Wright" <jeremy.wright@microfocus.com>
Thu, 13 May 2010 10:22:22 +0100

          From comp.compilers

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)
| List of all articles for this month |

From: "Jeremy Wright" <jeremy.wright@microfocus.com>
Newsgroups: comp.compilers
Date: Thu, 13 May 2010 10:22:22 +0100
Organization: Compilers Central
References: 10-05-062
Keywords: optimize
Posted-Date: 13 May 2010 13:02:34 EDT

At CC 2004, in Mary Lou Soffa's invited talk, she called for a better
theoretical understanding and underpinning of optimizations and
optimization implementations, rather than yet another register
allocator.


Prof. Soffa observed (I summarise) that in general we cannot formally
show that optimization actually improve code, that the optimization is
sound, and that the implementation of the optimization is sound.


Has the situation improved since then?


See also this from Mary Lou Soffa's homepage -
http://www.cs.virginia.edu/~soffa/research/Comp/zhao-cameraready.pdf


Jeremy Wright


"Stephan Ceram" <linuxkaffee_@_gmx.net> wrote in message
> I was wondering how compiler optimisations can be verified,
> i.e. whether they perform always valid code modifications? How is it
> done in practice?


Post a followup to this message

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