Re: Compiler Correctness

Marco van de Voort <marcov@stack.nl>
14 Feb 2006 10:21:05 -0500

          From comp.compilers

Related articles
[8 earlier articles]
Re: Compiler Correctness Sid.Touati@inria.fr (Sid Touati) (2006-02-11)
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
Re: Compiler Correctness henry@spsystems.net (2006-02-11)
Re: Compiler Correctness Xavier.Leroy@inria.fr (Xavier Leroy) (2006-02-12)
Re: Compiler Correctness DrDiettrich@compuserve.de (Hans-Peter Diettrich) (2006-02-14)
Re: Compiler Correctness marcov@stack.nl (Marco van de Voort) (2006-02-14)
Re: Compiler Correctness DrDiettrich@compuserve.de (Hans-Peter Diettrich) (2006-02-14)
Re: Compiler Correctness henry@spsystems.net (2006-02-17)
Re: Compiler Correctness henry@spsystems.net (2006-02-17)
Re: Compiler Correctness Sid.Touati@inria.fr (Sid Touati) (2006-02-17)
Re: Compiler Correctness gah@ugcs.caltech.edu (glen herrmannsfeldt) (2006-02-17)
Re: Compiler Correctness ingo.stuermer@gmx.de (=?iso-8859-1?Q?Ingo_St=FCrmer?=) (2006-04-27)
| List of all articles for this month |

From: Marco van de Voort <marcov@stack.nl>
Newsgroups: comp.compilers
Date: 14 Feb 2006 10:21:05 -0500
Organization: Stack Usenet News Service
References: 06-02-053 06-02-061 06-02-078
Keywords: arithmetic, theory

On 2006-02-11, Sid Touati <Sid.Touati@inria.fr> wrote:
> As explained by the author, an algorithm of constant propagation has
> been formally proved. That is, if you have the following program :
>
> y = 5 * 10
>
> then constant propagation may replace this instruction by y = 50 for
> instance. Generally, the compiler may statically compute some arithmetic
> operations if the operands are known constants. This is an usual
> optimization that avoids generating the code that will make the
> computation at execution time if we can do it at compile time. Such code
> optimization has been proved correct by coq, but an informal assumption
> has been forgotten. Indeed, the machine executing the compiler may be
> distinct from the machine executing the final generated code. This is
> the case of cross compilers for example.


I'm not so deep into the matter, but since each deviating path between
compiler and verification tool could lead to differences, I'd say that
FPU operations are also a can of worms. This e.g. due to additional
precision in, at least x86, CPUs and the related rounding when saving
to mem, the outcome of FPU operations is also dependant on the path.


So result:=x*y*z is different from a1:=x*y result:=a1*z (if a1 is a memory
location)


This could probably be remedied with a tolerance (but even those could trip
in case of badly conditioned problems?)


[...]
> We can imagine more complex cases with floating point computations...


(Hmm, seen to late that you already mentioned it)


Post a followup to this message

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