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.
Liste complète des métadonnées

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-01515239
Contributor : Hal Ifip <>
Submitted on : Thursday, April 27, 2017 - 10:46:45 AM
Last modification on : Thursday, April 27, 2017 - 2:43:59 PM
Document(s) archivé(s) le : Friday, July 28, 2017 - 12:39:26 PM

File

978-3-642-38592-6_2_Chapter.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Martín Abadi, Frank Mcsherry, Derek Murray, Thomas 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⟩

Share

Metrics

Record views

77

Files downloads

32