一句话:提出静态与动态特化技术优化增量不动点计算,将高阶流分析加速56倍。
高效的程序分析实现依赖于增量求解不动点问题,这些解可视为底层分析函数的导数。然而,从程序语义系统推导高阶分析的方法(如抽象抽象机)并未阐明如何高效实现这些分析。本文探索优化导数计算的互补技术:静态特化(通过部分求值和重写)与动态特化(在不动点计算中跟踪依赖),从而得到高效的增量不动点。我们将这些优化应用于CPS λ演算的示例分析,并说明它们如何与可调优的基于工作集的优化不动点方法良好配合。在Standard ML语言的流分析上,该方法相比文献中现有的高阶分析不动点方法平均加速56倍。
Attheheartofefficientprogramanalysisimplementationsareincrementalsolutionstofixpointproblems.These solutions can be interpreted as the derivative of the underlying analysis function. Methods that describe how to systematically derive higher-order analyses from program semantics, such as Abstracting Abstract Machines, don’t shed light on how to efficiently implement those analyses. In this paper, we explore complementary techniques to optimize the derivative computation towards deriving efficient implementations. In particular, we use static specializations (by partial evaluation and rewriting) and dynamic specializations (in the form of tracking dependencies during the fixpoint), yielding efficient incremental fixpoints. We present how these optimizations apply to an example analysis of continuation-passing-style 𝜆-calculus, and describe how they pair particularly well with tunable and optimized workset-based fixpoint methods. We demonstrate the efficacy of this approach on a flow analysis for the Standard ML language, yielding an average speed-up of 56x over an existing fixpoint method for higher-order analyses from the literature.
@article{QuiringH24,
title = {Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis},
author = {Benjamin Quiring and David Van Horn},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674650}
}