Numerical programs are widely used in high-performance computing, graphics, finance, deep learning, and other fields. The use of high-precision floating-point numbers can ensure the accuracy and robustness of the program and reduce the accumulation of errors. However, this approach also increases the program’s execution time, memory usage, and energy consumption. Therefore, the reasonable use of mixed precision is beneficial to balance the accuracy and performance of program results. To look for efficient mixed-precision configurations, we propose an LLVM toolchain, FuncTuner, that obtains the program transformation range by identifying the #pragma directive in the front end of Clang, uses a recursive search algorithm to access the configuration information of functions in the range, and uses LLVM Pass to modify the LLVM IR of the program according to the given configuration, pioneering the use of function-level mixed-precision optimization. Our approach achieves significant results in the HPL-AI program, with a maximum floating-point performance of 24.78 GFLOPs at fp16 precision and a performance improvement of 304.73 % at the max scale.

Floating-point exceptions are hard to avoid and can cause disastrous consequences. However, testing methods for floating-point exceptions in GPU programs are currently quite limited due to their closed-source nature. Existing tools, even the state-of-the-art Xscope, still exhibit low search efficiency and poor input coverage. In this paper, we combine interval-wise random sampling and Markov Chain Monte Carlo (MCMC) sampling in a synergistic way to efficiently detect exception-inducing inputs in GPU programs. To improve the search efficiency, based on the bit patterns of exceptional floating-point values, we propose a floating-point format-aware input space partitioning method for random sampling and define a unified fitness function for MCMC sampling. We implement our approach in a tool DFEG and demonstrate it on 76 functions from the CUDA Math Library, HPC programs, and FPBench. DFEG outperforms Xscope in terms of both effectiveness and efficiency. DFEG finds$949 \times$more exceptions than Xscope and detects new exceptions in 9 functions where Xscope fails. Moreover, compared to Xscope, DFEG achieves an average$34 \times$speedup.

Correctly rounded elementary mathematical functions are crucial for numerical computations and scientific applications. Generating these functions accurately is a challenging task. The latest methods automate this process by transforming the problem of generating correctly rounded elementary mathematical functions into a linear programming problem. However, this generation process is serial, and the inefficiency of serialization hinders the creation of new elementary mathematical functions and limits the broader application of the technique.

Floating-point arithmetic is notorious for its rounding errors, which can propagate and accumulate, leading to unacceptable results. Detecting inputs that can trigger significant floating-point errors is crucial for enhancing the reliability of numerical programs. Existing methods for generating error-triggering inputs often rely on costly shadow executions that involve high-precision computations or suffer from false positives. This paper introduces chain conditions to capture the propagation and accumulation of floating-point errors, using them to guide the search for error-triggering inputs. We have implemented a tool named FPCC and evaluated it on 88 functions from the GNU Scientific Library, as well as 21 functions with multiple inputs from previous research. The experimental results demonstrate the effectiveness and efficiency of our approach: (1) FPCC achieves 100% accuracy in detecting significant errors for the reported rank-1 inputs, while 72.69% rank-1 inputs from the state-of-the-art tool ATOMU can trigger significant errors. Overall, 99.64% (1049/1053) of the inputs reported by FPCC can trigger significant errors, whereas only 19.45% (141/723) of the inputs reported by ATOMU can trigger significant errors; (2) FPCC exhibits a 2.17x speedup over ATOMU in detecting significant errors; (3) FPCC also excels in supporting functions with multiple inputs, outperforming the state-of-the-art technique. To facilitate further research in the community, we have made FPCC available on GitHub at https://github.com/DataReportRe/FPCC .

Message-passing programs involve several processes with channel-based communications to deal with tasks concurrently. The complex computations and communications between processes make the verification of message-passing programs hard. By regarding the functions in programs as uninterpreted functions, we focus on the verification problem of message-passing uninterpreted programs. Although the usage of uninterpreted functions alleviates the computational difficulties brought by functions, the verification problem is still undecidable in general. In this work, we provide a decidable subclass of message-passing uninterpreted programs, wherein programs in this subclass satisfy the property of k-record coherence . The decidability result closely relies on communicating finite-state machine (CFM) with bounded channels. Based on the decidability result, we proposed a verification framework for message-passing uninterpreted programs.

Constraint solving stands out as a significant bot-tleneck in symbolic execution. Caching is a commonly adopted approach to alleviate this bottleneck. However, the cutting-edge caching technique targeting unsatisfiable constraints, known as unsatisfiable core caching, primarily involves checking whether the constraint being solved contains an unsatisfiable core that has been previously collected. Such straightforward reuse frequently proves less effective in numerous scenarios. In this paper, we present a novel method to enhance the utilization of unsatisfiable cores. By excavating unsatisfiable cores, our method can compute an easily solvable over-approximation that tends to be unsatis-fiable for each constraint, which facilitates the determination of the satisfiability of the original constraint. We implemented our method on KLEE symbolic executor. The evaluation results on 27 real-world programs are encouraging.

In scientific computation, developers usually exploit the compiler to improve the performance of floating-point programs. However, many compiler optimizations might affect the floating-point behavior, which can cause numerical variations. This paper proposes an efficient generation method of floating-point inputs for compiler-induced variability. Specifically, we formulate the problem of generating high variability-inducing inputs as a mathematical optimization problem and solve it through input space partition and Markov Chain Monte Carlo (MCMC) sampling. To improve the sampling efficiency, besides the result variation, we utilize the difference between the execution traces of floating-point instructions to guide the search. We have implemented our approach in the tool CIV. Compared to the state-of-the-art method, CIV achieves an average 11x speedup for generating an equivalent or better input to trigger large result variations. Moreover, CIV finds better inputs for 100% programs and has better stability for detecting large result variations. The experimental results demonstrate the effectiveness and efficiency of our approach.

F1oating-point numbers use limited precision to represent real numbers and have rounding errors, so floating-point calculations are inherently inaccurate. Revealing high floating-point errors is critical to software safety. Recently, two representative testing approaches, DEMC and ATOMU, have been proposed to find inputs triggering high floating-point errors in numerical programs. However, DEMC does not process the entire input domain and suffers from the high search cost, while ATOMU may get trapped in a local maximum. In this paper, we propose a novel approach that combines ranking analysis and search algorithms to detect high floating-point errors in numerical programs. The key idea is to use ranking analysis over the input domain to reduce search space quickly, and exploit search algorithms to find the inputs that may trigger high floating-point errors. We have implemented our approach and evaluated it on 88 numerical programs in GNU Numerical Library(GSL). The experimental results demonstrate our approach can find more high floating-point errors compare to ATOMU and DEMC. Moreover, our approach achieves 14× and 4× improvement in detecting higher floating-point errors compare to ATOMU and DEMC, respectively. As a black-box method, RADE achieves a 5. 25× speedup compared to DEMC which is the state-of-the-art black-box method.

The Message Passing Interface (MPI) is the standard paradigm of programming in high performance computing. However, the inherent complexity and the large size of MPI standard make it difficult for programmers to use the MPI APIs correctly. This paper focuses on the mismatch errors of message signatures. Considering that MPI errors may occur during some intricate, low probability interleavings under specific inputs, we adopt symbolic verification to verify the correct match of message signatures. Specifically, we propose a precise method for modeling the match of message signatures of an execution path in terms of communicating sequential processes. To improve the scalability, we give a partial order reduction based optimization to reduce the complexity of path-level communication models. We have implemented our method as a prototype tool and evaluated it on the typical correctness benchmark MPI-Corbench and 8 real-world open source MPI programs, totaling 37K lines of code. The experimental results demonstrate the effectiveness and scalability of our method.

Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV1 and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.

Verifying the regular properties of programs has been a significant challenge. This paper tackles this challenge by presenting symbolic regular verification (SRV) that offers significant speedups over the state-of-the-art. SRV is based on dynamic symbolic execution (DSE) and enabled by novel techniques for mitigating path explosion: (1) a regular property-oriented path slicing algorithm, and (2) a synergistic combination of property-oriented path slicing and guiding. Slicing prunes redundant paths, while guiding boosts the search for counterexamples. We have implemented SRV for Java and evaluated it on 15 real-world open-source Java programs (totaling 259K lines of code). Our evaluation results demonstrate the effectiveness and efficiency of SRV. Compared with the state-of-the-art --- pure DSE, pure guiding, and pure path slicing --- SRV achieves average speedups of more than 8.4X, 8.6X, and 7X, respectively, making symbolic regular property verification significantly more practical.

It is challenging to verify regular properties of programs. This paper presents symbolic regular verification (SRV), a dynamic symbolic execution based technique for verifying regular properties. The key technique of SRV is a novel synergistic combination of property-oriented path slicing and guiding to mitigate the path explosion problem. Indeed, slicing can prune redundant paths, while guiding can boost the finding of counterexamples. We have implemented SRV for Java and evaluated it on 16 real-world open-source Java programs (totaling 270K lines of code). The experimental results demonstrate the effectiveness and efficiency of SRV.

It is challenging to effectively check a regular property of a program. This paper presents RGSE, a regular property guided dynamic symbolic execution (DSE) engine, for finding a program path satisfying a regular property as soon as possible. The key idea is to evaluate the candidate branches based on the history and future information, and explore the branches along which the paths are more likely to satisfy the property in priority. We have applied RGSE to 16 real-world open source Java programs, totaling 270K lines of code. Compared with the state-of-the-art, RGSE achieves two orders of magnitude speedups for finding the first target path. RGSE can benefit many research topics of software testing and analysis, such as path-oriented test case generation, typestate bug finding, and performance tuning. The demo video is at: https://youtu.be/7zAhvRIdaUU, and RGSE can be accessed at: http://jrgse.github.io.

MPI is widely used in high performance computing. In this extended abstract, we report our current status of analyzing MPI programs. Our method can provide coverage of both input and non-determinism for MPI programs with mixed blocking and non-blocking operations. In addition, to improve the scalability further, a deadlock-oriented guiding method for symbolic execution is proposed. We have implemented our methods, and the preliminary experimental results are promising.