Mon 19 Jun 2023 09:20 - 09:40 at Royal - PLDI: Welcome & Opening Session Chair(s): Nate Foster

We introduce Mosaic, a sparse tensor algebra compiler that can bind tensor (sub-)expressions to external functions of other tensor algebra libraries or compilers. Users can extend Mosaic by adding new functions and can bind a sub-computation to a function using a scheduling API. Mosaic substitutes the bound(sub-)expressions with the specified function call and automatically fills in the rest of the unbound code using a default code generator. Mosaic also has a search system that can automatically map an expression to a set of registered external functions. Both the explicit binding and automatic search are verified by Mosaic. We demonstrate the benefits of our approach by showing that calling hand-written CPU and specialized hardware functions can provide speedup of up to 206x and 173x, respectively, over a homogeneous compiler. Mosaic’s external function interface is simple and general. Currently, 38 external functions have been added to Mosaic, with each addition averaging 20 lines of C++ code.

Mon 19 Jun

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

09:00 - 11:00
PLDI: Welcome & Opening SessionPLDI Research Papers at Royal
Chair(s): Nate Foster Cornell University

#pldi-mon-0900-opening-royal Discord icon small YouTube icon small

09:00
20m
Day opening
Welcome to PLDI
PLDI Research Papers
Steve Blackburn Google and Australian National University, Nate Foster Cornell University
09:20
20m
Talk
Mosaic: An Interoperable Compiler for Tensor AlgebraDistinguished Paper
PLDI Research Papers
Manya Bansal Stanford University, Olivia Hsu Stanford University, Kunle Olukotun Stanford University, Fredrik Kjolstad Stanford University
DOI
09:40
20m
Talk
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic PrimitivesDistinguished Paper
PLDI Research Papers
Joel Kuepper University of Adelaide, Andres Erbsen MIT, Jason Gross MIT CSAIL, Owen Conoly MIT, Chuyue Sun Stanford, Samuel Tian MIT, David Wu University of Adelaide, Adam Chlipala Massachusetts Institute of Technology, Chitchanok Chuengsatiansup The University of Melbourne, Daniel Genkin Georgia Tech, Markus Wagner Monash University, Australia, Yuval Yarom Ruhr University Bochum
DOI Pre-print
10:00
20m
Talk
Synthesizing MILP Constraints for Efficient and Robust OptimizationDistinguished Paper
PLDI Research Papers
Jingbo Wang University of Southern California, Aarti Gupta Princeton University, Chao Wang University of Southern California
DOI
10:20
20m
Talk
An Automata-Based Framework for Verification and Bug Hunting in Quantum CircuitsDistinguished Paper
PLDI Research Papers
Yu-Fang Chen Academia Sinica, Taiwan, Kai-Min Chung Academia Sinica, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin Academia Sinica, Wei-Lun Tsai Academia Sinica, Di-De Yen Academia Sinica
DOI
10:40
20m
Talk
Covering All the Bases: Type-Based Verification of Test Input GeneratorsDistinguished Paper
PLDI Research Papers
Zhe Zhou Purdue University, Ashish Mishra Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
DOI Pre-print