Evaluate Profile-Guided Optimization (PGO) and LLVM BOLT

[zamazan4ik]

Hi!

I did a lot of Profile-Guided Optimization (PGO) benchmarks recently on different kinds of software (including many compilers and compiler-like projects like Clang, Rustc, Clangd, clang-tidy, etc.) - all currently available results are located at https://github.com/zamazan4ik/awesome-pgo . According to the tests, PGO usually helps a lot for compiler-like workloads. I think testing PGO would be a good idea for Kani.

I can suggest to do the following things:

• Evaluate PGO on Kani
• If it benefits Kani - add a note to the Kani documentation about building with PGO. In this case, users and maintainers who build their own Kani binaries will be aware of PGO as an additional way to optimize the project
• Optimize provided by Kani project binaries on the CI (like it's already done for other projects like Rustc), if any
• After that, I suggest trying to apply LLVM BOLT as an additional post-PGO step. Rustc already does it on some platforms

For the Rust projects, I suggest PGO optimizing with cargo-pgo.

[adpaco-aws]

Hi @zamazan4ik , thanks for the suggestions!

Would you mind explaining what "Evaluate PGO" would mean in this context? Kani is essentially a static analysis tool which does not produce executable binaries. More specifically, the Kani compiler replaces the LLVM back-end with an alternative GotoC back-end to generate GotoC programs (the ones accepted by CBMC). What do you think?

[zamazan4ik]

Would you mind explaining what "Evaluate PGO" would mean in this context?

Sure! Here I mean optimizing Kani itself with PGO, so hopefully Kani will work faster.

[adpaco-aws]

Oh, understood. Please let me bring this up for discussion with the team. Thanks!