Verrou

Verrou helps you look for floating-point round-off errors in programs. It implements various forms of arithmetic, including:

all IEEE-754 standard rounding modes;
three variants of stochastic floating-point arithmetic based on random rounding: all floating-point operations are perturbed by randomly switching rounding modes. These can be seen as an asynchronous variant of the CESTAC method, or a subset of Monte Carlo Arithmetic, performing only output randomization through random rounding;
an emulation of single-precision rounding, in order to test the effect of reduced precision without any need to change the source code.

Verrou also comes with a verrou_dd utility, which simplifies the Verrou-based debugging process by implementing several variants of the Delta-Debugging algorithm. This allows easily locating which parts of the analyzed source code are likely to be responsible for Floating-Point-related instabilities.

The documentation for Verrou is available as a dedicated chapter in the Valgrind manual.

Installation

Get the sources

The preferred way to get Verrou sources is to download the latest stable version: v2.5.0. Older versions are available in the releases page. After downloading one of the released versions, skip to the "Configure and build" section below.

In order to build the development version of Verrou, it is necessary to first download a specific Valgrind version, and patch it. Fetch valgrind's sources:

git clone --branch=VALGRIND_3_24_0 --single-branch https://sourceware.org/git/valgrind.git valgrind-3.24.0+verrou-dev

Add verrou's sources to it:

cd valgrind-3.24.0+verrou-dev
git clone https://github.com/edf-hpc/verrou.git verrou

cat verrou/valgrind.*diff | patch -p1

Configure and build

First, install all required dependencies (the names of relevant Debian packages are put in parentheses as examples):

C & C++ compilers (build-essential),
autoconf & automake (automake),
Python 3 (python3)
C standard library with debugging symbols (libc6-dbg).

Configure valgrind:

./autogen.sh
./configure --enable-only64bit --prefix=PREFIX

Depending on your system, it may be required to set CFLAGS in order to enable the use of FMA in your compiler:

./configure --enable-only64bit --prefix=PREFIX CFLAGS="-mfma"

On systems that don't support FMA instructions the --enable-verrou-fma=no configure switch need to be used, but be aware that this causes some tests to fail:

./configure --enable-only64bit --enable-verrou-fma=no --prefix=PREFIX

Advanced users can use the following configure flags :

--enable-verrou-check-naninf=yes|no (default yes). If NaN does not appear in the verified code set this option to 'no' can slightly speed up verrou.
--with-det-hash=hash_name with hash_name in [dietzfelbinger,multiply_shift,double_tabulation,xxhash,mersenne_twister] to select the hash function used for [random|average]_[det|comdet] rounding mode. The default is xxhash. double_tabulation was the previous default(before introduction of xxhash). mersenne_twister is the reference but slow. dietzfelbinger and multiply_shift are faster but are not able to reproduce the reference results.
--with-verrou-denorm-hack=[none|float|double|all] (default float). With denormal number the EFT are no more necessary exact. With the average* rounding modes this problem is always ignored, but the random* rounding, there are the following available options : with none the problem is ignored. With float a hack based on computation in double is applied on float operations ; With double an experimental hack is applied for double operations ; With all the float and double hacks are applied. float is selected by default.
--enable-verrou-xoshiro=[no|yes] (default yes). If set to yes the tiny mersenne twister prng is replaced (for random, prandom and average) by the xo[ro]shiro prng.
--enable-verrou-quad=[yes|no] (default yes). If set to no the backend mcaquad is disabled. This option is only useful to reduce the dependencies.

Build and install:

make
make install

Load the environment

In order to actually use Verrou, you must load the correct environment. This can be done using:

source PREFIX/env.sh

Test (optional)

General tests

You can test the whole platform:

make check
perl tests/vg_regtest --all

or only verrou:

make -C tests check
make -C verrou check
perl tests/vg_regtest verrou

Specific tests

These tests are more closely related to the arithmetic part in Verrou:

make -C verrou/unitTest

Documentation

The documentation for verrou is available as a chapter in valgrind's manual.

You can also re-build it:

make -C docs html-docs man-pages

and browse it locally:

firefox docs/html/vr-manual.html

Beware, this requires lots of tools which are not necessarily tested for in configure, including (but not necessarily limited to):

xsltproc
docbook-xsl

Bibliography & References

The following papers explain in more details the internals of Verrou, as well as some of its applications. If you use Verrou for a research work, please consider citing one of these references:

François Févotte and Bruno Lathuilière. Debugging and optimization of HPC programs with the Verrou tool. In International Workshop on Software Correctness for HPC Applications (Correctness), Denver, CO, USA, Nov. 2019. DOI: 10.1109/Correctness49594.2019.00006
Hadrien Grasland, François Févotte, Bruno Lathuilière, and David Chamont. Floating-point profiling of ACTS using Verrou. EPJ Web Conf., 214, 2019. DOI: 10.1051/epjconf/201921405025
François Févotte and Bruno Lathuilière. Studying the numerical quality of an industrial computing code: A case study on code_aster. In 10th International Workshop on Numerical Software Verification (NSV), pages 61--80, Heidelberg, Germany, July 2017. DOI: 10.1007/978-3-319-63501-9_5
François Févotte and Bruno Lathuilière. VERROU: a CESTAC evaluation without recompilation. In International Symposium on Scientific Computing, Computer Arithmetics and Verified Numerics (SCAN), Uppsala, Sweden, September 2016.

(These references are also available in bibtex format)