Re: Compiler Correctness

Sometimes, even large proofs contain some holes :-)


Here is a possible example with Xavier Leroy's certified compiler that
shows that it is very hard to really provide a full proof, even for
simple optimizing compilers.


I didn't read its last POPL article yet, but I remembered one of his
talks about this subject (certifying a simple compiler). At that time, I
noticed the following hole in their proof.


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.


For this case, constant propagation cannot be stated as formally correct
unless you prove that the semantics of computation of these two distinct
machines are equivalent. This has not been done at the time of the talk
(maybe they did it after that time, but I am not sure).


As example, suppose that the compiler executes on a 32 bits machine and
    generates a code for a 64 bits machine. If the compiler makes static
constant propagation, it makes arithmetic computation on the 32 bit
machine. This would not give you the same result if you generate the
code on the 64 bits machines.


We can imagine more complex cases with floating point computations...


S

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