Towards a Compiler for Reals

TL;DR

This paper introduces Rosa, a source-to-source compiler that automatically synthesizes code with appropriate numerical data types by estimating errors in real-valued programs, aiding in safe and accurate scientific and embedded computations.

Contribution

The paper presents a unified, automated technique for numerical error estimation in floating-point and fixed-point arithmetic, handling nonlinearities and discontinuities.

Findings

Rosa effectively estimates errors in scientific computing benchmarks.

It balances accuracy and performance better than existing tools.

The approach supports nonlinear and discontinuous operations.

Abstract

Numerical software, common in scientific computing or embedded systems, inevitably uses an approximation of the real arithmetic in which most algorithms are designed. In many domains, roundoff errors are not the only source of inaccuracy and measurement and other input errors further increase the uncertainty of the computed results. Adequate tools are needed to help users select suitable approximations, especially for safety-critical applications. We present the source-to-source compiler Rosa which takes as input a real-valued program with error specifications and synthesizes code over an appropriate floating-point or fixed-point data type. The main challenge of such a compiler is a fully automated, sound and yet accurate enough numerical error estimation. We present a unified technique for floating-point and fixed-point arithmetic of various precisions which can handle nonlinear arithmetic, determine closed- form symbolic invariants for unbounded loops and quantify the effects of discontinuities on numerical errors. We evaluate Rosa on a number of benchmarks from scientific computing and embedded systems and, comparing it to state-of-the-art in automated error estimation, show it presents an interesting trade-off between accuracy and performance.