CompCert: A formally verified optimizing C compiler

http://www.absint.com/compcert/

by adamnemecek • 11 years ago

96 62 11 years ago

soup10• 11 years ago

"CompCert typically runs twice as fast as the code generated by GCC without optimizations." Lol, That's like saying you run faster than Usain Bolt when he's walking.

lifthrasiir2• 11 years ago

There are certain applications that fear the breakage due to the compiler optimization. (Compilers are prone to break, for your information. They are really complex applications after all.) CompCert has a fully verified optimization engine comparable to (I guess) GCC's -O2, so that really is an improvement.

pascal_cuoq2• 11 years ago

It doesn't get close to “gcc -O2” (the page says within 20% of “gcc -O3”). It is only the most useful optimizations that are implemented in CompCert, at perhaps an implementation cost of one PhD thesis per optimization pass. But that is still better than no optimizations in contexts where none of the optimizations from an off-the-shelf's compiler could be trusted, as discussed in this thread.

sanxiyn2• 11 years ago

Since GCC optimizations can miscompile, target audience ("safety-critical and mission-critical software written in C and meeting high levels of assurance", aka Airbus) is currently using GCC without optimizations. So it is a fair comparison for that case, since they can now enable proven-correct optimizations.

craftit2• 11 years ago

Interesting they are using it without optimisations. The compilers is used far more with optimisations, so those code paths are actually far better tested. I have heard of cases where bugs only appear in unoptimised code.

pascal_cuoq2• 11 years ago

You are right, but this sentence makes sense in the context for which CompCert is intended.

The requirements of the DO-178 standard for aeronautics, for instance, are such that the choice for compiling safety-critical C code that runs within the aircraft is basically between either:

- the equivalent of “gcc -O0”, that is, an off-the-shelf compiler with no optimization so that source-level constructs can be mapped to assembly constructs and vice versa, or

- CompCert with optimizations, because the soundness of the optimizations can be justified to a level of formality such that it matters less to be able to trace assembly to source.

A source without much detail, but the best I can find within 5 minutes of googling: http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris...

ngrilly8• 11 years ago

This is probably a Philistine question, but how do we make sure the proof -- that CompCert works as intended -- itself is correct? In mathematics and science, it happens all the time that someone finds a mistake in a proof years later after its first publication.

arcatek• 11 years ago

In science it may happen because everything is based on a lot of assumptions, themselves based on our physical perception of the world, which may be proved wrong later in time.

Are mathematics subject to this kind of flaws ? There is a very restricted set of axioms, and almost everything else is based on formal proofs.

Drakim2• 11 years ago

Surely the implementation of the mathematics may be subject to errors, just like any implementation of anything? There is nothing that is so perfect that humans cannot err while applying it.

one-more-minute• 11 years ago

See, for example:

https://en.wikipedia.org/wiki/Wiles%27_proof_of_Fermat%27s_L...

http://rsta.royalsocietypublishing.org/content/roypta/363/18...

sanxiyn2• 11 years ago

While formal proof is not perfect, humanity is not yet aware of methods to achieve higher assurance. It is basically better than anything else we have tried.

more_original4• 11 years ago

The proof is written in Coq, an automatic proof checker.

Of course, Coq itself could have bugs, but it has a small trusted kernel and it produces proof objects that can be checked, so what you get is much, much more reliable than the typical published proof in mathematics.

userbinator• 11 years ago

I think the parent's question might not be asking about whether the proof is correct in the "do all the statements in it logically hold" sense, but more like "is the proof a proof of what a 'correct' compiler should do", i.e. does the translation follow the C standard on one side, and the target machine's ISA on the other? Starting with the wrong assumptions can lead to valid reasoning to the wrong conclusion, and AFAIK Coq only helps with the "valid reasoning".

In other words, if you have the wrong idea of what a compiler is, you can write one and a proof that it is correct. Humans have to be involved at some point to tell the machine what their idea of a correct compiler is. (Even if the machine somehow knows, that would also be a result of humans teaching it at some point in the past.)

Jimmy• 11 years ago

Why would this situation be disanalogous to when we prove anything else in mathematics? There's always a chance that anything we believe (well, almost anything) could be wrong.

If you think that disqualifies any man-made proof from being worthy of the name "proof"... perhaps you would be interested in studying philosophy of mathematics? :)

Tomte• 11 years ago

Although there seem to have been parts of it that hadn't been formally verified:

"Using Csmith, we found previously unknown bugs in unproved parts of CompCert—bugs that cause this compiler to silently produce incorrect code." (http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf)

The CompCert homepage tells us that the same authors did a study in the same year (2011) without finding any wrong-code errors.

But even if they hadn't; I'd still be excited about CompCert demonstrating that this level of verification is indeed possible. Because then verifying the unverified parts would probably be just as feasible, given enough resources.

jbapple2• 11 years ago

The Csmith paper notes two types of errors found in CompCert: front-end errors and a misunderstanding of PPC semantics.

The former type of bug was apparently due to a part of the compiler that wasn't verified at the time. According to the Csmith paper, " This bug and five others like it were in CompCert’s unverified front-end code. Partly in response to these bug reports, the main CompCert developer expanded the verified portion of CompCert to include C’s integer promotions and other tricky implicit casts."

Additionally, the CompCert team produced a validated parser which they discussed in their ESOP 2012 paper, "Validating LR(1) Parsers"

The second type of bug (misunderstanding the semantics of the target architecture) is, as far as I know, impossible to avoid. Any verification project can end up with a true proof of the wrong theorem!

DanWaterworth• 11 years ago

The second type of bug (misunderstanding the semantics of the target architecture) is, as far as I know, impossible to avoid. Any verification project can end up with a true proof of the wrong theorem!

Indeed. However, although it's impossible to avoid, you can still take steps to make it less likely.

When you formally verify code, you are showing that a program has a particular specification.

If you want to eliminate errors in your specification, you should aim to make it as simple as possible, so that people with domain knowledge (in this case, people with a correct understanding of PPC) would be able to tell whether your specification is correct.

nathell• 11 years ago

The fact that Xavier Leroy has been working on CompCert gives it an extra level of credibility for me.

(Xavier Leroy of INRIA is the main author of OCaml, among other things.)

peterfirefly• 11 years ago

And the original Linux threading support.

His report on the Zinc Experiment is well worth reading:

http://gallium.inria.fr/~xleroy/bibrefs/Leroy-ZINC.html

Keyframe2• 11 years ago

Note that it can't be used commercially without a proper license. Also, no 64 bit.

jk4930• 11 years ago

Two thoughts here:

1. If you use it commercially, you can pay for it.

2. In most cases where it's needed, 64 bit doesn't matter.

(Though I might be wrong on the second one.)

Keyframe2• 11 years ago

1. Nobody argued that.

2. What do you mean it doesn't matter? You think embedded and similar systems don't need/use 64-bit space? True for most I guess.

wolfgke• 11 years ago

But if I don't use it commercially, but also not for research, it's not sure, whether I can pay for it.

e12e• 11 years ago

It can't be used for anything other than research for free. So you can't write useful systems and give them away without a license either. (You might of course be able to get a license for free, but it rules out using it as a foundation for a Free embedded kit, like writing something like the Arduino platform. Which is a pity, but quite understandable).

jbapple2• 11 years ago

See also CakeML, "A verified implementation of a significant subset of Standard ML in the HOL4 theorem prover".

https://cakeml.org/

Not that this project, unlike CompCert, is Free Software in the Stallman sense:

https://github.com/CakeML/cakeml/blob/master/COPYING

khaki54• 11 years ago

So is this protected from the "Ken Thompson Hack"? http://c2.com/cgi/wiki?TheKenThompsonHack

I guess it would have to be cross compiled for your system otherwise your existing compiler could corrupt it...

puetzk• 11 years ago

As long as it's also capable of reproducible builds (and I would think the proofs would be very hard if the output is not even predictable!), you should be able to cross-build it from a certified platform, and bootstrap it from a trusted one (or more than one), and the bootstraps should converge to an identical binary, thus giving you both claims.

jerf• 11 years ago

Unless you implement the proved compiler from scratch yourself, no.

If you're not doing massive amounts of implementation yourself, you have not escaped from Ken Thompson's hack. All this does is rephrase how they promise to not hack you... it doesn't change the fact that what they say they do and what they actually do have nothing in particular connecting them.

I wouldn't worry about it until strong AI comes along though. Humans are barely capable of making compilers that work, let alone shipping compromised compilers. (I know Ken demonstrated his hack, but to make something that does that under controlled conditions is one thing, to make one that could be shipped and robustly implement the hack quite another.)

vilhelm_s2• 11 years ago

It's not self-hosted, so it is not yet at the point where the Thompson hack would apply.

That is, CompCert is a C compiler, but it's not written in C, it's written in Coq. So when you use it, you have to trust that the Coq implementation was written correctly, and that nobody has inserted any backdoors in Coq which insert backdoors in Compcert which insert backdoors in your program.

The next level would be to also have a verified Coq compiler, which would make the whole system that much more trustworthy. And at _that_ point you could worry about self-perpetuating backdoors in that compiler, and ways to mitigate them.

more_original4• 11 years ago

Oh, but they're already building a verified Coq compiler: http://www.cs.princeton.edu/~appel/certicoq/

venomsnake• 11 years ago

And who verifies the verify-er? (That is generally the problem I have with the concept of unit tests too)

vilhelm_s2• 11 years ago

Ideally, a simpler and therefore more trustworthy verifier. So far, the most fleshed out implementation of this idea is Milawa, which developed a chain of 11 increasingly sophisticated verifiers, each one checked by the previous.

http://www.cs.utexas.edu/users/jared/milawa/Web/

whitten• 11 years ago

Does anyone know if CompCert can be used to formally verify a commpiler of some other language than C, such as Assembly Language or Python ?

CompCert: A formally verified optimizing C compiler

Related Stories