Evaluate Profile-Guided Optimization (PGO)

[zamazan4ik]

Hi!

Recently I checked Profile-Guided Optimization (PGO) improvements on multiple projects. The results are here. LLVM-related results are here.

Since PGO showed measurable improvements in compiler-like loads (Clang, Clangd, clang-format, GCC, Rustc, etc.) I think it could be useful to check PGO on IKOS as well.

We need to perform PGO benchmarks on IKOS. And if it shows improvements - add a note about possible improvements in IKOS performance with PGO. Providing an easier way (e.g. a build option) to build scripts with PGO can be useful for the end-users too. Probably trying LLVM BOLT would be a good thing too (but after PGO).

[arthaud]

cf facebook/mariana-trench#137

[ivanperez-keera]

This sounds like a great idea. However, I don't really know what the action item would be on this. I'm moving it to a discussion for now; we can open issues when there's a clear plan of how to complete this.

[zamazan4ik]

However, I don't really know what the action item would be on this

I can propose the following action items:

1. Build Ikos with PGO and perform a performance comparison with the current Release build with some benchmarks
2. If PGO shows some improvements - add this information somewhere to the documentation/README file about it. In this case, users will be aware of additional ways how to increase Ikos's performance and can decide to perform PGO builds manually in their environments
3. Integrate PGO build into the build scripts. E.g. like it's done in LLVM: https://github.com/llvm/llvm-project/blob/main/clang/cmake/caches/PGO.cmake
4. Integrate building Ikos with PGO into the CI if have some prebuilt binaries distributed to users