4 ms·

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

by soup10 12y 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.

lifthrasiir 12y 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_cuoq 12y 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.
  - deleted 12y ago
    [deleted]
  - lifthrasiir 12y ago
    Yeah, -O2 was my wild guess and in the reality the figure may vary a lot. I think that it is quite great anyway.
  - sklogic 12y ago
    http://www.irisa.fr/celtique/ext/compcertSSA/ http://www.irisa.fr/celtique/ext/compcertSSA/ may bring in a whole bunch of optimisations nearly for free. We'll see...
  - eruquen 12y ago
    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/ http://www.mpi-sws.org/~neis/pils/
  - duaneb 12y ago
    > 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.
sanxiyn 12y 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.
- craftit 12y 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.
  - andrewchambers 12y ago
    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.
    - craftit 12y ago
      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.
  - justincormack 12y ago
    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.
  - edwintorok 12y ago
    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=27603 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=26763 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=28045 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=37573 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=37573 https://bugzilla.clamav.net/show_bug.cgi?id=670 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://bugs.gentoo.org/show_bug.cgi?id=275928#c29 https://bugzilla.clamav.net/show_bug.cgi?id=1581 https://bugzilla.clamav.net/show_bug.cgi?id=1581
pascal_cuoq 12y 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.pdf http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris...

by soup10 12y 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.

lifthrasiir 12y 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_cuoq 12y 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.
- deleted 12y ago
  [deleted]
- lifthrasiir 12y ago
  Yeah, -O2 was my wild guess and in the reality the figure may vary a lot. I think that it is quite great anyway.
- sklogic 12y ago
  http://www.irisa.fr/celtique/ext/compcertSSA/ http://www.irisa.fr/celtique/ext/compcertSSA/ may bring in a whole bunch of optimisations nearly for free. We'll see...
- eruquen 12y ago
  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/ http://www.mpi-sws.org/~neis/pils/
- duaneb 12y ago
  > 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.

sanxiyn 12y 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.

craftit 12y 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.
- andrewchambers 12y ago
  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.
  - craftit 12y ago
    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.
- justincormack 12y ago
  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.
- edwintorok 12y ago
  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=27603 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=26763 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=28045 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=37573 http://gcc.gnu.org/bugzilla/show_bug.cgi?id=37573 https://bugzilla.clamav.net/show_bug.cgi?id=670 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://bugs.gentoo.org/show_bug.cgi?id=275928#c29 https://bugzilla.clamav.net/show_bug.cgi?id=1581 https://bugzilla.clamav.net/show_bug.cgi?id=1581

pascal_cuoq 12y 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.pdf http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris...