SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 11:40 - 12:00 at SPLASH-I - F-3A Chair(s): Stefan Marr, Reuben Rowe
Fri 20 Nov 2020 23:40 - 00:00 at SPLASH-I - F-3A Chair(s): Hidehiko Masuhara, Ramy Shahin

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, while operating over the undecidable theory of integers. 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 in order to craft new, provably correct rules from failure cases where the compiler was unable to prove properties. We identify and fix 4 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.

Fri 20 Nov

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

11:00 - 12:20
F-3AOOPSLA at SPLASH-I +12h
Chair(s): Stefan Marr University of Kent, Reuben Rowe University College London
11:00
20m
Talk
Contextual Dispatch for Function Specialization
OOPSLA
Olivier Flückiger Northeastern University, Guido Chari Asapp, Ming-Ho Yee Northeastern University, Jan Ječmen Czech Technical University, Jakob Hain Northeastern University, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Pre-print Media Attached
11:20
20m
Talk
Fixpoints for the Masses: Programming with First-Class Datalog Constraints
OOPSLA
Magnus Madsen Aarhus University, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached
11:40
20m
Talk
Verifying and Improving Halide’s Term Rewriting System with Program Synthesis
OOPSLA
Julie L. Newcomb University of Washington, Andrew Adams Adobe Research, Steven Johnson Google, Rastislav Bodik University of Washington, Shoaib Kamil Adobe Research
Link to publication DOI Media Attached
12:00
20m
Talk
Polymorphic Types and Effects with Boolean Unification
OOPSLA
Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University
Link to publication DOI Media Attached
23:00 - 00:20
F-3AOOPSLA at SPLASH-I
Chair(s): Hidehiko Masuhara Tokyo Institute of Technology, Ramy Shahin University of Toronto
23:00
20m
Talk
Contextual Dispatch for Function Specialization
OOPSLA
Olivier Flückiger Northeastern University, Guido Chari Asapp, Ming-Ho Yee Northeastern University, Jan Ječmen Czech Technical University, Jakob Hain Northeastern University, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Pre-print Media Attached
23:20
20m
Talk
Fixpoints for the Masses: Programming with First-Class Datalog Constraints
OOPSLA
Magnus Madsen Aarhus University, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached
23:40
20m
Talk
Verifying and Improving Halide’s Term Rewriting System with Program Synthesis
OOPSLA
Julie L. Newcomb University of Washington, Andrew Adams Adobe Research, Steven Johnson Google, Rastislav Bodik University of Washington, Shoaib Kamil Adobe Research
Link to publication DOI Media Attached
00:00
20m
Talk
Polymorphic Types and Effects with Boolean Unification
OOPSLA
Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University
Link to publication DOI Media Attached