On Thu, 2008-03-27 at 12:10 -0600, John Regehr wrote:> > Don't forget prover. :-) > > Say on that note here's something that I want to see: a formal semantics > for LLVM in for example higher order logic. This would probably not be > that difficult. > > The problem that this solves is that current verified compiler efforts > appear to be highly specific to both the language and the target.Hmm. Maintaining this would impose a significant burden of long-term stability on LLVM. From the rate of change that I see, I suspect that Chris may not be ready to firm things up quite that much just yet. Also, I think that a verified compiler is not the right goal. I think that what we want is a verifying compiler. We are not interested in whether the compiler is correct in any general sense. We are interested in whether the transformations performed by the compiler during some particular compilation are correct. That may be much easier to achieve, but I am not convinced that the LLVM team should adopt it as a goal. Their objectives are already complex enough. shap
> Also, I think that a verified compiler is not the right goal. I think > that what we want is a verifying compiler. We are not interested in > whether the compiler is correct in any general sense. We are interested > in whether the transformations performed by the compiler during some > particular compilation are correct.My intuition is the same: translation validation sounds far easier than compiler verification. On the other hand general-purpose translation validation does not exist (that I know of) whereas the compiler verification people are making genuine steps forward: http://pauillac.inria.fr/~xleroy/publi-by-topic.html#compcert> That may be much easier to achieve, but I am not convinced that the LLVM > team should adopt it as a goal. Their objectives are already complex > enough.I agree, I was thinking of this as a separate project based on a fork of LLVM. If it happened to be wildly successful, some aspects could be folded back in. John
On Thu, 2008-03-27 at 14:20 -0600, John Regehr wrote:> My intuition is the same: translation validation sounds far easier than > compiler verification. On the other hand general-purpose translation > validation does not exist (that I know of) whereas the compiler > verification people are making genuine steps forward.Very interesting. Thanks for that pointer. It is surprising that one problem is not a subset of the other. One issue I did not mention: even if one decides only to emit a proof for the transformation of the code that is emitted, one must still verify the correctness of the IR reader (if applicable) and the code emitter. A verified transformation of a low-confidence input would still be a step forward, but the break in the confidence chain at the parser is significant. shap