View in EDS PDF Full Text

Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware.

Saved in:
Bibliographic Details
Title: Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware.
Authors: Carbin, Michael1, Misailovic, Sasa1, Rinard, Martin C.1
Source: Communications of the ACM. Aug2016, Vol. 59 Issue 8, p83-91. 9p. 2 Diagrams, 4 Charts.
Subjects: Programming languages, Computer reliability, High performance computing, Computer architecture, Soft errors
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. [ABSTRACT FROM AUTHOR]
Copyright of Communications of the ACM is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 117173598
AccessLevel: 6
PubType: Periodical
PubTypeId: serialPeriodical
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Carbin%2C+Michael%22">Carbin, Michael</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Misailovic%2C+Sasa%22">Misailovic, Sasa</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Rinard%2C+Martin+C%2E%22">Rinard, Martin C.</searchLink><relatesTo>1</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Communications+of+the+ACM%22">Communications of the ACM</searchLink>. Aug2016, Vol. 59 Issue 8, p83-91. 9p. 2 Diagrams, 4 Charts.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+reliability%22">Computer reliability</searchLink><br /><searchLink fieldCode="DE" term="%22High+performance+computing%22">High performance computing</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+architecture%22">Computer architecture</searchLink><br /><searchLink fieldCode="DE" term="%22Soft+errors%22">Soft errors</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Communications of the ACM is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=117173598
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1145/2958738
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 9
        StartPage: 83
    Subjects:
      – SubjectFull: Programming languages
        Type: general
      – SubjectFull: Computer reliability
        Type: general
      – SubjectFull: High performance computing
        Type: general
      – SubjectFull: Computer architecture
        Type: general
      – SubjectFull: Soft errors
        Type: general
    Titles:
      – TitleFull: Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Carbin, Michael
      – PersonEntity:
          Name:
            NameFull: Misailovic, Sasa
      – PersonEntity:
          Name:
            NameFull: Rinard, Martin C.
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 08
              Text: Aug2016
              Type: published
              Y: 2016
          Identifiers:
            – Type: issn-print
              Value: 00010782
          Numbering:
            – Type: volume
              Value: 59
            – Type: issue
              Value: 8
          Titles:
            – TitleFull: Communications of the ACM
              Type: main
ResultId 1