Finding Code That Explodes under Symbolic Evaluation
Finding Code That Explodes under Symbolic Evaluation
复制标题
DOI：
10.1145/3276519
复制
发表时间：
2018-11-01
影响因子：
1.8
通讯作者：
Torlak, Emina
中科院分区：
文献类型：
--
作者：
Bornholt, James;Torlak, Emina
求解器辅助工具依赖于符号评估，以减少编程任务，如验证和综合，可满足性查询。许多可重复使用的符号求值引擎现在可以作为求解器辅助语言和框架的一部分，这使得广大程序员可以创建并将求解器辅助工具应用于新的领域。但是，为了解决现实世界中的问题，程序员仍然需要编写有效利用底层引擎的代码，并了解他们的代码需要精心设计以获得最佳性能的地方。这一任务是困难的所有路径的执行模型的符号评估，这违背了人类的直觉和标准profilingtechniques.本文提出了符号profiling，一种新的方法来识别和诊断性能瓶颈的程序符号评估。为了帮助诊断，我们在求解器辅助代码中开发了一个常见性能反模式目录。为了定位这些瓶颈，我们开发了SymPro，一种新的分析技术的符号评估。SymPro通过分析每个符号计算引擎核心的两个隐含资源来识别瓶颈：符号堆和符号计算图。这些资源形成了一种新的符号评估性能模型，它是通用的（包括所有形式的符号评估），可解释的（为程序员提供理解符号评估的概念框架）和可操作的（实现瓶颈的精确定位）。性能求解器辅助代码仔细管理这些隐式结构的形状; SymPro使他们的演变明确的programer.To评估SymPro，我们实现的Rosette求解器辅助语言和Jalangi程序分析框架的剖析器。将SymPro应用于15个已发布的求解器辅助工具，我们发现了8个以前未诊断的性能问题。修复这些问题可以将性能提高几个数量级，并且我们的补丁被工具的开发人员接受。我们还与Rosette程序员进行了一项小型用户研究，发现SymPro可以帮助他们理解符号评估器正在做什么，并识别他们无法找到的性能问题。
Solver-aided tools rely on symbolic evaluation to reduce programming tasks, such as verification and synthesis, to satisfiability queries. Many reusable symbolic evaluation engines are now available as part of solver-aided languages and frameworks, which have made it possible for a broad population of programmers to create and apply solver-aided tools to new domains. But to achieve results for real-world problems, programmers still need to write code that makes effective use of the underlying engine, and understand where their code needs careful design to elicit the best performance. This task is made difficult by the all-paths execution model of symbolic evaluators, which defies both human intuition and standard profiling techniques.This paper presents symbolic profiling, a new approach to identifying and diagnosing performance bottlenecks in programs under symbolic evaluation. To help with diagnosis, we develop a catalog of common performance anti-patterns in solver-aided code. To locate these bottlenecks, we develop SymPro, a new profiling technique for symbolic evaluation. SymPro identifies bottlenecks by analyzing two implicit resources at the core of every symbolic evaluation engine: the symbolic heap and symbolic evaluation graph. These resources form a novel performance model of symbolic evaluation that is general (encompassing all forms of symbolic evaluation), explainable (providing programmers with a conceptual framework for understanding symbolic evaluation), and actionable (enabling precise localization of bottlenecks). Performant solver-aided code carefully manages the shape of these implicit structures; SymPro makes their evolution explicit to the programmer.To evaluate SymPro, we implement profilers for the Rosette solver-aided language and the Jalangi program analysis framework. Applying SymPro to 15 published solver-aided tools, we discover 8 previously undiagnosed performance issues. Repairing these issues improves performance by orders of magnitude, and our patches were accepted by the tools' developers. We also conduct a small user study with Rosette programmers, finding that SymPro helps them both understand what the symbolic evaluator is doing and identify performance issues they could not otherwise locate.