TY - GEN
T1 - Aloe
T2 - 18th ACM/IEEE International Symposium on Code Generation and Optimization, CGO 2020
AU - Joshi, Keyur
AU - Fernando, Vimuth
AU - Misailovic, Sasa
N1 - Funding Information:
We thank our shepherd Fabrice Rastello and the anonymous reviewers for useful suggestions. The research presented in this paper was supported in part by NSF Grants CCF-1629431, CCF-1703637, and CCF-1846354, and DARPA DSSOC program, part of the Electronics Resurgence Initiative (ERI), under Contract No. HR0011-18-C-0122.
Funding Information:
The research presented in this paper was supported in part by NSF Grants CCF-1629431, CCF-1703637, and CCF-1846354, and DARPA DSSOC program, part of the Electronics Resurgence Initiative (ERI), under Contract No. HR0011-18-C-0122.
Publisher Copyright:
© 2020 Copyright held by the owner/author(s).
PY - 2020/2/22
Y1 - 2020/2/22
N2 - 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.
AB - 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.
KW - Approximate Computing
KW - Reliability
UR - http://www.scopus.com/inward/record.url?scp=85082125603&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85082125603&partnerID=8YFLogxK
U2 - 10.1145/3368826.3377924
DO - 10.1145/3368826.3377924
M3 - Conference contribution
AN - SCOPUS:85082125603
T3 - CGO 2020 - Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization
SP - 56
EP - 67
BT - CGO 2020 - Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization
A2 - Mars, Jason
A2 - Tang, Lingjia
A2 - Xue, Jingling
A2 - Wu, Peng
PB - Association for Computing Machinery
Y2 - 22 February 2020 through 26 February 2020
ER -