1.1k citations · 1.2k across the 14 of their papers we have counts for
9 papers · 1 filter
TensorRight: Automated Verification of Tensor Graph Rewrites
Jai Arora, Sirui Lu, Devansh Jain +9
Tensor compilers, essential for generating efficient code for deep learning models across various applications, employ tensor graph rewrites as one of the key optimizations. These…
Morello: Compiling Fast Neural Networks with Dynamic Programming and Spatial Compression
Samuel J. Kaufman, René Just, Rastislav Bodik
High-throughput neural network inference requires coordinating many optimization decisions, including parallel tiling, microkernel selection, and data layout. The product of these…
Synthesizing Analytical SQL Queries from Computation Demonstration
Xiangyu Zhou, Rastislav Bodik, Alvin Cheung +1
Analytical SQL is widely used in modern database applications and data analysis. However, its partitioning and grouping operators are challenging for novice users. Unfortunately, p…
Fireiron: A Scheduling Language for High-Performance Linear Algebra on GPUs
Bastian Hagedorn, Archibald Samuel Elliott, Henrik Barthels +2
Achieving high-performance GPU kernels requires optimizing algorithm implementations to the targeted GPU architecture. It is of utmost importance to fully use the compute and memor…
Visualization by Example
Chenglong Wang, Yu Feng, Rastislav Bodik +2
While visualizations play a crucial role in gaining insights from data, generating useful visualizations from a complex dataset is far from an easy task. Besides understanding the…
Using human-in-the-loop synthesis to author functional reactive programs
Julie L Newcomb, Rastislav Bodik
Programs that respond to asynchronous events are challenging to write; they are difficult to reason about and tricky to test and debug. Because these programs can have a huge space…
Bonsai: Synthesis-Based Reasoning for Type Systems
Kartik Chandra, Rastislav Bodik
We describe algorithms for symbolic reasoning about executable models of type systems, supporting three queries intended for designers of type systems. First, we check for type sou…
Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions
Grigory Fedyukovich, Rastislav Bodík
We present GraSSP, a novel approach to perform automated parallelization relying on recent advances in formal verification and synthesis. GraSSP augments an existing sequential pro…
SIMPL: A DSL for Automatic Specialization of Inference Algorithms
Rohin Shah, Emina Torlak, Rastislav Bodik
Inference algorithms in probabilistic programming languages (PPLs) can be thought of as interpreters, since an inference algorithm traverses a model given evidence to answer a quer…