Universal High-Performance CFL-Reachability via Matrix Multiplication
summary
FastMatrixCFPQ implements a universal, matrix-based CFL-reachability solver built on SuiteSparse:GraphBLAS that uses delta-matrix multiplication, boolean decomposition into per-symbol bitmatrices, batched block multiplications, dual row/column formats and partial-merge accumulation. Benchmarks on C/C++/Java program graphs and five client analyses show it often speeds up universal solvers by orders of magnitude and in many cases outperforms specialized tools, eliminating many 3‑hour timeouts; correctness matches other solvers and geometric-mean memory use drops about 30% less memory.
AI-written summary · about
chapters (20)
- 0:00Introduction
- 0:22CFL-reachability overview
- 1:04Value flow with sparse graphs
- 2:29Context-free constraints
- 3:13Simplifying grammar rules
- 4:16Reachability to linear algebra
- 5:21Matrix-based CFL baseline
- 6:26Matrix CPQ performance
- 7:29Slow convergence challenges
- 8:12Incremental matrix optimization
- 9:14Boolean matrix decomposition
- 10:39Batch optimizations
- 10:59Matrix format speed
- 11:41Sparse additions handling
- 12:43Grammar optimization
- 13:47Correctness results
- 14:30Future plans
- 15:13Q&A
- 16:17Q&A
- 18:43Q&A
related talks
18mCompiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels
21mMassive proofs for the masses
44mDraft SVP64 in-place Matrix Multiply and FFT / DCT
20mExploiting Sparsity and Redundancy
15mMat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free P...
14mFast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
18mLoop Fusion in Matrix Multiplications with Sparse Dependence
14mFast Linear Programming through Transprecision Computing on Small and Sparse Data