Martin Abadi, Frank McSherry, Derek G. Murray, and Thomas L. Rodeheffer
3 June 2013
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.
In FMOODS-FORTE'13: 15th Formal Methods for Open Object-Based Distributed Systems and 33nd Formal Techniques for Networked and Distributed Systems
Copyright © International Federation for Information Processing 2013. Published by Springer-Verlag GmbH Berlin Heidelberg 2013. All Rights Reserved.
Thomas L. Rodeheffer. The Naiad Clock Protocol: Specification, Model Checking, and Correctness Proof, Microsoft Technical Report, 12 February 2013.