一句话:提出基于抽象解释的高阶环境共享分析并形式化,支持调用者提供环境以减少环境分配。
高阶语言中,函数表示包含代码与捕获自由变量的环境结构。本文研究“调用者提供环境”:不再由闭包打包全部环境,而允许调用者在调用点提供函数环境的一部分。由于高阶语言难以静态确定调用点及可用环境片段,作者提出一种新的基于抽象解释的分析,发现函数定义与调用者之间总是共享的环境片段,从而可由调用者传入。该分析在Rocq证明助手中形式化。对一组程序的评估表明,它可扩展,且比常见语法方法和轻量闭包转换提供更精确信息,许多程序上达到理论上界。论文还讨论如何避免额外运行时开销的变换决策,并通过插桩解释器评估,证明能有效减少环境动态分配。
The representation of functions in higher-order languages includes both the function’s code and an environment structure that captures the bindings of the function’s free variables. This paper explores caller-provided environments, where instead of packaging the entirety of a function’s environment in its closure, a function can be provided with a portion of its environment by its caller. In higher-order languages, it is difficult to determine where functions are called, let alone what pieces of the function’s environment are available to be provided by the caller, thus we need a higher-order control-flow analysis to enable caller-provided environments. In this paper, we present a new abstract-interpretation-based analysis that discovers which pieces of a function’s environment are always shared between its definition and its callers. In such cases, the caller can provide the environment to the callee. Our analysis has been formalized in the Rocq proof assistant. We evaluate our analysis on a collection of programs demonstrating that it is both scalable and provides significantly better information over the common syntactic approach and better information than lightweight closure conversion . In fact, it yields the theoretical upper-bound for many programs. For caller-provided environments, deciding how to transform the program based on these revealed facts is also non-trivial and has the potential to incur extra runtime cost over standard strategies. We discuss how to make these decisions in a way that avoids the extra costs and how to transform a program accordingly. We also propose other uses of the analysis results beyond enabling caller-provided environments. We evaluate our transformation using an instrumented interpreter, showing that our approach is effective in reducing dynamic allocations for environments.
@article{paperbot3031,
title = {Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages},
author = {J. A. Carr and Benjamin Quiring and John Reppy and Olin Shivers and Skye Soss and Byron Zhong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747516}
}