From 24468837dd293121f93ad6694a963a5efeaffa23 Mon Sep 17 00:00:00 2001 From: Tobias Meggendorfer Date: Tue, 2 Apr 2024 23:33:01 +0200 Subject: [PATCH] Improve readme --- README.md | 202 ++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 144 insertions(+), 58 deletions(-) diff --git a/README.md b/README.md index b219802c3..6f2cb0a19 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,7 @@ SPDX-License-Identifier: Apache-2.0 --> # BenchExec + ## A Framework for Reliable Benchmarking and Resource Measurement [![Build Status](https://gitlab.com/sosy-lab/software/benchexec/badges/main/pipeline.svg)](https://gitlab.com/sosy-lab/software/benchexec/pipelines) @@ -15,58 +16,118 @@ SPDX-License-Identifier: Apache-2.0 [![PyPI version](https://img.shields.io/pypi/v/BenchExec.svg)](https://pypi.python.org/pypi/BenchExec) [![DOI](https://zenodo.org/badge/30758422.svg)](https://zenodo.org/badge/latestdoi/30758422) - **News and Updates**: -- BenchExec is part of [Google Summer of Code](https://summerofcode.withgoogle.com/) again! If you are interested in being paid by Google for contributing to BenchExec, check our [project ideas and instructions](https://www.sosy-lab.org/gsoc/) and [contact us](https://github.com/sosy-lab/benchexec/discussions)! + +- BenchExec is part of [Google Summer of Code][GSOC] again! If you are + interested in being paid by Google for contributing to BenchExec, check our + [project ideas and instructions][GSOC-proj] and [contact us][github-discuss]! - BenchExec 3.18 brings support for systems with cgroups v2! -- Linux kernel 5.11 finally [makes it possible](https://github.com/sosy-lab/benchexec/blob/main/doc/INSTALL.md#kernel-requirements) to use all BenchExec features on distributions other than Ubuntu! -- We now provide an [Ubuntu PPA](https://launchpad.net/~sosy-lab/+archive/ubuntu/benchmarking) that makes installing and upgrading BenchExec easier ([docs](https://github.com/sosy-lab/benchexec/blob/main/doc/INSTALL.md#debianubuntu)). -- An extended version of our paper on BenchExec and its background was published as open access in the journal STTT, - you can read [Reliable Benchmarking: Requirements and Solutions](https://doi.org/10.1007/s10009-017-0469-y) online. - We also provide a set of [overview slides](https://www.sosy-lab.org/research/prs/Latest_ReliableBenchmarking.pdf). +- Linux kernel 5.11 finally + [makes it possible](doc/INSTALL.md#kernel-requirements) + to use all BenchExec features on distributions other than Ubuntu! +- We provide an [Ubuntu PPA][ubuntu-ppa] that makes installing and upgrading + BenchExec easier ([docs](doc/INSTALL.md#debianubuntu)). +- An extended version of our paper on BenchExec and its background was + published as open access in the journal STTT, you can read + [Reliable Benchmarking: Requirements and Solutions][publication] online. + We also provide a set of [overview slides][slides]. + +[GSOC]: https://summerofcode.withgoogle.com/ +[GSOC-proj]: https://www.sosy-lab.org/gsoc/ +[ubuntu-ppa]: https://launchpad.net/~sosy-lab/+archive/ubuntu/benchmarking +[publication]: https://doi.org/10.1007/s10009-017-0469-y +[slides]: https://www.sosy-lab.org/research/prs/Latest_ReliableBenchmarking.pdf + +## Features BenchExec provides three major features: -- execution of arbitrary commands with precise and reliable measurement - and limitation of resource usage (e.g., CPU time and memory), - and isolation against other running processes -- an easy way to define benchmarks with specific tool configurations - and resource limits, - and automatically executing them on large sets of input files +- execution of arbitrary commands with precise and reliable measurement and + limitation of resource usage (e.g., CPU time and memory), and isolation + against other running processes +- an easy way to define benchmarks with specific tool configurations and + resource limits, and automatically executing them on large sets of input files - generation of interactive tables and plots for the results - -Unlike other benchmarking frameworks, -BenchExec is able to reliably measure and limit resource usage -of the benchmarked tool even if the latter spawns subprocesses. -In order to achieve this, -it uses the [cgroups feature](https://www.kernel.org/doc/Documentation/cgroup-v1/cgroups.txt) -of the Linux kernel to correctly handle groups of processes. -For proper isolation of the benchmarks, it uses (if available) -Linux [user namespaces](http://man7.org/linux/man-pages/man7/namespaces.7.html) -and an [overlay filesystem](https://www.kernel.org/doc/Documentation/filesystems/overlayfs.txt) -to create a [container](https://github.com/sosy-lab/benchexec/blob/main/doc/container.md) -that restricts interference of the executed tool with the benchmarking host. +Unlike other benchmarking frameworks, BenchExec is able to reliably measure and +limit resource usage of the benchmarked tool even if the latter spawns +subprocesses. +In order to achieve this, it uses the [cgroups feature][linux-cgroup] of the +Linux kernel to correctly handle groups of processes. +For proper isolation of the benchmarks, it uses (if available) Linux +[user namespaces][linux-namespace] and an [overlay filesystem][linux-overlayfs] +to create a [container](doc/container.md) that restricts interference of the +executed tool with the benchmarking host. BenchExec is intended for benchmarking non-interactive tools on Linux systems. -It measures CPU time, wall time, and memory usage of a tool, -and allows to specify limits for these resources. +It measures CPU time, wall time, and memory usage of a tool, and allows to +specify limits for these resources. It also allows to limit the CPU cores and (on NUMA systems) memory regions, and the container mode allows to restrict filesystem and network access. -In addition to measuring resource usage, -BenchExec can verify that the result of the tool was as expected, -and extract further statistical data from the output. -Results from multiple runs can be combined into CSV and interactive HTML tables, -of which the latter provide scatter and quantile plots -(have a look at our [demo table](https://sosy-lab.github.io/benchexec/example-table/svcomp-simple-cbmc-cpachecker.table.html)). - -BenchExec works only on Linux and needs a one-time setup of cgroups by the machine's administrator. +In addition to measuring resource usage, BenchExec can verify that the result +of the tool was as expected, and extract further statistical data from the +output. +Results from multiple runs can be combined into CSV and interactive HTML +tables, of which the latter provide scatter and quantile plots (have a look +at our [demo table][demo-table]). + +[linux-cgroup]: https://www.kernel.org/doc/Documentation/cgroup-v1/cgroups.txt +[linux-namespace]: http://man7.org/linux/man-pages/man7/namespaces.7.html +[linux-overlayfs]: https://www.kernel.org/doc/Documentation/filesystems/overlayfs.txt +[demo-table]: https://sosy-lab.github.io/benchexec/example-table/svcomp-simple-cbmc-cpachecker.table.html + +## Usage + +BenchExec is more than just the tool `benchexec`: +For benchmarking, BenchExec offers two command line utilities to execute +benchmarks, `benchexec` and `runexec`, as well as a Python API, which are +described in the following. + +Before benchmarking, please consider the +[general guidelines](doc/benchmarking.md) for benchmarking. + +### runexec: Benchmark a Single Command + +The tool `runexec` allows to run a single command with the isolation and +resource limitation features provided by benchexec. +It can be viewed as a (much more powerful) replacement to a combination of +utilities like `taskset`, `time`, and `timeout`. +For example, +``` + runexec --cores 0 --timelimit 5 --memlimit 1GB -- echo Test +``` +executes the command `echo Test`, restricted to a single core, 1 GB of memory, +and 5 seconds of CPU-time, and displays precise measurements related to time, +memory, I/O, etc. +Use `runexec` to reliably measure a single to a handful of executions. +See [`runexec`'s documentation](doc/runexec.md) for further usage instructions. + +### benchexec: Run a Benchmark Suite + +The tool `benchexec` is an eleborate wrapper around the base functionality of +`runexec`. +This tool provides management for defining and executing a large number +individual invocations as well as checking and aggregating their results. +We recommend using `benchexec` when executing a concrete benchmark suite, +especially when multiple different tools are involved. +See [`benchexec`'s documentation](doc/benchexec.md) for further details, e.g., +how to define benchmark sets, run `benchexec`, view results, or integrate +tools. + +### API + +Benchexec also provides a +[python API](doc/runexec.md#integration-into-other-benchmarking-frameworks) +from which all features of `runexec` can be accessed directly. + +### Setup & Requirements + +BenchExec only works on Linux and needs a one-time setup of cgroups by the +machine's administrator. The actual benchmarking can be done by any user and does not need root access. +See the [installation guide](doc/INSTALL.md) for detailed setup steps and +troubleshooting. -BenchExec was originally developed for use with the software verification framework -[CPAchecker](https://cpachecker.sosy-lab.org) -and is now developed as an independent project -at the [Software Systems Lab](https://www.sosy-lab.org) -of the [Ludwig-Maximilians-Universität München (LMU Munich)](https://www.uni-muenchen.de). +## Useful Resources ### Links @@ -75,9 +136,12 @@ of the [Ludwig-Maximilians-Universität München (LMU Munich)](https://www.uni-m - [Downloads](https://github.com/sosy-lab/benchexec/releases) - [Changelog](https://github.com/sosy-lab/benchexec/tree/main/CHANGELOG.md) - [BenchExec GitHub Repository](https://github.com/sosy-lab/benchexec), - use this for [reporting issues and asking questions](https://github.com/sosy-lab/benchexec/issues) + use this for + [reporting issues and asking questions](https://github.com/sosy-lab/benchexec/issues) - [BenchExec at PyPI](https://pypi.python.org/pypi/BenchExec) -- [BenchExec at Zenodo](https://doi.org/10.5281/zenodo.1163552): Each release gets a DOI such that you can reference it from your publications and artifacts. +- [BenchExec at Zenodo](https://doi.org/10.5281/zenodo.1163552): Each release + gets a DOI such that you can reference it from your publications and + artifacts. ### Literature @@ -87,17 +151,27 @@ of the [Ludwig-Maximilians-Universität München (LMU Munich)](https://www.uni-m ### License and Copyright -BenchExec is licensed under the [Apache 2.0 License](https://www.apache.org/licenses/LICENSE-2.0), +BenchExec is licensed under the +[Apache 2.0 License](https://www.apache.org/licenses/LICENSE-2.0), copyright [Dirk Beyer](https://www.sosy-lab.org/people/beyer/). -Exceptions are some tool-info modules -and third-party code that is bundled in the HTML tables, -which are available under several other free licenses -(cf. [folder `LICENSES`](https://github.com/sosy-lab/benchexec/tree/main/LICENSES)). +Exceptions are some tool-info modules and third-party code that is bundled in +the HTML tables, which are available under several other free licenses (cf. +[folder `LICENSES`](https://github.com/sosy-lab/benchexec/tree/main/LICENSES)). + +## Developers + +BenchExec was originally developed for use with the software verification +framework [CPAchecker](https://cpachecker.sosy-lab.org) and is now developed as +an independent project at the [Software Systems Lab](https://www.sosy-lab.org) +of the +[Ludwig-Maximilians-Universität München (LMU Munich)](https://www.uni-muenchen.de). -### Authors -Maintainer: [Philipp Wendler](https://www.philippwendler.de) +### Maintainer + +[Philipp Wendler](https://www.philippwendler.de) + +### Contributors -Contributors: - [Aditya Arora](https://github.com/alohamora) - [Levente Bajczi](https://github.com/leventeBajczi) - [Dirk Beyer](https://www.sosy-lab.org/people/beyer/) @@ -126,23 +200,35 @@ Contributors: - [Ilja Zakharov](https://github.com/IljaZakharov) - and [lots of more people who integrated tools into BenchExec](https://github.com/sosy-lab/benchexec/graphs/contributors) -### Users of BenchExec +## Users of BenchExec -BenchExec was successfully used for benchmarking in all instances -of the international competitions on [Software Verification](https://sv-comp.sosy-lab.org) -and [Software Testing](https://test-comp.sosy-lab.org) -with a wide variety of benchmarked tools and hundreds of thousands benchmark runs. +BenchExec was successfully used for benchmarking in all instances of the +international competitions on [Software Verification][svcomp] and +[Software Testing][testcomp] with a wide variety of benchmarked tools and +hundreds of thousands benchmark runs. It is integrated into the cluster-based logic-solving service -[StarExec](https://www.starexec.org/starexec/public/about.jsp) ([GitHub](https://github.com/StarExec/StarExec)). +[StarExec][starexec-web] ([GitHub][starexec-github]). + +[svcomp]: https://sv-comp.sosy-lab.org +[testcomp]: https://test-comp.sosy-lab.org +[starexec-web]: https://www.starexec.org/starexec/public/about.jsp +[starexec-github]: https://github.com/StarExec/StarExec The developers of the following tools use BenchExec: - [CPAchecker](https://cpachecker.sosy-lab.org), also for regression testing - [Dartagnan](https://github.com/hernanponcedeleon/Dat3M) -- [ESBMC](https://github.com/esbmc/esbmc), also for regression testing and even with a [GitHub action](https://github.com/esbmc/esbmc/blob/master/.github/workflows/benchexec.yml) for BenchExec +- [ESBMC](https://github.com/esbmc/esbmc), also for regression testing and + even with a + [GitHub action](https://github.com/esbmc/esbmc/blob/master/.github/workflows/benchexec.yml) + for BenchExec - [SMACK](https://github.com/smackers/smack) - [SMTInterpol](https://github.com/ultimate-pa/smtinterpol) - [TriCera](https://github.com/uuverifiers/tricera) - [Ultimate](https://github.com/ultimate-pa/ultimate) -If you would like to be listed here, [contact us](https://github.com/sosy-lab/benchexec/issues/new). +If you would like to be listed here, [contact us][github-issues]. + + +[github-discuss]: https://github.com/sosy-lab/benchexec/discussions +[github-issues]: https://github.com/sosy-lab/benchexec/issues/new