SHF: Small: Stabilizing Numeric Programs Against Platform Uncertainties

大多数计算机程序处理大量的数值数据。不幸的是，由于空间和性能的要求，计算机运算有自己的规则。更糟糕的是，不同的计算机有不同的规则：虽然有标准化的努力，但效率方面的考虑给了硬件和编译器设计者很大的自由来弯曲规则以满足他们的口味。因此，计算机计算的结果不仅取决于输入，而且还取决于进行计算的特定机器和环境。这使得程序脆弱且不可移植，并导致它们产生不可信的结果。本项目旨在解决这些问题，设计方法检测计算机程序中表现出太多平台依赖性的输入，并通过使其行为更健壮来修复此类程序。本项目的技术目标包括：（i）自动警告用户其数值算法的不成比例的平台依赖结果;（ii）修复具有平台不稳定性的程序;（iii）修复具有平台不稳定性的程序;（iv）修复具有平台不稳定性的程序。以及（iii）证明程序对于平台变化是稳定的。数值计算的平台无关性是一种健壮性形式，它的缺乏破坏了程序语义的可移植性。该项目是少数几个解决当今机器使用的理论（浮点运算）规范（IEEE 754）中的非确定性问题的项目之一。这项工作需要新的抽象，健全的近似值的一组程序变量对各种编译器和硬件的行为和功能，甚至可能不知道在分析时。该项目涉及研究生和本科生。

Most computer programs process vast amounts of numerical data. Unfortunately, due to space and performance demands, computer arithmetic comes with its own rules. Making matters worse, different computers have different rules: while there are standardization efforts, efficiency considerations give hardware and compiler designers much freedom to bend the rules to their taste. As a result, the outcome of a computer calculation depends not only on the input, but also on the particular machine and environment in which the calculation takes place. This makes programs brittle and un-portable, and causes them to produce untrusted results. This project addresses these problems, by designing methods to detect inputs to computer programs that exhibit too much platform dependence, and to repair such programs, by making their behavior more robust.Technical goals of this project include: (i) automatically warning users of disproportionately platform-dependent results of their numeric algorithms; (ii) repairing programs with platform instabilities; and (iii) proving programs stable against platform variations. Platform-independence of numeric computations is a form of robustness whose lack undermines the portability of program semantics. This project is one of the few to tackle the question of non-determinism in the specification (IEEE 754) of the theory (floating-point arithmetic) that machines are using today. This work requires new abstractions that soundly approximate the set of values of a program variable against a variety of compiler and hardware behaviors and features that may not even be known at analysis time. The project involves graduate and undergraduate students.