SATune: A Study-Driven Auto-Tuning Approach for Configurable Software Verification Tools
SATune: A Study-Driven Auto-Tuning Approach for Configurable Software Verification Tools
复制标题
DOI：
10.1109/ase51524.2021.9678761
复制
发表时间：
2021-11
期刊：
影响因子：
--
通讯作者：
Ugur Koc;Austin Mordahl;Shiyi Wei;J. Foster;A. Porter
中科院分区：
文献类型：
--
作者：
Ugur Koc;Austin Mordahl;Shiyi Wei;J. Foster;A. Porter
许多程序验证工具可以通过运行时配置选项来定制，以兑现性能，精度和健全性。但是，实际上，用户经常在其默认配置下运行工具，因为了解这些权衡需要大量的专业知识。在本文中，我们询问单个默认配置一般可以运行的效果，并提出了一种新颖的工具，该工具用于自动为给定的目标程序配置程序验证工具。为了回答我们的问题，我们收集了一个数据集，该数据集运行了四个众所周知的程序验证工具，可针对C和Java基准测试，结果标记为正确，错误或不确定（例如超时）。在检查数据集时，我们发现通常没有一定大小的最佳配置。此外，统计分析表明，许多单独的配置选项并不具有简单的权衡：根据程序的不同或更糟。通过这些结果激发，我们开发了SANUNE，我们开发了使用Meta-Heuristic搜索来构建配置。搜索是由在我们的数据集上训练的替代健身功能的指导。我们将SASUNE的性能与三个基线的性能进行比较：单个配置在我们数据集中具有最正确的结果；最精确的配置，然后是最正确的配置（如果需要的话）；以及最精确的配置，然后是随机搜索（如果需要的话）。我们发现，通过以高精度完成更正确的任务，Sanune优于这些方法。总而言之，我们的工作表明，良好的验证工具配置并不简单，而SASUNE朝着自动化寻找它们的过程迈出了重要一步。
Many program verification tools can be customized via run-time configuration options that trade off performance, precision, and soundness. However, in practice, users often run tools under their default configurations, because understanding these tradeoffs requires significant expertise. In this paper, we ask how well a single, default configuration can work in general, and we propose SATune, a novel tool for automatically configuring program verification tools for given target programs. To answer our question, we gathered a dataset that runs four well-known program verification tools against a range of C and Java benchmarks, with results labeled as correct, incorrect, or inconclusive (e.g., timeout). Examining the dataset, we find there is generally no one-size-fits-all best configuration. Moreover, a statistical analysis shows that many individual configuration options do not have simple tradeoffs: they can be better or worse depending on the program.Motivated by these results, we developed SATune, which constructs configurations using a meta-heuristic search. The search is guided by a surrogate fitness function trained on our dataset. We compare the performance of SATune to three baselines: a single configuration with the most correct results in our dataset; the most precise configuration followed by the most correct configuration (if needed); and the most precise configuration followed by random search (also if needed). We find that SATune outperforms these approaches by completing more correct tasks with high precision. In summary, our work shows that good configurations for verification tools are not simple to find, and SATune takes an important step towards automating the process of finding them.