Fri 21 Jan 2022 16:40 - 17:05 at Salon I - Verification 2 Chair(s): Jonathan Protzenko

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.

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:40 - 17:30
Verification 2POPL at Salon I
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
16:40
25m
Research paper
Verified Tensor-Program Optimization Via High-Level Scheduling RewritesRemote
POPL
Amanda Liu Massachusetts Institute of Technology, Gilbert Bernstein University of California at Berkeley, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
DOI Media Attached
17:05
25m
Research paper
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding ModesDistinguished PaperRemote
POPL
Jay P. Lim Rutgers University, Santosh Nagarakatte Rutgers University
DOI Media Attached