TAL_CF - Online Proof Appendix

Reasoning about Control Flow in the Presence of Transient Faults - Online Proof Appendix

Frances Perry and David Walker

October 12, 2007

This online appendix includes the full proofs for the Princeton University Technical Report TR-799-07: Reasoning About Control Flow in the Presence of Transient Faults.

These notes are written in ascii text using abbrieviations like |- for \vdash and G for \Gamma. A few of the symbols differ from those in the tech report, including R for orange, A for \sigma, to for \tau opt, and alpha and Y as expression variables. The provided syntax should clear up any confusion. Also, the use of ascii has resulted in some symbol duplication. R is used for both orange and register files, S is used for both \Sigma and substitutions, and G is used for both green and \Gamma. The context should make it clear which is meant.

Section 3: The Control-Flow Machine

Syntax
Dynamic Semantics

Section 4: Typing

Section 5: Fault Tolerance

Definitions - definitions needed for fault tolerance, including block evaluation, transition evaluation, and program execution
Lemmas - useful lemmas for fault tolerance
CF Recovery Lemma - When there has been a cf fault, control always transfers to the recovery code before leaving the block
Block Lemmas - Outcome of evaluating a block
Transition Lemmas - Outcome of transitioning between blocks
Fault Tolerance Theorem

Section 6: Translation

Definitions - Defintion of while language, wellformedness, type translation, etc
Lemmas - Lemmas used in the translation theorem
Translation Theorem - Well typed while language programs translate into well typed assembly programs

Misc

Example Program