This artifact for our TACAS'20 paper "CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering" consists of the tool CPU Energy Meter which is available under the BSD 2-clause license. Furthermore, the tool BenchExec, which is available under the Apache 2.0 license, is included to demonstrate the integration of CPU Energy Meter into BenchExec.
The tools CPU Energy Meter and BenchExec are already archived on Zenodo.
Download:
This artifact is also archived on Zenodo with DOI 10.5281/zenodo.3679337. Please cite as
Beyer, D., Wendler, P.: Replication package for article ‘CPU Energy Meter: A tool for energy-aware algorithms engineering’ in Proc. TACAS ’20. Zenodo (2020). https://doi.org/10.5281/zenodo.3679337
Verification algorithms are among the most resource-intensive computation tasks. Saving energy is important for our living environment and to save cost in data centers. Yet, researchers compare the efficiency of algorithms still in terms of consumption of CPU time (or even wall time). Perhaps one reason for this is that measuring energy consumption of computational processes is not as convenient as measuring the consumed time and there is no sufficient tool support. To close this gap, we contribute CPU Energy Meter, a small tool that takes care of reading the energy values that Intel CPUs track inside the chip. In order to make energy measurements as easy as possible, we integrated CPU Energy Meter into BenchExec, a benchmarking tool that is already used by many researchers and competitions in the domain of formal methods. As evidence for usefulness, we explored the energy consumption of some state-of-the-art verifiers and report some interesting insights, for example, that energy consumption is not necessarily correlated with CPU time.
CPU Energy Meter requires an Intel CPU with the RAPL feature, which is present in x86 CPUs since the Sandy Bridge generation (e.g., Core i3/5/7 2000 and above or Xeon E3/E5/E7). Furthermore, the tool works only on a real machine (no VM and no container) because it needs direct access to the so-called model-specific registers (MSRs) of the CPU. To access these registers, it requires a Linux kernel with the module "msr" (this module should be available in standard distribution kernels). The tool was tested on 64-bit Linux systems. Furthermore, for installation, root access is required (for example to activate the mentioned kernel module).
For a Debian-based distribution (e.g., Ubuntu), it is recommended to install the Debian packages (cf. deb/INSTALL.md in the artifact). Otherwise, please follow the instructions for installing from source in source/INSTALL.md in the artifact.
Note that in both cases, CPU Energy Meter can be installed either alone (for experimenting with this tool alone) or in addition to BenchExec.
If CPU Energy Meter is correctly installed, the tool can be executed with cpu-energy-meter. It will produce output (showing the consumed energy while it was running) only after Ctrl+C is pressed to terminate it. A mode with debug output is available via cpu-energy-meter -d.
The installation attempts to configure the host system such that CPU Energy Meter is usable for all users. If the tool does not work, please try executing it with root privileges: sudo cpu-energy-meter. Please also check that the kernel module "msr" is loaded with lsmod | grep msr and that the appropriate device modules are present: ls /dev/cpu/*/msr.
CPU Energy Meter is intended to be used primarily by benchmarking frameworks instead of end users. If BenchExec is installed, it is possible to benchmark a single tool execution with "runexec", e.g., runexec --read-only-dir / -- /bin/sh -c 'echo "scale=2000; a(1)*4" | bc -l' (this example calculates 2000 digits of pi, of course different commands can be used). The command sudo sysctl -w kernel.unprivileged_userns_clone=1 might be necessary for BenchExec on non-Ubuntu systems to configure the kernel appropriately. If CPU Energy Meter is installed, BenchExec will automatically use it to measure the energy consumption and will report values such as
cpuenergy=16.387085J
cpuenergy-pkg0=16.387085J
cpuenergy-pkg0-core=14.647461J
cpuenergy-pkg0-dram=1.449158J
cpuenergy-pkg0-psys=28.922119J
cpuenergy-pkg0-uncore=0.013672JThe value cpuenergy is the sum of the cpuenergy-pkg[0-9]+ values for all CPUs that were used. The other values report the energy consumption of the various measurement domains that the CPU(s) support (it depends on the CPU which values are available).
BenchExec also supports executing and measuring large sets of tool executions automatically. This is independent of CPU Energy Meter and just requires the same steps as benchmarking with BenchExec alone would.
As an example for those who are not familiar with BenchExec we provide an example benchmark definition that calculates pi with 1000 to 10000 digits. To execute this benchmark set, run benchexec benchmark-example-calculatepi.xml. BenchExec needs a proper setup of cgroups and uses some kernel features that might not be available on all systems. If you have problems executing benchexec, run sudo sysctl -w kernel.unprivileged_userns_clone=1 and benchexec benchmark-example-calculatepi.xml --read-only-dir / -T -1 -M -1. This will run BenchExec in a restricted mode with less measurements, but measuring CPU energy will still work if cpu-energy-meter is properly installed. In any case, to generate HTML and CSV tables with the results (including the energy measurements), run table-generator results/benchmark-example-calculatepi.*.results.xml.bz2 --all-columns --show afterwards.
In order to use benchexec with other tools (e.g., verifiers), a tool-specific module needs to be added to BenchExec and an appropriate benchmark definition needs to be written. This had been done for all participants of SV-COMP, so it is possible to benchmark any participating verifier using the verifier archives from https://gitlab.com/sosy-lab/sv-comp/archives-2019 and the benchmark definitions similar to those at https://github.com/sosy-lab/sv-comp/tree/svcomp19.
Fig. 1 was produced by measuring the energy consumption of an Intel Core i5-6440HQ CPU in a Lenovo ThinkPad T460p for 10s. This experiment can be replicated with the command
cpu-energy-meter & sleep 10s ; kill -INT %1(reported domains and results will vary depending on the system).
The results for these figures where taken from the literature (Dirk Beyer, "Automatic Verification of C and Java Programs: SV-COMP 2019", Proc. TACAS'19). The raw data are available at https://sv-comp.sosy-lab.org/2019/results/results-verified/All-Raw.zip.
More information on replicating these results is in the above publication and on the SV-COMP website. The SV-COMP benchmark set, all participating tools, and the benchmark definitions are available online.
We provide baseline measurements (of an idle state) of the same system on which SV-COMP'19 was executed as a comparison for the data in Table 1 and Figs. 2-4:
| Domain | Avg. Idle Power (W) |
|---|---|
| Package | 1.1 |
| PP0 (Core) | 0.34 |
| DRAM | 1.5 |
For the package domain, this is one order of magnitude less than the average power when benchmarking CBMC or CPA-Seq. Note that in Figs. 2 and 3 (which show the package domain) the gray line towards the bottom of the plot represents an average power of 1 W and is thus roughly showing the idle energy consumption. If we were to subtract the idle energy consumption from the energy measurements in Table 1 and Figs. 2-4, the overall picture would not change and the conclusions would remain the same.