Re: How to verify that optimizations preserve semantics

=?ISO-8859-1?Q?Bj=F6rn_Franke?= <bfranke@inf.ed.ac.uk>
Wed, 12 May 2010 11:39:13 +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: =?ISO-8859-1?Q?Bj=F6rn_Franke?= <bfranke@inf.ed.ac.uk>
Newsgroups: comp.compilers
Date: Wed, 12 May 2010 11:39:13 +0100
Organization: Edinburgh University
References: 10-05-062
Keywords: optimize
Posted-Date: 12 May 2010 17:11:45 EDT

Stephan,


> I was wondering how compiler optimisations can be verified,
> i.e. whether they perform always valid code modifications? How is it
> done in practice?


Do you want an academic or realistic answer? ;-)


In theory, you can use model checking to prove equivalence between a
high-level specification of an optimisation and its implementation. This
is tricky and, so far, has only been done for a few "real"
optimisations. For simplified languages and compilers you can also try
proving equivalence of the source code of your application and the
generated machine code.


In practice, you use regression testing against a test suite such as
SuperTest or similar. If your compiler passes the regression test you
assume it's probably ok and release it. If your customers discover more
bugs you'd try to come up with the smallest possible test case that
still exhibits this bug, fix it in your compiler and include the test
case in your regression suite for future tests.


Cheers,


        Bjoern



Post a followup to this message

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