Strided Difference Bound Matrices
Arjun Pitchanathan, Albert Cohen, Oleksandr Zinenko, Tobias Grosser
TL;DR
This work introduces Strided Difference Bound Matrices (SDBMs), a sub-polyhedral domain that combines unit two-variable inequalities with single-variable congruences to capture relational constraints common in machine-code generation and ML compilers. It proves SDBM satisfiability is NP-hard but offers practical, pseudo-linear algorithms parameterized by the least common multiple of congruence divisors, and a tractable $O(n^4)$ algorithm for the HSDBM subcase. The authors develop a normalization framework and linear-time join/equality checks, enabling effective abstract-interpretation workflows. Empirical studies across MLIR, Polygeist, and PPCG demonstrate the prevalence and usefulness of SDBMs in real compiler pipelines, highlighting potential for accelerating verification and optimization tasks in practice.
Abstract
A wide range of symbolic analysis and optimization problems can be formalized using polyhedra. Sub-classes of polyhedra, also known as sub-polyhedral domains, are sought for their lower space and time complexity. We introduce the Strided Difference Bound Matrix (SDBM) domain, which represents a sweet spot in the context of optimizing compilers. Its expressiveness and efficient algorithms are particularly well suited to the construction of machine learning compilers. We present decision algorithms, abstract domain operators and computational complexity proofs for SDBM. We also conduct an empirical study with the MLIR compiler framework to validate the domain's practical applicability. We characterize a sub-class of SDBMs that frequently occurs in practice, and demonstrate even faster algorithms on this sub-class.