A Formally Verified Algorithm for Clock Synchronization Under a Hybrid Fault Model

摘要

A small modification to the interactive convergence clock synchronization 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 (i.e., 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 is greater than 3a2sm. A further extension to the fault model includes link faults with bound n is greater than 3a2smI where I is the maximum, over all pairs of processors, of the number of processors that have faulty links to one or other of the pair. The mechanically-checked formal verification of the modified algorithm was achieved by extending one for the classical Interactive Convergence algorithm, and was accomplished relatively easily. A mechanically-checked formal specification and verification is a reusable intellectual resource whose initial cost is amply repaid by the support it provides for inexpensive and reliable investigation of modified assumptions and algorithms such as those reported here.