Hacker News Reader

Comment by soup10 | Hacker News Reader

"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.

View on HN

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

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.

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.

I don't think this is really true. Generally all optimization passes are run upon the unoptimized version, hence ALL code paths first pass through the -O0 machinery.

Besides, they seem to manually inspect the assembly output themselves for the final production build.

But the code path is first pass + optimisation gives correct code. That doesn't guarantee the first pass generates correct code. I believe there were bugs along those lines at one stage, though I admit they are rare. I've not had to track down a compiler bug in quite a few years.

It is not because those code paths are better tested, it is because people's code is not actually quite correct. eg something declared cost is not const unless the compiler evaluates it at compile time.

That may be true as long as you use the same compiler versions as the developer used when writing/testing their code. But then someone decides to deploy that code on an (old and) stable version of Linux with old(er) GCC version and things break.

For example ClamAV used to break quite often when built with older compiler versions, in the end we had to add runtime tests to configure based on testcases from the GCC bugzilla to make sure people are not using a "stable" and broken compiler. GCC 4.1.0 and 4.1.1 were particularly bad versions

http://gcc.gnu.org/bugzilla/show_bug.cgi?id=27603 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=26763 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=28045 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=37573 https://bugzilla.clamav.net/show_bug.cgi?id=670

You might think that you could still use -O2 and selectively turn off optimizations that are known to cause trouble (i.e. -fno-strict-aliasing), but there are cases where turning off that optimization exposes bugs in other optimization passes and a compiler that would be otherwise good at -O2 would break at "-O2 -fno-strict-aliasing": https://bugs.gentoo.org/show_bug.cgi?id=275928#c29 https://bugzilla.clamav.net/show_bug.cgi?id=1581

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.

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.

Yeah, -O2 was my wild guess and in the reality the figure may vary a lot. I think that it is quite great anyway.

http://www.irisa.fr/celtique/ext/compcertSSA/ may bring in a whole bunch of optimisations nearly for free. We'll see...

There is on-going research on more modular frameworks that allow for faster implementation of optimizations. One of them is [1]. I worked on that project and implemented (and proved correct) several optimizations within just weeks. This is not industry-ready stuff, though.

[1] http://www.mpi-sws.org/~neis/pils/

> an implementation cost of one PhD thesis per optimization pass.

This strikes me as a little much. This kind of proof requires insight, yes, but it's hardly the level of a thesis, it hardly requires innovation to demonstrate. Just exhaustiveness.

Reply on news.ycombinator.com