Verifying quantitative reliability for programs that execute on unreliable hardware
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, approx...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery (ACM)
2015
|
| Online Access: | http://hdl.handle.net/1721.1/93888 https://orcid.org/0000-0003-0313-9270 https://orcid.org/0000-0001-8095-8523 |
| _version_ | 1811076419361439744 |
|---|---|
| author | Misailovic, Sasa Rinard, Martin C. Carbin, Michael James |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Misailovic, Sasa Rinard, Martin C. Carbin, Michael James |
| author_sort | Misailovic, Sasa |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T10:21:30Z |
| format | Article |
| id | mit-1721.1/93888 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T10:21:30Z |
| publishDate | 2015 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/938882022-09-26T17:23:51Z Verifying quantitative reliability for programs that execute on unreliable hardware Misailovic, Sasa Rinard, Martin C. Carbin, Michael James Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Rinard, Martin C. Carbin, Michael James Misailovic, Sasa Rinard, Martin C. 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. National Science Foundation (U.S.) (Grant CCF-0905244) National Science Foundation (U.S.) (Grant CCF-1036241) National Science Foundation (U.S.) (Grant CCF-1138967) National Science Foundation (U.S.) (Grant IIS-0835652) United States. Dept. of Energy (Grant DE-SC0008923) United States. Defense Advanced Research Projects Agency (Grant FA8650-11-C-7192) United States. Defense Advanced Research Projects Agency (Grant FA8750-12-2-0110) 2015-02-06T15:14:44Z 2015-02-06T15:14:44Z 2013-10 Article http://purl.org/eprint/type/ConferencePaper 9781450323741 http://hdl.handle.net/1721.1/93888 Michael Carbin, Sasa Misailovic, and Martin C. Rinard. 2013. Verifying quantitative reliability for programs that execute on unreliable hardware. In Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications (OOPSLA '13). ACM, New York, NY, USA, 33-52. https://orcid.org/0000-0003-0313-9270 https://orcid.org/0000-0001-8095-8523 en_US http://dx.doi.org/10.1145/2509136.2509546 Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications (OOPSLA '13) Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) Prof. Rinard via Chris Sherratt |
| spellingShingle | Misailovic, Sasa Rinard, Martin C. Carbin, Michael James Verifying quantitative reliability for programs that execute on unreliable hardware |
| title | Verifying quantitative reliability for programs that execute on unreliable hardware |
| title_full | Verifying quantitative reliability for programs that execute on unreliable hardware |
| title_fullStr | Verifying quantitative reliability for programs that execute on unreliable hardware |
| title_full_unstemmed | Verifying quantitative reliability for programs that execute on unreliable hardware |
| title_short | Verifying quantitative reliability for programs that execute on unreliable hardware |
| title_sort | verifying quantitative reliability for programs that execute on unreliable hardware |
| url | http://hdl.handle.net/1721.1/93888 https://orcid.org/0000-0003-0313-9270 https://orcid.org/0000-0001-8095-8523 |
| work_keys_str_mv | AT misailovicsasa verifyingquantitativereliabilityforprogramsthatexecuteonunreliablehardware AT rinardmartinc verifyingquantitativereliabilityforprogramsthatexecuteonunreliablehardware AT carbinmichaeljames verifyingquantitativereliabilityforprogramsthatexecuteonunreliablehardware |