11 Feb 2006 13:04:03 -0500

Related articles |
---|

Compiler Correctness Pramod.Patangay@gmail.com (pramod) (2006-02-07) |

Re: Compiler Correctness find@my.address.elsewhere (Matthias Blume) (2006-02-07) |

Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-07) |

Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-07) |

Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-11) |

Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-11) |

Re: Compiler Correctness torbenm@app-1.diku.dk (2006-02-11) |

Re: Compiler Correctness henry@spsystems.net (2006-02-11) |

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) |

[10 later articles] |

From: | Neelakantan Krishnaswami <neelk@cs.cmu.edu> |

Newsgroups: | comp.compilers |

Date: | 11 Feb 2006 13:04:03 -0500 |

Organization: | Carnegie Mellon Univ. -- Computer Science Dept. |

References: | 06-02-053 06-02-061 |

Keywords: | theory, debug |

Neelakantan Krishnaswami wrote:

*>> I have a simple question. Can we prove that a compiler is correct? I*

*>> mean we are given a language with it's syntax and semantics and a*

*>> compiler whose correctness needs to be proved. Is this theoretically*

*>> possible?*

*>*

*> Yes, it is. In the POPL 2006 conference proceedings, Xavier Leroy*

*> reported on his efforts implementing a provably-correct compiler for a*

*> subset of C.*

*>*

*> The proof is extremely large, however, and in order to ensure the*

*> proof's correctness he had to develop the compiler in a theorem*

*> proving system that verified the correctness of all his proofs.*

*>*

*> "Formal certification of a compiler back-end, or: programming a*

*> compiler with a proof assistant"*

*>*

*> <http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf>*

*>*

*> [Interesting paper. I wonder how likely it is that the tools, which*

*> are not small, or the set of axioms have bugs that could affect the*

*> validity of the proof. If it sounds like I'm channelling the famous*

*> 1979 proof paper by Perlis et al, it's not surprising since he was my*

*> thesis advisor. -John]*

A lot of the design of these tools has been shaped in specific

response to Perlis's paper.

Basically, the idea is that a theorem prover is inherently

untrustworthy. It's large, complex, and relies on very advanced math

for its correct operation -- it will have bugs with basically 100%

certainty.

So what these programs do is construct the actual proof of the theorem

as a data structure which you can print out. Then, you can write a

proof *checker* to verify the operations that the theorem prover has

carried out.

A proof checker is much smaller than the theorem prover; usually they

are a few hundred lines of code. Thus, they are small enough that

Perlis's criticisms don't apply to them -- the checkers are programs

that people can manually verify and easily write multiple competing

implementations to increase trust.

So, the process is:

1. You develop your proof interactively with the prover.

2. You dump out the proof and run your proof checkers on it.

3. If it says your proof is good, then you're done.

4. If it says your proof is bad, then you curse, and fix the

bug in the theorem prover and redo your proof.

Interestingly, this is a technique that Leroy used in his compiler.

For example, the register allocator would find a coloring, and then

he'd run a checker on it to ensure that it was okay before proceeding.

If the check failed, then his compiler would report that it failed to

compile that program rather than emitting incorrect code.

IIRC, the logic in Coq is equivalent to ZFC with countably many

inaccessible cardinals. That's a very rich foundation, but still

pretty conventional.

--

Neel Krishnaswami

neelk@cs.cmu.edu

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.