diff --git a/docs/user-guide/benchmarking.md b/docs/user-guide/benchmarking.md index 44811b61a5..5417375bdb 100644 --- a/docs/user-guide/benchmarking.md +++ b/docs/user-guide/benchmarking.md @@ -1,6 +1,31 @@ # Benchmarking +The following best practices should be followed when benchmarking Goblint. +This is to ensure valid, reproducible and representative benchmarking results. -To achieve reproducible builds and the best performance for benchmarking, it is recommended to compile Goblint using the `release` option: +# External benchmarking +External users should choose the version of Goblint to evaluate or benchmark as follows: + +1. Use the newest version release. + + The version from git `master` branch or any other intermediate git commit come without any guarantees. + They are bleeding-edge and haven't gone through validation like the version releases. + + SV-COMP releases are highly preferable since they've gone through rigorous validation in SV-COMP. + +2. Download the corresponding version from a Zenodo artifact or by checking out the respective git tag. **Do not install directly from opam repository!** + + Goblint pins optimized versions of some dependencies which cannot be done on the opam repository releases. + Thus, using the latter would yield unrepresentative results. + + Zenodo artifacts come with DOIs, which make them ideal for citation. + +3. Use OCaml 4.14. **Do not use OCaml 5!** + + OCaml 5 has significant performance regressions, which yield unrepresentative benchmarking results. + Goblint's `make setup` installs the correct OCaml version into a new opam switch. + +# Release build +To achieve the best performance for benchmarking, Goblint should be compiled using the `release` option: ```sh make release