Merge pull request #1160 from goblint/benchmarking-docs

Document Goblint benchmarking best practices

README.md

@@ -13,6 +13,7 @@ Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/e
 
 ## Installing
 Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository.
+For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs](https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/).
 
 ### Linux
 1. Install [opam](https://opam.ocaml.org/doc/Install.html).

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

goblint.opam

@@ -81,3 +81,6 @@ pin-depends: [
   # TODO: add back after release, only pinned for CI stability
   [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
 ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
+]

goblint.opam.locked

@@ -140,3 +140,6 @@ pin-depends: [
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
   ]
 ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
+]

goblint.opam.template

@@ -8,3 +8,6 @@ pin-depends: [
   # TODO: add back after release, only pinned for CI stability
   [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
 ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
+]