Conditionally correct superoptimization
Abstract
The aggressive optimization of heavily used kernels is an important problem in high-performance computing. However, both general purpose compilers and highly specialized tools such as superoptimizers often do not have sufficient static knowledge of restrictions on program inputs that could be exploited to produce the very best code. For many applications, the best possible code is conditionally correct: the optimized kernel is equal to the code that it replaces only under certain preconditions on the kernel's inputs. The main technical challenge in producing conditionally correct optimizations is in obtaining non-trivial and useful conditions and proving conditional equivalence formally in the presence of loops. We combine abstract interpretation, decision procedures, and testing to yield a verification strategy that can address both of these problems. This approach yields a superoptimizer for x86 that in our experiments produces binaries that are often multiple times faster than those produced by production compilers.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 23, 2015
- Source ID
- 10.1145/2858965.2814278
Entities
People
- Alex Aiken
- Berkeley Churchill
- Eric Schkufza
- Rahul Sharma
Organizations
- Defense Advanced Research Projects Agency
- Microsoft Research
- National Science Foundation
- Stanford University