Formal Analysis of a Distributed Algorithm for Tracking Progress

Martin Abadi, Frank McSherry, Derek G. Murray, and Thomas L. Rodeheffer

Abstract

Tracking the progress of computations can be both important and delicate in distributed systems. In a recent distributed algorithm for this purpose, each processor maintains a delayed view of the pending work, which is represented in terms of points in virtual time. This paper presents a formal specification of that algorithm in the temporal logic TLA, and describes a mechanically verified correctness proof of its main properties.

Details

Publication typeInproceedings
Published inFMOODS-FORTE'13: 15th Formal Methods for Open Object-Based Distributed Systems and 33nd Formal Techniques for Networked and Distributed Systems
PublisherSpringer

Previous versions

Thomas L. Rodeheffer. The Naiad Clock Protocol: Specification, Model Checking, and Correctness Proof, Microsoft Technical Report, 12 February 2013.

> Publications > Formal Analysis of a Distributed Algorithm for Tracking Progress