Evaluate Profile-Guided Optimization (PGO) and LLVM BOLT

[zamazan4ik]

Hi!

Recently I checked Profile-Guided Optimization (PGO) improvements on multiple projects. The results are here. LLVM-related results are here. According to the tests, PGO usually helps a lot with the compiler and compiler-like workloads (like static analysis). That's why I think trying to optimize Prusti with PGO can be a good idea.

I can suggest the following action points:

• Perform PGO benchmarks on Prusti. And if it shows improvements - add a note about possible improvements in Prusti's performance with PGO.
• Providing an easier way (e.g. a build option) to build scripts with PGO can be useful for the end-users and maintainers since they will be able to optimize Prusti according to their own workloads.
• Optimize pre-built Prusti binaries with PGO.

Maybe testing Post-Link Optimization techniques (like LLVM BOLT) would be interesting too but I recommend starting from the usual PGO.

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

[fpoli]

Thanks for the suggestions! In almost all of our cases the bottleneck is the Viper tool that we have to use internally, not Rust code. So, I don't think that in practice the benefits of PGO would be visible. However, it might be worth trying it when evaluating the future Lithium backend, which is 100% Rust.