Merge branch 'documentation-improvements'

README.md

@@ -29,15 +29,31 @@ SPDX-License-Identifier: Apache-2.0
   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).
 
-BenchExec provides three major features:
+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
+  and isolation against other running processes  
+  (provided by [`runexec`](https://github.com/sosy-lab/benchexec/blob/main/doc/runexec.md),
+  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
-- generation of interactive tables and plots for the results
+  and automatically executing them on large sets of input files  
+  (provided by [`benchexec`](https://github.com/sosy-lab/benchexec/blob/main/doc/benchexec.md)
+  on top of `runexec`)
+- generation of interactive tables and plots for the results  
+  (provided by [`table-generator`](https://github.com/sosy-lab/benchexec/blob/main/doc/table-generator.md)
+  for results produced with `benchexec`)
 
 
 Unlike other benchmarking frameworks,
@@ -51,13 +67,19 @@ 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.
+More information on why this is necessary and the problems with other tools
+can be found in our paper
+[Reliable Benchmarking: Requirements and Solutions](https://doi.org/10.1007/s10009-017-0469-y) (open access)
+and our [slides](https://www.sosy-lab.org/research/prs/Latest_ReliableBenchmarking.pdf)
+(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 verify that the result of the tool was as expected,
+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

doc/INDEX.md

@@ -11,9 +11,11 @@ SPDX-License-Identifier: Apache-2.0
 
 BenchExec consists of three programs:
 
-- `benchexec`: main benchmarking utility
-- `table-generator`: for generating result tables
-- `runexec`: for benchmarking a single tool execution (can also be integrated into other benchmarking frameworks)
+- `benchexec`: main benchmarking utility, especially for large sets of benchmark runs
+- `table-generator`: for generating result tables from `benchexec` results
+- `runexec`: for benchmarking a single tool execution as a simple replacement for `time`
+  with better measurement accuracy and more features,
+  or for integrating into other benchmarking frameworks and scripts
 
 The documentation for BenchExec is available in the following files:
 

doc/INSTALL.md

@@ -332,12 +332,15 @@ or whether additional settings are necessary as [described below](#testing-cgrou
 
 If you want to run BenchExec inside a container,
 we recommend Podman and systems with cgroups v2.
-Then pass `--security-opt unmask=/sys/fs/cgroup` to `podman run`.
+Then use the following command-line arguments:
+
+    podman run --security-opt unmask=/sys/fs/cgroup --cgroups=split ...
+
 This will work if BenchExec is the main process inside the container,
 otherwise you need to create an appropriate cgroup hierarchy inside the container,
 i.e., one where BenchExec has its own separate cgroup.
 
-For other cases, if the cgroups file system is not available within the container,
+For other cases, e.g., with cgroups v1,
 please use the following command line argument
 to mount the cgroup hierarchy within the container when starting it
 (same for Podman):

doc/runexec.md

@@ -13,7 +13,7 @@ SPDX-License-Identifier: Apache-2.0
 BenchExec provides a program called `runexec` that can be used to
 easily execute a single command while measuring its resource consumption,
 similarly to the tool `time` but with more reliable time measurements
-and with measurement of memory usage.
+and with more features such measurement of memory usage as well as resource limits.
 To use it, simply pass as parameters the command that should be executed
 (adding `--` before the command will ensure that the arguments to the command
 will not be misinterpreted as arguments to `runexec`):

doc/table-generator.md

@@ -10,7 +10,8 @@ SPDX-License-Identifier: Apache-2.0
 # BenchExec: table-generator
 ## Generating Tables of Results
 
-The program `table-generator` allows to generate HTML and CSV tables.
+The program `table-generator` allows to generate HTML and CSV tables
+from results produced with [`benchexec`](benchexec.md).
 You can have a look at a
 [demo table](https://sosy-lab.github.io/benchexec/example-table/svcomp-simple-cbmc-cpachecker.table.html)
 to see how the result looks like.