A tool for automatic Montecarlo Arithmetic analysis.
A docker image is available at https://hub.docker.com/r/verificarlo/verificarlo/. This image uses the latest git master version of Verificarlo and includes support for Fortran. It uses llvm-3.5 and gcc-4.7.
Example of usage:
$ cat > test.c <<HERE
#include <stdio.h>
int main() {
double a = 0;
for (int i=0; i < 10000; i++) a += 0.1;
printf("%0.17f\n", a);
return 0;
}
HERE
$ docker pull verificarlo/verificarlo
$ docker run -v "$PWD":/workdir verificarlo/verificarlo \
verificarlo test.c -o test
$ docker run -v "$PWD":/workdir -e VFC_BACKENDS="libinterflop_mca.so" \
verificarlo/verificarlo ./test
999.99999999999795364
$ docker run -v "$PWD":/workdir -e VFC_BACKENDS="libinterflop_mca.so" \
verificarlo/verificarlo ./test
999.99999999999761258Please ensure that Verificarlo's dependencies are installed on your system:
- GNU mpfr library http://www.mpfr.org/
- LLVM, clang and opt from 3.3 up to 4.0.1 (the last version with Fortran support is 3.6), http://clang.llvm.org/
- gcc, gfortran and dragonegg (for Fortran support), http://dragonegg.llvm.org/
- python3 and NumPy
- autotools (automake, autoconf)
Then run the following command inside verificarlo directory:
$ ./autogen.sh
$ ./configure
$ make
$ sudo make installIf you do not care about Fortran support, you can avoid installing gfortran and
dragonegg, by passing the option --without-dragonegg to configure:
$ ./autogen.sh
$ ./configure --without-dragonegg
$ make
$ sudo make installIf needed LLVM path, dragonegg path, and gcc path can be configured with the following options:
$ ./configure --with-llvm=<path to llvm install directory> \
--with-dragonegg=<path to dragonegg.so> \
CC=<gcc binary compatible with installed dragonegg>Once installation is over, we recommend that you run the test suite to ensure verificarlo works as expected on your system:
$ make installcheckIf you disable dragonegg support during configure, fortran_test will fail.
For example on an x86_64 Ubuntu 14.04 release, you should use the following install procedure:
$ sudo apt-get install libmpfr-dev clang-3.3 llvm-3.3-dev dragonegg-4.7 \
gcc-4.7 gfortran-4.7 autoconf automake build-essential python3 python3-numpy
$ cd verificarlo/
$ ./autogen.sh
$ ./configure \
--with-dragonegg=/usr/lib/gcc/x86_64-linux-gnu/4.7/plugin/dragonegg.so \
CC=gcc-4.7
$ make
$ sudo make installIn order to use the delta debug features, you need to export the path of the corresponding python packages. For example, for a global install, this would resemble (edit for your installed Python version):
$ export PYTHONPATH=${PYTHONPATH}:/usr/local/lib/pythonXXX.XXX/site-packagesYou can then check if your install was successful using:
$ make installcheckAlternatively, you can make the changes required for ddebug permanent by editing your ~/.bashrc, ~/.profile or whichever configuration file is relevant for your system by adding the above line, and then reloading your environment using:
$ source ~/.bashrcTo automatically instrument a program with Verificarlo you must compile it using
the verificarlo command. First make sure that the verificarlo installation
directory is in your PATH.
Then you can use the verificarlo command to compile your programs. Either modify
your makefile to use verificarlo as the compiler (CC=verificarlo and
FC=verificarlo ) and linker (LD=verificarlo) or use the verificarlo command
directly:
$ verificarlo *.c *.f90 -o ./programIf you are trying to compile a shared library, such as those built by the Cython
extension to Python, you can then also set the shared linker environment variable
(LDSHARED='verificarlo -shared') to enable position-independent linking.
When invoked with the --verbose flag, verificarlo provides detailed output of
the instrumentation process.
It is important to include the necessary link flags if you use extra libraries.
For example, you should include -lm if you are linking against the math
library and include -lstdc++ if you use functions in the standard C++
library.
Once your program is compiled with Verificarlo, it can be instrumented with different floating-point backends. At least one backend must be selected when running your application,
$ verificarlo *.c -o program
$ ./program
program: VFC_BACKENDS is empty, at least one backend should be providedBackends are distributed as dynamic libraries. They are loaded with the
environment variable VFC_BACKENDS.
$ VFC_BACKENDS="libinterflop_mca.so" ./programMultiple backends can be loaded at the same time; they will be chained in the
order of appearance in the VFC_BACKENDS variable. They must be separated with
semi-colons,
$ VFC_BACKENDS="libinterflop_ieee.so; libinterflop_mca.so" ./program"Finally backends options can be configured by passing command line arguments after each backend,
$ VFC_BACKENDS="libinterflop_ieee.so --debug; \
libinterflop_mca.so --precision 10 --mode rr" \
./program"The IEEE backend implements straighforward IEEE-754 arithmetic. It should have no effect on the output and behavior of your program.
The options --debug and --debug_binary enable verbose output that print
every instrumented floating-point operation.
VFC_BACKENDS="libinterflop_ieee.so --help" ./test
test: verificarlo loaded backend libinterflop_ieee.so
Usage: libinterflop_ieee.so [OPTION...]
-b, --debug_binary enable binary debug output
-d, --debug enable debug output
-?, --help Give this help list
--usage Give a short usage message
VFC_BACKENDS="libinterflop_ieee.so --debug" ./test
test: verificarlo loaded backend libinterflop_ieee.so
interflop_ieee 1.23457e-05 - 9.87654e+12 -> -9.87654e+12
interflop_ieee 1.23457e-05 * 9.87654e+12 -> 1.21933e+08
interflop_ieee 1.23457e-05 / 9.87654e+12 -> 1.25e-18
...The MCA backends implements Montecarlo Arithmetic. It uses quad types to compute MCA operations on doubles and the double type to compute MCA operations on floats. It is much faster than the MCA-MPFR backend, but it is recent and still experimental.
VFC_BACKENDS="libinterflop_mca.so --help" ./test
test: verificarlo loaded backend libinterflop_mca.so
Usage: libinterflop_mca.so [OPTION...]
-m, --mode=MODE select MCA mode among {ieee, mca, pb, rr}
-p, --precision=PRECISION select precision (PRECISION >= 0)
-s, --seed=SEED fix the random generator seed
-?, --help Give this help list
--usage Give a short usage message
Two options control the behavior of the MCA backend.
The option --mode=MODE controls the arithmetic error mode. It accepts the
following case insensitive values:
mca: (default mode) Montecarlo Arithmetic with inbound and outbound errorsieee: the program uses standard IEEE arithmetic, no errors are introducedpb: Precision Bounding inbound errors onlyrr: Random Rounding outbound errors only
The option --precision=PRECISION controls the virtual precision used for the
floating point operations. It accepts an integer value that represents the
virtual precision at which MCA operations are performed. Its default value is
53. For a more precise definition of the virtual precision, you can refer to
https://hal.archives-ouvertes.fr/hal-01192668.
One should note when using the QUAD backend, that the round operations during MCA computation always use round-to-zero mode.
In Random Round mode, the exact operations in given virtual precision are preserved.
The option --seed fixes the random generator seed. It should not generally be used
except if one to reproduce a particular MCA trace.
The MCA-MPFR backends is an alternative and slower implementation of Montecarlo Arithmetic. It uses the GNU multiple precision library to compute MCA operations. It is heavily based on mcalib MPFR backend.
MCA-MPFR backend accepts the same options than the MCA backend.
If you only wish to instrument a specific function in your program, use the
--function option:
$ verificarlo *.c -o ./program --function=specificfunctionFor more complex scenarios, a white-list / black-list mechanism is also
available through the options --include-file INCLUSION-FILE and
--exclude-file EXCLUSION-FILE.
INCLUSION-FILE and EXCLUSION-FILE are files specifying which modules and
functions should be included or excluded from Verificarlo instrumentation.
Each line has a module name followed by a function name. Both the module or
function name can be replaced by the wildcard *. Empty lines or lines
starting with # are ignored.
# include.txt
# this inclusion file will instrument f1 in main.c and util.c, and instrument
# f2 in util.c everything else will be excluded.
main f1
util f1
util f2
# exclude.txt
# this exclusion file will exclude f3 from all modules and all functions in
# module3.c
* f3
module3 *
Inclusion and exclusion files can be used together, in that case inclusion takes precedence over inclusion.
The tests/ directory contains various examples of Verificarlo usage.
A tutorial in english and french is available.
The postprocessing/ directory contains postprocessing tools to compute floating
point accuracy information from a set of verificarlo generated outputs.
For now we only have a VTK postprocessing tool vfc-vtk.py which takes multiple
VTK outputs generated with verificarlo and generates a single VTK set of files that
is enriched with accuracy information for each floating point DataArray.
For more information about vfc-vtk.py, please use the online help:
$ postprocess/vfc-vtk.py --helpIt is possible to use Verificarlo to detect branches that are unstable due to
numerical errors. To detect unstable branches we rely on
llvm-cov coverage reports.
To activate coverage mode in verificarlo, you should use the --coverage flag.
This is demonstrated in
tests/test_unstable_branches/;
the idea first introduced by verrou, is to
compare coverage reports between multiple IEEE executions and multiple MCA
executions.
Branches that are unstable only under MCA noise, are identified as numerically unstable.
Verificarlo can instrument floating point comparison operations. By default,
comparison operations are not instrumented and default backends do not make use of
this feature. If your backend requires instrumenting floating point comparisons, you
must call verificarlo with the --inst-fcmp flag.
If you use Verificarlo in your research, please cite the following paper:
@inproceedings{verificarlo,
author = {Christophe Denis and
Pablo de Oliveira Castro and
Eric Petit},
title = {Verificarlo: Checking Floating Point Accuracy through Monte Carlo
Arithmetic},
booktitle = {23nd {IEEE} Symposium on Computer Arithmetic, {ARITH} 2016, Silicon
Valley, CA, USA, July 10-13, 2016},
pages = {55--62},
year = {2016},
url = {http://dx.doi.org/10.1109/ARITH.2016.31},
doi = {10.1109/ARITH.2016.31},
}
A preprint is available at https://hal.archives-ouvertes.fr/hal-01192668/file/verificarlo-preprint.pdf.
Thanks !
For questions, feedbacks or discussions about Verificarlo you can join our group at,
https://groups.google.com/forum/#!forum/verificarlo
Copyright (c) 2019 Verificarlo Contributors
Copyright (c) 2018 Universite de Versailles St-Quentin-en-Yvelines
Copyright (c) 2015 Universite de Versailles St-Quentin-en-Yvelines CMLA, Ecole Normale Superieure de Cachan
Verificarlo is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.
Verificarlo is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with Verificarlo. If not, see http://www.gnu.org/licenses/.