Loading...
Please wait, while we are loading the content...
Similar Documents
Strong fault tolerance for the faulty lambda calculus.
| Content Provider | CiteSeerX |
|---|---|
| Author | Mackey, Lester Walker, David |
| Abstract | Abstract. A transient hardware fault occurs when a high-energy particle penetrates the silicon of a processor, generates an electric charge and changes the state of a transistor. To mitigate the damage caused by transient faults, researchers have investigated hardware, software, and hybrid hardware-software fault tolerance schemes. However, there has been almost no formal analysis of the properties such schemes guarantee for software applications. One exception to the rule is our recent work on λzap, a lambda calculus that nondeterministically exhibits transient faults. In this original work, we proved there exists a compilation strategy that allows λzap to implement the simply-typed lambda calculus faithfully, despite the presence of transient faults. Unfortunately, however, our results do not fully justify using λzap as the foundation for a sound typed intermediate language — λzap’s type system, on its own, was not powerful enough to guarantee a strong fault tolerance property. Hence, in this paper, we extend λzap’s original, weak type system with new expression equivalence constraints that are, in fact, sufficient to provide strong fault tolerance guarantees independently of the compilation strategy. The new constraints come in two variants: (1) a semantic definition of equivalence used to prove important meta-theoretic properties including type safety and strong fault tolerance, and (2) a sound syntactic approximation of the former that is easily decideable. All in all, this new type system and meta-theory for λzap will serve as an effective foundation for a fully fault tolerant typed intermediate language. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Strong Fault Tolerance Faulty Lambda Calculus Transient Fault Compilation Strategy Lambda Calculus Type Safety Original Work Intermediate Language High-energy Particle Formal Analysis Recent Work Weak Type System Sound Syntactic Approximation Intermediate Language Zap Type System Effective Foundation Strong Fault Tolerance Guarantee Software Application New Constraint New Expression Equivalence Constraint Semantic Definition Important Meta-theoretic Property Hybrid Hardware-software Fault Tolerance Scheme Fault Tolerant Transient Hardware Fault Strong Fault Tolerance Property Property Scheme Guarantee Simply-typed Lambda Calculus Electric Charge New Type System |
| Content Type | Text |
| Resource Type | Article |
