Title: Sound Mixed-Precision Optimization with Rewriting,
Abstract: Finite-precision arithmetic computations face an inherent tradeoff between
accuracy and efficiency. The points in this tradeoff space are determined,
among other factors, by different data types but also evaluation orders. To put
it simply, the shorter a precision's bit-length, the larger the roundoff error
will be, but the faster the program will run. Similarly, the fewer arithmetic
operations the program performs, the faster it will run; however, the effect on
the roundoff error is less clear-cut. Manually optimizing the efficiency of
finite-precision programs while ensuring that results remain accurate enough is
challenging. The unintuitive and discrete nature of finite-precision makes
estimation of roundoff errors difficult; furthermore the space of possible data
types and evaluation orders is prohibitively large. We present the first fully
automated and sound technique and tool for optimizing the performance of
floating-point and fixed-point arithmetic kernels. Our technique combines
rewriting and mixed-precision tuning. Rewriting searches through different
evaluation orders to find one which minimizes the roundoff error at no
additional runtime cost. Mixed-precision tuning assigns different finite
precisions to different variables and operations and thus provides
finer-grained control than uniform precision. We show that when these two
techniques are designed and applied together, they can provide higher
performance improvements than each alone.