Formal Analysis of a Distributed Algorithm for Tracking Progress

Martin Abadi; Frank McSherry; Derek Murray; Tom Rodeheffer

Formal Analysis of a Distributed Algorithm for Tracking Progress

Martin Abadi ,
Frank McSherry ,
Derek Murray ,
Tom Rodeheffer

FMOODS-FORTE'13: 15th Formal Methods for Open Object-Based Distributed Systems and 33nd Formal Techniques for Networked and Distributed Systems | June 2013

Published by Springer

Download BibTex

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.