Floating-point data types are a natural choice for software developers when implementing numerical computations. They are widely used in computer science and engineering, including in cyber-physical systems that interact with the physical world. Unfortunately, floating-point numbers do not exactly represent real values and thus can suffer from roundoff errors. Further, their non-intuitive nature can make it hard to predict when and how these errors accumulate to the extent that they invalidate the final result. Thus, it is important to provide guarantees (i.e, sound floating-point arithmetic) and do so fast for any given input.
We introduce IGen, a source-to-source compiler that translates a numerical program performing floating-point computations to an equivalent sound numerical program using interval arithmetic. By sound we mean that the resulting intervals are guaranteed to contain the result of the original program if it were performed using real arithmetic.
The picture below provides an overview of IGen’s internal structure. The input is a C function, possibly using SIMD intrinsics, performing floating-point computations and a target precision for the interval endpoints. This target precision can be either single or double precision (the default) or the higher double-double precision. The output is an equivalent C function performing the same computation soundly using interval arithmetic, optionally optimized with SIMD intrinsics.
IGen uses the Clang LibTooling library to construct the abstract syntax tree (AST) of the computation. The AST is then traversed and, for each node, an equivalent set of interval operations is generated, possibly in increased precision. The support of SIMD intrinsics in the input function is handled by a generator that automatically produces the interval implementation of (a large subset of) SIMD intrinsics from its XML specification. Finally, IGen uses Polly and a transformation technique to improve the accuracy of the common reduction pattern in linear-algebra-like computations.
We evaluated IGen on an Intel Xeon E-2176M CPU (Coffee Lake microarchitecture) running at 2.7 GHz, under Ubuntu 18.04 with Linux kernel v4.15. Turbo Boost is disabled. All tests are compiled using gcc 7.5 with flags -O3 -march=host. To evaluate performance, we use RDTSC to measure the cycle count for each test, performing 30 repetitions with warm cache, and using the median as a result. The accuracy of an interval is determined as the number of most-significant bits shared by the mantissas of the endpoints assuming same exponent.
For each benchmark, IGen generates interval code with the following configurations:
- IGen-ss: scalar code generated from scalar input code.
- IGen-sv: vectorized code (SSE) from scalar input code.
- IGen-vv: vectorized code (AVX) from vectorized code.
- IGen-sv-dd: as IGen-sv but with double-double precision output.
Performance. The figures below show the performance of IGen and other interval libraries for a set of benchmarks. The problem size is on the x-axis and the interval operations (iops) per cycle on the y-axis. Here, an interval multiplication and an addition count as one operation each.
Real performance and accuracy. The plots below show the real performance of IGen-vv (left) and its accuracy (right) when using double and double-double precision. Using double-double can keep error accumulation small enough to compute certified double precision results, i.e., results with at most one bit of error in double precision.
Accuracy of reductions. The figure below shows the gain in accuracy when using reduction transformations in a double-loop matrix-vector multiplication (mvm) benchmark. The results show an improvement between 3 and 13 bits depending on the size of the reduction.
Test $(s,p)$ means an input vector of size $n = 10^s$, where $p\%$ of the inputs are negative numbers. Arrows start from the accuracy of the interval program without reduction improvement and point to the generated accuracy with reduction improvement.
1. Joao Rivera, Franz Franchetti, Markus Püschel
An Interval Compiler for Sound Floating-Point Computations
in Proc. Code Generation and Optimization (CGO), pp. 52-64, 2021