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...
| Publicado en: | Communications of the ACM Vol. 59; no. 8; pp. 83 - 92 |
|---|---|
| Autores principales: | , , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Aug2016
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=117173598&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 117173598 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Aug2016 vid: 59 iid: 8 pid: 68 pub: Association for Computing Machinery artinfo: ui: 117173598 10.1145/2958738 ppf: 83 ppct: 9 formats: tig: atl: Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware. aug: au: Carbin, Michael Misailovic, Sasa Rinard, Martin C. affil: Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MA su: Programming languages Computer reliability High performance computing Computer architecture Soft errors sug: subj: Programming languages Computer reliability High performance computing Computer architecture Soft errors 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. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2016 holdings: @attributes: islocal: N |
|---|