Verified tensor-program optimization via high-level scheduling rewrites
Abstract
We present a lightweight Coq framework for optimizing tensor kernels written in a pure, functional array language. Optimizations rely on user scheduling using series of verified, semantics-preserving rewrites. Unusually for compilation targeting imperative code with arrays and nested loops, all rewrites are source-to-source within a purely functional language. Our language comprises a set of core constructs for expressing high-level computation detail and a set of what we call reshape operators, which can be derived from core constructs but trigger low-level decisions about storage patterns and ordering. We demonstrate that not only is this system capable of deriving the optimizations of existing state-of-the-art languages like Halide and generating comparably performant code, it is also able to schedule a family of useful program transformations beyond what is reachable in Halide.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 12, 2022
- Source ID
- 10.1145/3498717
Entities
People
- Adam Chlipala
- Amanda Liu
- Gilbert Louis Bernstein
- Jonathan Ragan-Kelley
Organizations
- Defense Advanced Research Projects Agency
- Massachusetts Institute of Technology
- National Science Foundation
- University of California, Berkeley