A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
summary
Mechanized framework extends ATL and uses the Rock proof assistant to produce a verified compression/decompression adjoint that rewrites dense tensor kernels into sparse implementations. It formalizes a level-format abstraction and proves five concrete level instances (dense, compress/CSR-style, bitmask, hash, scalar), plus a compositional compressor so new formats need only local proofs. New iteration primitives scatter and co-iteration compile multi-operand sparse kernels, artifacts are available (DOI) and end-to-end evaluation shows throughput mostly comparable to TACO.
AI-written summary · about
chapters (10)
- 0:00Tensor program optimization
- 0:36Tensor operations in HPC
- 2:43ATL tensor programming language
- 6:33Extending ATL for sparse formats
- 9:43Parametric compression for sparse formats
- 12:06Level format abstraction
- 14:54Compositional sparse formats
- 16:19Performance vs Taco
- 17:41New ATL iteration constructs
- 18:02Q&A
related talks
28mFunctional Sparse Tensor Compilation
25mFormat Abstraction for Sparse Tensor Algebra Compilers
18mA Verified Compiler for a Functional Tensor Language
14mCompressed and Parallelized Structured Tensor Algebra
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
20mExploiting Sparsity and Redundancy
11mExtending the Scope of the Array Abstraction beyond Sparsity
19mCompiler Support for Sparse Tensor Convolutions