一句话：提出每次更新 O(n·α(n)) 的动态双向 Dyck 可达性算法，用于即时静态分析并实现千倍加速。
静态分析常可归约为 Dyck 可达性，双向图则用于建模可变堆数据上的数据流，并是需求驱动指针/别名分析的常见形式。已有离线最优算法耗时为 O(m+n·α(n))，最坏 O(n^2)，难以应对源代码持续增删带来的在线更新。本文提出面向双向 Dyck 可达性的动态算法，每次更新的最坏时间复杂度为 O(n·α(n))，优于 O(n^2)，并在某些设置下达到最优。作者实现了该算法，在即时数据依赖与别名分析上，与最优离线算法和全动态 Datalog 求解器比较，性能始终最佳，取得约 1000 倍加速，单次更新耗时几乎不可察觉。
Dyck reachability is a principled, graph-based formulation of a plethora of static analyses. Bidirected graphs are used for capturing dataflow through mutable heap data, and are usual formalisms of demand-driven points-to and alias analyses. The best (offline) algorithm runs in O ( m + n · α ( n ) ) time, where n is the number of nodes and m is the number of edges in the flow graph, which becomes O ( n 2 ) in the worst case. In the everyday practice of program analysis, the analyzed code is subject to continuous change, with source code being added and removed. On-the-fly static analysis under such continuous updates gives rise to dynamic Dyck reachability , where reachability queries run on a dynamically changing graph, following program updates. Naturally, executing the offline algorithm in this online setting is inadequate, as the time required to process a single update is prohibitively large. In this work we develop a novel dynamic algorithm for bidirected Dyck reachability that has O ( n · α ( n ) ) worst-case performance per update, thus beating the O ( n 2 ) bound, and is also optimal in certain settings. We also implement our algorithm and evaluate its performance on on-the-fly data-dependence and alias analyses, and compare it with two best known alternatives, namely (i) the optimal offline algorithm, and (ii) a fully dynamic Datalog solver. Our experiments show that our dynamic algorithm is consistently, and by far, the top performing algorithm, exhibiting speedups in the order of 1000X. The running time of each update is almost always unnoticeable to the human eye, making it ideal for the on-the-fly analysis setting.
@article{paperbot2652,
title = {On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability},
author = {Shankaranarayanan Krishna and Aniket Lal and Andreas Pavlogiannis and Omkar Tuppe},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632884}
}