Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Documentation: Part I #1029

Closed
wants to merge 1 commit into from
Closed

Documentation: Part I #1029

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
202 changes: 144 additions & 58 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,65 +8,126 @@ 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)
[![Apache 2.0 License](https://img.shields.io/badge/license-Apache--2-brightgreen.svg)](https://www.apache.org/licenses/LICENSE-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

Expand All @@ -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

Expand All @@ -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/)
Expand Down Expand Up @@ -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