|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)|
|Date:||Wed, 12 May 2010 11:39:13 +0100|
|Posted-Date:||12 May 2010 17:11:45 EDT|
> 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.
Return to the
Search the comp.compilers archives again.