paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis

用导数进行推导:优化高阶流分析的增量不动点
ICFP 8(ICFP)2024匹配度 3/10 · 论文属于程序分析与抽象解释中的基础优化工作,聚焦高阶流分析的增量不动点计算,理论形式化与工程实现兼具;但未涉及用户当前关注的 LLM/Agent、浮点程序分析或贝叶斯程序分析等交叉方向,也不是针对机器学习系统或 Agentic 程序的静态分析。引用 3 inbox
Benjamin Quiring, David Van Horn
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:提出静态与动态特化技术优化增量不动点计算,将高阶流分析加速56倍。

高效的程序分析实现依赖于增量求解不动点问题,这些解可视为底层分析函数的导数。然而,从程序语义系统推导高阶分析的方法(如抽象抽象机)并未阐明如何高效实现这些分析。本文探索优化导数计算的互补技术:静态特化(通过部分求值和重写)与动态特化(在不动点计算中跟踪依赖),从而得到高效的增量不动点。我们将这些优化应用于CPS λ演算的示例分析,并说明它们如何与可调优的基于工作集的优化不动点方法良好配合。在Standard ML语言的流分析上,该方法相比文献中现有的高阶分析不动点方法平均加速56倍。

问题
如何高效实现由程序语义推导出的高阶程序分析,特别是增量不动点计算。
方法
使用静态特化(部分求值与重写)和动态特化(跟踪不动点中的依赖)来优化导数计算,并与基于工作集的优化不动点方法结合。
评估
在Standard ML流分析上评估,相比现有高阶分析不动点方法平均加速56倍。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@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}
}