11 Feb 2006 13:15:22 -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) |

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

[9 later articles] |

From: | "Daniel C. Wang" <danwang74@gmail.com> |

Newsgroups: | comp.compilers |

Date: | 11 Feb 2006 13:15:22 -0500 |

Organization: | Compilers Central |

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

Keywords: | theory, debug |

Posted-Date: | 11 Feb 2006 13:15:22 EST |

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

Andrew Appel, has been doing related work in this area. He also gives a

talk where he explains point by point why Perlis was off the mark.

Unfortunately, I can't find a pointer to it now. The FPCC project tries

to establish the type-safety of SPARC machine code from a minimal TCB.

Some interesting facts that come from the FPCC project are.

A minimal proof verifier is 1-2 thousand lines of C code. This proof

verifier uses no library calls. It's designed so you can compile it to

assembly and can eyeball the output of the compiler. The basic logic

has around 10 axioms from which all of modern mathematics can be

derived. Then there is a 4000 line partial specification of the SPARC

machine semantics.

Proofs of compiler correctness are more involved. However, a minimal

proof verifier I suspect would be on order of Appel's verifier. The

statement of the theorem needs to include the machine semantics so

let's say another 4000 lines specification, plus the semantics for the

C subset. I'll guess this also is on the order of 2000 lines.

I'd say there is under 10 thousands lines of stuff you have to eye ball

very carefully, before you trust the result and believe the proof is true.

One problem with the POPL06 result is that their correctness result only

applies to program that are known to terminate. This is a flaw in the

way their semantics is set up.

In any case. It's been demonstrated that simple proof verifiers can be

written in about 2000 lines of C. To trust any machine checked proof is

simply a matter of encoding a known sound logic, encoding the statement

of your theorem in that logic and then generating the proof to be checked.

For compiler correctness the statement of the theorem is relatively

complex. You need a semantics for the source and target languages. A

good deal of the challenge in a compiler correctness proof is the

statement of the theorem.

Dan (former student of Andrew W. Appel)

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.