Skip to content

Commit

Permalink
Tweak advertisement and connections between tools in documentation
Browse files Browse the repository at this point in the history
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 <[email protected]>
  • Loading branch information
PhilippWendler and incaseoftrouble committed May 21, 2024
1 parent 624357c commit 48cfd9b
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 9 deletions.
26 changes: 21 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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
Expand Down
7 changes: 4 additions & 3 deletions doc/INDEX.md
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down
3 changes: 2 additions & 1 deletion doc/table-generator.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 48cfd9b

Please sign in to comment.