Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Formal Analysis of a Distributed Algorithm for Tracking Progress

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.
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, April 27, 2017 - 10:46:45 AM
Last modification on : Thursday, July 25, 2019 - 3:06:02 PM
Long-term archiving on: : Friday, July 28, 2017 - 12:39:26 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Martín Abadi, Frank Mcsherry, Derek G. Murray, Thomas L. Rodeheffer. Formal Analysis of a Distributed Algorithm for Tracking Progress. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. pp.5-19, ⟨10.1007/978-3-642-38592-6_2⟩. ⟨hal-01515239⟩



Record views


Files downloads