SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 16:25 - 16:40 at Zurich G - OOPSLA 2020 Papers 3 Chair(s): Anders Miltner

Halide is a domain-specific language for high-performance image processing and tensor computations, widely adopted in industry. Internally, the Halide compiler relies on a term rewriting system to prove properties of code required for efficient and correct compilation. This rewrite system is a collection of handwritten transformation rules that incrementally rewrite expressions into simpler forms; the system requires high performance in both time and memory usage to keep compile times low. In this work, we apply formal techniques to prove the correctness of existing rewrite rules and provide a guarantee of termination. Then, we build an automatic program synthesis system that operates over the undecidable theory of integers in order to craft new, provably correct rules from failure cases where the compiler was unable to prove properties. We identify and fix 5 incorrect rules as well as 8 rules which could give rise to infinite rewriting loops. We demonstrate that the synthesizer can produce better rules than hand-authored ones in five bug fixes, and describe four cases in which it has served as an assistant to a human compiler engineer. We further show that it can proactively improve weaknesses in the compiler by synthesizing a large number of rules without human supervision and showing that the enhanced ruleset lowers peak memory usage of compiled code without appreciably increasing compilation times.

Wed 20 Oct

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

15:40 - 17:00
OOPSLA 2020 Papers 3SIGPLAN Papers at Zurich G
Chair(s): Anders Miltner The University of Texas at Austin, Texas, USA
15:40
15m
Talk
DynamiTe: Dynamic Termination and Non-termination Proofs
SIGPLAN Papers
Ton Chanh Le Stevens Institute of Technology, Timos Antonopoulos Yale University, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, ThanhVu Nguyen George Mason University
15:55
15m
Talk
TacTok: Semantics-Aware Proof Synthesis
SIGPLAN Papers
Emily First University of Massachusetts at Amherst, Yuriy Brun University of Massachusetts Amherst, Arjun Guha Northeastern University
Link to publication DOI Pre-print
16:10
15m
Talk
Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic
SIGPLAN Papers
Xiaohong Chen University of Illinois at Urbana-Champaign, Minh-Thai Trinh Advanced Digital Sciences Center, Nishant Rodrigues University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
16:25
15m
Talk
Verifying and Improving Halide’s Term Rewriting System with Program Synthesis
SIGPLAN Papers
Julie L. Newcomb University of Washington, Andrew Adams Adobe, Steven Johnson Google, Rastislav Bodik University of Washington, Shoaib Kamil Adobe Research
16:40
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers