The floating-point research community has developed many tools that
authors of numerical software can use to test, analyze, or improve their code.
They are listed here in alphabetical order and categorized into four general
types: 1) dynamic tools, 2) static
tools, 3) commercial tools, and 4)
miscellaneous. You can find tutorials for some of these
tools at fpanalysistools.org, and
many of the reduced-precision tools were compared in a
2020 survey by authors from
the Polytechnic University of Milan.
Tools on the list are not endorsed, and need not endorse or
support the FPTalks community. The list is intended to be
exhaustive.
Additionally, the
FPBench project
provides benchmarks,
compilers,
and standards for floating-point
research tools.
Dynamic Tools
- ADAPT
- ADAPT (Automatic Differentiation Applied to Precision Tuning) is a tool
developed by Mike Lam from JMU
and Harshitha Menon from LLNL. It
uses the reverse mode of algorithmic differentiation to determine how much
precision is needed in a program's inputs and intermediate results in order
to achieve a desired accuracy in its output, converting this information
into precision recommendations.
-
- AMP
- AMP (Automated Mixed Precision) is a tool developed by Ralph Nathan and
Daniel Sorin (Duke University)
for mixed-precision analysis. It begins with a single-precision version of a
program and uses a variety of metrics and heuristics to gradually raise certain
portions of the program to higher precision in order to achieve the desired
accuracy in the outputs.
-
- AMPT-GA
- AMPT-GA is a tool developed by a multi-institutional team for automated
source-level mixed-precision for GPU applications, combining various static and
dynamic analysis approaches.
-
- Atomu
- Atomu is a tool
developed by Daming Zou
(Peking University) that uses "atomic" condition numbers of individual
floating-point operations to estimate the introduced error. It also performs
an evolutionary search to find inputs that trigger the highest condition
number for each operation. The instrumentation portion of the tool is
implemented as an LLVM pass.
-
- CADNA / PROMISE
- CADNA (Control of Accuracy and Debugging for Numerical Applications)
estimates round-off errors by replacing floating-point arithmetic with
discrete stochastic arithmetic (DSA), essentially modeling error using
randomized rounding (up or down) instead of round-to-nearest-even. A tool
called PROMISE (PRecision OptiMISE) uses this technique to perform a
delta-debugging search and report mixed precisions for C and C++ programs.
-
- CRAFT
- CRAFT (Configurable Runtime Analysis for Floating-Point Tuning) was
originally a framework based on the Dyninst
binary analysis toolkit to perform various dynamic floating-point analyses,
including cancellation detection, dynamic range tracking, and automated
mixed-precision analysis. CRAFT can perform an automated search of a
program's instruction space, determining the level of precision necessary in
the result of each instruction to pass a user-provided verification routine
assuming all other operations are done in double precision. This gives a
general overview of the approximate precision requirements of the program,
providing insights and guidance for mixed-precision implementation.
-
- There is a branch of CRAFT by Andrew Shewmaker (OpenEye Scientific,
formerly LANL) that adds a new analysis mode for extracting histograms of
all floating-point values encountered during a program run. He has also been
building a variant of this tool based on SHVAL (described below).
-
- FloatSmith
- FloatSmith is an integration project that provides automated
source-to-source tuning and transformation of floating-point code for mixed
precision using three existing tools: 1) CRAFT, 2) ADAPT, and 3) TypeForge. The
primary search loop is guided by CRAFT and uses TypeForge to prototype
mixed-precision versions of an application. ADAPT results can optionally be used
to help narrow the search space, and there are a variety of options to customize
the search.
-
- FPDetect
- FPDetect is a tool from the University of Utah for synthesizing error
detectors for stencil applications. It begins with an offline phase where
affine analysis is used to tightly estimate the floating-point precision
preserved across computations for intervals of data points. This bound along
with an auxiliary direct evaluation technique is then utilized to
instantiate optimally situated detectors across the compute space when
executing online. Violations of this bound can be attributed with certainty
to errors such as soft-errors or logical bugs.
-
- FPDiff
- FPDiff is a tool by Jackson Vanover (UC Davis) that performs automated
differential testing on mathematical library source code, extracting
numerical function signatures, synthesizing drivers, creating equivalence
classes of synonymous functions, and executing tests to detect meaningful
numerical discrepancies between implementations.
-
- FPED
- FPED is a dynamic analysis that detects arithmetic expression errors
using MPFR and test set generation.
-
- FPGen
- FPGen is a tool by Hui Guo
(UC Davis) that uses symbolic execution to generate inputs that maximize numerical error,
finding more errors than S3FP or KLEE.
-
- fpPrecisionTuning
- fpPrecisionTuning is a combination of two Python tools (C2mpfr and
DistributedSearch) that together can be used to find mixed-precision versions
of C programs. Like CRAFT and Precimonious, this tool performs a search over
the mixed-precision search space using a user-given error bound, but this tool
uses MPFR and source code modification to simulate non-standard precisions. The
authors have applied this toolchain to a variety of examples from different
domains including fixed-precision computations on an FPGA.
-
- FPSpy
- FPSpy is a tool by Peter Dinda
(Northwestern) that uses several different forms of runtime analysis to
detect and measure various floating-point issues. It is implemented as an
LD_PRELOAD library and works on unmodified x64 executables,
monitoring floating-point exceptions and other events of interest to
report results with varying levels of granularity and overhead.
-
- GPU-FPtuner
- GPU-FPtuner is a mixed-precision autotuner for GPU applications, built
on top of the Rose compiler framework.
-
- GPUMixer
- GPUMixer is a tool written by a multi-institutional team for LLVM-based
mixed-precision analysis that is performance-focused, looking for potential
speedups first and then verifying their accuracy afterwards.
-
- Herbgrind
- Herbgrind is a dynamic analysis tool for binaries (built on Valgrind)
to help find the root cause of floating-point error in large programs.
-
- Herbie
- Herbie automatically improves the accuracy of floating-point
expressions. Herbie has been used to fix two bugs in
math.js, and it also provides a
web interface.
-
- The authors of Daisy and Herbie have worked together to
combine their tools:
-
- HiFPTuner
- HiFPTuner is an extension of Precimonious (see below) that uses dependence
analysis and edge profiling to enable a more efficient hierarchical search
algorithm for mixed-precision configurations.
-
- pLiner
- pLiner is a tool for automatically identifying code that will trigger
compiler-induced numerical variability. It works by combining selective
precision enhancements and a guided dynamic search, decreasing the amount
of time required to detect issues.
-
- PositDebug / FPSanitizer
- PositDebug and FPSanitizer are tools from the Rutgers Architecture and
Programming Languages group. Both use LLVM-based instrumentation and MPFR
shadow values to check Posit (the former) and regular floating-point code
(the latter). This approach is faster than the Valgrind-based
instrumentation used by Herbgrind.
-
- Precimonious
- Precimonious is a tool written by Cindy Rubio González (UC
Davis) that leverages the LLVM framework to tweak
variable declarations to build and prototype mixed-precision configurations.
-
- More recent work uses shadow value analysis to speed up the search.
-
- PyFloT
- PyFloT is a tool for mixed-precision tuning of applications using an
instruction-centric analysis that uses call stack information and temporal
locality to address the large scale of HPC scientific programs. PyFloT
supports applications written in a combination of Python, CUDA, C++, and
Fortran.
-
- Shaman
- Shaman is a library that uses operator overloading and error-free
transformations to track numerical error through computations by
replacing floating-point numbers with instrumented alternatives. It can
evaluate the number of significant digits of any floating-point number in
a computation and has been designed with a focus on high-performance
computing and simulation. It is compatible with mixed precision and
parallelism and does not interfere with the control flow of the program.
-
- SHVAL
- SHVAL (SHadow Value Analysis Library) is a tool by
Mike Lam that uses the
Intel Pin
instrumentation framework to perform full heavyweight shadow-value analysis for
floating-point arithmetic, effectively allowing developers to simulate any
real-numbered representation for which a plugin can be developed.
-
- This work was extended by Ramy Medhat (U. of Waterloo) to perform
per-address or per-instruction floating-point error analysis. Using this
framework, he developed several mixed-precision versions of an image processing
library, demonstrating how the tool can assist with making performance, energy,
and accuracy tradeoffs in the embedded domain.
-
- STOKE
- STOKE is a general stochastic
optimization and program synthesis tool from Stanford that has been extended
to handle floating-point computation. STOKE can trade off accuracy for
performance for floating-point computations.
-
- Verificarlo
- Verificarlo is a tool written by Pablo de
Oliveira Castro (Université de Versailles St-Quentin-en-Yvelines), Eric
Petit, and Christophe Denis (ENS Cachan). It leverages the LLVM
framework for automated Monte Carlo Arithmetic analysis.
-
- VeriTracer
- Verificarlo (see above) has been extended by Yohan Chatelain,
including the addition of contextual information as well as a temporal
visualization tool called VeriTracer.
-
- Verrou
- Verrou is a Valgrind-based tool written by François Févotte and others from
EDF in France. The tool can simulate choosing a random rounding mode for every
operation, and performs a delta debugging search to find areas of code that fail
a user-provided verification routine under this scheme. It can also use the
Verificarlo front-end (see above) for lower overhead.
-
Static Tools
- Alive / LifeJacket
- Alive verifies that LLVM IR optimizations don't change program
behavior, and includes support for floating-point instructions in
an extension named LifeJacket. LifeJacket has verified 43 LLVM
optimizations and discovered eight incorrect ones.
-
- Alive-NJ
- Alive-NJ verifies that LLVM IR optimizations don't change
program behavior, and includes support for floating-point
instructions. Alive-NJ has found five bugs in LLVM optimization
passes.
-
- cohd / syhd
- Laurent Thévenoux at LIP, ENS de Lyon has written tools for source-to-source
error compensation and synthesis of floating-point code.
-
- Daisy
- Daisy is another tool by Eva
Darulova (the author of Rosa, see below) that combines various types
of static and dynamic analysis of floating-point code and is designed to be
modular and extensible. Eva also has a paper with Anastasiia Izycheva on
computing sound relative errors. They find that this can produce much
tighter error bounds than analyzing absolute error, and an implementation is
included in Daisy. Finally, Eva has a paper with Einar Horn and Saksham
Sharma on mixed-precision tuning in Scala and C, which is also included in
Daisy.
-
- The authors of Daisy and Herbie have worked together to
combine their tools:
-
- dco / scorpio
- A group from CERTH & University of Thessaly and RWTH Aachen have written
a significance analysis system using a combination of interval arithmetic and
automatic differentiation.
-
- ESBMC
- The Efficient SMT-based Bounded Model Checker (ESBMC) is an SMT-based
model checker for single- and multi-threaded C/C++ programs with support for
floating-point arithmetic.
-
- Flocq
- Flocq is a floating-point formalization for Coq, written by
Sylvie Boldo and others. It provides a library of theorems for analyzing
arbitrary-precision floating-point arithmetic.
-
- FPhile
- Floating-point stability analysis via SMT solving and theorem proving.
-
- FPSyn
- FPSyn is an implementation of a floating-point predicate synthesis
technique that automatically derives an expression to calculate the
round-off error bound of the input computation.
-
- FPTaylor / FPTuner
- A group at the University of Utah describes a way of using partial
derivatives and symbolic Taylor series expansions to bound floating-point
roundoff error; this achieves much tighter bounds than interval/affine/SMT
methods. More recently, they have extended their work by performing a broad
comparison of many error bounding analyses.
-
- They have also built a mixed-precision tool for Python code based on this
technique. Note that it also requires the commercial
Gurobi Optimizer.
-
- Gappa
- Gappa helps automated reasoning about floating-point and
fixed-point arithmetic. It has been used to prove the CRlibm
implementations of elementary functions correct.
-
- moTuner
- moTuner is a framework built on LLVM for efficiently tuning
mixed-precision operators during compilation.
-
- POP
- POP (Precision OPtimizer) is a tool written by Dorra Ben Khalifa
(Laboratory of Mathematics and Physics, University of Perpignan Via Domitia)
that uses abstract interpretation to determine the minimal precision
required on inputs. The primary current contribution is the application of
these techniques to the Internet of Things (IoT) domain.
-
- PRECiSA / FPRoCK
- PRECiSA (Program Round-off Error Certifier via Static Analysis) is a
tool from the NIA and NASA that calculates symbolic error
bounds using the PVS language. The authors
also provide a web interface. More recently, the FPRoCK tool was written in
collaboration with authors at the University of Utah to solve mixed real and
floating-point programs, which improved the accuracy of PRECiSA.
-
- Real2Float
- Victor Magron and others present a framework for providing upper bounds on
absolute roundoff errors using semidefinite programming and sums of squares
certificates. The results can be checked using the Coq theorem prover.
-
- Rosa
- Rosa is a source-to-source translator written by Eva Darulova for the Scala language.
It uses an SMT solver to annotate a program with mixed-precision types.
-
- Salsa
- Salsa is an abstract-interpretation-based floating-point analysis tool that
suggests transformations to minimize floating-point error, and is the dissertation
work of Nasrine Damouche. The source code is not available.
-
- Satire
- Satire is a sound rounding error analysis and estimator that uses
several techniques like path strength reduction and bound optimization to
improve the scalability of static analysis. This analysis scales to hundreds
of thousands of operations.
-
- TAFFO
- TAFFO is an LLVM-based conversion and autotuning framework that tries
to replace floating-point operations with fixed-point operations to the
extent possible.
-
- VP Float
- VP Float is an extension of the C type system to represent
variable-precision floating-point arithmetic. The extension is built using
LLVM and has two backend code generators, one for a RISC-V coprocessor and one
for the GNU MPFR multi-precision library.
-
Commercial Tools
- Astrée
- Astrée is a commercial static analysis tool for proving the correctness
of C code, including all floating-point computation. It has been used to
prove the absence of runtime exceptions in flight control software for
Airbus planes.
-
- Fluctuat
- Fluctuat is a commercial, abstract-interpretation-based static analysis tool
for analyzing numerical code in C or Ada and characterizing the errors
caused by the approximation inherent in floating-point arithmetic. Fluctuat
has been used to verify safety-critical embedded systems. It was originally
written by Eric Goubault, Matthieu Martel, and Sylvie Putot.
-
- Numalis Software Suite
- Numalis Software Suite is a collection of several commercial tools for
static and dynamic analysis of floating-point code with the goal of
generating more accurate codes and making mixed-precision decisions,
targeted primarily at AI and neural network domains.
-
Miscellaneous
- CompCert
- CompCert is a compiler that has been formally verified to preserve
floating-point semantics using Coq.
-
- Fbench / Ffbench
- Fbench and Ffbench are two floating-point performance benchmarks by
John Walker (Fourmilab).
-
- FLiT: Floating-point Litmus Tests
- FLiT is a test infrastructure for detecting variability in floating-point
code due to differences in compilers and execution environments. It was
developed by Michael Bentley at the University of Utah.
-
- FPBench
- FPBench is a community benchmark project for floating-point examples.
-
- FPHPC Benchmark Suite
- This is a collection of programs containing floating-point arithmetic
with the immediate goal of aiding the development and evaluation of
floating-point precision and correctness analysis tools. The long-term goal
is to support and enable the scaling of such tools to provide insights for
high-performance computing (HPC) applications. This collection aims to
address the "middle ground" between real-valued expressions (such as those
contained in the FPBench collection) and full HPC applications.
-
- FPVM
- FPVM is a floating-point virtual machine proposed and prototyped by
Peter Dinda and others at Northwestern University. The goal is to allow an
existing application binary to be extended to support alternative
arithmetic systems. The current implementation combines static binary
analysis with trap-and-emulate execution.
-
- KLEE
- KLEE is a symbolic execution engine built on LLVM. One
fork
supports reasoning over floating-point constraints;
another, for numerical
precision analysis, has a
benchmark suite
of example programs.
-
- Posit libraries
- Posits are the newest iteration on
John Gustafson's Unum representation
(see below). Unlike Unums, Posits have a fixed overall width but the number
of exponent and significand bits varies according to a run-length-encoded
"regime" field. They provide higher accuracy and a greater dynamic range than
identically-sized IEEE formats.
-
- S3FP
- Another project from the University of Utah (see FPTaylor and FPTuner
above), S3FP is a tool for finding floating-point inputs that will maximize
error.
-
- SOAP
- SOAP (Structural Optimisation of Arithmetic Programs) is a tool for
optimizing FPGA-based implementations of floating-point code.
-
- Sollya
- Sollya is a library and environment for safe floating-point
development, specifically intended to aid the development of math
library functions.
-
- Unum library
- Unums ("universal numbers") are a novel binary representation for real
numbers by John Gustafson that exactly
quantifies the uncertainty of a stored value. It extends IEEE floating-point by
making both the exponent and significand fields variable-sized, and it adds an
"exact" bit that is set if the number is exact and unset if the number
represents a range between representable numbers. It provides a way to obtain
mathematically-rigorous results in numeric code at the cost of computational
efficiency.
-
- VFLOAT
- VFLOAT is a variable-precision floating-point library for FPGAs, developed
and maintained by Miriam Leeser at Northeastern University.
-
This list is primarily maintained for the FPTalks research community by
Mike Lam.
If you are developing or are maintaining a floating-point tool, or know of a
tool that isn't on the list, please
join and email the list.
