Numerical results of scientific computations are stored in computers as floating-point numbers, an approximation of real numbers that accounts for the fact that a computer's storage is limited. This need for approximation has the unfortunate side effect that floating-point numbers don't abide by common laws of arithmetic known from high school, such as the associativity of addition. As a consequence, apparently equivalent implementations of floating-point operations on computer hardware may produce very different results, such as when the order of operands of an addition is changed by a compiler. Programs generically written for high-performance parallel computing platforms are likely to be compiled using different floating-point implementations and schedulings, as the executable resulting from the compilation depends on the available hardware. Such parallel scientific programs are therefore susceptible to reliability and portability issues that can range from simple deviations in precision to drastic changes of program control flow when moving from one architecture to another. The results of this research will be tools and techniques to help scientists find bugs more effectively in such programs. This research has important implications for the reliability of important scientific programs such as those used in biomedical imaging applications, climate modelling, and vehicle design.
This project develops rigorous methods for analyzing parallel scientific code, specifically written using the now emerging OpenCL parallel programming standard. The goal is to detect potential sources of reliability and portability deficiencies in such code that are due to dependencies of the floating-point behavior on the underlying hardware, which may be unknown to the programmer. Traditional reliability methods such as program testing and debugging are ineffective for parallel OpenCL programs, because program behavior may vary across runs, making after-test behavior uncertain. For these reasons, the investigators will use rigorous analysis methods that are not solely based on program execution. Instead, the program is formally modeled as a transition system; the model is encoded symbolically, using logical formula representations that can often compactly represent the set of executions of the program without executing it. The program model is then analyzed for portability violations and program errors using floating point-capable decision procedures and model checkers. To achieve scalability, the investigators plan to exploit the highly symmetric and parametric form of OpenCL programs, where identical operations are performed by many computational threads in Single Instruction Multiple Data (SIMD) style.
