From f643bb5ad0ae3c7e4f012d91be88e1557de7bd1a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Sep 2023 13:37:25 +0300 Subject: [PATCH 1/3] Add external benchmarking guide --- docs/user-guide/benchmarking.md | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) 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 From a3eaf9aece32da7a67d65dc17bffa57dbc9b8530 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Sep 2023 13:39:42 +0300 Subject: [PATCH 2/3] Refer to benchmarking guide in README --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index b03b7bbe36..4d97baa842 100644 --- a/README.md +++ b/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). From cd45df53d63174ad77f05d93d34472f4cdbd639a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Sep 2023 14:02:11 +0300 Subject: [PATCH 3/3] Add opam post-message about OCaml 5 benchmarking --- goblint.opam | 3 +++ goblint.opam.locked | 3 +++ goblint.opam.template | 3 +++ 3 files changed, 9 insertions(+) diff --git a/goblint.opam b/goblint.opam index a20df919d0..59f8a59c09 100644 --- a/goblint.opam +++ b/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"} +] diff --git a/goblint.opam.locked b/goblint.opam.locked index acb49a7b14..fe5bb65a00 100644 --- a/goblint.opam.locked +++ b/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"} +] diff --git a/goblint.opam.template b/goblint.opam.template index b7f5a7abff..5c13293196 100644 --- a/goblint.opam.template +++ b/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"} +]