4 ms·
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
by 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 agoYeah, -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 agohttp://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 agoThere 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.