Fault Tolerance Theorem ----------------------- If |- S and S -->^h S' then either (1) S -->^h_1 Sf and Sf sim_c S' // fault wasn't detected (2) S -->^hf_1 hw-error(S.h,hf) and hf prefix of h // hardware caught error and at most one wrong block visite (3) S -->^hf_1 recover(S.h,hf) and hf prefix of h // recover called even though no cf fault (4) S -->^hf_1 recover(S.h,hf) and hf = (h1,l') and h = (h1,l,h2) // recover called after cf fault (only one wrong block visited) Proof: ------ Case on the structure of S -->^h S' CASE PROG-EXEC-BLK: ~~~~~~~~~~~~~~~~~~~ S -->* MS ------------------------- (prog-exec-blk) S -->^() MS 1. Exists c. S -->*_1 Sf and Sf sim_c MS [ Fault Introduction Lemma, p1 ] OR S -->*_1 recover(S.h) subcase on 1. Subcase A: aa1. S -->*_1 Sf aa2. Sf sim_c MS 2a. S -->^() Sf [ (prog-exec-blk), aa1 ] 3a. S -->^() and Sf sim_c MS [ 2a, aa2 ] * PROG-EXEC-BLK.A complete Subcase B: ab1. S -->*_1 recover(S.h) 2b. S -->^() recover(S.h) [ (prog-exec-blk), ab1 ] 3b. S -->^() recover(S.h) and () prefix of () [ 2b ] * PROG-EXEC-BLK-B complete CASE PROG-EXEC-SEQ-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ S -->^h S' S' -->_0 hw-error -------------------------------------- (prog-exec-seq-hw-error) S -->^h hw-error S -/->^h hw-error [ Non Faulty Execution Lemma ] subcase does not apply * PROG-EXEC-SEQ-HW-ERROR complete CASE PROG-EXEC-SEQ-TRANS-BLK: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ S -->^h S'' S'' -->^l S''' S''' -->*_k MS -------------------------------------------- (prog-exec-seq-trans-blk) S -->^(h,l)_k MS 1. Exists S1,S2,S3 h1, h2. [ Lemma Prog Exec Split, a2 ] 2. S -->^h1 S1 3. S1 -->^l S2 4. S2 -->* S3 5. S3 -->^h2 S' 6. h = (h1,l,h2). 7. Exists c. S2 -->*_1 Sf and Sf sim_c S3 [ Lemma Fault Introduction, 4 ] OR S2 -->*_1 recover(S.h,h1,l) 8. Either [ Faulty Computation Lemma, 7, 5 ] (8.1) Sf -->^h Sf' and Sf' sim_c S' (8.2) Sf -->^hf hw-error(S.h,h1,l,hf) and hf prefix of h2 (8.3) Sf -->^hf recover(S.h,h1,l,hf) and hf prefix of h2 (8.4) Sf -->^hf recover(S.h,h1,l,hf) and hf = (h',l') and h = (h',l,h'') 9. Either [ Lemma Prog Exec Join, 8 ] (8.1) S -->^h_1 Sf' and Sf' sim_c S' (8.2) S -->^hf hw-error(S.h,h1,l,hf) and (h1,l,hf) prefix of (h1,l,h2) (8.3) S -->^hf recover(S.h,h1,l,hf) and (h1,l,hf) prefix of (h1,l,h2) (8.4) S -->^hf recover(S.h,h1,l,hf) and hf = (h1,l') and h = (h1,l,h2) * PROG-EXEC-SEQ-TRANS-BLK complete * FAULT TOLERANCE THEOREM COMPLETE ============================================================================================================================================== ============================================================================================================================================== Faulty Computation Lemma ------------------------- If Sf sim_c S and S -->^h S' then either (1) Sf -->^h Sf' and Sf' sim_c S' // fault wasn't detected (2) Sf -->^hf hw-error(S.h,hf) and hf prefix of h // hardware caught error and at most one wrong block visited (3) Sf -->^hf recover(S.h,hf) and hf prefix of h // recover called even though no cf fault (4) Sf -->^hf recover(S.h,hf) and hf = (h1,l') and h = (h1,l,h2) // recover called after cf fault (only one wrong block visited) PROOF: By induction on the structure of S -->^h S' ------ a1. Sf sim_c S CASE PROG-EXEC-BLK: ~~~~~~~~~~~~~~~~~~~ S -->* MS' ------------------------- (prog-exec-blk) S -->^() MS' 1. MS' = S' [ NonFaulty Block Execution Lemma, Inversion of (sim-S), a1 ] 2. Sf -->* Sf' and Sf' sim_c S' [ Block Execution Lemma, a1, p1 ] or Sf -->* recover(S.h) subcase on 2. SUBCASE PROG-EXEC-BLK.A: Faulty computation executes first block and continues to simulate original aa1. Sf -->* Sf' aa2. Sf' sim_c S' 3a. Sf -->^() Sf' [ (prog-exec-blk), aa1 ] 4a. Sf -->^() Sf' and Sf' sim_c S' [ 3a, aa2 ] * PROG-EXEC-BLK.A complete SUBCASE PROG-EXEC-BLK.B: Faulty computation recovers while executing first block ab1. Sf -->* recover(S.h) 1b. Sf -->^() recover(S.h) [ (prog-exec-blk), ab1 ] 2b. Sf -->^() recover(S.h) and () prefix () [ 1b, ab1 ] * PROG-EXEC-BLK.B complete CASE PROG-EXEC-SEQ-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ S -->^h S'' S'' -->_0 hw-error -------------------------------------- (prog-exec-blk-hw-error) S -->^h hw-error 1. S -/->_0 hw-error [ Non Faulty Block Execution Lemma, Inversion of (sim-S), a1] subcase does not apply * PROG-EXEC-SEQ-HW-ERROR complete CASE PROG-EXEC-SEQ-TRANS-BLK: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ S -->^h S'' S'' -->^l S''' S''' -->*_k MS' -------------------------------------------- (prog-exec-seq-trans-blk) S -->^(h,l)_k MS' 1. MS' = S' [ NonFaulty Block Execution Lemma, Inversion of (sim-S), a1 ] 2. Sf -->^h Sf'' and Sf'' sim_c S'' [ I.H., a1, p1 ] OR Sf -->^hf hw-error(S.h,hf) and hf prefix of h OR Sf -->^hf recover(S.h,hf) and hf prefix of h OR Sf -->^hf recover(S.h,hf) and hf = (h1,l') and h = (h1,l2,h3) subcase on 2 SUBCASE PROG-EXEC-SEQ-TRANS-BLK.A: First part of faulty execution simulates original aa1. Sf -->^h Sf'' aa2. Sf'' sim_c S'' 3a. Sf'' -->^l Sf''' and Sf''' sim_c S''' [ Block Transition Lemma, aa2, p2 ] OR Sf'' -->_0 hw_error(S.h,h) OR Sf'' -->^l' Sf' and Sf' -->* recover(S.h,h,l') subsubcase on 3a. SUBSUBCASE PROG-EXEC-SEQ-TRANS-BLK.A1: Faulty execution takes the correct transition... aa11. Sf'' -->^l Sf''' aa12. Sf''' sim_c S''' 3a1. Sf''' -->* Sf' and Sf' sim_c S' [ Block Evaluation Lemma, aa12, p3 ] OR Sf''' -->* recover(S.h,h,l) subsubsubcase on 3a1. subsubsubcase PROG-EXEC-SEQ-TRANS-BLK.A1A: ...and continues to simulate the original aa1a1. Sf''' -->* Sf' aa1a2. Sf' sim_c S' 4a1a. Sf -->^(h,l) Sf' [ (prog-exec-seq-trans-blk), aa1, aa11, aa1a1 ] 5a1a. Sf -->^(h,l) Sf' and Sf' sim_c S' [ 4a1a, aa1a2 ] * subsubsubcase PROG-EXEC-SEQ-TRANS-BLK.A1A complete subsubsubcase PROG-EXEC-SEQ-TRANS-BLK.A1B: ...and recovers prematurely aa1b1. Sf''' -->* recover(S.h,h,l) 4a1b. Sf -->^(h,l) recover(S.h,h,l) [ (prog-exec-seq-trans-blk), aa1, aa11, aa1b1 ] 5a1b. Sf -->^(h,l) recover(S.h,h,l) and (h,l) prefixof (h,l) [ 4a1b ] * subsubsubcase PROG-EXEC-SEQ-TRANS-BLK.A1B complete SUBSUBCASE PROG-EXEC-SEQ-TRANS-BLK.A2: Faulty execution encounters a hw-error aa21. Sf'' -->_0 hw_error(S.h,h) 3a2. Sf -->^h hw-error(S.h,h) [ (prog-exec-seq-hw-error), aa1, aa21 ] 3a2. Sf -->^h hw-error(S.h,h) and h prefixof h [ 3a2 ] * SUBSUBCASE PROG-EXEC-SEQ-TRANS-BLK.A2 complete SUBSUBCASE PROG-EXEC-SEQ-TRANS-BLK.A3: Faulty execution goes to the wrong place aa31. Sf'' -->^l' Sf' aa32. Sf' -->* recover(S.h,h,l') 3a3. Sf -->^(h,l') recover(S.h,h,l') [ (prog-exec-seq-trans-blk), aa1, aa31, aa32 ] 4a3. Sf -->^(h,l') recover(S.h,h,l') and (h,l') = (h,l') and (S.h,h,l) = ((S.h,h),l,.) [ 3a3 ] * PROG-EXEC-SEQ-TRANS-BLK.A3 complete SUBCASE PROG-EXEC-SEQ-TRANS-BLK.B: First part of faulty execution encounters a hw-error ab1. Sf -->^hf hw-error(S.h,hf) ab2. hf prefix of h 3b. Sf -->^hf hw-error(S.h,hf) and hf prefix of (h,l) [ ab1, ab2 ] * PROG-EXEC-SEQ-TRANS-BLK.B complete SUBCASE PROG-EXEC-SEQ-TRANS-BLK.C: First part of faulty execution recovers prematurely ac1. Sf -->^hf recover(S.h,h) ac2. hf prefix of h 3c. Sf -->^hf recover(S.h,h) and hf prefix of (h,l) [ ac1, ac2 ] * PROG-EXEC-SEQ-TRANS-BLK.C complete SUBCASE PROG-EXEC-SEQ-TRANS-BLK.D: First part of faulty execution heads off on it's own and recovers ad1. Sf -->^hf recover ad2. hf = (h1,l') and h = (h1,l2,h3) 3d. Sf -->^hf recover and hf = (h1,l') and h = (h1,l2,h3,l) [ ad1, ad2 ] * PROG-EXEC-SEQ-TRANS-BLK.D complete