|
Abstract : |
A small modification to the interactive convergence clock synchroniza-tion algorithm allows it to tolerate a larger number of simple faults than the standard algorithm, without reducing its ability to tolerate arbitrary or ?Byzantine ? faults. Because the extended case-analysis required by the new fault model complicates the already intricate argument for correctness of the algorithm, it has been subjected to mechanically-checked formal verification. The fault model examined is similar to the ?hybrid ? one previously used for the problem of distributed consensus: in addition to arbitrary faults, we also admit symmetric (Le., consistent) and manifest (i.e., detectable) faults. With n processors, the modified algorithm can withstand a arbitrary, s symmetric, and m manifest faults simultaneously, provided n> 3a + 29 + m. A further extension to the fault model includes link faults with bound n> 3a + 2s + m + 1 where 1 is the maximum, over all pairs of processors, of the number of processors that have faulty links to one or other of the pair., |
