SHF: Small: Ensuring Reliability and Portability of Scientific Software for Heterogeneous Architectures

点击翻译按钮获取中文摘要

Numerical results of scientific computations are stored in computers asfloating-point numbers, an approximation of real numbers that accounts forthe fact that a computer's storage is limited. This need for approximationhas the unfortunate side effect that floating-point numbers don't abide bycommon laws of arithmetic known from high school, such as the associativityof addition. As a consequence, apparently equivalent implementations offloating-point operations on computer hardware may produce very differentresults, such as when the order of operands of an addition is changed by acompiler. Programs generically written for high-performance parallel computingplatforms are likely to be compiled using different floating-pointimplementations and schedulings, as the executable resulting from thecompilation depends on the available hardware. Such parallel scientificprograms are therefore susceptible to reliability and portability issuesthat can range from simple deviations in precision to drastic changes ofprogram 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 scientificcode, specifically written using the now emerging OpenCL parallelprogramming standard. The goal is to detect potential sources ofreliability and portability deficiencies in such code that are due todependencies of the floating-point behavior on the underlying hardware,which may be unknown to the programmer. Traditional reliability methodssuch as program testing and debugging are ineffective for parallel OpenCLprograms, because program behavior may vary across runs, making after-testbehavior uncertain. For these reasons, the investigators will use rigorousanalysis methods that are not solely based on program execution. Instead,the program is formally modeled as a transition system; the model isencoded symbolically, using logical formula representations that can oftencompactly represent the set of executions of the program without executingit. The program model is then analyzed for portability violations andprogram errors using floating point-capable decision procedures and modelcheckers. To achieve scalability, the investigators plan to exploit thehighly symmetric and parametric form of OpenCL programs, where identicaloperations are performed by many computational threads in SingleInstruction Multiple Data (SIMD) style.