Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities

Read full text
Authors: Yichen Tao, Hongfei Fu, Jiawei Chen, Jean-Baptiste Jeannin
Cited by: 0

Abstract

# Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities Yichen Tao, Hongfei Fu, Jiawei Chen, Jean-Baptiste Jeannin This artifact is run on VirtualBox 7.1.4. The Guest OS is Ubuntu 18.04. The login is `ychtao` and the password is `probtaylor`. This artifact includes a VM image for running ProbTaylor (the tool we developed), PrAn (an extension of Daisy that we compare against), and PAF (a tool we compare against). GELPIA (a global optimization tool used to bound the second-order error) is also installed on the VM, and called by ProbTaylor and PAF. All these tools and their dependencies have been installed and compiled, and are ready to use. All experiments should be run under the `~/yichen` directory. ## Download, installation, and sanity-testing (Kick-the-tires instructions) All programs relevant to the experiments are under the `~/yichen` directory. The directory `~/yichen/daisy` contains contents for PrAn. The directory `~/yichen/paf` contains contents for PAF. The directory `~/yichen/probtaylor` contains contents for ProbTaylor. To do a sanity check, execute the following steps: 1. From the home directory `~`, run `cd yichen`.2. Under `~/yichen`, run `sh sanity_test.sh`. The `sanity_test.sh` script runs one benchmark for each of the three tools. On our machine, the ProbTaylor benchmark finishes within seconds; the PrAn (Daisy) benchmark finishes within 3 minutes; the PAF benchmark finishes within 13 minutes. The output generated by the sanity check experiments can be found in `~/yichen/probtaylor/results/poly_u_nm/bsplines0.out`, `~/yichen/daisy/probtaylor_expr/Bsplines.out`, and `~/yichen/paf/results/filters1`, respectively. ## Evaluation Instructions To run the experiments to reproduce the results in our manuscript, execute the following steps: 1. From the home directory `~`, run `cd yichen`.2. Under `~/yichen`, run `sh pt_expr.sh`. The resulting outputs are generated in `~/yichen/probtaylor/results`, `~/yichen/daisy/probtaylor_expr`, and `~/yichen/paf/results`, respectively. Reference outputs are provided in `~/yichen/probtaylor/expected_output`, `~/yichen/daisy/expected_output`, and `~/yichen/paf/expected_output`. We expect the results generated on the evaluators' machines to be consistent with the reference outputs, except for variations in execution time.Note that the full PAF experiment takes weeks to finish. Therefore, we only include three simple examples (`filters1`, `nonlin1` and `traincars1`) from PAF in our experiment script. More experiments can be run using commands similar to the ones in `~/yichen/paf/probtaylor_expr.sh`. The thresholds output by PAF can be found in their [paper](https://arxiv.org/pdf/2105.13217) (Table 2 on page 22). There are some Type errors generated while running PAF or GELPIA, which we cannot modify. These are intended behaviors and can be omitted. ## Reproducibility guidelines Our tool ProbTaylor implements a sequence of algorithms for generating probabilistic thresholds for floating-point round-off errors of programs involving arithmetic operations. The algorithms include: the Naive Markov (NM) algorithm, the Central-Moment-Based (CMB) algorithm, and its extension to incorporate fractional expressions. The experiment section in our manuscript answers four research questions: 1. **RQ1:** How does the NM algorithm compare to the SOTA tools, PAF and PrAn, in terms of accuracy and time efficiency on polynomial benchmarks? 2. **RQ2:** How well does our approach scale when analyzing expressions with a large number of variables and operations? 3. **RQ3:** How does the CMB algorithm, equipped with the range partition refinement, perform relative to the NM algorithm and the existing tools on polynomial benchmarks? How does its extension for fractional expressions perform compared to existing tools? 4. **RQ4:** To what extent can ProbTaylor improve upon the results obtained from conservative deterministic analysis tools (such as FPTaylor)? We will now explain how our answer to each of the RQs is supported by our artifact. ### Answering RQ1 The experimental data are recorded in Tables 1, 2, and 3 of our manuscript. These tables present the experiments with input variables following uniform distribution, normal districution, and Laplace distribution, respectively. The results from ProbTaylor in this artifact can be found in `~/yichen/probtaylor/results/poly_*_nm` where `*` is to be replaced by `u`, `n`, `e` or `ewide`. The four letters stand for uniform distribution, normal distribution, Laplace distribution with `sigma=0.01` and Laplace distribution with `sigma=1`. The PrAn results can be found in `~/yichen/daisy/probtaylor_expr`, where the file names with `_n` at the end assumes normal distribution, and uniform distribution otherwise. There is no experiments on Laplace distribution from PrAn, since it is not supported. Note that in Table 3, the sigma value of Laplace distribution is 1 for benchmarks `classids0`, `classids1`, `classids2` and `solvecubic`, and 0.01 for all others. The Naive Markov time, threshold, and optimal $n$ in the tables from our manuscript can be found directly in the `.out` files. The Threshold ratios can be computed by dividing the ProbTaylor threshold by the PrAn/PAF threshold. The Speedups can be computed by dividing the ProbTaylor running time by the PrAn/PAF running time. ### Answering RQ2 The experimental data for RQ2 are recorded in Table 4 of our manuscript. This table presents the performance of our tool on vector inner product. The results generated by our artifact can be found in `~/yichen/probtaylor/results/scalability`, where files `dpgen_n.out` records the result for vector length `n`. Due to the long running time, our artifact only presents the results on first-order error analysis, corresponding to the "FO time(s)" column in Table 4. ### Answering RQ3 The answer to RQ3 involves data in Tables 5, 6 and 7. The CMB algorithm threshold results on polynomial benchmarks can be found in `~/yichen/probtaylor/results/poly_*_cmb`, where `*` is to be replaced by `u`, `n`, `e` or `ewide`, with each corresponding to a distribution. The data in Table 5 can be derived by dividing the CMB thresholds by the NM thresholds. Notice that all ratios in the "Laplace" column assume `sigma=1` in Table 5. The data in Table 6 can be derived by dividing the CMB thresholds by the PAF/PrAn thresholds. For the Laplace column, the sigma value is 1 for benchmarks `classids0`, `classids1`, `classids2` and `solvecubic`, and 0.01 for all others. The ProbTaylor experimental data for fractional (division) benchmarks are in `~/yichen/probtaylor/div_*_cmb`, where `*` is to be replaced by a letter standing for the distribution considered. The data for PrAn is in `~/yichen/daisy/probtaylor_expr`. The interpretation of data is similar to that in RQ1. ### Answering RQ4 The RQ4 data is documented in Table 8 of our manuscript. The ProbTaylor results can be found in `~/yichen/probtaylor/results/poly_n_nm`, `~/yichen/probtaylor/results/doubled` and `~/yichen/probtaylor/results/quadrupled`. FPTaylor is not installed on the VM, but it can be run online [here](https://monadius.github.io/FPTaylorJS/#/). The data in Table 8 can be derived by dividing the ProbTaylor threshold by the FPTaylor bound. ## Reusability guidelines The core part of our artifact is the ProbTaylor tool, with PrAn and PAF mainly for comparison. The input file to ProbTaylor consists of two parts – the variable declarations and an arithmetic expression. Each line of the variable declarations part is in the form of ` : ( , )`. The distribution can be one of `U`, `N` and `E`, standing for uniform, normal, and Laplace distribution, respectively. The lower and upper value indicates the range of the variable. The arithmetic expression involves only declared variables, and is either a division-free expression, or a fractional expression, where the outermost operator is division. The examples of input files can be found in `~/yichen/probtaylor/benchmarks`. To run ProbTaylor, use the following command under directory `~/yichen/probtaylor`: `./bin/pt -o `, where the options can be: + `-o `: generate output at ` ` + `--nm`: run the NM algorithm + `--nmopt`: run the NM algorithm with different analysis orders and output the best result + `--cmb`: run the CMB algorithm + `--div`: run the extended CMB algorithm for fractional expressions + `--order n`: highest analysis order set to `n` in `nmopt` mode; analysis order set to `n` otherwise + `--num b`: number of intervals set to `b` in `cmb` or `div` mode + `--eps e`: unit round-off set to `e` (default value 2**(-24)) + `--dlt d`: subnormal unit set to `d` (default value 2**(-126)) + `--sigma s`: variance of Laplace distribution set to `s` (default value 0.01) + `--tri`: analyze second-order error with the brute-force method (default: using GELPIA) + `--er1`: analyze first-order error only Examples of commands running ProbTaylor can be found in the scripts files in `~/yichen/probtaylor/scripts`. ### Compilation instructions Since the dependency GELPIA has not been actively maintained, the whole system only runs on Ubuntu 18.04. To compile the whole system: 1. Under the same directory, git clone from `https://github.com/rospoly/gelpia.git` and put the unzipped ProbTaylor code. 2. Run `cd gelpia`, and then, under the `gelpia` directory, run `make requirements` and then `make`. This step compiles the GELPIA tool. 3. Run `cd ../probtaylor` and then compile ProbTaylor by running `make`. 4. Under the `probtaylor` directory, follow the instructions above to run the tool on benchmarks.

Fields of Study & Subjects

Numerical Methods and Algorithms Formal Methods in Verification Logic programming and type systems

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
5 February 2026