BenchExec 使用教程

1. 项目介绍

BenchExec 是一个用于在 Linux 系统上可靠地进行非交互式工具基准测试和资源测量的框架。它能够精确测量工具的 CPU 时间、墙钟时间和内存使用情况，并允许为这些资源设置限制。BenchExec 通过使用 Linux 内核的 cgroups 功能来正确处理进程组，确保即使在工具生成子进程的情况下也能可靠地测量和限制资源使用。

BenchExec 提供了三个主要功能：

• 执行任意命令，并精确可靠地测量和限制资源使用（如 CPU 时间和内存）。
• 定义具有特定工具配置和资源限制的基准测试，并自动在大规模输入文件上执行这些测试。
• 生成交互式表格和图表，用于结果的可视化。

2. 项目快速启动

安装 BenchExec

首先，确保你的系统满足 BenchExec 的依赖要求，包括 Python 3 和 cgroups。然后，可以通过以下命令安装 BenchExec：

pip install benchexec

运行基准测试

以下是一个简单的示例，展示如何使用 BenchExec 运行一个基准测试：

# 创建一个基准测试配置文件 example.xml
cat <<EOF > example.xml
<benchmark tool="mytool" common="true">
  <tasks>
    <include>input1.txt</include>
    <include>input2.txt</include>
  </tasks>
  <rundefinition id="default">
    <option name="--timeout">30</option>
    <option name="--memory">1024</option>
  </rundefinition>
</benchmark>
EOF

# 运行基准测试
benchexec example.xml

生成结果报告

BenchExec 会自动生成 CSV 和 HTML 格式的结果报告。你可以使用 table-generator 工具生成交互式 HTML 报告：

table-generator results/*.xml.bz2

3. 应用案例和最佳实践

应用案例

BenchExec 广泛应用于国际软件验证竞赛（SV-COMP）中，用于对各种工具进行基准测试。例如，CPAchecker 工具使用 BenchExec 进行回归测试和性能评估。

最佳实践

1. 资源限制设置：根据工具的实际需求设置合理的 CPU 时间和内存限制，避免资源浪费和测试不准确。
2. 输入文件管理：使用 <include> 标签管理输入文件，确保测试覆盖所有必要的场景。
3. 结果分析：利用 BenchExec 生成的交互式 HTML 报告，深入分析工具的性能瓶颈和改进点。

4. 典型生态项目

CPAchecker

CPAchecker 是一个开源的软件验证工具，广泛用于静态分析和模型检查。它与 BenchExec 紧密集成，用于性能评估和回归测试。

SMTInterpol

SMTInterpol 是一个高效的 SMT 求解器，使用 BenchExec 进行性能基准测试，确保其在不同输入下的稳定性和效率。

Ultimate

Ultimate 是一个用于软件验证和分析的工具集，通过 BenchExec 进行大规模基准测试，验证其功能和性能。

通过以上模块的介绍，你应该能够快速上手并深入使用 BenchExec 进行可靠的基准测试和资源测量。