Efficient algorithms for dynamic bidirected Dyck-reachability
Yuanbo Li, Kris Satya, Qirun Zhang
Abstract
Dyck-reachability is a fundamental formulation for program analysis, which has been widely used to capture properly-matched-parenthesis program properties such as function calls/returns and field writes/reads. Bidirected Dyck-reachability is a relaxation of Dyck-reachability on bidirected graphs where each edge ๐ข ๐ -โ ๐ฃ labeled by an open parenthesis " ๐ " is accompanied with an inverse edge ๐ฃ ๐ -โ ๐ข labeled by the corresponding close parenthesis " ๐ ", and vice versa. In practice, many client analyses such as alias analysis adopt the bidirected Dyck-reachability formulation. Bidirected Dyck-reachability admits an optimal reachability algorithm. Specifically, given a graph with ๐ nodes and ๐ edges, the optimal bidirected Dyck-reachability algorithm computes all-pairs reachability information in ๐ (๐) time.
This paper focuses on the dynamic version of bidirected Dyck-reachability. In particular, we consider the problem of maintaining all-pairs Dyck-reachability information in bidirected graphs under a sequence of edge insertions and deletions. Dynamic bidirected Dyck-reachability can formulate many program analysis problems in the presence of code changes. Unfortunately, solving dynamic graph reachability problems is challenging. For example, even for maintaining transitive closure, the fastest deterministic dynamic algorithm requires ๐ (๐ 2 ) update time to achieve ๐ (1) query time. All-pairs Dyck-reachability is a generalization of transitive closure. Despite extensive research on incremental computation, there is no algorithmic development on dynamic graph algorithms for program analysis with worst-case guarantees.
Our work fills the gap and proposes the first dynamic algorithm for Dyck reachability on bidirected graphs. Our dynamic algorithms can handle each graph update (i.e., edge insertion and deletion) in ๐ (๐ โข ๐ผ (๐)) time and support any all-pairs reachability query in ๐ (1) time, where ๐ผ (๐) is the inverse Ackermann function. We have implemented and evaluated our dynamic algorithm on an alias analysis and a context-sensitive datadependence analysis for Java. We compare our dynamic algorithms against a straightforward approach based on the ๐ (๐)-time optimal bidirected Dyck-reachability algorithm and a recent incremental Datalog solver. Experimental results show that our algorithm achieves orders of magnitude speedup over both approaches.
CCS Concepts: โข Theory of computation โ Dynamic graph algorithms; โข Software and its engineering โ Automated static analysis.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers6
- On-the-Fly Static Analysis via Dynamic Bidirected Dyck ReachabilityShankaranarayanan Krishna, Aniket Lal, Andreas Pavlogiannis, Omkar TuppePOPL 2024 ยท 7 citations
- Two Birds with One Stone: Multi-Derivation for Fast Context-Free Language Reachability AnalysisChenghang Shi, Haofeng Li, Yulei Sui, Jie Lu et al.ASE 2023 ยท 6 citations
- Boosting the Performance of Alias-Aware IFDS Analysis with CFL-Based Environment TransformersHaofeng Li, Chenghang Shi, Jie Lu, Lian Li et al.OOPSLA 2024 ยท 6 citations
- Bounded Treewidth, Multiple Context-Free Grammars, and Downward ClosuresC. Aiswarya, Pascal Baumann, Prakash Saivasan, Lia Schรผtze et al.POPL 2026 ยท 1 citation
- FlowLog: Efficient and Extensible Datalog via IncrementalityHangdong Zhao, Zhenghong Yu, Srinag Rao, Simon Frisk et al.VLDB 2026
Builds on4
- Incremental whole-program analysis in Datalog with latticesTamรกs Szabรณ, Sebastian Erdweg, Gรกbor BergmannPLDI 2021 ยท 39 citations
- Fast graph simplification for interleaved Dyck-reachabilityYuanbo Li, Qirun Zhang, Thomas W. RepsPLDI 2020 ยท 30 citations
- A systematic approach to deriving incremental type checkersAndrรฉ Pacak, Sebastian Erdweg, Tamรกs SzabรณOOPSLA 2020 ยท 16 citations
- On-the-Fly Static Analysis via Dynamic Bidirected Dyck ReachabilityShankaranarayanan Krishna, Aniket Lal, Andreas Pavlogiannis, Omkar TuppePOPL 2024 ยท 7 citations
Related papers
- On the complexity of bidirected interleaved Dyck-reachabilityYuanbo Li, Qirun Zhang, Thomas W. RepsPOPL 2021 ยท 12 citations
- Indexing the extended Dyck-CFL reachability for context-sensitive program analysisQingkai Shi, Yongchao Wang, Peisen Yao, Charles ZhangOOPSLA 2022 ยท 11 citations
- The decidability and complexity of interleaved bidirected Dyck reachabilityAdam Husted Kjelstrรธm, Andreas PavlogiannisPOPL 2022 ยท 17 citations
- Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear ProgrammingYuanbo Li, Qirun Zhang, Thomas W. RepsPOPL 2023 ยท 6 citations
- Taming transitive redundancy for context-free language reachabilityYuxiang Lei, Yulei Sui, Shuo Ding, Qirun ZhangOOPSLA 2022 ยท 16 citations
