Fault-tolerant typed assembly language

Frances Perry, Lester MacKey, George A. Reis, Jay Ligatti, David I. August, David P. Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Scopus citations

Abstract

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 transfers. In this paper, we propose a new scheme for provably safe and reliable computing in the presence of transient hardware faults. In our scheme, software computations are replicated to provide redundancy while special instructions compare the independently computed results to detect errors before writing critical data. In stark contrast to any previous efforts in this area, we have analyzed our fault tolerance scheme from a formal, theoretical perspective. To be specific, first, we provide an operational semantics for our assembly language, which includes a precise formal definition of our fault model. Second, we develop an assembly-level type system designed to detect reliability problems in compiled code. Third, we provide a formal specification for program fault tolerance under the given fault model and prove that all well-typed programs are indeed fault tolerant. In addition to the formal analysis, we evaluate our detection scheme and show that it only takes 34% longer to execute than the unreliable version.

Original languageEnglish (US)
Title of host publicationPLDI'07
Subtitle of host publicationProceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages42-53
Number of pages12
DOIs
StatePublished - 2007
EventPLDI'07: 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation - San Diego, CA, United States
Duration: Jun 10 2007Jun 13 2007

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

OtherPLDI'07: 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation
Country/TerritoryUnited States
CitySan Diego, CA
Period6/10/076/13/07

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Fault tolerance
  • Soft faults
  • Transient hardware faults
  • Typed assembly language

Fingerprint

Dive into the research topics of 'Fault-tolerant typed assembly language'. Together they form a unique fingerprint.

Cite this