A tool for debugging and assessing floating point precision and reproducibility.
- Verificarlo v2.0.0
- Installation
- Using Verificarlo through its Docker image
- Usage
- Branch instrumentation
- FMA instrumentation
- Cast instrumentation
- Examples and Tutorial
- Backends
- Inclusion/exclusion options
- Pinpointing numerical errors with Delta-Debug
- VPREC Function Instrumentation
- Postprocessing
- Interflop user call instrumentation
- How to cite Verificarlo
- Discussion Group
- License
To install Verificarlo please refer to the installation documentation. Verificarlo supports both amd64 and aarch64 architectures.
A docker image is available at https://hub.docker.com/r/verificarlo/verificarlo/. This image uses the latest release 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.99999999999761258To 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=clangfor Cverificarlo --linker=clang++for C++verificarlo --linker=flangfor Fortran
Verificarlo uses the linker clang by default.
You can also use the provided wrappers to call verificarlo with the right linker:
verificarlo-cfor Cverificarlo-c++for C++verificarlo-ffor 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 ./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 --linker=<linker> -shared') to enable position-independent linking.
When invoked with the --verbose flag, verificarlo provides a 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.
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.
Verificarlo can instrument Fused Multiply-Add (FMA) operations. By default, FMA operations are not instrumented and default backends do not make use of this feature. If your backend requires instrumenting FMA operations, you must call verificarlo with the --inst-fma flag.
Verificarlo can also instrument cast operations. By default, cast operations are not instrumented and default backends do not make use of this feature. If your backend requires instrumenting cast operations, you must call verificarlo with the --inst-cast flag.
The tests/ directory contains various examples of Verificarlo usage.
A tutorial is available.
Verificarlo includes different numerical backends. Please refer to the backends' documentation.
- IEEE Backend (libinterflop_ieee.so)
- MCA Backends (libinterflop_mca.so and lib_interflop_mca_int.so)
- Bitmask Backend (libinterflop_bitmask.so)
- Cancellation Backend (libinterflop_cancellation.so)
- VPREC Backend (libinterflop_vprec.so)
To include only certain parts of the code in the analysis or exclude parts of the code from instrumentation please refer to inclusion/exclusion options documentation.
To pinpoint numerical errors please refer to the Delta-Debug documentation.
A function instrumentation pass enables VPREC exploration and optimization at the function granularity level. Please refer to the VPREC Function Instrumentation documentation.
Verificarlo includes a set of postprocessing tools to help analyze Verificarlo results and produce high-level reports.
- Find Optimal precision with vfc_precexp and vfc_report
- Unstable branch detection
- VFC-VTK
- Verificarlo CI
Verificarlo provides the ability to call low-level backend functions directly through
the interflop_call function. Please refer to the Interflop user call instrumentation documentation.
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! ✨
For questions, feedback, or discussions about Verificarlo, you can use the Discussions section on our GitHub project page.
This file is part of the Verificarlo project,
under the Apache License v2.0 with LLVM Exceptions.
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception.
See https://llvm.org/LICENSE.txt for license information.
Copyright (c) 2019-2024 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