[stds-1788] New paper on correctness of compiler optimizations of floating-point arithmetic
Inasmuch as the underlying real floating-arithmetic architecture, and
compilers for it, affects implementations of interval arithmetic, this
new paper by two Stanford University researchers should be of interest
to list members:
@Article{Notzli:2016:LVP,
author = "Andres N{\"o}tzli and Fraser Brown",
title = "{LifeJacket}: Verifying precise floating-point
optimizations in {LLVM}",
journal = "arxiv.org",
volume = "??",
number = "??",
pages = "??--??",
day = "30",
month = mar,
year = "2016",
bibdate = "Sat Apr 2 06:26:03 2016",
bibsource = "http://www.math.utah.edu/pub/tex/bib/fparith.bib";,
URL = "http://arxiv.org/abs/1603.09290";,
abstract = "Optimizing floating-point arithmetic is vital because
it is ubiquitous, costly, and used in compute-heavy
workloads. Implementing precise optimizations
correctly, however, is difficult, since developers must
account for all the esoteric properties of
floating-point arithmetic to ensure that their
transformations do not alter the output of a program.
Manual reasoning is error prone and stifles
incorporation of new optimizations. We present an
approach to automate reasoning about floating-point
optimizations using satisfiability modulo theories
(SMT) solvers. We implement the approach in LifeJacket,
a system for automatically verifying precise
floating-point optimizations for the LLVM assembly
language. We have used LifeJacket to verify 43 LLVM
optimizations and to discover eight incorrect ones,
including three previously unreported problems.
LifeJacket is an open source extension of the Alive
system for optimization verification.",
acknowledgement = ack-nhfb,
}
-------------------------------------------------------------------------------
- Nelson H. F. Beebe Tel: +1 801 581 5254 -
- University of Utah FAX: +1 801 581 4148 -
- Department of Mathematics, 110 LCB Internet e-mail: beebe@xxxxxxxxxxxxx -
- 155 S 1400 E RM 233 beebe@xxxxxxx beebe@xxxxxxxxxxxx -
- Salt Lake City, UT 84112-0090, USA URL: http://www.math.utah.edu/~beebe/ -
-------------------------------------------------------------------------------