Re: Compiler Correctness

Sid Touati <Sid.Touati@inria.fr> writes:


> 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. [...]
> 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.


There is no hole of that kind in my compiler proof. The compiler
implements its own 32-bit integer arithmetic, as Coq functions that
are proved to satisfy all the arithmetic and logic properties that the
compiler optimizations rely on (associativity, distributivity,
multiplication by power of 2 is a left shift, etc). This arithmetic
is completely independent of that of the processor executing the
compiler.


These arithmetic operations are used both during compilation (e.g. the
constant propagation phase you mention) and in the formal semantics
for the target processor. That's what ensures that constant
propagation preserves semantics. If const.prop. were to use a
different arithmetic than the target processor, Coq would of course
reject the proof.


Now, you can have doubts that the arithmetic used by the compiler
matches that implemented by the target compiler. This comes back to
the issue raised by other posters in this thread, namely that the
formal semantics for the source language and the target processors
have not been formally proved correct, but only validated informally
by careful reading and by testing. (This is still much easier than
validating a whole compiler using these informal approaches.)


Formal validation of the semantics is possible, e.g. for the target
processor by relating it to the formal models used by processor
manufacturers to verify their chips. Unfortunately, such formal
models of hardware are generally trade secrets, so this is beyond the
scope of my compiler certification project.


- Xavier Leroy


--
Valid e-mail address (without the underscores): Xavier.Leroy@i_n_r_i_a.f_r
Home page: http://pauillac.inria.fr/~xleroy/

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