Comment by MaxBarraclough
11 days ago
CompCert produces surprisingly fast native code.
This 2022 article [0] says it generates binaries that run about 7% slower than what GCC produces with -O1.
[0] https://www.cs.cornell.edu/courses/cs6120/2022sp/blog/compce...
That's a big gap, especially with the norm for releases being O2 if I understand correctly.
> That's a big gap
I wouldn't say so. The gap between GCC and Clang/LLVM is bigger than that on some benchmarks, [0] although the gap between their overall performance (using geometric mean) is much less. [1]
It's a very impressive result considering how much effort has gone into GCC. It highlights how compiler optimisation work can face diminishing returns.
> the norm for releases being O2 if I understand correctly
Agreed, but the difference isn't that great. From the article:
> CompCert code is 7% slower than gcc-01 and 12% slower than gcc-02 on average.
Reminds me of how the cproc/qbe C compiler gets very roughly 50% of the performance of Clang/LLVM in 0.1% the lines-of-code. [2]
[0] https://www.phoronix.com/review/gcc-16-vs-clang-22/3
[1] https://www.phoronix.com/review/gcc-16-vs-clang-22/6
[2] https://drewdevault.com/talks/qbe/ (and see the linked slideshow PDF, as the abstract is a little misleading)
Maybe we just have different experiences, but I've experienced a huge amount of friction trying to enable features that cost something resembling 0.5% of fleet performance, even when they provide massive benefits. 12% loss would be laughed out of the room.
I agree that this is an impressive feat. I also don't see why an equivalent for rust would be adopted.
1 reply →