SHF: Small: Stabilizing Numeric Programs Against Platform Uncertainties

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

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.