Aloe: Verifying reliability of approximate programs in the presence of recovery mechanisms

Keyur Joshi, Vimuth Fernando, Sasa Misailovic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationCGO 2020 - Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization
EditorsJason Mars, Lingjia Tang, Jingling Xue, Peng Wu
PublisherAssociation for Computing Machinery, Inc
Pages56-67
Number of pages12
ISBN (Electronic)9781450370479
DOIs
StatePublished - Feb 22 2020
Event18th ACM/IEEE International Symposium on Code Generation and Optimization, CGO 2020 - San Diego, United States
Duration: Feb 22 2020Feb 26 2020

Publication series

NameCGO 2020 - Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization

Conference

Conference18th ACM/IEEE International Symposium on Code Generation and Optimization, CGO 2020
CountryUnited States
CitySan Diego
Period2/22/202/26/20

Keywords

  • Approximate Computing
  • Reliability

ASJC Scopus subject areas

  • Applied Mathematics
  • Computer Science Applications
  • Control and Optimization
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'Aloe: Verifying reliability of approximate programs in the presence of recovery mechanisms'. Together they form a unique fingerprint.

  • Cite this

    Joshi, K., Fernando, V., & Misailovic, S. (2020). Aloe: Verifying reliability of approximate programs in the presence of recovery mechanisms. In J. Mars, L. Tang, J. Xue, & P. Wu (Eds.), CGO 2020 - Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization (pp. 56-67). (CGO 2020 - Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization). Association for Computing Machinery, Inc. https://doi.org/10.1145/3368826.3377924