167 citations · 494 across the 20 of their papers we have counts for
14 papers · 1 filter
When Double Rounding is Correct
Brett Saiki, Bill Zorn, Cynthia Richey +1
Number libraries, which implement number formats and their arithmetic in software, are used to simulate hardware, making hardware behavior reproducible and thus verifiable and easi…
Efficient Extraction for Effectful E-Graphs
Oliver Flatt, Anjali Pal, Yihong Zhang +7
Egraphs have enabled recent advances in program optimization, synthesis, and verification, yet remain difficult to apply to effectful programs whose memory and I/O operations must…
Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators
Akash Gaonkar, Mike He, Yi Li +8
To meet the performance needs of modern machine learning (ML) applications, ML compiler frameworks support compiler-to-accelerator mappings that offload parts of application code t…
Target-Aware Implementation of Real Expressions
Brett Saiki, Jackson Brough, Jonas Regehr +5
New low-precision accelerators, vector instruction sets, and library functions make maximizing accuracy and performance of numerical code increasingly challenging. Two lines of wor…
Generate Compilers from Hardware Models!
Gus Henry Smith, Ben Kushigian, Vishal Canumalla +3
Compiler backends should be automatically generated from hardware design language (HDL) models of the hardware they target. Generating compiler components directly from HDL can pro…
Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey +2
Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification…
Pure Tensor Program Rewriting via Access Patterns (Representation Pearl)
Gus Henry Smith, Andrew Liu, Steven Lyubomirsky +5
Tensor kernels in machine learning (ML) often correspond to pure mathematical expressions, making term rewriting an attractive strategy for optimization and mapping to specialized…
Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference
Haichen Shen, Jared Roesch, Zhi Chen +6
Modern deep neural networks increasingly make use of features such as dynamic control flow, data structures and dynamic tensor shapes. Existing deep learning systems focus on optim…
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang +3
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a mor…
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi, Max Willsey, Adam Anderson +4
Recent program synthesis techniques help users customize CAD models(e.g., for 3D printing) by decompiling low-level triangle meshes to Constructive Solid Geometry (CSG) expressions…
Relay: A New IR for Machine Learning Frameworks
Jared Roesch, Steven Lyubomirsky, Logan Weber +4
Machine learning powers diverse services in industry including search, translation, recommendation systems, and security. The scale and importance of these models require that they…
Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Pancheckha, Eva Darulova +1
Recent renewed interest in optimizing and analyzing floating-point programs has lead to a diverse array of new tools for numerical programs. These tools are often complementary, ea…
Finding Root Causes of Floating Point Error with Herbgrind
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner +1
Floating-point arithmetic plays a central role in science, engineering, and finance by enabling developers to approximate real arithmetic. To address numerical issues in large floa…
Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock +1
Optimizations in a traditional compiler are applied sequentially, with each optimization destructively modifying the program to produce a transformed program that is then passed to…