一句话：提出用路径表达式与整数线性规划求解单源单目标 InterDyck 可达性，避免传统汇总边并显著加速。
交错 Dyck（InterDyck）语言由多个平衡括号语言交错而成，InterDyck 可达性是同时跟踪调用/返回、加锁/解锁等成对动作的程序分析框架。本文针对单源单目标变体，用路径表达式概括源到目标路径，将可达性转化为路径表达式识别问题，再表达为括号计数问题，从而用整数线性规划（ILP）求解，无需传统汇总边。作者实现算法并在并发可达性与污点分析上评估：相较全对 LCL、SPDS 和领域专用工具，并发分析最高加速 28.24×，污点分析最高加速 69.9×，并提升精度（污点分析最高提升 11.1%）。
An interleaved-Dyck (InterDyck) language consists of the interleaving of two or more Dyck languages, where each Dyck language represents a set of strings of balanced parentheses.InterDyck-reachability is a fundamental framework for program analyzers that simultaneously track multiple properly-matched pairs of actions such as call/return, lock/unlock, or write-data/read-data.Existing InterDyck-reachability algorithms are based on the well-known tabulation technique. This paper presents a new perspective on solving InterDyck-reachability. Our key observation is that for the single-source-single-target InterDyck-reachability variant, it is feasible to summarize all paths from the source node to the target node based on path expressions . Therefore, InterDyck-reachability becomes an InterDyck-path-recognition problem over path expressions. Instead of computing summary edges as in traditional tabulation algorithms, this new perspective enables us to express InterDyck-reachability as a parenthesis-counting problem, which can be naturally formulated via integer linear programming (ILP). We implemented our ILP-based algorithm and performed extensive evaluations based on two client analyses (a reachability analysis for concurrent programs and a taint analysis). In particular, we evaluated our algorithm against two types of algorithms: (1) the general all-pairs InterDyck-reachability algorithms based on linear conjunctive language (LCL) reachability and synchronized pushdown system (SPDS) reachability, and (2) two domain-specific algorithms for both client analyses. The experimental results are encouraging. Our algorithm achieves 1.42×, 28.24×, and 11.76× speedup for the concurrency-analysis benchmarks compared to all-pair LCL-reachability, SPDS-reachability, and domain-specific tools, respectively; 1.2×, 69.9×, and 0.98× speedup for the taint-analysis benchmarks. Moreover, the algorithm also provides precision improvements, particularly for taint analysis, where it achieves 4.55%, 11.1%, and 6.8% improvement, respectively.
@article{paperbot2116,
title = {Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming},
author = {Yuanbo Li and Qirun Zhang and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571228}
}