Aloe: verifying reliability of approximate programs in the presence of recovery mechanisms
Aloe: verifying reliability of approximate programs in the presence of recovery mechanisms
复制标题
DOI：
10.1145/3368826.3377924
复制
发表时间：
2020-02
期刊：
影响因子：
--
通讯作者：
Keyur Joshi;V. Fernando;Sasa Misailovic
中科院分区：
文献类型：
--
作者：
Keyur Joshi;V. Fernando;Sasa Misailovic
现代硬件越来越容易受到无声数据损坏的影响。由于检测和从错误中恢复的一般方法既耗时又耗能，因此选择性检测和恢复对于具有可变精度水平的自由产生结果的应用程序是很有希望的替代方法。一些编程语言已经为表示检测和恢复操作提供了专门的结构，但是现有的安全性静态分析和程序定量分析没有对这些语言结构提供适当的支持。这项工作提出了Aloe，一个带有恢复块的程序可靠性的定量静态分析-一个检查错误的结构，并在必要时应用相应的恢复策略。该分析支持对可靠和可能不可靠的检测和恢复机制进行推理。它实现了一种新的恢复块的先决条件生成器，建立在最先进的命令式程序的定量可靠性分析工具Rely之上。Aloe可以用标量和数组表达式、if-then-else条件和没有提前退出的有界循环来推理程序。被分析的计算是幂等的，恢复代码重新执行原来的计算。我们实现了Aloe，并将其应用于以前用于近似计算研究的一组八个程序。与现有的Rely分析相比，我们的结果具有更高的可靠性和更好的规模。此外，验证计算的端到端精度只有很小的精度损失。
Modern hardware is becoming increasingly susceptible to silent data corruptions. As general methods for detection and recovery from errors are time and energy consuming, selective detection and recovery are promising alternatives for applications that have the freedom to produce results with a variable level of accuracy. Several programming languages have provided specialized constructs for expressing detection and recovery operations, but the existing static analyses of safety and quantitative analyses of programs do not have the proper support for such language constructs. This work presents Aloe, a quantitative static analysis of reliability of programs with recovery blocks - a construct that checks for errors, and if necessary, applies the corresponding recovery strategy. The analysis supports reasoning about both reliable and potentially unreliable detection and recovery mechanisms. It implements a novel precondition generator for recovery blocks, built on top of Rely, a state-of-the-art quantitative reliability analysis for imperative programs. Aloe can reason about programs with scalar and array expressions, if-then-else conditionals, and bounded loops without early exits. The analyzed computation is idempotent and the recovery code re-executes the original computation. We implemented Aloe and applied it to a set of eight programs previously used in approximate computing research. Our results present significantly higher reliability and scale better compared to the existing Rely analysis. Moreover, the end-to-end accuracy of the verified computations exhibits only small accuracy losses.