Strided Difference Bound Matrices

TL;DR

The paper introduces the Strided Difference Bound Matrix (SDBM) domain, a new polyhedral sub-class optimized for machine learning compiler tasks, with efficient algorithms validated through empirical studies.

Contribution

It presents the SDBM domain, decision algorithms, and complexity proofs, along with empirical validation and optimized algorithms for common sub-classes.

Findings

SDBM effectively models sub-polyhedral domains in compilers.

Empirical validation shows practical applicability in MLIR.

Faster algorithms for frequently occurring sub-classes.

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.