Skip to content

INSTALL.md

Latest commit

 

History

History
291 lines (209 loc) · 12.3 KB

INSTALL.md

File metadata and controls

291 lines (209 loc) · 12.3 KB

BenchExec: Setup

Download and Installation

Requirements

The following packages are optional but recommended dependencies:

  • cpu-energy-meter will let BenchExec measure energy consumption on Intel CPUs.
  • libseccomp2 provides better container isolation.
  • LXCFS provides better container isolation.
  • coloredlogs provides nicer log output.
  • pqos_wrapper and pqos library provide isolation of L3 cache and measurement of cache usage and memory bandwidth (only in benchexec).

Note that the table-generator utility requires only Python and works on all platforms.

Debian/Ubuntu

For installing BenchExec on Debian or Ubuntu we recommend installing from our PPA:

sudo add-apt-repository ppa:sosy-lab/benchmarking
sudo apt install benchexec

Alternatively, you can download our .deb package from GitHub and install manually (note that the leading ./ is important, otherwise apt will not find the package):

apt install --install-recommends ./benchexec_*.deb

Our package automatically configures the necessary cgroup permissions if the system uses cgroups v1. Just add the users that should be able to use BenchExec to the group benchexec (group membership will be effective after the next login of the respective user):

adduser <USER> benchexec

Afterwards, please check whether everything works or whether additional settings are necessary as described below.

Note that pqos_wrapper is currently not available as a Debian package and needs to be installed manually according to its documentation.

Other Distributions

For other distributions we recommend to use the Python package installer pip. To automatically download and install the latest stable version and its dependencies from the Python Packaging Index with pip, run this command:

sudo pip3 install benchexec coloredlogs

You can also install BenchExec only for your user with

pip3 install --user benchexec coloredlogs

In the latter case you probably need to add the directory where pip installs the commands to the PATH environment by adding the following line to your ~/.profile file:

export PATH=~/.local/bin:$PATH

Of course you can also install BenchExec in a virtualenv if you are familiar with Python tools.

Please make sure to configure cgroups as described below and install cpu-energy-meter, libseccomp2, LXCFS, and pqos_wrapper if desired.

Development version

To install the latest development version from the GitHub repository, run this command:

pip3 install --user git+https://github.com/sosy-lab/benchexec.git coloredlogs

It is useful to install the system package python3-lxml before, otherwise pip will try to download and build this module, which needs a compiler and several development header packages.

Please make sure to configure cgroups as described below and install cpu-energy-meter, libseccomp2, LXCFS, and pqos_wrapper if desired.

Kernel Requirements

To execute benchmarks and reliably measure and limit their resource consumption, BenchExec requires that the user which executes the benchmarks can create and modify cgroups (see below for how to allow this).

If you are using an Ubuntu version that is still supported, everything else should work out of the box. For other distributions, please read the following detailed requirements.

Except on Ubuntu, the full feature set of BenchExec is only usable on Linux 5.11 or newer, so we suggest at least this kernel version.

On older kernels, you need to avoid using the overlay filesystem (cf. below), all other features are supported. However, we strongly recommend to use at least Linux 4.14 or newer because it reduces the overhead of BenchExec's memory measurements and limits. For even older kernel versions, please read our previous documentation with more details.

Using BenchExec on kernels without NUMA support is not guaranteed to work (but this is enabled by all common distributions).

In container mode (i.e., always except when using --no-container), BenchExec uses two main kernel features that are not usable on all distributions by default:

  • User Namespaces: This is available on most distros (the kernel option is CONFIG_USER_NS), but Debian and Arch Linux disable this feature for regular users, so the system administrator needs to enable it with sudo sysctl -w kernel.unprivileged_userns_clone=1 or a respective entry in /etc/sysctl.conf. On CentOS it can be necessary to enable this feature with sudo sysctl -w user.max_user_namespaces=10000 or a respective entry in /etc/sysctl.conf (the exact value is not important).

  • Unprivileged Overlay Filesystem: This is only available since Linux 5.11 (kernel option CONFIG_OVERLAY_FS), but also present in all Ubuntu kernels, even older ones. Users of older kernels on other distributions can still use container mode, but have to choose a different mode of mounting the file systems in the container, e.g., with --read-only-dir / (see below).

If container mode does not work, please check the common problems.

Setting up Cgroups

If you have installed the Debian package and you are running systemd (default since Debian 8 and Ubuntu 15.04), the package should have configured everything automatically as long as the system is using cgroups v1. Just add your user to the group benchexec and reboot:

adduser <USER> benchexec

Support for cgroups v2 is still under development for BenchExec. On recent distributions (e.g., Ubuntu 22.04), please switch back to cgroups v1 for now by putting systemd.unified_cgroup_hierarchy=0 on the kernel command line. On Debian/Ubuntu, this could be done with the following steps and rebooting afterwards:

echo 'GRUB_CMDLINE_LINUX_DEFAULT="${GRUB_CMDLINE_LINUX_DEFAULT} systemd.unified_cgroup_hierarchy=0"' | sudo tee /etc/default/grub.d/cgroupsv1-for-benchexec.cfg
sudo update-grub

Setting up Cgroups on Machines with systemd

Most distributions today use systemd, and systemd makes extensive usage of cgroups and claims that it should be the only process that accesses cgroups directly. Thus it would interfere with the cgroups usage of BenchExec.

By using a dummy service we can let systemd create an appropriate cgroup for BenchExec and prevent interference. The following steps are necessary:

  • Decide which set of users should get permissions for cgroups. Our recommendation is to create a group named benchexec with groupadd benchexec and add the respective users to this group. Note that users need to logout and login afterwards to actually get the group membership.

  • Put the file benchexec-cgroup.service into /etc/systemd/system/ and enable the service with systemctl daemon-reload; systemctl enable --now benchexec-cgroup.

    By default, this gives permissions to users of the group benchexec, this can be adjusted in the Environment line as necessary.

  • If the system is using cgroups v2, you need to tell systemd to use cgroups v1 instead as described above.

By default, BenchExec will automatically attempt to use the cgroup system.slice/benchexec-cgroup.service that is created by this service file. If you use a different cgroup structure, you need to ensure that BenchExec runs in the correct cgroup by executing the following commands once per terminal session:

echo $$ > /sys/fs/cgroup/cpuset/<CGROUP>/tasks
echo $$ > /sys/fs/cgroup/cpuacct/<CGROUP>/tasks
echo $$ > /sys/fs/cgroup/memory/<CGROUP>/tasks
echo $$ > /sys/fs/cgroup/freezer/<CGROUP>/tasks

In any case, please check whether everything works or whether additional settings are necessary as described below.

Setting up Cgroups on Machines without systemd

The cgroup virtual file system is typically mounted at or below /sys/fs/cgroup. If it is not, you can mount it with

sudo mount -t cgroup cgroup /sys/fs/cgroup

To give all users on the system the ability to create their own cgroups, you can use

sudo chmod o+wt,g+w /sys/fs/cgroup/

Of course permissions can also be assigned in a more fine-grained way if necessary.

Alternatively, software such as cgrulesengd from the cgroup-bin package can be used to setup the cgroups hierarchy.

Note that cgrulesengd might interfere with the cgroups of processes, if configured to do so via cgrules.conf. This can invalidate the measurements. BenchExec will try to prevent such interference automatically, but for this it needs write access to /run/cgred.socket.

It may be that your Linux distribution already mounts the cgroup file system and creates a cgroup hierarchy for you. In this case you need to adjust the above commands appropriately. To optimally use BenchExec, the cgroup controllers cpuacct, cpuset, freezer, and memory should be mounted and usable, i.e., they should be listed in /proc/self/cgroups and the current user should have at least the permission to create sub-cgroups of the current cgroup(s) listed in this file for these controllers.

In any case, please check whether everything works or whether additional settings are necessary as described below.

Setting up Cgroups in a Docker/Podman Container

If you want to run benchmarks within a Docker/Podman container, and the cgroups file system is not available within the container, please use the following command line argument to mount the cgroup hierarchy within the container when starting it (same for Podman):

docker run -v /sys/fs/cgroup:/sys/fs/cgroup:rw ...

Note that you additionally need some flags for container mode, which are explained in the container documentation.

Testing Cgroups Setup and Known Problems

After installing BenchExec and setting up the cgroups file system, please run

python3 -m benchexec.check_cgroups

This will report warnings and exit with code 1 if something is missing. If you find that something does not work, please check the following list of solutions.

If your machine has swap, cgroups should be configured to also track swap memory. This is turned off by several distributions. If the file memory.memsw.usage_in_bytes does not exist in the directory /sys/fs/cgroup/memory (or wherever the cgroup file system is mounted), this needs to be enabled by setting swapaccount=1 on the command line of the kernel. On Ubuntu, you can for example set this parameter by creating the file /etc/default/grub.d/swapaccount-for-benchexec.cfg with the following content:

GRUB_CMDLINE_LINUX_DEFAULT="${GRUB_CMDLINE_LINUX_DEFAULT} swapaccount=1"

Then run sudo update-grub and reboot. On other distributions, please adjust your boot loader configuration appropriately.

In some Debian kernels (and those derived from them, e.g. Raspberry Pi kernel), the memory cgroup controller is disabled by default, and can be enabled by setting cgroup_enable=memory on the kernel command line, similar to swapaccount=1 above.

Installation for Development

Please refer to the development instructions.