Taming Transitive Redundancy for Context-Free Language ReachabilityPre-recorded
Given an edge-labeled graph, context-free language reachability (CFL-reachability) computes reachable node pairs by deriving new edges and adding them to the graph. The redundancy that limits the scalability of CFL-reachability manifests as redundant derivations, i.e., identical edges can be derived multiple times due to the many paths between two reachable nodes. We observe that most redundancy arises from the derivations involving transitive relations of reachable node pairs. Unfortunately, existing techniques for reducing redundancy in transitive-closure-based problems are either ineffective or inapplicable to identifying and eliminating redundant derivations during on-the-fly CFL-reachability solving.
This paper proposes a scalable yet precision-preserving approach to all-pairs CFL-reachability analysis by taming its transitive redundancy.
Our key insight is that transitive relations are intrinsically ordered, and utilizing the order for edge derivation can avoid most redundancy.
To address the challenges in determining the derivation order from the dynamically changed graph during CFL-reachability solving, we introduce a hybrid graph representation by combining spanning trees and adjacency lists, together with a dynamic construction algorithm.
Based on this representation, we propose a fast and effective partially ordered algorithm POCR
to boost the performance of CFL-reachability analysis by reducing its transitive redundancy during on-the-fly solving.
Our experiments on context-sensitive value-flow analysis and field-sensitive alias analysis for C/C++ demonstrate the promising performance of POCR.
On average, POCR eliminates 98.50% and 97.26% redundant derivations respectively for the value-flow and alias analysis, achieving speedups of 21.48$\times$ and 19.57$\times$ over the standard CFL-reachability algorithm.
We also compare POCR with two recent open-source tools, Graspan (a CFL-reachability solver) and Souffl'e (a Datalog engine).
The results demonstrate that POCR is over 3.67$\times$ faster than Graspan and Souffl'e on average for both value-flow analysis and alias analysis.
Wed 30 NovDisplayed time zone: Auckland, Wellington change
21:00 - 22:45 | Session 2V-OOPSLA at Virtual Airmeet Room Chair(s): Sophia Drossopoulou Meta and Imperial College London | ||
21:00 15mTalk | Taming Transitive Redundancy for Context-Free Language ReachabilityPre-recorded V-OOPSLA Yuxiang Lei University of Technology Sydney, Yulei Sui University of New South Wales, Sydney, Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology DOI | ||
21:15 15mTalk | Scalable Linear Invariant Generation with Farkas’ Lemma V-OOPSLA Hongming Liu Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, zhiyong yu Shanghai Jiao Tong University, Jiaxin Song Shanghai Jiao Tong University, Guoqiang Li Shanghai Jiao Tong University DOI | ||
21:30 15mTalk | Consistency-Preserving Propagation for SMT Solving of Concurrent Program VerificationPre-recorded V-OOPSLA DOI | ||
21:45 15mTalk | Oracle-Free Repair Synthesis for Floating-Point ProgramsPre-recorded V-OOPSLA Daming Zou ETH Zurich, Yuchen Gu Peking University, Yuanfeng Shi Peking University, Mingzhe Wang Princeton University, Yingfei Xiong Peking University, Zhendong Su ETH Zurich DOI | ||
22:00 15mTalk | Neurosymbolic Repair for Low-Code Formula Languages V-OOPSLA Rohan Bavishi University of California at Berkeley, Harshit Joshi Microsoft, José Pablo Cambronero Microsoft, Anna Fariha Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Ivan Radiček Microsoft, Ashish Tiwari Microsoft DOI | ||
22:15 30mLive Q&A | Q&A for Session 2 V-OOPSLA | ||