@inproceedings{6ddd5548f26e4a5382ebc155dc4ba40a,
title = "Aloe: Verifying reliability of approximate programs in the presence of recovery mechanisms",
abstract = "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 stateof- 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.",
keywords = "Approximate Computing, Reliability",
author = "Keyur Joshi and Vimuth Fernando and Sasa Misailovic",
note = "Publisher Copyright: {\textcopyright} 2020 Copyright held by the owner/author(s).; 18th ACM/IEEE International Symposium on Code Generation and Optimization, CGO 2020 ; Conference date: 22-02-2020 Through 26-02-2020",
year = "2020",
month = feb,
day = "22",
doi = "10.1145/3368826.3377924",
language = "English (US)",
series = "CGO 2020 - Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization",
publisher = "Association for Computing Machinery",
pages = "56--67",
editor = "Jason Mars and Lingjia Tang and Jingling Xue and Peng Wu",
booktitle = "CGO 2020 - Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization",
address = "United States",
}