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): Ramy Shahin, Hidehiko Masuhara

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
Times are displayed in time zone: Central Time (US & Canada) change

11:00 - 12:20
F-3AOOPSLA at SPLASH-I +12h
Chair(s): Stefan MarrUniversity of Kent, Reuben RoweUniversity College London
11:00
20m
Talk
Contextual Dispatch for Function Specialization
OOPSLA
Olivier FlückigerNortheastern University, Guido ChariAsapp, Ming-Ho YeeNortheastern University, Jan JečmenCzech Technical University, Jakob HainNortheastern University, Jan VitekNortheastern 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 MadsenAarhus University, Ondřej LhotákUniversity 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. NewcombUniversity of Washington, Andrew AdamsAdobe Research, Steven JohnsonGoogle, Rastislav BodikUniversity of Washington, Shoaib KamilAdobe Research
Link to publication DOI Media Attached
12:00
20m
Talk
Polymorphic Types and Effects with Boolean Unification
OOPSLA
Magnus MadsenAarhus University, Jaco van de PolAarhus University
Link to publication DOI Media Attached
23:00 - 00:20
F-3AOOPSLA at SPLASH-I
Chair(s): Ramy ShahinUniversity of Toronto, Hidehiko MasuharaTokyo Institute of Technology
23:00
20m
Talk
Contextual Dispatch for Function Specialization
OOPSLA
Olivier FlückigerNortheastern University, Guido ChariAsapp, Ming-Ho YeeNortheastern University, Jan JečmenCzech Technical University, Jakob HainNortheastern University, Jan VitekNortheastern 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 MadsenAarhus University, Ondřej LhotákUniversity 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. NewcombUniversity of Washington, Andrew AdamsAdobe Research, Steven JohnsonGoogle, Rastislav BodikUniversity of Washington, Shoaib KamilAdobe Research
Link to publication DOI Media Attached
00:00
20m
Talk
Polymorphic Types and Effects with Boolean Unification
OOPSLA
Magnus MadsenAarhus University, Jaco van de PolAarhus University
Link to publication DOI Media Attached