Tweak advertisement and connections between tools in documentation

We want to make it clear that BenchExec is not only benchexec
and one can use runexec on its own as a replacement for time.
This is not mentioned in the README and also not prominently
in the documentation, and has led to misunderstandings
about BenchExec in the past.

In particular, we want to advertise runexec for users
who already have their own benchmarking scripts,
while still advertising benchexec as the main and recommended solution
in general for most users.
For this it seems useful to make the connections
between the tools more explicit in the documentation.

This commit is an outcome of the discussion in #1031
and implements a part of what is suggested in #999 and #1031.

Co-authored-by: Tobias Meggendorfer <tobias@meggendorfer.de>

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,
@@ -63,7 +79,7 @@ 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,10 @@ 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`,
+ or for integrating into other benchmarking frameworks and scripts
 
 The documentation for BenchExec is available in the following files:
 

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.