Re: Compiler Correctness

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)

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