paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Iterative-Epoch Online Cycle Elimination for Context-Free Language Reachability

面向上下文无关语言可达性的迭代-纪元在线环消除
OOPSLA 8(OOPSLA1)2024匹配度 4/10 · 该论文研究 CFL-reachability 的在线环消除与静态分析加速,属于程序分析/抽象解释方向,具有理论形式化和工程评估;但它不涉及 LLM/Agent、机器学习系统、浮点程序分析或贝叶斯程序分析,与用户当前主攻的 PL↔AI 交叉问题没有直接关联。引用 3 inbox
Pei Xu, Yuxiang Lei, Yulei Sui, Jingling Xue
crossref: 2026-09-10

AI 速览

一句话:提出基于传递性符号的迭代-纪元在线环消除,动态压缩 CFL-可达性图并显著加速静态分析。

CFL-可达性是多种静态分析的基础,但其求解复杂度对图规模呈(次)立方级,且已有图简化多在预处理阶段进行,无法消除动态求解中才出现的可约简节点和边。本文提出在线环消除方法:由输入上下文无关文法识别传递性符号,据此发现可折叠的环,并给出迭代-纪元(iterative-epoch)框架,使其兼容标准无序求解器与最新有序求解器。在 C/C++ 上下文敏感值流分析和 Java 域敏感别名分析上,该技术显著加速并降低内存:标准求解器分别加速 17.17× 和 13.94×,内存减少 48.8% 和 45.0%;有序求解器分别加速 14.32× 和 8.36×,内存减少 55.2% 和 57.8%。

问题
CFL-可达性求解复杂度高,且现有图简化仅限预处理,无法在线消除动态求解过程中出现的可约简节点和边,限制其可扩展性。
方法
通过识别上下文无关文法中的传递性符号来检测可折叠环,提出迭代-纪元在线环消除框架,并与标准及有序 CFL-可达性求解器集成。
评估
在 C/C++ 上下文敏感值流分析和 Java 域敏感别名分析上进行实验,比较标准/有序求解器的加速比与内存缩减。
原文摘要(Abstract)

Context-free language reachability (CFL-reachability) is a fundamental framework for implementing various static analyses. CFL-reachability utilizes context-free grammar (CFG) to extend the expressiveness of ordinary graph reachability from an unlabeled graph to an edge-labeled graph. Solving CFL-reachability requires a (sub)cubic time complexity with respect to the graph size, which limits its scalability in practice. Thus, an approach that can effectively reduce the graph size while maintaining the reachability result is highly desirable. Most of the existing graph simplification techniques for CFL-reachability work during the preprocessing stage, i.e., before the dynamic CFL-reachability solving process. However, in real-world CFL-reachability analyses, there is a large number of reducible nodes and edges that can only be discovered during dynamic solving, leaving significant room for on-the-fly improvements. This paper aims to reduce the graph size of CFL-reachability dynamically via online cycle elimination. We propose a simple yet effective approach to detect collapsible cycles in the graph based on the input context-free grammar. Our key insight is that symbols with particular forms of production rules in the grammar are the essence of transitivity of reachability relations in the graph. Specifically, in the graph, a reachability relation to a node v_i can be "transited" to another node v_j if there is a transitive relation from v_i to v_j, and cycles formed by transitive relations are collapsible. In this paper, we present an approach to identify the transitive symbols in a context-free grammar and propose an iterative-epoch framework for online cycle elimination. From the perspective of non-parallelized CFL-reachability solving, our iterative-epoch framework is well compatible with both the standard (unordered) solver and the recent ordered solver, and can significantly improve their performance. Our experiment on context-sensitive value-flow analysis for C/C++ and field-sensitive alias analysis for Java demonstrates promising performance improvement by our iterative-epoch cycle elimination technique. By collapsing cycles online, our technique accelerates the standard solver by 17.17× and 13.94× for value-flow analysis and alias analysis, respectively, with memory reductions of 48.8% and 45.0%. Besides, our technique can also accelerate the ordered solver by 14.32× and 8.36× for value-flow analysis and alias analysis, respectively, with memory reductions of 55.2% and 57.8%.

链接与引用

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

BibTeX
@article{paperbot2567,
  title = {Iterative-Epoch Online Cycle Elimination for Context-Free Language Reachability},
  author = {Pei Xu and Yuxiang Lei and Yulei Sui and Jingling Xue},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA1},
  year = {2024},
  doi = {10.1145/3649862}
}