Name
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. |
Year | DOI | Venue |
|---|---|---|
2022 | 10.1145/3498717 | PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL |
Keywords | DocType | Volume |
formal verification, proof assistants, array programming, optimization | Journal | 6 |
Issue | Citations | PageRank |
POPL | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Amanda Liu | 1 | 0 | 0.34 |
| Gilbert Louis Bernstein | 2 | 0 | 0.68 |
| Adam Chlipala | 3 | 0 | 0.34 |
| Jonathan Ragan-Kelley | 4 | 0 | 0.34 |