On Thu, 2008-03-27 at 09:51 -0600, John Regehr wrote:> Hey, you need to be careful with this reasoning or else you'll end up > implementing a whole new language, compiler, and OS. > > Oh wait nevermind :).Don't forget prover. :-) shap
> 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. Once the semantics exists, you can either prove once and for all the that each LLVM->LLVM optimization pass preserves the semantics of the code, or else just do translation validation. Verifying the LLVM->native backends should not be incredibly difficult. Verifying a real LLVM front end would be a big projet but substantial headway is being made on that kind of thing for example by Xavier Leroy's group. I've tried to sell some of the HOL folks on this idea (they have a formal semantics for an ARM ISA, for example) but so far no dice. John Regehr
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
John Regehr wrote:> 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.Except that some aspects of the host platform leak through to .bc files. This may or may not be a problem.> Once the semantics exists, you can either prove once and for all the that > each LLVM->LLVM optimization pass preserves the semantics of the code, or > else just do translation validation.That would be quite nice indeed.> I've tried to sell some of the HOL folks on this idea (they have a formal > semantics for an ARM ISA, for example) but so far no dice.You could sell it to me. How much money do you have? ;-) But seriously, that is something I would very much like to see. One of the reasons why you have not had success may be that with current prover technology, formalizing LLVM semantics and carrying out proofs would be a fairly straightforward exercise, but not a trivial amount of work. Not a good combination in academic sense. On the other hand, formalizing LLVM and proving some properties would make for a very nice open source proof project, which would be an interesting beast. -- Pertti