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

Article

Static typing for a faulty lambda calculus

Authors:

George A. Reis,

David I. AugustAuthors Info & Claims

ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming

Pages 38 - 49

https://doi.org/10.1145/1159803.1159809

Published: 16 September 2006 Publication History

Abstract

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. These faults do not cause permanent damage, but may result in incorrect program execution by altering signal transfers or stored values. While the likelihood that such transient faults will cause any significant damage may seem remote, over the last several years transient faults have caused costly failures in high-end machines at America Online, eBay, and the Los Alamos Neutron Science Center, among others [6, 44, 15]. Because susceptibility to transient faults is proportional to the size and density of transistors, the problem of transient faults will become increasingly important in the coming decades.This paper defines the first formal, type-theoretic framework for studying reliable computation in the presence of transient faults. More specifically, it defines λzap, a lambda calculus that exhibits intermittent data faults. In order to detect and recover from these faults, λzap programs replicate intermediate computations and use majority voting, thereby modeling software-based fault tolerance techniques studied extensively, but informally [10, 20, 30, 31, 32, 33, 41].To ensure that programs maintain the proper invariants and use λzap primitives correctly, the paper defines a type system for the language. This type system guarantees that well-typed programs can tolerate any single data fault. To demonstrate that λzap can serve as an idealized typed intermediate language, we define a type-preserving translation from a standard simply-typed lambda calculus into λzap.

References

[1]

M. Abadi, M. Budiu, Úlfar Erlingsson, and J. Ligatti. Control-flow integrity: Principles, implementations, and applications. In ACM Conference on Computer and Communications Security, Nov. 2005.

Digital Library

[2]

M. Abadi, M. Budiu, Úlfar Erlingsson, and J. Ligatti. A theory of secure control flow. In International Conference on Formal Engineering Methods, Nov. 2005.

Digital Library

[3]

A. W. Appel. Foundational proof-carrying code. In Sixteenth Annual IEEE Symposium on Logic in Computer Science, pages 247--258. IEEE, 2001.

Digital Library

[4]

T. M. Austin. DIVA: a reliable substrate for deep submicron microarchitecture design. In Proceedings of the 32nd Annual ACM/IEEE International Symposium on Microarchitecture, pages 196--207. IEEE Computer Society, 1999.

Digital Library

[5]

R. C. Baumann. Soft errors in advanced semiconductor devices-part I: the three radiation sources. IEEE Transactions on Device and Materials Reliability, 1(1):17-22, March 2001.

[6]

R. C. Baumann. Soft errors in commercial semiconductor technology: Overview and scaling trends. In IEEE 2002 Reliability Physics Tutorial Notes, Reliability Fundamentals, pages 121_01.1 - 121_01.14, April 2002.

[7]

C. Bolchini and F. Salice. A software methodology for detecting hardware faults in vliw data paths. In IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, 2001.

Digital Library

[8]

J. Chang, G. A. Reis, and D. I. August. Automatic instructionlevel software-only recovery methods. In Proceedings of the 2006 International Conference on Dependendable Systems and Networks, June 2006.

Digital Library

[9]

A. Dimock, R. Muller, F. Turbak, and J. B. Wells. Strongly typed flow-directed representation transformations. In ACM International Conference on Functional Programming, pages 85--98, Amsterdam, June 1997.

Digital Library

[10]

M. Gomaa, C. Scarbrough, T. N. Vijaykumar, and I. Pomeranz. Transient-fault recovery for chip multiprocessors. In Proceedings of the 30th annual international symposium on Computer architecture, pages 98--109. ACM Press, 2003.

Digital Library

[11]

S. Govindavajhala and A. W. Appel. Using memory errors to attack a virtual machine. In IEEE Symposium on Security and Privacy, pages 154--165, May 2003.

Digital Library

[12]

J. G. Holm and P. Banerjee. Low cost concurrent error detection in a VLIW architecture using replicated instructions. In Proceedings of the 1992 International Conference on Parallel Processing, volume 1, pages 192--195, August 1992.

[13]

R.W. Horst, R.L. Harris, and R.L. Jardine. Multiple instruction issue in the NonStop Cyclone processor. In Proceedings of the 17th International Symposium on Computer Architecture, pages 216--226, May 1990.

Digital Library

[14]

A. Mahmood and E.J. McCluskey. Concurrent error detection using watchdog processors-a survey. IEEE Transactions on Computers, 37(2):160--174, 1988.

Digital Library

[15]

S.E. Michalak, K.W. Harris, N.W. Hengartner, B.E. Takala, and S.A. Wender. Predicting the number of fatal soft errors in Los Alamos National LabratoryÆs ASC Q computer. IEEE Transactions on Device and Materials Reliability, 5(3):329--335, September 2005.

[16]

G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based Typed Assembly Language. In Second International Workshop on Types in Compilation, pages 95--117, Kyoto, Mar. 1998. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, volume 1473, pages 28--52. Springererlag, 1998.

Digital Library

[17]

G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based Typed Assembly Language. Journal of Functional Programming, 12(1):43--88, Jan. 2002.

Digital Library

[18]

G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In ACM Conference on Functional Programming and Computer Architecture, pages 66--77, La Jolla, June 1995.

Digital Library

[19]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to Typed Assembly Language. ACM Transactions on Programming Languages and Systems, 3(21):528--569, May 1999.

Digital Library

[20]

S.S. Mukherjee, M. Kontz, and S. K. Reinhardt. Detailed design and evaluation of redundant multithreading alternatives. In Proceedings of the 29th Annual International Symposium on Computer Architecture, pages 99--110. IEEE Computer Society, 2002.

Digital Library

[21]

G. Necula. Proof-carrying code. In Twenty-Fourth ACM Symposium on Principles of Programming Languages, pages 106--119, Paris, 1997.

Digital Library

[22]

G. Necula and P. Lee. Safe kernel extensions without runtime checking. In Proceedings of Operating System Design and Implementation, pages 229--243, Seattle, Oct. 1996.

Digital Library

[23]

T.J. O'Gorman, J.M. Ross, A.H. Taber, J.F. Ziegler, H.P. Muhlfeld, I.C.J. Montrose, H.W. Curtis, and J.L. Walsh. Field testing for cosmic ray soft errors in semiconductor memories. In IBM Journal of Research and Development, pages 41--49, January 1996.

Digital Library

[24]

N. Oh and E.J. McCluskey. Low energy error detection technique using procedure call duplication. In Proceedings of the 2001 International Symposium on Dependable Systems and Networks, 2001.

[25]

N. Oh, P.P. Shirvani, and E.J. McCluskey. Control-flow checking by software signatures. In IEEE Transactions on Reliability, volume 51, pages 111--122, March 2002.

[26]

N. Oh, P.P. Shirvani, and E.J. McCluskey. ED⁴I: Error detection by diverse data and duplicated instructions. In IEEE Transactions on Computers, volume 51, pages 180--199, February 2002.

Digital Library

[27]

N. Oh, P.P. Shirvani, and E.J. McCluskey. Error detection by duplicated instructions in super-scalar processors. In IEEE Transactions on Reliability, volume 51, pages 63--75, March 2002.

[28]

J. Ohlsson and M. Rimen. Implicit signature checking. In International Conference on Fault-Tolerant Computing, June 1995.

Digital Library

[29]

M. Rebaudengo, M.S. Reorda, M. Violante, and M. Torchiano. A source-to-source compiler for generating dependable software. In IEEE International Workshop on Source Code Analysis and Manipulation, pages 33--42, 2001.

[30]

S.K. Reinhardt and S.S. Mukherjee. Transient fault detection via simultaneous multithreading. In Proceedings of the 27th Annual International Symposium on Computer Architecture, pages 25--36. ACM Press, 2000.

Digital Library

[31]

G.A. Reis, J. Chang, N. Vachharajani, R. Rangan, and D.I. August. SWIFT: Software implemented fault tolerance. In Proceedings of the 3rd International Symposium on Code Generation and Optimization, March 2005.

Digital Library

[32]

E. Rotenberg. AR-SMT: A microarchitectural approach to fault tolerance in microprocessors. In Proceedings of the Twenty-Ninth Annual International Symposium on Fault-Tolerant Computing, page 84. IEEE Computer Society, 1999.

Digital Library

[33]

N. Saxena and E. J. McCluskey. Dependable adaptive computing systems - the ROAR project. In International Conference on Systems, Man, and Cybernetics, pages 2172--2177, October 1998.

[34]

Z. Shao. An overview of the FLINT/ML compiler. In Workshop on Types in Compilation, Amsterdam, June 1997. ACM. Published as Boston College Computer Science Dept. Technical Report BCCS-97-03.

[35]

Z. Shao and A. Appel. A type-based compiler for Standard ML. In ACM Conference on Programming Language Design and Implementation, pages 116--129, La Jolla, June 1995.

Digital Library

[36]

P.P. Shirvani, N. Saxena, and E.J. McCluskey. Softwareimplemented EDAC protection against SEUs. In IEEE Transactions on Reliability, volume 49, pages 273--284, 2000.

[37]

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. In Proceedings of the 2002 International Conference on Dependable Systems and Networks, pages 389--399, June 2002.

Digital Library

[38]

T.J. Slegel, R.M. Averill III, M.A. Check, B.C. Giamei, B.W. Krumm, C.A. Krygowski, W.H. Li, J.S. Liptay, J.D. MacDougall, T.J. McPherson, J.A. Navarro, E.M. Schwarz, K. Shum, and C.F. Webb. IBMÆs S/390 G5 Microprocessor design. In IEEE Micro, volume 19, pages 12--23, March 1999.

Digital Library

[39]

D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In ACM Conference on Programming Language Design and Implementation, pages 181--192, Philadelphia, May 1996.

Digital Library

[40]

R. Venkatasubramanian, J. P. Hayes, and B. T. Murray. Low-cost on-line fault detection using control flow assertions. In Proceedings of the 9th IEEE International On-Line Testing Symposium, pages 137--143, July 2003.

[41]

T. N. Vijaykumar, I. Pomeranz, and K. Cheng. Transient-fault recovery using simultaneous multithreading. In Proceedings of the 29th Annual International Symposium on Computer Architecture, pages 87--98. IEEE Computer Society, 2002.

Digital Library

[42]

Y. Yeh. Triple-triple redundant 777 primary flight computer. In Proceedings of the 1996 IEEE Aerospace Applications Conference, volume 1, pages 293--307, February 1996.

[43]

Y. Yeh. Design considerations in Boeing 777 fly-by-wire computers. In Proceedings of the Third IEEE International High-Assurance Systems Engineering Symposium, pages 64--72, November 1998.

Digital Library

[44]

J.F. Ziegler and H. Puchner. SER-History, Trends, and Challenges: A Guide for Designing with Memory ICs. 2004.

Cited By

Inoue JNishihara HMori A(2022)Quantitative Analysis of Sparsely Synchronized Fail-Safe Processors2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00109(1057-1068)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00109
Dullien T(2020)Weird Machines, Exploitability, and Provable UnexploitabilityIEEE Transactions on Emerging Topics in Computing10.1109/TETC.2017.27852998:2(391-403)Online publication date: 1-Apr-2020
https://doi.org/10.1109/TETC.2017.2785299
Jangda APinckney DBrun YGuha A(2019)Formal foundations of serverless computingProceedings of the ACM on Programming Languages10.1145/33605753:OOPSLA(1-26)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360575
Show More Cited By

Index Terms

Static typing for a faulty lambda calculus

Recommendations

Fault-tolerant typed assembly language
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. Although transient faults do not permanently damage the hardware, they may corrupt computations by altering stored values and signal ...
Static typing for a faulty lambda calculus
Proceedings of the 2006 ICFP conference

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. These faults do not cause permanent damage, but may result in incorrect program execution by altering signal transfers or stored values. While ...
Fault-tolerant typed assembly language
Proceedings of the 2007 PLDI conference

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. Although transient faults do not permanently damage the hardware, they may corrupt computations by altering stored values and signal ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming

September 2006

308 pages

ISBN:1595933093

DOI:10.1145/1159803

General Chair:
John Reppy
University of Chicago, USA
,
Program Chair:
Julia Lawall
University of Copenhagen, Denmark

ACM SIGPLAN Notices Volume 41, Issue 9
Proceedings of the 2006 ICFP conference
September 2006
296 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1160074
Issue’s Table of Contents

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part 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 components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 September 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP06

Sponsor:

ICFP06: ACM SIGPLAN International Conference on Functional Programming

September 16 - 21, 2006

Oregon, Portland, USA

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
346
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Inoue JNishihara HMori A(2022)Quantitative Analysis of Sparsely Synchronized Fail-Safe Processors2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00109(1057-1068)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00109
Dullien T(2020)Weird Machines, Exploitability, and Provable UnexploitabilityIEEE Transactions on Emerging Topics in Computing10.1109/TETC.2017.27852998:2(391-403)Online publication date: 1-Apr-2020
https://doi.org/10.1109/TETC.2017.2785299
Jangda APinckney DBrun YGuha A(2019)Formal foundations of serverless computingProceedings of the ACM on Programming Languages10.1145/33605753:OOPSLA(1-26)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360575
Hung SHietala KZhu SYing MHicks MWu X(2019)Quantitative robustness analysis of quantum programsProceedings of the ACM on Programming Languages10.1145/32903443:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290344
Karl ASchilling RBloem RMangard S(2019)Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded ProgramsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_9(183-204)Online publication date: 11-Jan-2019
https://doi.org/10.1007/978-3-030-11245-5_9
Perez I(2018)Fault tolerant functional reactive programming (functional pearl)Proceedings of the ACM on Programming Languages10.1145/32367912:ICFP(1-30)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236791
Stanley-Marbell PRinard M(2017)Error-Efficient Computing SystemsFoundations and Trends in Electronic Design Automation10.1561/100000004911:4(362-461)Online publication date: 18-Dec-2017
https://dl.acm.org/doi/10.1561/1000000049
CHENEY JMOMIGLIANO A(2017)αCheck: A mechanized metatheory model checkerTheory and Practice of Logic Programming10.1017/S147106841700003517:3(311-352)Online publication date: 22-May-2017
https://doi.org/10.1017/S1471068417000035
Chen HZiegler DChajed TChlipala AKaashoek MZeldovich NMiller EHand S(2015)Using Crash Hoare logic for certifying the FSCQ file systemProceedings of the 25th Symposium on Operating Systems Principles10.1145/2815400.2815402(18-37)Online publication date: 4-Oct-2015
https://dl.acm.org/doi/10.1145/2815400.2815402
Zheng LMyers ARusso ATripp O(2014)A Language-Based Approach to Secure Quorum ReplicationProceedings of the Ninth Workshop on Programming Languages and Analysis for Security10.1145/2637113.2637117(27-39)Online publication date: 28-Jul-2014
https://dl.acm.org/doi/10.1145/2637113.2637117
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents