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

科学计算的数值结果以浮点数的形式存储在计算机中，浮点数是实数的近似值，说明了计算机存储空间有限的事实。这种对近似的需要有一个不幸的副作用，即浮点数不遵守从高中就知道的常见算术法则，例如加法的结合性。因此，计算机硬件上浮点运算的表面上等价的实现可能会产生非常不同的结果，例如当编译器改变加法操作数的顺序时。通常为高性能并行计算平台编写的程序可能会使用不同的浮点实现和调度来编译，因为编译产生的可执行文件取决于可用的硬件。因此，这样的并行科学程序容易受到可靠性和可移植性问题的影响，从简单的精度偏差到从一个体系结构迁移到另一个体系结构时程序控制流的剧烈变化。这项研究的结果将成为帮助科学家更有效地发现此类程序中的错误的工具和技术。这项研究对生物医学成像应用、气候建模和车辆设计等重要科学程序的可靠性具有重要影响。这个项目开发了分析并行科学代码的严格方法，特别是使用现在正在兴起的OpenCL并行编程标准编写的代码。目标是检测这类代码中的可靠性和可移植性缺陷的潜在来源，这些缺陷是由于底层硬件上浮点行为的依赖而引起的，而这可能是程序员不知道的。传统的可靠性方法，如程序测试和调试，对于并行OpenCL程序来说是无效的，因为程序的行为在不同的运行中可能会发生变化，使得后测试行为不确定。出于这些原因，调查人员将使用严格的分析方法，而不仅仅是基于程序的执行。取而代之的是，程序被形式化地建模为一个转换系统；该模型被符号化地编码，使用逻辑公式表示法，通常可以紧凑地表示程序的一组执行而不执行它。然后，使用支持浮点的决策过程和模型检查器来分析程序模型的可移植性违规和程序错误。为了实现可伸缩性，研究人员计划利用OpenCL程序的高度对称和参数形式，其中相同的操作由许多计算线程以单指令多数据(SIMD)风格执行。

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.