Skip to main content

A Framework for Reliable Benchmarking and Resource Measurement.

Project description

BenchExec

A Framework for Reliable Benchmarking and Resource Measurement

Build Status Apache 2.0 License PyPI version DOI

News and Updates:

To help new or inexperienced users get started with reliable benchmarking right away, we offer a quickstart guide that contains a brief explanation of the issues of common setups as well as the (few) steps necessary to setup and use BenchExec instead.

BenchExec is a framework for reliable benchmarking and resource measurement and provides a standalone solution for benchmarking that takes care of important low-level details for accurate, precise, and reproducible measurements as well as result handling and analysis for large sets of benchmark runs. However, even users of other benchmarking frameworks or scripts can benefit from BenchExec by letting it perform the resource measurements and limits instead of less reliable tools and techniques like time or ulimit, and results produced by BenchExec can easily be exported for use with other tools.

In particular, 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
    (provided by runexec, a replacement for time and similar tools)
  • an easy way to define benchmarks with specific tool configurations and resource limits, and automatically executing them on large sets of input files
    (provided by benchexec on top of runexec)
  • generation of interactive tables and plots for the results
    (provided by table-generator for results produced with benchexec)

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 of the Linux kernel to correctly handle groups of processes. For proper isolation of the benchmarks, it uses (if available) Linux user namespaces and an overlay filesystem (either kernel-based or fuse-overlayfs) to create a container that restricts interference of the executed tool with the benchmarking host. More information on why this is necessary and the problems with other tools can be found in our paper Reliable Benchmarking: Requirements and Solutions (open access) and our slides (starting with slide "Checklist").

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 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 optionally 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).

BenchExec works only 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.

BenchExec was originally developed for use with the software verification framework CPAchecker and is now developed as an independent project at the Software Systems Lab of the Ludwig-Maximilians-Universität München (LMU Munich).

Links

Literature

License and Copyright

BenchExec is licensed under the Apache 2.0 License, copyright Dirk 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).

Authors

Maintainer: Philipp Wendler

Contributors:

Users of BenchExec

Several well-known international competitions use BenchExec, such as SMT-COMP, SV-COMP (software verification), the Termination Competition, and Test-Comp. In particular in SV-COMP BenchExec was used successfully for benchmarking in all instances of the competition and with a wide variety of benchmarked tools and millions of benchmark runs per year. BenchExec is also integrated into the cluster-based logic-solving service StarExec (GitHub).

The developers of the following tools use BenchExec:

If you would like to be listed here, contact us.

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

benchexec-3.30.tar.gz (1.2 MB view details)

Uploaded Source

Built Distribution

benchexec-3.30-py3-none-any.whl (739.7 kB view details)

Uploaded Python 3

File details

Details for the file benchexec-3.30.tar.gz.

File metadata

  • Download URL: benchexec-3.30.tar.gz
  • Upload date:
  • Size: 1.2 MB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/6.1.0 CPython/3.12.3

File hashes

Hashes for benchexec-3.30.tar.gz
Algorithm Hash digest
SHA256 1fc7f735cbe9eb0ba12c9b65f71f7b5cfdfcaa72af53678b7f8ca6e25cdfe9c3
MD5 4bb1a9f0465db8ef7208d0bc5b514408
BLAKE2b-256 b03409b1929c65f6991d2c9d087580442ab156054209ccedd04a71e8515b7fb9

See more details on using hashes here.

File details

Details for the file benchexec-3.30-py3-none-any.whl.

File metadata

  • Download URL: benchexec-3.30-py3-none-any.whl
  • Upload date:
  • Size: 739.7 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/6.1.0 CPython/3.12.3

File hashes

Hashes for benchexec-3.30-py3-none-any.whl
Algorithm Hash digest
SHA256 b9168715600fcc7e8034656fa021577a48cc6dcfa491f02535be30c132d1bc3a
MD5 c6d5b797ffcc50942cdee2e435630dbc
BLAKE2b-256 66f1d96d61f58221edaa69c145ae6907ec37ec6c54a8c3b21b93ab79da7a105e

See more details on using hashes here.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page