利用透明大页面向更快的推理器迈进
计算机科学中的逻辑
2020-04-30 v1 人工智能
性能
摘要
各种最先进的自动化推理（AR）工具被广泛用作知识表示与推理研究以及工业应用中的后端工具。在测试与验证中，这些工具经常连续或夜间运行。本文中，我们提出一种方法，使 AR 工具的平均运行时间减少 10%，对长时间运行任务最多减少 20%。我们的改进针对基于冲突驱动 no-good 学习的 AR 工具所使用数据结构带来的高内存占用。我们建立了一种通用方法，通过更有效地利用现代硬件的内存缓存行来实现更快的内存访问。为此，我们扩展了标准 C 库（glibc），动态允许使用称为大页面（huge pages）的内存管理特性。大页面允许减少在操作系统虚拟内存与硬件物理内存之间转换内存地址所需的开销。以此方式，我们仅需在编译时将工具链接到这一新 glibc 库，即可降低具有类似内存访问模式的 AR 工具及应用的运行时间、成本与能耗。在日常工业应用中，这轻易实现更环保的计算。为佐证所声称的加速，我们给出了 AR 社区常用工具的实验结果，包括 ASP、BMC、MaxSAT、SAT 和 SMT 领域。
引用
@article{arxiv.2004.14378,
title = {Towards Faster Reasoners By Using Transparent Huge Pages},
author = {Johannes K. Fichte and Norbert Manthey and Julian Stecklina and André Schidler},
journal= {arXiv preprint arXiv:2004.14378},
year = {2020}
}