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

科学计算的数值结果以浮点数的形式存储在计算机中，这是真实的数字的近似值，这说明了计算机存储空间有限的事实。这种对近似值的需求有一个不幸的副作用，即浮点数不遵守高中时就知道的算术定律，比如加法的结合性。因此，在计算机硬件上的浮点运算的明显等效实现可能产生非常不同的结果，例如当加法的操作数的顺序被编译器改变时。一般为高性能并行计算平台编写的程序可能会使用不同的浮点实现和编译，因为编译产生的可执行文件取决于可用的硬件。因此，这种并行科学程序容易受到可靠性和可移植性问题的影响，这些问题的范围可以从简单的精度偏差到从一种体系结构转移到另一种体系结构时程序控制流的急剧变化。这项研究的结果将成为帮助科学家更有效地发现此类程序中错误的工具和技术。这项研究对重要科学项目的可靠性具有重要意义，例如用于生物医学成像应用，气候建模和车辆设计的项目。该项目开发了用于分析并行科学代码的严格方法，特别是使用现在新兴的OpenCL并行编程标准编写的。我们的目标是检测潜在的源ofreliability和可移植性的缺陷，在这样的代码是由于依赖的浮点行为对底层硬件，这可能是未知的程序员。传统的可靠性方法，如程序测试和调试是无效的并行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.