Verificarlo v0.4.2
A tool for debugging and assessing floating point precision and reproducibility.
- Installation
- Using Verificarlo through its Docker image
- Usage
- Branch instrumentation
- Examples and Tutorial
- Backends
- Delta Debug and inclusion / exclusion options
- VPREC Function instrumentation
- Postprocessing
- How to cite Verificarlo
- Discussion Group
- License
Installation
To install Verificarlo please refer to the installation documentation.
Using Verificarlo through its Docker image
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-7 and gcc-7.
Example of usage with Monte Carlo arithmetic:
$ 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-c 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.99999999999761258
Usage
To automatically instrument a program with Verificarlo you must compile it using
the verificarlo --linker=<linker>
command, where <linker>
depends on the targeted language:
verificarlo --linker=clang
for Cverificarlo --linker=clang++
for C++verificarlo --linker=flang
for Fortran
Verificarlo uses the linker clang
by default.
You can also use the provided wrappers to call verificarlo
with the right linker:
verificarlo-c
for Cverificarlo-c++
for C++verificarlo-f
for Fortran
First make sure that the verificarlo installation directory is in your PATH.
Then you can use the verificarlo-c
, verificarlo-f
and verificarlo-c++
commands to compile your programs.
Either modify your makefile to use verificarlo
as the compiler (CC=verificarlo-c
,
FC=verificarlo-f
and CXX=verificarlo-c++
) and linker (LD=verificarlo --linker=<linker>
) or use the verificarlo command
directly:
$ verificarlo-c program.c -o ./program
If 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 --linker=<linker> -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.
Branch instrumentation
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.
Examples and Tutorial
The tests/
directory contains various examples of Verificarlo usage.
A tutorial is available.
Backends
Verificarlo includes different numerical backends. Please refer to the backends documentation.
- IEEE Backend (libinterflop_ieee.so)
- MCA Backend (libinterflop_mca.so)
- MCA-MPFR Backend (libinterflop_mca_mpfr.so)
- Bitmask Backend (libinterflop_bitmask.so)
- Cancellation Backend (libinterflop_cancellation.so)
- VPREC Backend (libinterflop_vprec.so)
Inclusion / exclusion options
To inlude only certain parts of the code in the analysis or exclude parts of the code from instrumentation please refer to inclusion / exclusion options documentation.
Pinpointing numerical errors with Delta-Debug
To pinpoint numerical errors please refer to the Delta-Debug documentation.
VPREC Function Instrumentation
A function instrumentation pass enables VPREC exploration and optimization at the function granularity level. Please refer to the VPREC Function Instrumentation documentation.
Postprocessing
Verificarlo includes a set of postprocessing tools to help analyse Verificarlo results and produce high-level reports.
How to cite Verificarlo
If you use Verificarlo in your research, please cite one of the following papers:
- Verificarlo: http://dx.doi.org/10.1109/ARITH.2016.31, preprint available here.
- VPREC Backend: https://hal.archives-ouvertes.fr/hal-02564972
- VPREC Function Instrumentation and exploration: http://dx.doi.org/10.1109/TETC.2021.3070422
Thanks !
Discussion Group
For questions, feedbacks or discussions about Verificarlo you can join our group at,
https://groups.google.com/forum/#!forum/verificarlo
License
Copyright (c) 2019-2021 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/.