From Thirteenth ACM Symposium on Principles of Distributed Computing.
Los Angeles, CA.
August, 1994.

Also available as NASA Contractor Report 198289

A simple modification to the Interactive Convergence clock synchronization algorithm allows it to tolerate a larger number of certain kinds of faults than the standard algorithm, without reducing its tolerance to 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 Interactive Consistency (Byzantine Agreement): in addition to arbitrary faults, we also admit manifest (i.e., detectable) and symmetric (i.e., consistent) faults. With n channels, the modified algorithm can withstand a arbitrary, s symmetric, and m manifest faults simultaneously, provided n > 3a + 2s + m. This is better than the bound achieved for the problem of interactive consistency under the similar fault model. Unlike interactive consistency, we have been able to further extend the fault model for clock synchronization to include link faults with bound n > 3a + 2s + m + l where l is the maximum, over all pairs of channels, of the number of channels 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 in just a few days of work. 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.

@inproceedings{Rushby94:icah,
    AUTHOR = {John Rushby},
    TITLE = {{A} Formally Verified Algorithm for Clock Synchronization Under a Hybrid Fault Model},
    BOOKTITLE = {Thirteenth {ACM} Symposium on Principles of Distributed Computing},
    YEAR = {1994},
    ADDRESS = {Los Angeles, {CA}},
    MONTH = {August},
    NOTE = {Also available as {NASA} Contractor Report 198289},
    URL = {http://www.csl.sri.com/papers/podc94/}
}

• podc94.dvi.gz
• podc94.ps.gz