More Web Proxy on the site http://driver.im/

research-article

Open access

Verifying quantitative reliability for programs that execute on unreliable hardware

Authors:

Michael Carbin,

Sasa Misailovic,

Martin C. RinardAuthors Info & Claims

OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications

Pages 33 - 52

https://doi.org/10.1145/2509136.2509546

Published: 29 October 2013 Publication History

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.

References

[1]

J. Ansel, C. Chan, Y. L. Wong, M. Olszewski, Q. Zhao, A. Edelman, and Amarasinghe. PetaBricks: A language and compiler for algorithmic choice. PLDI, 2009.

Digital Library

[2]

W. Baek and T. M. Chilimbi. Green: A framework for supporting energy-conscious programming using controlled approximation. PLDI, 2010.

Digital Library

[3]

T. Bao, Y. Zheng, and X. Zhang. White box sampling in uncertain data processing enabled by program analysis. In OOPSLA, 2012.

Digital Library

[4]

G. Barthe, D. Demange, and D. Pichardie. A formally verified ssa-based middle-end: Static single assignment meets compcert. ESOP, 2012.

Digital Library

[5]

G. Barthe, B. Grégoire, and S. Zanella Béguelin. Formal certification of code-based cryptographic proofs. POPL, 2009.

Digital Library

[6]

G. Barthe, B. Köpf, F. Olmedo, and S. Zanella Béguelin. Probabilistic reasoning for differential privacy. POPL, 2012.

Digital Library

[7]

M. Blum and S. Kanna. Designing programs that check their work. STOC, 1989.

Digital Library

[8]

M. Blum, M. Luby, and R. Rubinfeld. Self-testing/correcting with applications to numerical problems. Journal of computer and system sciences, 1993.

Digital Library

[9]

F. Cappello, A. Geist, B. Gropp, L. Kale, B. Kramer, and M. Snir. Toward exascale resilience. International Journal of High Performance Computing Applications, 2009.

Digital Library

[10]

M. Carbin, D. Kim, S. Misailovic, and M. Rinard. Proving acceptability properties of relaxed nondeterministic approximate programs. PLDI, 2012.

Digital Library

[11]

M. Carbin, D. Kim, S. Misailovic, and M. Rinard. Verified integrity properties for safe approximate program transformations. PEPM, 2013.

Digital Library

[12]

M. Carbin and M. Rinard. Automatically identifying critical input regions and code in applications. ISSTA, 2010.

Digital Library

[13]

L. Chakrapani, B. Akgul, S. Cheemalavagu, P. Korkmaz, K. Palem, and B. Seshasayee. Ultra-efficient (embedded) soc architectures based on probabilistic cmos (pcmos) technology. DATE, 2006.

Digital Library

[14]

S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. Navidpour. Proving programs robust. FSE, 2011.

Digital Library

[15]

P. Cousot and M. Monerau. Probabilistic abstract interpretation. ESOP, 2012.

Digital Library

[16]

M. de Kruijf, S. Nomura, and K. Sankaralingam. Relax: an architectural framework for software recovery of hardware faults. ISCA, 2010.

Digital Library

[17]

A. Di Pierro and H. Wiklicky. Concurrent constraint programming: Towards probabilistic abstract interpretation. PPDP'00.

Digital Library

[18]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. CACM, 18(8), August 1975.

Digital Library

[19]

D. Ernst, N. S. Kim, S. Das, S. Pant, R. Rao, T. Pham, C. Ziesler, D. Blaauw, T. Austin, K. Flautner, and T. Mudge. Razor: A low-power pipeline based on circuit-level timing speculation. MICRO, 2003.

Digital Library

[20]

H. Esmaeilzadeh, A. Sampson, L. Ceze, and D. Burger. Architecture support for disciplined approximate programming. ASPLOS, 2012.

Digital Library

[21]

H. Esmaeilzadeh, A. Sampson, L. Ceze, and D. Burger. Neural acceleration for general-purpose approximate programs. MICRO, 2012.

Digital Library

[22]

S. Feng, S. Gupta, A. Ansari, and S. Mahlke. Shoestring: probabilistic soft error reliability on the cheap. ASPLOS'10.

Digital Library

[23]

A. Filieri, C. P\uas\uareanu, and W. Visser. Reliability analysis in symbolic pathfinder. In ICSE, 2013.

Digital Library

[24]

M. Hiller, A. Jhumka, and N. Suri. On the placement of software mechanisms for detection of data errors. DSN, 2002.

Digital Library

[25]

H. Hoffmann, S. Sidiroglou, M. Carbin, S. Misailovic, A. Agarwal, and M. Rinard. Dynamic knobs for responsive power-aware computing. ASPLOS, 2011.

Digital Library

[26]

M. Kling, S. Misailovic, M. Carbin, and M. Rinard. Bolt: on-demand infinite loop escape in unmodified binaries. OOPSLA, 2012.

Digital Library

[27]

K. Knobe and V. Sarkar. Array ssa form and its use in parallelization. POPL, 1998.

Digital Library

[28]

D. Kozen. Semantics of probabilistic programs. Journal of Computer and System Sciences, 1981.

[29]

K. Lee, A. Shrivastava, I. Issenin, N. Dutt, and N. Venkatasubramanian. Mitigating soft error failures for multimedia applications by selective data protection. CASES, 2006.

Digital Library

[30]

L. Leem, H. Cho, J. Bau, Q. Jacobson, and S. Mitra. Ersa: error resilient system architecture for probabilistic applications. DATE, 2010.

Digital Library

[31]

N. Leveson, S. Cha, J. C. Knight, and T. Shimeall. The use of self checks and voting in software error detection: An empirical study. IEEE TSE, 1990.

Digital Library

[32]

N. Leveson and P. Harvey. Software fault tree analysis. Journal of Systems and Software, 3(2), 1983.

Digital Library

[33]

X. Li and D. Yeung. Application-level correctness and its impact on fault tolerance. HPCA, 2007.

Digital Library

[34]

S. Liu, K. Pattabiraman, T. Moscibroda, and B. Zorn. Flikker: saving dram refresh-power through critical data partitioning. ASPLOS, 2011.

Digital Library

[35]

M. Rinard M. Carbin, S. Misailovic. Verifying quantitative reliability of programs that execute on unreliable hardware (appendix). http://groups.csail.mit.edu/pac/rely.

Digital Library

[36]

M. Rinard M. Carbin, S. Misailovic. Verifying quantitative reliability of programs that execute on unreliable hardware. Technical Report MIT-CSAIL-TR-2013-014, MIT, 2013.

[37]

Xiph.org Video Test Media. http://media.xiph.org/video/derf.

[38]

J. Meng, A. Raghunathan, S. Chakradhar, and S. Byna. Exploiting the forgiving nature of applications for scalable parallel execution. In IPDPS, 2010.

[39]

S. Misailovic, D. Kim, and M. Rinard. Parallelizing sequential programs with statistical accuracy tests. ACM TECS Special Issue on Probabilistic Embedded Computing, 2013.

Digital Library

[40]

S. Misailovic, D. Roy, and M. Rinard. Probabilistically accurate program transformations. SAS, 2011.

Digital Library

[41]

S. Misailovic, S. Sidiroglou, H. Hoffmann, and M. Rinard. Quality of service profiling. ICSE, 2010.

Digital Library

[42]

D. Monniaux. Abstract interpretation of probabilistic semantics. SAS, 2000.

Digital Library

[43]

C. Morgan, A. McIver, and K. Seidel. Probabilistic predicate transformers. TOPLAS, 1996.

Digital Library

[44]

D. Murta and J. N. Oliveira. Calculating fault propagation in functional programs. Technical report, Univ. Minho, 2013.

[45]

S. Narayanan, J. Sartori, R. Kumar, and D. Jones. Scalable stochastic processors. DATE, 2010.

Digital Library

[46]

J. Nelson, A. Sampson, and L. Ceze. Dense approximate storage in phase-change memory. ASPLOS Ideas & Perspectives, 2011.

[47]

K. Pattabiraman, V. Grover, and B. Zorn. Samurai: protecting critical data in unsafe languages. EuroSys, 2008.

Digital Library

[48]

J. Perkins, S. Kim, S. Larsen, S. Amarasinghe, J. Bachrach, M. Carbin, C. Pacheco, F. Sherwood, S. Sidiroglou, G. Sullivan, W. Wong, Y. Zibin, M. Ernst, and M. Rinard. Automatically patching errors in deployed software. SOSP, 2009.

Digital Library

[49]

F. Perry, L. Mackey, G.A. Reis, J. Ligatti, D.I. August, and D. Walker. Fault-tolerant typed assembly language. PLDI'07.

Digital Library

[50]

F. Perry and D. Walker. Reasoning about control flow in the presence of transient faults. SAS, 2008.

Digital Library

[51]

P. Prata and J. Silva. Algorithm based fault tolerance versus result-checking for matrix computations. FTCS, 1999.

Digital Library

[52]

J. Reed and B. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. ICFP, 2010.

Digital Library

[53]

G. Reis, J. Chang, N. Vachharajani, R. Rangan, and D. August. Swift: Software implemented fault tolerance. CGO'05.

Digital Library

[54]

M. Rinard. Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. ICS, 2006.

Digital Library

[55]

M. Rinard. Using early phase termination to eliminate load imbalances at barrier synchronization points. OOPSLA, 2007.

Digital Library

[56]

M. Rinard, C. Cadar, D. Dumitran, D.M. Roy, T. Leu, and W.S. Beebee Jr. Enhancing server availability and security through failure-oblivious computing. OSDI, 2004.

Digital Library

[57]

M. Rinard, C. Cadar, and H. Nguyen. Exploring the acceptability envelope. OOPSLA, 2005.

Digital Library

[58]

M. Rinard, H. Hoffmann, S. Misailovic, and S. Sidiroglou. Patterns and statistical analysis for understanding reduced resource computing. 2010.

Digital Library

[59]

A. Sampson, W. Dietl, E. Fortuna, D. Gnanapragasam, L. Ceze, and D. Grossman. Enerj: Approximate data types for safe and general low-power computation. PLDI, 2011.

Digital Library

[60]

S. Sankaranarayanan, A. Chakarov, and S. Gulwani. Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In PLDI, 2013.

Digital Library

[61]

C. Schlesinger, K. Pattabiraman, N. Swamy, D. Walker, and B. Zorn. Yarra: An extension to c for data integrity and partial safety. CSF, 2011.

[62]

P. Shivakumar, M. Kistler, S.W. Keckler, D. Burger, and L. Alvisi. Modeling the effect of technology trends on the soft error rate of combinational logic. DSN, 2002.

Digital Library

[63]

S. Sidiroglou, S. Misailovic, H. Hoffmann, and M. Rinard. Managing performance vs.\ accuracy trade-offs with loop perforation. FSE, 2011.

Digital Library

[64]

M. Smith. Probabilistic abstract interpretation of imperative programs using truncated normal distributions. Electronic\,Notes\,in\,Theoretical\,Computer\,Science, 2008.

Digital Library

[65]

W. N. Sumner, T. Bao, X. Zhang, and S. Prabhakar. Coalescing executions for fast uncertainty analysis. In ICSE, 2011.

Digital Library

[66]

A. Thomas and K. Pattabiraman. Error detector placement for soft computation. DSN, 2013.

Digital Library

[67]

x264. http://www.videolan.org/x264.html.

[68]

Z. Zhu, S. Misailovic, J. Kelner, and M. Rinard. Randomized accuracy-aware program transformations for efficient approximate computations. POPL, 2012.

Digital Library

Cited By

Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Canty RAbolhasani M(2024)Reproducibility in automated chemistry laboratories using computer science abstractionsNature Synthesis10.1038/s44160-024-00649-83:11(1327-1339)Online publication date: 10-Oct-2024
https://doi.org/10.1038/s44160-024-00649-8
Bao JTrivedi NPathak DHsu JRoy S(2024)Data-driven invariant learning for probabilistic programsFormal Methods in System Design10.1007/s10703-024-00466-xOnline publication date: 3-Dec-2024
https://doi.org/10.1007/s10703-024-00466-x
Show More Cited By

Index Terms

Verifying quantitative reliability for programs that execute on unreliable hardware
1. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Verifying quantitative reliability for programs that execute on unreliable hardware
OOPSLA '13

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 ...
Verifying quantitative reliability for programs that execute on unreliable hardware
Aloe: verifying reliability of approximate programs in the presence of recovery mechanisms
CGO '20: Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications

October 2013

904 pages

ISBN:9781450323741

DOI:10.1145/2509136

Co-chair:
Antony Hosking
Purdue University, USA
,
General Chair:
Patrick Eugster
Purdue University, USA
,
Program Chair:
Cristina V. Lopes
University of California, Irvine, USA

ACM SIGPLAN Notices Volume 48, Issue 10
OOPSLA '13
October 2013
867 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2544173
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Copyright © 2013 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 October 2013

Check for updates

Author Tag

approximate computing

Qualifiers

Research-article

Conference

SPLASH '13

Sponsor:

SIGPLAN

SPLASH '13: Conference on Systems, Programming, and Applications: Software for Humanity

October 29 - 31, 2013

Indiana, Indianapolis, USA

Acceptance Rates

OOPSLA '13 Paper Acceptance Rate 50 of 189 submissions, 26%;

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

175
Total Citations
View Citations
2,086
Total Downloads

Downloads (Last 12 months)165
Downloads (Last 6 weeks)36

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Canty RAbolhasani M(2024)Reproducibility in automated chemistry laboratories using computer science abstractionsNature Synthesis10.1038/s44160-024-00649-83:11(1327-1339)Online publication date: 10-Oct-2024
https://doi.org/10.1038/s44160-024-00649-8
Bao JTrivedi NPathak DHsu JRoy S(2024)Data-driven invariant learning for probabilistic programsFormal Methods in System Design10.1007/s10703-024-00466-xOnline publication date: 3-Dec-2024
https://doi.org/10.1007/s10703-024-00466-x
Feng SYang TChen MZhan N(2024)A Unified Framework for Quantitative Analysis of Probabilistic ProgramsPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_10(230-254)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_10
Bao JTrivedi NPathak DHsu JRoy SElkind E(2023)Data-driven invariant learning for probabilistic programs (extended abstract)Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/712(6415-6419)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/712
Raza MJaved SKazmi MAziz AUl Haque MQazi S(2023)Approximate Computing: Hardware and Software Techniques, Tools and Their ApplicationsJournal of Circuits, Systems and Computers10.1142/S021812662430001033:04Online publication date: 20-Sep-2023
https://doi.org/10.1142/S0218126624300010
Dal Lago UGavazzo F(2022)Effectful program distancingProceedings of the ACM on Programming Languages10.1145/34986806:POPL(1-30)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498680
Seyedfaraji SDaryani JSabry Aly MRehman S(2022)EXTENT: Enabling Approximation-Oriented Energy Efficient STT-RAM Write CircuitIEEE Access10.1109/ACCESS.2022.319467910(82144-82155)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3194679
Bao JTrivedi NPathak DHsu JRoy S(2022)Data-Driven Invariant Learning for Probabilistic ProgramsComputer Aided Verification10.1007/978-3-031-13185-1_3(33-54)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_3
Misailovic S(2022)Accuracy-Aware CompilersApproximate Computing Techniques10.1007/978-3-030-94705-7_7(177-214)Online publication date: 3-Jan-2022
https://doi.org/10.1007/978-3-030-94705-7_7
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents