Verifying quantitative reliability for programs that execute on unreliable hardware

Michael Carbin, Sasa Misailovic, Martin C. Rinard

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

Abstract

Emerging high-performance architectures are anticipated to contain unreliable components that may exhibit soft errors, which silently corrupt the results of computations. Full detection and masking of soft errors is challenging, expensive, and, for some applications, unnecessary. For example, approximate computing applications (such as multimedia processing, machine learning, and big data analytics) can often naturally tolerate soft errors. We present Rely, a programming language that enables developers to reason about the quantitative reliability of an application - namely, the probability that it produces the correct result when executed on unreliable hardware. Rely allows developers to specify the reliability requirements for each value that a function produces. We present a static quantitative reliability analysis that verifies quantitative requirements on the reliability of an application, enabling a developer to perform sound and verified reliability engineering. The analysis takes a Rely program with a reliability specification and a hardware specification that characterizes the reliability of the underlying hardware components and verifies that the program satisfies its reliability specification when executed on the underlying unreliable hardware platform. We demonstrate the application of quantitative reliability analysis on six computations implemented in Rely.

Original languageEnglish (US)
Title of host publicationSPLASH Indianapolis 2013
Subtitle of host publicationOOPSLA 2013 - Proceedings of the 2013 International Conference on Object Oriented Programming Systems Languages and Applications
Pages33-52
Number of pages20
DOIs
StatePublished - Nov 28 2013
Event2013 28th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2013 - Indianapolis, IN, United States
Duration: Oct 29 2013Oct 31 2013

Publication series

NameProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA

Other

Other2013 28th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2013
CountryUnited States
CityIndianapolis, IN
Period10/29/1310/31/13

Fingerprint

Hardware
Reliability analysis
Specifications
Computer programming languages
Learning systems
Acoustic waves
Processing

Keywords

  • Approximate computing

ASJC Scopus subject areas

  • Software

Cite this

Carbin, M., Misailovic, S., & Rinard, M. C. (2013). Verifying quantitative reliability for programs that execute on unreliable hardware. In SPLASH Indianapolis 2013: OOPSLA 2013 - Proceedings of the 2013 International Conference on Object Oriented Programming Systems Languages and Applications (pp. 33-52). (Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA). https://doi.org/10.1145/2509136.2509546

Verifying quantitative reliability for programs that execute on unreliable hardware. / Carbin, Michael; Misailovic, Sasa; Rinard, Martin C.

SPLASH Indianapolis 2013: OOPSLA 2013 - Proceedings of the 2013 International Conference on Object Oriented Programming Systems Languages and Applications. 2013. p. 33-52 (Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA).

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

Carbin, M, Misailovic, S & Rinard, MC 2013, Verifying quantitative reliability for programs that execute on unreliable hardware. in SPLASH Indianapolis 2013: OOPSLA 2013 - Proceedings of the 2013 International Conference on Object Oriented Programming Systems Languages and Applications. Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA, pp. 33-52, 2013 28th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2013, Indianapolis, IN, United States, 10/29/13. https://doi.org/10.1145/2509136.2509546
Carbin M, Misailovic S, Rinard MC. Verifying quantitative reliability for programs that execute on unreliable hardware. In SPLASH Indianapolis 2013: OOPSLA 2013 - Proceedings of the 2013 International Conference on Object Oriented Programming Systems Languages and Applications. 2013. p. 33-52. (Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA). https://doi.org/10.1145/2509136.2509546
Carbin, Michael ; Misailovic, Sasa ; Rinard, Martin C. / Verifying quantitative reliability for programs that execute on unreliable hardware. SPLASH Indianapolis 2013: OOPSLA 2013 - Proceedings of the 2013 International Conference on Object Oriented Programming Systems Languages and Applications. 2013. pp. 33-52 (Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA).
@inproceedings{5855c915c70343a682a3dba3e82f2dda,
title = "Verifying quantitative reliability for programs that execute on unreliable hardware",
abstract = "Emerging high-performance architectures are anticipated to contain unreliable components that may exhibit soft errors, which silently corrupt the results of computations. Full detection and masking of soft errors is challenging, expensive, and, for some applications, unnecessary. For example, approximate computing applications (such as multimedia processing, machine learning, and big data analytics) can often naturally tolerate soft errors. We present Rely, a programming language that enables developers to reason about the quantitative reliability of an application - namely, the probability that it produces the correct result when executed on unreliable hardware. Rely allows developers to specify the reliability requirements for each value that a function produces. We present a static quantitative reliability analysis that verifies quantitative requirements on the reliability of an application, enabling a developer to perform sound and verified reliability engineering. The analysis takes a Rely program with a reliability specification and a hardware specification that characterizes the reliability of the underlying hardware components and verifies that the program satisfies its reliability specification when executed on the underlying unreliable hardware platform. We demonstrate the application of quantitative reliability analysis on six computations implemented in Rely.",
keywords = "Approximate computing",
author = "Michael Carbin and Sasa Misailovic and Rinard, {Martin C.}",
year = "2013",
month = "11",
day = "28",
doi = "10.1145/2509136.2509546",
language = "English (US)",
isbn = "9781450323741",
series = "Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA",
pages = "33--52",
booktitle = "SPLASH Indianapolis 2013",

}

TY - GEN

T1 - Verifying quantitative reliability for programs that execute on unreliable hardware

AU - Carbin, Michael

AU - Misailovic, Sasa

AU - Rinard, Martin C.

PY - 2013/11/28

Y1 - 2013/11/28

N2 - Emerging high-performance architectures are anticipated to contain unreliable components that may exhibit soft errors, which silently corrupt the results of computations. Full detection and masking of soft errors is challenging, expensive, and, for some applications, unnecessary. For example, approximate computing applications (such as multimedia processing, machine learning, and big data analytics) can often naturally tolerate soft errors. We present Rely, a programming language that enables developers to reason about the quantitative reliability of an application - namely, the probability that it produces the correct result when executed on unreliable hardware. Rely allows developers to specify the reliability requirements for each value that a function produces. We present a static quantitative reliability analysis that verifies quantitative requirements on the reliability of an application, enabling a developer to perform sound and verified reliability engineering. The analysis takes a Rely program with a reliability specification and a hardware specification that characterizes the reliability of the underlying hardware components and verifies that the program satisfies its reliability specification when executed on the underlying unreliable hardware platform. We demonstrate the application of quantitative reliability analysis on six computations implemented in Rely.

AB - Emerging high-performance architectures are anticipated to contain unreliable components that may exhibit soft errors, which silently corrupt the results of computations. Full detection and masking of soft errors is challenging, expensive, and, for some applications, unnecessary. For example, approximate computing applications (such as multimedia processing, machine learning, and big data analytics) can often naturally tolerate soft errors. We present Rely, a programming language that enables developers to reason about the quantitative reliability of an application - namely, the probability that it produces the correct result when executed on unreliable hardware. Rely allows developers to specify the reliability requirements for each value that a function produces. We present a static quantitative reliability analysis that verifies quantitative requirements on the reliability of an application, enabling a developer to perform sound and verified reliability engineering. The analysis takes a Rely program with a reliability specification and a hardware specification that characterizes the reliability of the underlying hardware components and verifies that the program satisfies its reliability specification when executed on the underlying unreliable hardware platform. We demonstrate the application of quantitative reliability analysis on six computations implemented in Rely.

KW - Approximate computing

UR - http://www.scopus.com/inward/record.url?scp=84888167548&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84888167548&partnerID=8YFLogxK

U2 - 10.1145/2509136.2509546

DO - 10.1145/2509136.2509546

M3 - Conference contribution

AN - SCOPUS:84888167548

SN - 9781450323741

T3 - Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA

SP - 33

EP - 52

BT - SPLASH Indianapolis 2013

ER -