SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 11:40 - 12:00 at OOPSLA/ECOOP - F-3A
Fri 20 Nov 2020 23:40 - 00:00 at OOPSLA/ECOOP - F-3A

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.

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

11:00 - 12:20: F-3AOOPSLA at OOPSLA/ECOOP +12h
11:00 - 11:20
Talk
OOPSLA
Olivier FlückigerNortheastern University, USA, Guido ChariASAPP Inc, Ming-Ho YeeNortheastern University, Jan JecmenCzech Technical University, Jakob HainNortheastern University, Jan VitekNortheastern University
DOI Pre-print
11:20 - 11:40
Talk
OOPSLA
Magnus MadsenAarhus University, Ondřej LhotákUniversity of Waterloo
11:40 - 12:00
Talk
OOPSLA
Julie L. NewcombUniversity of California at Berkeley, Andrew AdamsAdobe, Steven JohnsonGoogle, Rastislav BodikUniversity of Washington, Shoaib KamilAdobe
12:00 - 12:20
Talk
OOPSLA
Magnus MadsenAarhus University, Jaco van de PolAarhus University
23:00 - 00:20: F-3AOOPSLA at OOPSLA/ECOOP
23:00 - 23:20
Talk
OOPSLA
Olivier FlückigerNortheastern University, USA, Guido ChariASAPP Inc, Ming-Ho YeeNortheastern University, Jan JecmenCzech Technical University, Jakob HainNortheastern University, Jan VitekNortheastern University
DOI Pre-print
23:20 - 23:40
Talk
OOPSLA
Magnus MadsenAarhus University, Ondřej LhotákUniversity of Waterloo
23:40 - 00:00
Talk
OOPSLA
Julie L. NewcombUniversity of California at Berkeley, Andrew AdamsAdobe, Steven JohnsonGoogle, Rastislav BodikUniversity of Washington, Shoaib KamilAdobe
00:00 - 00:20
Talk
OOPSLA
Magnus MadsenAarhus University, Jaco van de PolAarhus University