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